AI progress is happening too fast.

Frontier model capabilities are progressing faster than our understanding of how to control them. Models are already hacking billion-dollar companies and breaking into government networks. Soon we may be able to build models so capable that we risk irrevocably losing control over them, and potentially over the future of humanity. To prepare for that, we need robust, cost-effective ways to pause the training of new models.

Suppose the United States government and the Chinese Communist Party agree to pause the training of newer, more capable models. How can each party be confident that the other is not covertly training models, especially when there are potentially enormous economic and military advantages to doing so? How can they be confident that the access needed to enforce the pause won’t be abused to gain top-secret information, such as model weights, architectures, or sensitive data?

This post aims to communicate the core of a proposal that uses cryptography (zero-knowledge proofs) and physical hardware (network taps) to verify compliance with a training pause, while allowing current AI models to remain in use. The ideas presented here are not our own; to learn more, see the reading list at the end.

Threat Model: Prover and Verifier

We model the enforcement of a training pause as an interaction between two adversarial actors: the prover and the verifier.

Under an international treaty regulating frontier AI development, any country with a data centre is a prover. They must convince the verifier that they are using their compute for approved purposes and not secretly diverting it to train models. The verifier could be an international body that makes sure everyone is following the rules.

The arrangement structurally favours the inspecting side: the prover has to evade every check, while the verifier only has to catch them once.^[1] This is the same logic behind the International Atomic Energy Agency, which verifies that countries aren’t secretly diverting nuclear material to build weapons.

Proposal Overview

The proposal has two key pieces: zero-knowledge proofs and network taps. Together they aim to ensure that everything leaving a compute pod (a group of GPUs that runs workloads inside the prover’s data centre) over the network was generated by inference. We explain both pieces in more depth later, but at a high level, zero-knowledge proofs tell the verifier what is happening. They let the prover convince the verifier that a given output was generated by model inference, without revealing sensitive information such as model weights, architecture, or input and output data. Network taps tell the verifier what isn’t happening. They let the verifier confirm that nothing other than data generated by approved inference is leaving the compute pod.

This protocol is one layer of a defence-in-depth approach. Other mechanisms are still needed to ensure that models aren’t being covertly trained and exfiltrated by other means. These include air-gapping compute clusters, monitoring, resource accounting, and memory wiping. In this post we treat these problems as out of scope; to learn more, see Naci Cankaya’s excellent post, A system overview for near-term, low-trust AI compute verification.

Inside the prover’s facility are two key pieces of hardware:

1. Compute Pods: collections of GPUs that run the workloads.
2. Network Taps: devices that collect all data passing into and out of the compute pods.

Diagram inspired by the one in Naci Cankaya’s post, A system overview for near-term, low-trust AI compute verification

This approach rests on a few assumptions that we take as given in this post. Most chips capable of training frontier models need to be accounted for and monitored in the way we describe below; otherwise, a rogue actor could train a frontier model on a secret compute cluster. The hardware inside the prover’s data centre must be installed correctly and the facility physically secure. Finally, all data leaving the compute pods must pass through a network tap.^[2]

We now outline a protocol that lets the prover keep running inference in their data centre while convincing the verifier that they are not covertly training a model.

Prover: Commits to a set of model weights and architecture M by sending the verifier a Pedersen commitment to M, which we denote ⟦M⟧. For now, you can think of a Pedersen commitment as a kind of cryptographic lockbox. The prover places M inside the lockbox and hands it to the verifier. The verifier can’t open the box, and can’t learn anything about M purely from having it. But the prover can convince the verifier of properties of the box’s contents and, if they wish, open it. Importantly, once the prover has sent the verifier ⟦M⟧, they can’t switch to a different model later in the protocol.

The prover then sends a stream of data (input₁, input₂, …) to the compute pods, claiming these are the inputs they want to feed to their model. Every input passes through the network tap, which sends a Pedersen commitment ⟦inputᵢ⟧ of each input to both the prover and the verifier.

The compute pods then perform a computation, which the prover claims is inference. The outputs of this computation (output₁, output₂, …) are returned to the prover.^[3] The network tap captures these outputs and sends a commitment ⟦outputᵢ⟧ of each one to both the prover and the verifier.

