The Math Behind Pacing the Frontier

The Math Behind Pacing the Frontier

Efficient open-source zero-knowledge proofs are possible

The need to pace the development of frontier AI is one of the rare points of agreement between people like Sam Altman, Barack Obama, and Elon Musk. The biggest obstacle is working out how to verify whether others – be they companies or countries – are doing the same.

At a minimum, pacing the frontier requires being able to tell if a given datacenter is being used for inference or to train new models. Many proposals for how to do so involve using human inspectors or specialised hardware to acquire evidence about what AI datacenters are being used for. However, human inspections risk exposing confidential information and may be difficult to scale, and specialised datacenter monitoring hardware will require extremely robust cybersecurity and will need to be auditable by both parties in an agreement.

Our research suggests zero-knowledge proofs (ZKPs) could provide this evidence and that there may be a path to make them efficient and secure enough to be used in international agreements on frontier AI.

Below we explain what ZKPs are, what role they can play in governing frontier AI, and introduce an open-source implementation of ZKPs for AI inference.

Zero-Knowledge Proofs of Inference

ZKPs of AI inference are a cryptographic technique that provides a mathematical guarantee that the response to a query was computed by the exact model you specified. What makes this “zero-knowledge” is that the guarantee can be made even when some parts, like the exact model weights, remain secret. We can also get a guarantee that the output received to a query was computed by an approved model, without revealing which one.

One way to understand how ZKPs for AI verification work is to think about train crashes. In the 1800s, the routes trains took were controlled by human track operators who pulled mechanical levers at railway junctions. Two levers set to the wrong positions often led to two trains colliding head-on. To help solve this, mechanical interlocks were built into the signalling levers, which made it impossible to configure the levers in a way that led to two trains heading down the same piece of track in opposite directions.

ZKPs provide a similar constraint on what can pass verification. A mechanical interlock prevents a signal operator from giving conflicting routes the all-clear. By binding together the “ingredients” of a computation—the model, the prompt, and the output—a ZKP can produce a proof that is valid only if the computation satisfies the specified rules. If an unauthorised change is made to the inference process or a non-inference computation has been run, the proof cannot be created. Just like the mechanical interlocking systems made it impossible to send two trains down the same track, ZKPs make it impossible for an improperly produced AI operation to generate a valid proof.

In the context of AI verification, this could allow two parties that distrust each other to request spot checks of each other’s datacenter workloads. For example, the figure above demonstrates how one party could check that the other is serving them the right model and that their queries are not being modified in transit.

ZKPs of inference can also be used to help categorise workloads. Say, Side A claims their datacenter is only being used to serve Model Y and not to train new models. To check this claim, Side B could request proofs for a random sample of the datacenter’s computations. If Side A attempted to use that datacenter for unauthorised training, genuinely random checks could catch computations for which it cannot supply valid inference proofs. With enough checks, the chance of missing that training could become vanishingly small.

Previously, ZKPs were slow and expensive to generate: producing a proof could take 10,000 times as long as running the inference itself. Because generating proofs requires electricity and ties up hardware that could be used for other purposes, slowness had financial consequences. As a result, other compute verification tools were prioritised by most researchers. But more recent breakthroughs suggest ZKPs are becoming efficient enough to be viable.

ZKPs are only one part of a broader toolkit for compute verification. Other mechanisms, especially off-chip monitoring and physical inspections, could also play important roles in pacing the frontier. ZKPs may be particularly useful where parties need strong verification while protecting sensitive information, but they are not the only option. Where privacy requirements are less stringent, or sensitive facilities can be excluded from an agreement, a combination of physical inspections, chip supply-chain monitoring, and off-chip mechanisms may be enough to provide strong assurance.

Trustless Agreements

One way to understand the strengths of ZKPs as a means of verifying agreements about frontier AI is to compare them to alternative methods that are being developed. In particular, they can provide strong evidence while requiring relatively little trust in the party being monitored.

Different verification mechanisms shift that trust to different places.

Trusted Execution Environments (TEEs) — sealed-off parts of chips that can privately run computations without even the machines’ owners being able to inspect or modify them — place trust in the AI chips themselves. However, TEEs can be easily compromised by an adversary with in-person access to the chip. Additionally, since TEE computations are attested to by the chip manufacturer, governments may be unwilling to rely on a foreign manufacturer’s attestation.

Datacenter inspections are another intuitive option since they can gather direct evidence about the datacenter and its activity. However, this requires trusting the personnel conducting the inspections not to share this information or gain additional sensitive information not required to verify whether the datacenter is being used to train new models. Additionally, in-person inspections may be difficult to scale if there are hundreds or thousands of datacenters capable of training new frontier models spread across the world. However, with the right personnel controls and inspection protocols, in-person inspections can complement other technical mechanisms — especially if an agreement is needed before technical mechanisms are mature.

Recomputation takes a different approach. A trusted third party receives the model and inputs and independently re-runs the computation according to agreed-upon rules to check whether it produces the same result. While initial experimental results have been promising, practical and security challenges remain: finding a mutually trusted third party, inspecting the hardware used to perform the recomputation, and preventing operators from exploiting gaps in the checks to conceal unauthorised computation.

