auto: 2026-08-29T21:08:12Z [skip ci]

content/essays/verified-inference/index.md

@@ -24,71 +24,71 @@ history:
   - date: "2026-08-29"
 ---
 
-A datacenter tells you it ran a 400-billion-parameter model on your prompt. It
+A datacenter asserts that 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.
 
+Similarly, assume that a treaty between two governments is reached regarding
+AI research and development. Both governments claim that they are using particular
+models that meet certain thresholds, have been approved by regulatory boards, etc.
+The same problem applies; there is not any obvious way for one party to such an
+agreement to verify the claims of the other.
+
 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.
+current deployment. Evaluations measure a model under conditions you
+control, saying nothing about the model served to somebody else afterward.
+Attestation binds a binary to a machine, rather than binding an output to a
+computation. What is missing is a way for an independent verifier, run on independent hardware,
+to check a claim about a computation without trusting the party that ran it, or the hardware it ran on.
 
 [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.
+addressing that gap, led by James Petrie at the Future of Life Institute. I
+work on it as a [MARS V](https://caish.org/mars) fellow. This living document
+details what the system does and does not currently prove, where we think it is heading,
+and my future ambitions for this line of work.
 
 ## 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.
+The naive framing — chiefly, "prove the model produced this output" — is the wrong one.
+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 even worse,
+it isn't really even addressing the right problem. 
 
 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.
+substitution is therefore expensive to hide.
 
-The certified statement is a conjunction of three parts, and they are held to
-different standards:
+Our certified statement is a conjunction of three parts 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;
+- a **transcript anchor**, which binds the committed token streams to digests
+  recorded independently at generation time. This ensures 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
+  assignment. Slack in an intermediate value would propagate through the
   remaining layers in directions nobody can analyze;
-- the **surprisal bound** itself, where freedom *is* permitted — provided every
+- 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.
+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.
+In an elegant twist, 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.
+A related move governs our predictor. The bound is computed against a predictor
+of the deployment's outputs that the *prover* supplies.
+By [Gibbs' inequality](https://en.wikipedia.org/wiki/Gibbs%27_inequality) the resulting sum 
+is a valid upper bound for *any* predictor, so the choice can indeed be left to the prover
+entirely. 
 
-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.
+Underneath, matrix products are checked with Freivalds projections over [Ligero](https://link.springer.com/content/pdf/10.1007/s10623-023-01222-8.pdf)
+commitments, which are hash-based — so there is no trusted setup, and the construction is plausibly post-quantum^[Future research intends to make this statement of "plausible" post-quantum security into one of "definitive" post-quantum security.].
 
-## Who trusts whom
-
-The two parties want different things, and the design is legible once you see
-that.
+## Where trust is required
 
 The **prover** wants confidentiality: weights, activations, and both token
 streams must not leak. The **verifier** wants soundness: the reported bound must
@@ -96,13 +96,18 @@ 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.
+Each side trusts only its own code, and only its own hardware. 
+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. Similarly, we envision that in a setup between 
+Governments, each government would be able to use their own hardware for their verifier of the other party's proofs, and no
+trust of the datacenter in which this takes place would be required.
 
 ## Results on record
 
-These are the published single-chip numbers, and they predate my involvement.
+These are the published single-chip results, and they predate my involvement.
+My own measurements — validation of the cost model, and the first figures from
+Blackwell hardware — are in [What I contributed](#what-i-contributed) below,
+separated there by what has merged upstream and what has not.
 
 | | Llama-4-Maverick | Llama-2-7B |
 |:---|:---|:---|
@@ -116,8 +121,7 @@ These are the published single-chip numbers, and they predate my involvement.
 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
+ 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."
 
@@ -128,8 +132,8 @@ 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
+My first deliverable was the measurement scaffolding that 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:
@@ -145,31 +149,102 @@ structure a future scheduler will consume:
   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.
+A profiler is only as good as its predictions, so validation came in two
+rounds. The first was retrodictive: predict the archived Maverick run from a
+synthetic manifest plus the development box's measured constants, then compare
+against what that run actually recorded.
+
+| quantity | predicted | measured |
+|:---|:---|:---|
+| witness rows | 108.7 M | 109.27 M |
+| proof size | 93.1 GB | 93.6 GB |
+| opened-column GPU payload | 34.8 GB | ~35 GB |
+| verifier peak RSS | 76.1 GB | 75.7 GB |
+| proof dump time | 751 s | 756 s |
+| prove wall-clock | 3.0 h floor / 9.9 h aggregate | 14.26 h |
+
+Prove time is deliberately a *bracket*, not a point estimate. The floor is the
+bandwidth-bound target the design should reach after planned reorganization;
+the aggregate is calibrated on today's code. The gap between bracket and
+measurement is not error — it is the itemized implementation overhead, which
+is to say the work-list.
+
+The second round I ran end to end myself, on hardware the tooling had never
+seen: a single rented B200, the class of machine the multi-GPU effort actually
+targets. One morning and about eleven dollars of GPU time later:
+
+- the calibration suite filled a complete machine profile from scratch, every
+  constant measured on the box with its provenance recorded (headline: 29×
+  the development box's memory bandwidth);
+- the exact tape-walker ran against real tapes for the first time and
+  **cross-checked clean against the closed-form builders — zero flags**: every
+  claim count, witness slot, linear constraint, and quadratic product matched
+  within the documented expected set, and the per-row witness layout agreed
+  with the prover's own accounting row for row;
+- the extracted Maverick manifest reported **109,273,513 witness rows,
+  against the production run's measured 109.27 M** — the profiler reproducing
+  reality, not merely its own model of it;
+- the first cost bracket priced on measured Blackwell constants put the full
+  Maverick proof at a **376-second floor** on one B200 — roughly 28× the
+  development box, tracking the measured bandwidth ratio almost exactly,
+  which is what the cost model's scaling story says should happen when the
+  dominant terms ride memory bandwidth.
 
 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:
+### A retraction
+
+The same B200 session produced a finding I later had to withdraw: an apparent
+interconnect bottleneck that turned out to be almost entirely an artifact of my
+own traffic model. Nothing was wrong with the machine; something was wrong with
+what I had assumed about it.
+
+I record it because it is the discipline the whole exercise exists to enforce.
+A profiler that only ever confirms its author is not a measurement instrument.
+Predictions go out before the measurement, and get corrected in public when the
+measurement disagrees — otherwise the numbers above would be worth very little.
+
+### What is upstream, and what is not
+
+**Merged** — the dry-run profiler (manifest contract, cost model, execution DAG,
+partition scorecard) and the RMSNorm cost-model correction.
+
+**Not yet merged, landing shortly** — the calibration suite, the tape-walker's
+first run against real tapes, the measured Blackwell machine profile, and the
+B200 figures reported above. Treat those as reported-by-me until they appear in
+the pull request list.
 
 ::: {.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.
+## Where this goes next
 
-## What this does not do
+The immediate step is a port to 2–8 GPUs, and the reason is not that more GPUs
+sound better. Multi-device proving is what lifts the ceiling on model scale,
+context length, and mixture-of-experts breadth — the dimensions along which a
+single box runs out first.
 
-The honest list, mostly from the paper's own limitations section:
+The honest projection carries the same bracket as everything else here. The
+anchor is a **376-second floor for the full Maverick proof on one B200**: a
+floor, not today's code, and it assumes the reorganization the cost model
+already itemizes. Distributing that across 2–8 devices puts a 400B proof in the
+low minutes if the partition scales cleanly, and under a minute at the
+optimistic end. Both numbers are projections from a model validated against one
+archived run and one live machine — good enough to plan against, not yet a
+measurement.
 
-- **No security review.** It is a research prototype.
-- **The proofs are enormous** — 93.6 GB at full scale. This is a real deployment
+Beyond that, fleets of 64–128 GPUs are what an order-of-magnitude larger model
+would require. That figure comes from the same cost model and has not been
+validated at that scale.
+
+## Current Limitations
+While VerInf looks promising, there are currently limitations:
+
+- **No security audit.** It is a research prototype.
+- **Proof Size** — 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
@@ -177,15 +252,20 @@ The honest list, mostly from the paper's own limitations section:
 - **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 claim list reveals the architecture.** 
 - **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.
+## Future Directions
+[TODO: review, and potentially rewrite or reposition. This should be a very strong place]
+My vision is to combine this work with other research projects of mine. LeVCS is a 
+federated version control system that is undergoing a rewrite for an agentic focus. 
+Similarly, my recent contract work on model evaluation alongside less recent work on
+agentic debugging has demonstrated many gaps to which bounding the information that
+comes from a model. I believe that there are major safety implications to applying
+ZKP proof techniques developed in VerInf to agentic contexts, and that further extensions
+of my work will also allow for breakthroughs in detection of and handling of alignment faking.
 
 ## Why this matters for assurance