Verifier: The verifier randomly samples a subset of the output commitments and asks the prover to prove that this data was generated by inference on M. For example, if the verifier wants 99.99% confidence that at least 99.99% of the outputs were generated as claimed, they need to randomly select roughly 92,000 output commitments.^[4] The number of samples needed doesn't depend on the total number of output commitments, so verifying one hundred thousand forward passes takes the same number of samples as verifying one hundred trillion. This gives us the very nice property that the relative overhead of generating proofs goes to zero as the amount being verified goes to infinity.

The white paper Proposals and challenges for zero-knowledge verification of frontier AI training proposes using random sampling, along with proving only random pieces of the computation of a forward pass rather than the whole forward pass, to make zero-knowledge training verification tractable; the same idea extends to inference verification. There are several other promising approaches that leverage this idea, which we link in the reading list.

For simplicity, let’s say the verifier samples a single output commitment, ⟦output₁₆₅₅⟧.

Prover: Responds with the commitment to the corresponding input, ⟦input₁₆₅₅⟧. The prover then sends the verifier a zero-knowledge proof that output₁₆₅₅ = M(input₁₆₅₅). If output₁₆₅₅ = M(input₁₆₅₅) is true, the prover can always convince the verifier of this. If it’s false, the verifier will catch this with high probability. Throughout, the verifier learns nothing beyond whether or not output₁₆₅₅ = M(input₁₆₅₅). They don’t learn the model weights, the architecture,^[5] or the input or output. Since the prover has already sent the verifier the commitment ⟦M⟧, they can’t switch to a different model for the proof.

Verifier: If the verifier is convinced by the proofs, they are confident that most of the output of the compute pod (with exact numbers determined by the random sampling) was generated by approved inference. If this is not the case, the verifier knows the prover is doing unapproved work on the compute pod.

In this post, we use zero-knowledge proofs to verify that training isn’t happening by verifying that the overwhelming majority of data leaving the compute pods is generated by inference. With more sophisticated zero-knowledge proofs, we could enforce a wide range of governance objectives, such as bounding the amount of compute spent training a model.

We are particularly excited about zero-knowledge proofs as a way of enforcing a training pause. This is because most of the research needed to make this a reality is writing code and doing math that can be formally verified. Both are things AIs are already very good at and will likely keep improving at.

Zero-Knowledge Inference Verification

Much of the exposition here is taken (sometimes directly) from Justin Thaler’s wonderful book Proofs, Arguments, and Zero-Knowledge.

In the following sections, we slowly build a toy zero-knowledge proof of model inference.

1. How to Quickly Tell Functions Apart: Mathematical results that we use throughout the rest of the post.
2. The Sum-Check Protocol: A proof protocol, not yet zero-knowledge, which allows the prover to convince the verifier that a certain sum has a claimed value.
3. Verification of Matrix Multiplication: Using the sum-check protocol, we construct a proof protocol showing that a matrix product was computed correctly.
4. Going Zero Knowledge: Basic ideas from cryptography that we need to make our proof zero-knowledge.
5. Zero-Knowledge Proof of Matrix-Vector Multiplication: We construct a toy zero-knowledge proof of model inference. Here the model is a matrix M and the input is a vector x.

Before getting into the mathematical details, we give a high-level overview of what we are trying to build.

Some forms of computation come with efficient proofs of their correctness for free. For example, it is computationally challenging to find the solution to a Sudoku puzzle. But given a solution, it is easy to check its correctness. However, there are many computations whose correctness we would like to prove where it is not obvious how to do so.

For example, suppose you are a climate researcher and you pay a cloud provider to run a weather simulation at very high resolution, costing thousands of compute-hours. How can you be confident that the provider ran the high-resolution simulation and not a cheaper one? The results might look similar, and you cannot rerun the simulation yourself since you lack the computational resources. We want to turn this hard-to-verify computation into something easy to verify. This is where interactive proofs come in. You and the provider exchange a series of prescribed messages, through which the provider convinces you that they ran the correct simulation while you do very little computational work.