ZKPs place trust in mathematical proofs. More precisely, they place trust in two things that can both be inspected. The first is a small set of cryptographic assumptions, of the same kinds that already protect online banking and most of the internet. The second is the software that produces and checks the proofs. That code, and specifically the verifier, can and should be fully open, so that both sides and anyone else can audit it, and ideally have its most critical parts formally verified using machine-checked mathematical proofs. This matters because a bug in a ZKP system can let a prover “prove” things that never happened, and such bugs have been found in high-stakes systems before.

What ZKPs can avoid is the need for ongoing trust in inspectors or trusted hardware. After an initial datacenter inspection to count the chips in a datacenter in order to ensure the ZKP checks are being applied to all the network traffic, the need for ongoing inspections is significantly reduced — provided changes to the facility and its hardware can also be accounted for. Initial inspections provides completeness: confidence that no compute is happening outside the system being monitored. The ZKP then provides correctness: cryptographic assurance that the computations covered by that system satisfy the agreed rules.on

Once this has been established, no trusted hardware is required": the proofs are produced by software running on the AI chips the provider already has, and they can be checked later by anyone on an ordinary laptop, not just by the other party to the agreement. If a weakness is found, the fix is a software update rather than a new generation of chips. And the trust runs the other way as well: the side being checked does not have to hand over its model or any other secrets, because all the proof does is establish compliance.

Getting to Open, Efficient ZKPs

To find out how far ZKPs are from being usable, we built one and measured it.

Our prototype is an open-source prover for Llama 3.1 8B, an open-weights model. It produces a proof that a given answer came from that exact model, without revealing the model weights. We built it to find out where the cost of proving goes, and we publish the code and all our measurements so that others can check them and build on them.

What we found. Until now, the field has assumed that proving an inference costs around 10,000 times more than running it. Our measurements come in far below that. A conversation that a server answers in a few seconds takes our prototype about an hour and a half to prove on a single GPU—at a cost of a few dollars at cloud prices, or roughly 50–1,000 times the cost of the inference, depending on the length of the prompt. Checking the proof takes two minutes on a normal computer.

While that is still too expensive to prove every request, a verifier does not have to: as described above, the verifier only asks for proofs of a random sample of requests. A provider that cheats on even a small share of its traffic would be caught quickly, and the verifier only pays for the sample. Requiring proofs for one in every 10,000 requests would cost a few hundred dollars a day for a provider serving a million requests daily. If 1% of sampled workloads were non-compliant, this would give a 63% chance of detection in one day and over 99.9% within a week. This renders sustained, compute-intensive operations, like model training, infeasible to conceal.

Where the cost goes. Most of the remaining work to reduce the overhead involves ordinary software engineering, not cryptography. Only a small part of the time is spent on the proof itself; the rest goes into preparing the data for it, and much of that work has not been optimised yet. We estimate that finishing it would bring our costs to roughly 10–350 times the cost of inference, depending on the length of the prompt and exactly how much time each optimisation saves us. This kind of engineering is well suited to AI: a proof either matches a trusted reference or it does not, so an AI can optimise the code while every change is checked against the reference implementation.

AI models, particularly ones tuned for mathematics research, could drive these costs down even further. As a result, we would be excited to collaborate with AI companies on applying these models to improve ZKPs. In particular, math models could dramatically improve ZKP efficiency and readiness for production by enabling us to:

• Prove floating point natively. Design field gadgets that make floating-point arithmetic nearly as cheap to prove as int8 and prove its soundness.
• Prove the real serving stack. Characterise production GPU kernels bit for bit and prove them as served, including batching, paged KV caches and sampling with committed seeds.
• Discover novel Freivalds-style shortcuts. Find randomised checks for everything that is expensive, such as attention, softmax, norms and rounding chains, each with a soundness bound.
• Invent new proof systems built for transformers. Go beyond gadgets and design a system around the structure of neural networks, then prove its soundness.
• Close the engineering gap. Port everything to the GPU and across many cards, with every change checked byte for byte against a reference.
• Verify the stack end-to-end. Build a machine-checked chain from a Lean statement of “this model produced this output” through the constraints and down to the prover/verifier code.

Frontier scale. We used our measurements to extrapolate the cost for larger models. Proving the same conversation with a 405-billion-parameter model, fifty times larger than the one we measured, would take 16 to 24 hours on one GPU today. If the engineering improvements we see for the 8B model carry over, that could come down to a few hours. The cost grows much more slowly than the model itself: fifty times the size, but only about sixteen times the cost.

Limitations. The prototype is a measurement tool, not something anyone should rely on yet. Nobody outside our team has checked the correctness of our implementation, and an independent audit is still to come. The model also has to be run in a quantised form to make it provable at that speed. On standard benchmarks, the modified model performs as well as the original, but providers would have to serve this exact version. Closing the gap between what we can prove and what providers serve in practice is where we think the most important work lies.