Tomer Solberg
7 min
Abstract
We present Sable, an argument system and single-GPU prover for the statement that a committed, integer-quantized transformer produced a given token sequence from a given prompt, bit for bit. Sable fixes an integer function F_O with no floating-point step, in which every rounding, normalization, softmax and sampling decision is determined by its inputs, and proves it with a constraint system whose relations provably never wrap modulo the 31-bit KoalaBear prime. The proof batches zerochecks and LogUp-GKR lookups into one sumcheck per domain, and commits to every witness tensor and weight in one multilinear commitment built from Reed-Solomon codes, BLAKE3 Merkle trees and a mixed-length BaseFold opening. The prover streams the model layer by layer on one GPU. On one NVIDIA RTX PRO 6000 Blackwell GPU, Sable proves all 64 layers of Qwen2.5-32B in 92.5 s for 4,096 tokens and 398 s for 16,384 tokens, and covers Qwen3-32B and the mixture-of-experts Qwen3-30B-A3B (4,096 tokens in 121.8 and 84.7 s). A proof costs 41 to 50 times the serving time, or 6.4 cents per 4,096-token request at public GPU prices, and 40 to 64 times less time per parameter and token than zkLLM. On WikiText-2, F_O's greedy token matches the BF16 model's at 86.3% of positions; on Qwen3, F_O is within 1.6 points of BF16 on MMLU and 1.7 points on GSM8K. A verifier with a compiled core checks a proof on one CPU core in 19 to 56 s. In the random-oracle model, the interactive proof has round-by-round soundness error 2^-103. The proof is not zero-knowledge, so the system targets open-weight models. Code: https://github.com/moonmath-ai/Sable
Alex: Earlier systems already proved neural-network calculations. What is new here, beyond carefully specifying the model?
Sam: The paper combines exactness with small-field arithmetic and a streamed prover. A finite field is arithmetic that wraps around a fixed prime. Small fields are fast on hardware, but that wraparound creates a serious correctness problem.
Alex: If the proof checks the arithmetic, how can wraparound let an incorrect calculation through?
Sam: Because equality after wrapping need not mean equality between ordinary integers. During development, the author found a specific loophole in left shifts, which multiply by powers of two. An oversized result could wrap into the allowed output range and satisfy the existing checks.
Alex: So checking that the final value looks small is not enough. You also need to establish that the calculation never crossed the boundary.
Sam: Sable adds an input bound that closes that gap, and a regression test checks the forged cases are rejected. More generally, each arithmetic gadget has explicit bounds. The paper proves that satisfying those checks means satisfying the intended integer calculation.
Alex: That handles correctness locally. What makes proving an entire large model fit on one graphics processor?
Sam: The key is not to keep the entire execution. The witness—the intermediate values used to establish the proof—is far too large. Sable saves the residual stream at layer boundaries, then rebuilds each layer’s detailed values when needed.
Alex: So it trades repeated calculation for storage. How does the proof follow that schedule?
Sam: The commitment pass runs forward, committing intermediate values and counting lookup uses. The proving pass moves backward, turning claims about a layer’s outputs into claims about its inputs and weights. The later query phase rebuilds layer values again rather than retaining the whole trace.
Alex: Where does the title’s “sumcheck” fit? Is that another storage trick?
Sam: Sumcheck reduces a claim about a large polynomial sum to smaller checks. Sable combines checks that constraints vanish with the bottom layer of its lookup proof, saving a separate sumcheck. It also partitions lookups into chunks, because too many repeated entries could cancel in the small field.
Alex: Let’s put the speed claim in context. What did the implementation actually prove?
Sam: On the reported Blackwell graphics processor, it proved the full Qwen2.5 model with roughly thirty-two billion parameters. For a sequence of about four thousand tokens, proving took about ninety-three seconds. Those timings cover the full model, not selected layers.
Alex: A minute and a half sounds manageable, but the relevant comparison is ordinary inference. How much extra work does verification add?
Sam: Producing the proof took roughly fifty times as long as computing the same tokens in the author’s exact-integer serving engine. That is not a comparison against an arbitrary hosted service. The same prover also handles the added query-and-key normalization and mixture-of-experts structure in Qwen3.
Alex: What about the person checking it? A fast prover does not necessarily make a convenient proof.
Sam: The full-model proof for that shorter sequence is about a hundred and thirty-five mebibytes. Checking it takes nineteen seconds on a single processor core with a compiled core verifier. The author calls this an auditor’s proof, rather than something ready for every client request.
Alex: There is another cost we have not measured yet. If you change the model’s arithmetic, how much does its behavior change?
Sam: On WikiText-2, the integer model’s greedy token matches the standard floating-point model at about eighty-six percent of positions. Its perplexity, a measure of predictive performance, is about eight percent higher. Exactness proves the integer model ran correctly; it does not erase that accuracy loss.
Alex: Does the paper offer evidence that the loss can be reduced without making proofs more expensive?
Sam: On Qwen3, it adjusts how attention-score scaling is divided between queries and keys. That reduces the reported perplexity gap without changing proof cost. The paper also reports close task-benchmark scores, but those do not make the models behaviorally identical.
Alex: How should a researcher judge the security claims, beyond the benchmarks?
Sam: There are formal bounds, under random-oracle and hash assumptions, and the code and measurement scripts are released. But the author identifies a commitment-analysis step combining existing results that no published theorem covers exactly. I would treat that explicit caveat as part of the security claim.
Alex: And privacy? Could a provider use this unchanged for a closed model or confidential prompts?
Sam: The proof is not zero-knowledge: it reveals information about the computation and weights. Repeated proofs can eventually expose closed weights, and batched verification requires access to every included prompt. The present system is intended for open-weight models and authorized auditors; privacy-preserving recursive compression remains future work.
Alex: Given those boundaries, who should read the full document, and where should they begin?
Sam: Researchers building verifiable inference should start with “The integer function” and “Threat Model and Scope.” Proof-system researchers should read “The protocol” and “Security,” especially the wraparound bounds and commitment-analysis caveat. For everyone else: a proof certifies the calculation you specified, not the model you merely meant to serve.
Alex: Thanks for listening.