An interactive proof can also be used to convince a verifier that model inference was performed correctly. The difficulty is that the model provider may want to keep parts of the computation secret, such as the model weights. We are therefore interested in a special type of interactive proof, called a zero-knowledge proof, in which the verifier learns nothing from the interaction beyond whether or not the computation was performed correctly. For example, the prover could convince the verifier that they know the solution to a Sudoku puzzle without revealing anything about the solution.

Before introducing our first interactive proof protocol, we cover some mathematical prerequisites that will be crucial for efficient verification.

1. How to Quickly Tell Functions Apart

This section introduces efficient ways of telling polynomials apart, which we will use later to reduce the overhead of verification.

The Schwartz–Zippel Lemma

Consider two distinct polynomials f, g: ℝ → ℝ. They agree with probability zero at a point drawn uniformly from any interval of positive length.

Hence, we can tell f and g apart with high confidence by simply evaluating them at a random point.

The Schwartz–Zippel lemma allows us to extend this intuition to multivariate polynomials over any field. Let 𝔽 be any field, v ∈ ℕ, and f: 𝔽^v → 𝔽 a non-zero polynomial of total degree at most d, meaning that every monomial in f has exponents summing to at most d. On any finite set S ⊆ 𝔽, if (x₁, …, x_v) is drawn uniformly at random from S^v, then

Therefore, for d ≪ |𝔽|, P(f(x₁, …, x_v) = 0) ≈ 0.

For finite 𝔽, we have a simple corollary: any two distinct polynomials f, g: 𝔽^v → 𝔽 of total degree at most d agree at a uniformly random point of 𝔽^v with probability at most d/|𝔽|. This is because f − g is a non-zero polynomial of total degree at most d, and f − g = 0 exactly where f and g agree.

Therefore, if d ≪ |𝔽|, we can know with high confidence that two polynomials differ by simply evaluating them at a single point.

Multilinear Extensions

The proof protocols in this post require polynomials that take specific values on the Boolean hypercube {0,1}^v. In this section, we will show how to construct them.

Let 𝔽 be a finite field. Given a function

the multilinear extension of f, denoted f ′, is the unique polynomial

such that f ′(x) = f(x) for all x ∈ {0,1}^v and f ′ is linear in each variable. We can construct such polynomials using a version of Lagrange interpolation. For details, see Section 3.5 of Thaler’s book.

Multilinear extensions can be thought of as a distance amplifying function.

For example, take a large field 𝔽 with |𝔽| = 2²⁵⁶, and consider two functions into 𝔽

that differ at just one point. These functions are close together in the sense that for a random x in {0,1}¹⁰⁰, f(x) = g(x) with probability 1 − 2⁻¹⁰⁰. To tell f and g apart by querying them directly, we would need about 2⁹⁹ queries for a 50% chance of detecting a difference. Whereas their multilinear extensions are far apart. For a random x in 𝔽¹⁰⁰, f ′(x) = g ′(x) with probability 100/2²⁵⁶ ≈ 0. You can easily tell them apart by evaluating them at a single point.

Now we have everything we need to discuss the most important proof protocol.

2. The Sum-Check Protocol

The prover claims to have computed

for g ∈ 𝔽[X₁, …, X_v], where 𝔽 is a finite field. The sum-check protocol allows the verifier to check this claim in O(v) time, plus the cost of a single evaluation of g, by offloading most of the work to the untrusted prover. This is much faster than the O(2^v) time required to compute H directly. Meanwhile, the prover’s cost is only a constant factor more than computing H in the first place.

We care about the sum-check protocol because verifying many kinds of computation such as

• Matrix multiplication
• Layered arithmetic circuit evaluation

can be re-expressed as verifying that a sum of the above form holds.

The sum-check protocol is an interactive proof in which the prover and verifier exchange messages over v rounds. If all of the verifier’s checks during these rounds pass, the verifier accepts the prover’s claim.

Setup

Prover: Sends the verifier a value H* claimed to be equal to H.

Round 1

Prover: Sends the polynomial g₁(X₁) which they claim equals

Verifier: Checks that

along with checking the degree of g₁(X₁) does not exceed the maximum degree of g(X₁, …, X_v) in the variable X₁.

Then the verifier sends a random element r₁ ∈ 𝔽.

Round j

During rounds 1 to j−1, the verifier has sent one random challenge per round: r₁, …, r_j−1 ∈ 𝔽.

