Autoregression & certification

Proving inference · Operator atlas · Autoregression & certification

Autoregression & certification

KV caching, sequence certification — the trick that kills the quadratic

$$\begin{aligned} \text{prompt} &: \texttt{"The cat"}\\ \text{claimed} &: \texttt{"sat on the mat"}\\[6pt] \text{concatenated} &: [\texttt{The},\, \texttt{cat},\, \texttt{sat},\, \texttt{on},\, \texttt{the},\, \texttt{mat}]\\ \text{predicted} &: [\texttt{cat},\, \texttt{sat},\, \texttt{on},\, \texttt{the},\, \texttt{mat},\, \bot]\\[6pt] \text{certify} &\iff \text{predicted}[t] = \text{concatenated}[t{+}1]\quad \forall t \end{aligned} \\[8pt] \text{one forward pass} \;\Rightarrow\; \text{prover } O(t\,|C|),\;\text{not } O(t^2 |C|)$$

The algorithm

Rather than proving $t$ sequential generation steps, prove one forward pass over the concatenated prompt-and-output, and check that every position predicts its successor.

Why it resists a proof

This is the difference between a demo and a system. Every prior work proves a single token, because the honest alternative — emulating a KV cache as in-circuit RAM — requires committing to auxiliary data linear in the number of reads and writes.

Cryptographic toolbox

Causal mask ⇒ position t cannot see token t+1
Argmax ⇒ the forward pass is deterministic
Many predictions in one pass ⇒ everything batches

How each scheme proves it

DeepProve

Certify the output rather than replay the computation. Soundness rests entirely on the causal mask plus determinism.

Our certification algorithm for this is extremely simple: It just feeds the entire sequence of input and output tokens into the model at once, essentially performing a single inference step. In practice, this translates to proving only the last inference step leading to prover times that are only linear to the input and output tokens rather than quadratic.
DeepProve · §3.1

Because of the Attention Mask, the model's calculation for the $t$-th token cannot use the values of the $(t+1)$-th token. Moreover, argmax in the final layer of GPT-2 and Gemma 3 provides determinism to the execution.
DeepProve · §3.1

The attention mask guarantees the model's computation at position $t$ cannot depend on token $t{+}1$. So if the prediction at $t$ equals the claimed token at $t{+}1$, that token was correctly computed. Argmax supplies the determinism.
Reduces prover cost from quadratic to linear in total sequence length, with no in-circuit RAM and no KV-cache emulation.
A single pass produces $s$ predictions simultaneously, which is exactly what the batched softmax, lookup and sumcheck variants exist to exploit. The trick and the batching are co-designed.
This is why throughput increases with sequence length (127 → 175 TPM as sequence goes 64 → 512): matmul's sublinear prover cost amortizes across more tokens.

Jolt Atlas

The prover proves a single forward pass over a fixed-length sequence — there is no autoregression and no KV cache in the proving path. Generation exists only as an unproven execution helper, and it re-runs the whole model per token.

The prover proves one forward pass. Every prover entry point (gpt2.rs, qwen.rs, bge.rs, gpt2_zk_bench.rs, e2e tests) builds one input with ("sequence_length", s), ("past_sequence_length", 0), calls ONNXProof::prove once and verify once. There is no loop over generated tokens anywhere in jolt-atlas-core.
No KV cache exists — grepping kv_cache / past_key_values / present_key / use_cache returns nothing. past_sequence_length is a plumbing parameter the exported ONNX graph accepts, but it is hard-coded to 0 at all ~10 call sites; a past-KV input is never populated.
Generation is a naive quadratic helper in the tracer (gpt2_generate.rs), not the prover: each token reloads the model and runs a full forward pass over the entire growing sequence [1, cur_len], argmaxes the last logit row, appends, repeats. It exists to sanity-check quantized-vs-float coherence, and produces no proof.
So the two systems live on opposite ends of this axis. DeepProve certifies the whole generated sequence in one pass with the trick on the left; Jolt Atlas proves a single forward pass and never composes tokens. zkPyTorch takes a third route — it batches all tokens into one circuit by decoupling the autoregressive dependency (a proof only verifies the output).
Note Jolt Atlas could express a KV cache as read/write consistency — it already has the Twist-and-Shout memory machinery for Gather. It simply doesn't, because there is no cache to check. That is the same trade DeepProve names: emulating a KV cache would introduce RAM into a computation that otherwise has none.