diff --git a/content/essays/verified-inference/index.md b/content/essays/verified-inference/index.md new file mode 100644 index 0000000..0c326cd --- /dev/null +++ b/content/essays/verified-inference/index.md @@ -0,0 +1,201 @@ +--- +title: "Verified Inference Between Adversaries" +date: 2026-08-29 +abstract: > + A compute operator who claims to have run a particular model can be lying, and + the logs that would settle it are written by the party under suspicion. VerInf + produces zero-knowledge proofs of LLM inference, bounding the information in an + output stream that a committed model does not account for. This is a working + note on what the system certifies, what it does not, and what I contributed to + it during the MARS V fellowship. +tags: + - ai + - tech + - research + - research/machine-learning +status: "Working model" +confidence: 85 +importance: 4 +evidence: 4 +scope: broad +novelty: moderate +practicality: moderate +history: + - date: "2026-08-29" +--- + +A datacenter tells you it ran a 400-billion-parameter model on your prompt. It +might have run a smaller one, an older checkpoint, or a quantized copy that +costs a fraction as much. Ordinary logging cannot settle this, because the logs +are produced by the party whose behavior is in question. Neither can a hash of +the weights: the operator can hold the right weights and still run something +else. + +This is not a hypothetical failure mode so much as an unresolved gap in every +current deployment story. Evaluations measure a model under conditions you +control; they say nothing about the model served to somebody else afterward. +Attestation binds a binary to a machine; it does not bind an output to a +computation. What is missing is a way for a verifier to check a claim about a +computation without trusting the party that ran it. + +[VerInf](https://github.com/JamesPetrie/VerInf) is a research prototype +addressing that gap, built by James Petrie at the Future of Life Institute. I +worked on it as a [MARS V](https://caish.org/mars) fellow. This note describes +what the system proves, what it does not, and which parts of it are mine. + +## What the proof certifies + +The naive framing — "prove the model produced this output" — is the wrong one, +and understanding why is most of the insight. Frontier inference runs in +floating point, on nondeterministic kernels, across hardware that does not +reproduce bit-for-bit. Demanding exact reproduction would make the problem +intractable and would not even be the property you want. + +VerInf instead bounds the **unexplained information** in an output stream: the +number of bits in the output that the committed model does not account for. If +the operator swapped in a different model, the outputs it produced would be +poorly predicted by the model it committed to, and the bound rises. A cheap +substitution is expensive to hide. + +The certified statement is a conjunction of three parts, and they are held to +different standards: + +- a **transcript anchor**, binding the committed token streams to digests + recorded independently at generation time, so the proof is about the run that + actually happened rather than a convenient reconstruction; +- the **forward pass**, where every claim must admit exactly one satisfying + assignment, because slack in an intermediate value propagates through the + remaining layers in directions nobody can analyze; +- the **surprisal bound** itself, where freedom *is* permitted — provided every + free direction pushes the reported number up rather than down. + +That asymmetry is the elegant part. Upstream of the logits the prover must have +no room at all; downstream, in the short arithmetic from logits to the reported +bound, the prover may have room so long as every rounding is forced upward. +Cheating can only make your own number worse. + +A related move governs the predictor. The bound is computed against a predictor +of the deployment's outputs that the *prover* supplies — which sounds like +handing the adversary the pen. By Gibbs' inequality the resulting sum is a valid +upper bound for *any* predictor, so the choice can be left to the prover +entirely. The scheme is sound whatever they pick; a bad choice only inflates +their own reported bound. + +Underneath, matrix products are checked with Freivalds projections over Ligero +commitments, which are hash-based — so there is no trusted setup, and the +construction is plausibly post-quantum. + +## Who trusts whom + +The two parties want different things, and the design is legible once you see +that. + +The **prover** wants confidentiality: weights, activations, and both token +streams must not leak. The **verifier** wants soundness: the reported bound must +be genuine. Their interface is a public claim list stating what kind of +computation was performed — which reveals the model architecture, though not the +weights. + +Each side trusts only its own code. The verifier's trusted base is deliberately +small, and it shares no code with the prover. A fault anywhere on the prover's +side can cause a proof to fail; it cannot cause one to falsely verify. + +## Results on record + +These are the published single-chip numbers, and they predate my involvement. + +| | Llama-4-Maverick | Llama-2-7B | +|:---|:---|:---| +| Parameters | 400B MoE, 48 layers, 128 experts committed per layer | 7B, 32 layers | +| Transcript | 1000 tokens, **all hidden** | 1000 tokens | +| Prove | 14.3 h, 78.1 GB GPU peak | ~44 min, 11.2 GB peak | +| Verify | 17.7 h, 20 CPU cores, 40 columns opened | ~23 min, 10 columns | +| Proof size | 93.6 GB | 1.44 GB | +| Bound | 0.880 bits/token | — | + +All on a single NVIDIA DGX Spark. The committed witness for the Maverick run is +roughly 7.2 TB, streamed at the working set rather than held. + +The bound is the number to read. At 0.880 bits per token against a +202,048-token vocabulary, the proof accounts for about 95% of the information a +token could carry. That is not "the model produced this"; it is "very little +here is unexplained by the model that was committed." + +## What I contributed + +Parallelizing the prover across GPUs is named future work in the paper, and it +is the direction I am working in. It runs into an immediate problem: you cannot +measure a cluster you do not yet have access to, and partitioning decisions have +to be made before the hardware arrives. + +So the first deliverable was not parallelism — it was the measurement +scaffolding parallelism needs. I built a **dry-run profiler** that predicts a +proving run's time, memory, bandwidth, and proof size *before* running it, from +a workload manifest plus measured hardware constants, and exposes the dependency +structure a future scheduler will consume: + +- a **manifest contract** — one record per tape operation, with two independent + producers (an exact tape-walker that runs where the prover runs, and + closed-form builders in pure Python that cross-check it); +- a **cost model** in per-claim accounting form, carrying the production + expressions from the paper's cost appendix; +- a **claim-level dependency DAG** with critical path and width profile, which + is what tells you how much parallelism actually exists; +- a **partition scorecard** that maps claims onto *N* shards under competing + strategies — contiguous tape ranges, pipelined layers, expert-sharded — and + scores them. + +One deliberate constraint: none of it touches the soundness-critical prover +path. A profiler that could perturb the proof would be a liability in a system +whose entire value is that a fault cannot cause false acceptance. + +I also corrected the cost model's RMSNorm row to the wrap-free bracket +constants, bringing it into line with the paper's own analysis. + +Both are merged upstream: + +::: {.work-entry-links} +[Merged pull requests](https://github.com/JamesPetrie/VerInf/pulls?q=is%3Apr+author%3Alevineuwirth) · +[Upstream repository](https://github.com/JamesPetrie/VerInf) +::: + +**In progress:** the multi-GPU port itself. The aim is not parallelism for its +own sake — multi-device proving is what lifts the ceiling on model scale, +context length, and mixture-of-experts breadth. Results are preliminary and +unmerged; I will report them here when they are not. + +## What this does not do + +The honest list, mostly from the paper's own limitations section: + +- **No security review.** It is a research prototype. +- **The proofs are enormous** — 93.6 GB at full scale. This is a real deployment + obstacle, not a rounding error. +- **0.880 bits per token is not zero.** For some applications that residue is + fine; for others it is not, and the paper is explicit that tightening it is + open work. +- **Soundness is a per-challenge bound** (about 2⁻¹⁶·⁶ in the demonstrated + configuration), raised by opening more columns at a measured cost in + verification time. It is a deployment choice, not a fixed property. +- **The claim list reveals the architecture.** Hiding that too is future work. +- **The transcript anchor is not yet demonstrated end to end.** The AES and + SHA-256 circuits are implemented and tested; binding them against + independently recorded digests is not yet shown. + +That last one is the gap I would press on hardest if I were reviewing this. The +anchor is what makes the bound a statement about a *particular real run* rather +than about some internally consistent transcript. Everything else is +cryptographic machinery; that is the part that connects it to the world. + +## Why this matters for assurance + +The reason to care is not that datacenters are presumed dishonest. It is that +"trust us, we ran the model we said" is the current state of the art, and it +does not scale to a world where the stakes of that claim keep rising — +third-party evaluation, regulatory audit, compute governance, any arrangement +where an inference claim carries weight and the parties are not aligned. + +Verified inference is one approach to a general question: how do you establish +trustworthy claims about an AI system when the system, the operator, and the +evaluator may each be untrusted? Cryptography attacks it from below. Evaluations +attack it from above. Neither is sufficient alone.