Prover: Sends a polynomial g_j(X_j) claimed to equal

Verifier: Checks that

along with checking the degree of g_j(X_j) does not exceed the maximum degree of g(X₁, …, X_v) in the variable X_j.

Then the verifier sends a random element r_j ∈ 𝔽.

Final round

Prover: Sends a polynomial g_v(X_v) claimed to equal

Verifier: Checks that

along with checking the degree of g_v(X_v) does not exceed the maximum degree of g(X₁, …, X_v) in the variable X_v.

Verifier: Picks a random element r_v ∈ 𝔽. Then with a single oracle query to g checks that

If all the checks the verifier has performed up to this point have passed, then the verifier accepts the proof.

No matter what the prover attempts, under the sum-check protocol they can only trick the verifier with probability ≤ vd/|𝔽|, where d is the maximum degree of g in any one variable. This bound is called the protocol’s soundness error. In practice we choose to work with a very large field, with on the order of 2²⁵⁶ elements, so the soundness error is negligible.

Proof of Soundness

The prover sends the value H* which they claim equals

Suppose H* is not equal to H. We prove by induction on v that a cheating prover tricks the verifier with probability at most vd/|𝔽|.

Base Case (v=1): The prover sends the verifier a univariate polynomial g₁(X₁). If this is equal to g, then g₁(0) + g₁(1) = H ≠ H* and the verifier rejects immediately. Otherwise, since any two distinct polynomials of degree at most d agree on at most d points, g₁(r₁) = g(r₁) with probability at most d/|𝔽|. So the prover passes the verifier’s final check with probability at most d/|𝔽|.

Inductive Hypothesis: For all v-variate polynomials g(X₁, …, X_v) of degree at most d in each variable, the sum-check protocol has soundness error at most vd/|𝔽|.

Inductive Step: Let g be a (v+1)-variate polynomial. In round one the prover sends g₁(X₁), claiming it equals

As before, g₁ cannot equal s₁, otherwise g₁(0) + g₁(1) = H ≠ H* and the verifier rejects immediately. Since g₁ ≠ s₁ we have g₁(r₁) = s₁(r₁) with probability at most d/|𝔽|. In this unlikely event, in round two the prover is left to prove the true statement

and the verifier accepts.

Otherwise g₁(r₁) ≠ s₁(r₁). The prover is left in round two to prove the false claim

By the inductive hypothesis the prover succeeds with probability at most vd/|𝔽|. Therefore the soundness error of the sum-check protocol on a (v+1)-variate polynomial is at most (v+1)d/|𝔽|.

QED

3. Verification of Matrix Multiplication

With the sum-check protocol in hand, we have everything we need to construct a proof of correct matrix multiplication. Let A, B, and C = AB be n × n matrices, where n = 2^ℓ for some integer ℓ. We define a function that sends each index of the matrix to the entry at that index.

If A is a 4 × 4 matrix, you can uniquely specify an entry with 4 bits: the first two bits specify the row, and the last two specify the column.

Given this way of encoding matrices we can rewrite matrix multiplication as

Therefore we have

This holds because both sides of the equation are multilinear extensions of f_C, and multilinear extensions are unique.

Our (not yet zero-knowledge) proof protocol for matrix multiplication falls out immediately.

Setup: Both the prover and the verifier know A and B. The prover sends C and claims that C = AB. The verifier wants to check this claim without computing AB themselves.

Verifier: Sends the prover random r₁, r₂ ∈ 𝔽^ℓ, and evaluates f ′_C(r₁, r₂) themselves.

Prover: Uses the sum-check protocol to convince the verifier that

So the two polynomials

agree at a random point. By Schwartz–Zippel, with high probability we have

and hence C = AB.

For a walkthrough of this protocol verifying a 2 × 2 matrix multiplication, see Section 4.4 of Thaler’s book.

Why not Freivalds’ algorithm? For those of you familiar with proof protocols, you may be wondering why we are introducing this rather complicated way of verifying matrix multiplication when we could just as easily use the much simpler Freivalds’ algorithm, which has the same verifier cost. The answer is that this is the algorithm used in practice because, when verifying matrix multiplication within a larger function such as a neural network, it reduces communication overhead far below that of Freivalds’ algorithm.

