From b0b76f1472039303699528ec782cacc9a55963d8 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 29 Aug 2026 23:08:12 +0200 Subject: [PATCH] auto: 2026-08-29T21:08:12Z [skip ci] --- content/essays/verified-inference/index.md | 208 ++++++++++++++------- 1 file changed, 144 insertions(+), 64 deletions(-) diff --git a/content/essays/verified-inference/index.md b/content/essays/verified-inference/index.md index 0c326cd..4368753 100644 --- a/content/essays/verified-inference/index.md +++ b/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