auto: 2026-08-29T20:21:22Z [skip ci]

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.