4. Going Zero Knowledge

The bedrock of many cryptographic protocols is functions that are easy to evaluate but very hard to invert. We can use such functions to build a cryptographic lockbox called a commitment scheme. The prover computes a commitment to x, denoted ⟦x⟧, from x and some secret randomness using a commitment scheme known to both parties, and sends it to the verifier. The prover can then prove properties of x using ⟦x⟧ alone. Later, the prover can open the commitment by revealing x (and the randomness), and the verifier can check that these match ⟦x⟧.

A good commitment scheme has two properties.

Computationally binding: Once the prover has sent ⟦x⟧, it is computationally infeasible to open ⟦x⟧ to another value x′ ≠ x.

Perfectly hiding: ⟦x⟧ reveals nothing about x to the verifier.

We will build a Pedersen commitment. Its binding property rests on the hardness of inverting exponentiation, known as the discrete logarithm problem.

The Discrete Logarithm Problem

Given an element h of a group 𝔾 generated by g, the discrete logarithm of h is the smallest non-negative integer x such that

The difficulty of the discrete logarithm problem depends on your choice of 𝔾. For some groups it is very easy, such as ℤ/mℤ under addition.^[6] For other groups it is incredibly difficult. For example, the discrete logarithm problem for well-chosen elliptic curves over a finite field is believed to be so difficult that it is the foundation of much of modern cryptography. For us, it is not important how this group is constructed, just that the best known algorithms for the discrete logarithm problem on these elliptic curves take exponential time, whereas exponentiation takes only polynomial time.

Pedersen Commitments

Let 𝔾 be a cyclic group of prime order q in which the discrete logarithm problem is hard. The Pedersen commitment scheme allows us to commit elements of 𝔽_q := ℤ/qℤ.

1. The prover and verifier randomly pick two generators g, h ∈ 𝔾.
2. To commit to an element m ∈ 𝔽_q known only to the prover, the prover picks r ∈ 𝔽_q uniformly at random^[7] and sends ⟦m⟧ = g^mh^r to the verifier. The verifier only receives the group element ⟦m⟧ and learns nothing about m or r.
3. To open the commitment, the prover sends (m, r) and the verifier checks that ⟦m⟧ = g^mh^r.

This scheme is perfectly hiding: the commitment ⟦m⟧ reveals nothing about the committed value m, since the randomness of r makes ⟦m⟧ uniformly distributed on 𝔾.

This scheme is computationally binding: to trick the verifier into believing they committed to some m′ ≠ m, the prover would need to find (m′, r′) such that ⟦m⟧ = g^m′h^r′. This amounts to solving the discrete logarithm problem, which is assumed to be computationally infeasible.

As the Pedersen commitment scheme involves randomness, committing to the same element twice gives different group elements. So to show that two commitments are to the same value, one must give a proof of this, called a proof of equality.^[8]

One very useful property is that Pedersen commitments are additively homomorphic. Since 𝔾 is abelian, we have

5. Zero-Knowledge Proof of Matrix–Vector Multiplication

Let M ∈ 𝔽^n×n be a secret matrix held by the prover, which one can think of as the secret model weights, and let x and y be the secret input and output of this model. The verifier holds the commitments ⟦M⟧, ⟦x⟧, and ⟦y⟧. We give a protocol for the prover to convince the verifier that Mx = y without revealing M, x, or y.

This protocol follows the same structure as the matrix multiplication proof given earlier, except that it is for matrix–vector multiplication, and that during the sum-check protocol the prover sends commitments to the polynomials rather than the polynomials themselves. This results in two important differences:

1. Our protocol is weakened from a proof to an argument. This means that a prover with unbounded computational resources could break the computational binding of the commitments and trick the verifier. Following standard usage, we nonetheless refer to it as a proof.
2. Our protocol is perfect zero-knowledge. Informally, this means the verifier has no way of learning anything beyond the fact that Mx = y.

For precise definitions, see Section 11.1 of Thaler’s book.

Prover: Claims that Mx = y.

Verifier: Computes the commitments to the multilinear extensions f ′_M, f ′_x, and f ′_y. For a detailed discussion of how to do this in general, see Section 3.5 of Thaler’s book. Here we give an example for a 2 × 2 matrix, to provide some intuition for how the verifier can compute ⟦f ′_M⟧ without access to M. Let

Then the multilinear extension of f_M is

Therefore the commitment to f ′_M, meaning the tuple of commitments to its coefficients, is

which the verifier can compute with access only to ⟦M⟧. It is also important to note that, because Pedersen commitments are additively homomorphic, the verifier can compute a commitment to f ′_M evaluated at any point using only ⟦f ′_M⟧.

Verifier: Doesn’t trust that Mx = y, so asks the prover for a zero-knowledge proof of this fact. As in the standard matrix multiplication proof, the verifier sends a random r ∈ 𝔽^ℓ, where ℓ = log n.

Now the prover must give a zero-knowledge sum-check proof that

where the verifier holds ⟦f ′_y(r)⟧, computed homomorphically from ⟦y⟧. Throughout, let

Round 1

Prover: Sends ⟦g₁(X₁)⟧, which they claim is a commitment to the polynomial

Verifier: Using the homomorphic property of the commitment scheme, the verifier computes ⟦g₁(0) + g₁(1)⟧. The prover then gives a proof of equality that

and also confirms that the degree of ⟦g₁(X₁)⟧ does not exceed the maximum degree of ⟦g(X₁, …, X_ℓ)⟧ in the variable X₁.

Then the verifier sends a random element r₁ ∈ 𝔽.

Round j

Prover: Sends ⟦g_j(X_j)⟧, which they claim is a commitment to the polynomial

Verifier: Uses the homomorphic property to compute ⟦g_j−1(r_j−1)⟧ and ⟦g_j(0) + g_j(1)⟧, then uses a proof of equality to check that

The verifier also checks that the degree of ⟦g_j(X_j)⟧ does not exceed the maximum degree of ⟦g(X₁, …, X_ℓ)⟧ in the variable X_j.

Then the verifier sends a random element r_j ∈ 𝔽.

Final Check

Prover: Sends ⟦g_ℓ(X_ℓ)⟧, which they claim is a commitment to the polynomial

Verifier: Using the homomorphic property of the commitment scheme and a proof of equality, checks that

The verifier also checks that the degree of ⟦g_ℓ(X_ℓ)⟧ does not exceed the maximum degree of ⟦g(X₁, …, X_ℓ)⟧ in the variable X_ℓ.

Verifier: Picks a random element r_ℓ ∈ 𝔽. Then computes ⟦g_ℓ(r_ℓ)⟧, ⟦f ′_M(r, r₁, …, r_ℓ)⟧, and ⟦f ′_x(r₁, …, r_ℓ)⟧. Since Pedersen commitments are only additively homomorphic, the verifier cannot compute a commitment to the product of the last two values on its own.

Prover: Gives a proof of product^[9] to show that

If all the checks the verifier has performed up to this point have passed, then the verifier accepts the proof.

The zero-knowledge version of the sum-check protocol inherits its soundness from the standard sum-check protocol. The one difference is that the soundness is now computational: the binding property of the Pedersen commitments means the prover can’t change polynomials after they are sent, but a prover who could break computational binding could switch polynomials mid-protocol and cheat.

The proof is zero-knowledge because the verifier only ever receives perfectly hiding commitments, which are uniformly random group elements, and proofs of equality and product, which are themselves zero-knowledge. As such, the verifier learns nothing beyond the fact that Mx = y.

Zero-Knowledge LLM Inference

In this post we built a zero-knowledge proof protocol for matrix–vector multiplication. A full proof for a large language model needs more building blocks. We need a way to verify non-arithmetic operations such as ReLU and softmax, and a way to stitch together the proofs for the attention heads, layer norm, and matrix multiplications. For an introduction to constructing efficient proofs of this kind, we recommend zkLLM: Zero Knowledge Proofs for Large Language Models. The state of the art for proof schemes of this form can prove the inference of a 400B-parameter model at roughly 70–95× the cost of running it; see Anthropic’s FlashProve.

How to Get Involved

Join the community

• Visit AI 2040’s how to get involved page and fill out their expression of interest form. Their list of organizations working in this space includes:
  • Lucid Computing
  • Amodo Design
  • FLI and the Singapore AI Safety Hub
  • The Compute Verification Project
  • RAND Center on AI, Security and Technology
  • The Oxford Martin AI Governance Initiative
  • ARIA: Trust Everything, Everywhere
  • The Frontier AI Security Residency
  • Verifiable Governance Community Night

Work on an open question

• Pursue a research direction outlined in Research Priorities for AI Compute Verification.
• Look at the open questions in A system overview for near-term, low-trust AI compute verification.
• Look at the thirteen open problems listed in Proposals and challenges for zero-knowledge verification of frontier AI training.
• Pick a project from the list at the end of The Compute Verification Post, which has concrete suggestions for engineers, funders, policy staff, and hobbyists.

This list is not exhaustive, and the right thing to work on depends on your skill set. If you are interested in getting involved, please reach out to me and I would be happy to help in any way I can.

Reading List

These are the resources I found most useful while writing this post, and the ones that have most influenced my thinking.

Proposals and challenges for zero-knowledge verification of frontier AI training — The white paper that convinced me to work on this problem.

A system overview for near-term, low-trust AI compute verification — An overview of compute verification approaches, mostly focused on recomputation. A fantastic resource.

Research Priorities for AI Compute Verification — What it says on the tin.

Verifying AI Compute by Bounding Unexplained Information Exfiltration — An approach to verification that bounds how much information could leave a data centre unaccounted for, rather than checking every output; the motivation for the sampling discussion above.

The Compute Verification Post — A broad primer on compute verification: what can be verified, under what trust assumptions, and with which techniques. Ends with a list of concrete projects.

zkLLM: Zero Knowledge Proofs for Large Language Models — An outline of an end-to-end implementation of zero-knowledge proofs for LLM inference.

Progress on provable inference for large language models — Anthropic’s FlashProve: an open-source, Lean-verified zero-knowledge proof of inference for a 400B-parameter model, with the current best overhead numbers.

An Introduction to the Theory of Elliptic Curves — A primer on the theory of elliptic curves and their use in cryptography.

Proofs, Arguments, and Zero-Knowledge — A fantastic overview of the full variety of proof protocols.

Acknowledgements

Thanks to Bennett Galamaga, Simon Schrader, Samantha Pease, Pierre Godfard, Ondřej Kubů, Pierre Peigné and Claude for helpful notes on drafts of this post. This work was done with the generous support of the Iliad Fellowship and a BlueDot Impact career transition grant.

1. ^{^}

   Some rate of false positives may be tolerated, as negotiated between the parties.

2. ^{^}

   This is quite a strong assumption. In reality we would want to use a combination of air-gapping compute clusters, monitoring, resource accounting, and memory wiping to prevent exfiltration of model weights via side channels.

3. ^{^}

   We model the compute pods’ inputs and outputs as a purely digital channel: everything the pods send or receive passes through the network tap as bits. Information leaking through physical side channels (e.g. electromagnetic emissions, power draw or acoustic signals) is out of scope here.

4. ^{^}

   In general, suppose a fraction p of the commitments are incorrect and the verifier checks n of them chosen independently at random. The probability that every check misses an incorrect commitment is (1 − p)ⁿ. To catch the prover with confidence at least 1 − δ, we need (1 − p)ⁿ ≤ δ, so the number of checks required is ⌈log_1-p(δ)⌉.

5. ^{^}

   While in principle the architecture can be kept secret, in this post we describe a protocol in which the architecture is public.

6. ^{^}

   You can compute the discrete logarithm in ℤ/mℤ under addition in polynomial time using the extended Euclidean algorithm.

7. ^{^}

   The binding property does not depend on r being random; only the hiding property does. So the prover is incentivized to actually pick a random r.

8. ^{^}

   Suppose the prover claims C₁ and C₂ are commitments to the same value. The prover uses Schnorr's protocol (see the section of Thaler's book on Σ-protocols) to prove knowledge of log_h(C₁C₂⁻¹). Knowing this discrete log lets the prover convert any opening of C₁ into an opening of C₂ to the same value, so either the two commitments really do commit to the same value, or the prover has broken the computational binding of the commitment scheme, which is assumed to be infeasible.

9. ^{^}

   See Section 12.3.2 of Thaler’s book.