Sable proves which tokens a quantized language model produced
Sable: A Small-Field Sumcheck Argument for Bit-Exact Inference of Large Language Models · arXiv:2611.14083
In plain words
Sable is a system for checking whether a language model produced particular words from a particular prompt and set of committed weights. It turns the model’s work into a fixed, exact integer calculation, then creates a proof that a verifier can check.
On one GPU, Sable proved runs of large Qwen models. The calculation it proves is not identical to the original model: on one text-prediction test, its Qwen2.5-32B version had higher perplexity than the original BF16 model.
The research
A proof can show that an output came from specified weights and a prompt, but only for the exact computation the proof describes.
Sable makes that check possible for large quantized transformers on one GPU; its separate accuracy comparison matters because a verifiable computation can still differ from the original model.
Sable defines an exact integer version of transformer inference and proves that a committed, quantized model produced the stated tokens from its prompt.
For its main scale test, Sable proved the specified computation for Qwen2.5-32B on one GPU.
A 4,096-token sequence, including 16 generated tokens, took a mean of 92.5 seconds to prove, and across three tested shapes proving took 41 to 50 times as long as the serving engine computed the same integer-model work.
A separate WikiText-2 comparison found 8.3% higher perplexity for this integer function than for the BF16 checkpoint. That measures a language-model prediction difference, so the proof’s result is feasibility for the tested workloads with an accuracy cost, not equivalence to the original model.
Sable proves the defined integer function, not that it matches the original BF16 model. Its current proofs also reveal information about the trace and weights, so the system is intended for auditing open-weight models.
What the evidence shows
- The verification problem
A verifier needs to check that an output came from the committed model weights and prompt, and that sampling followed a client-fixed seed. Ordinary floating-point inference can vary with the kernel, batch shape, or arithmetic order.
For a long run, the trace can also be too large to keep in memory, while checking all its lookups in one small prime field can undermine proof soundness.
- A fixed computation to prove
Sable is an argument system and single-GPU prover that proves a committed, quantized transformer produced a specified token sequence from a prompt. It defines a deterministic integer function, F_O, that fixes rounding and other choices so there is one exact computation to prove.
This makes the statement checkable, while defining what exactly the proof guarantees: execution of F_O, not equivalence to the original floating-point model.
- Proofs take time
The timing comparison shows the cost of proving the same integer-model computation. Across three tested Qwen2.5-32B shapes, proof generation took 41 to 50 times as long as the serving engine; for one 4,096-token sequence that includes 16 generated tokens, mean proof time was 92.5 seconds on one GPU.
- The accuracy tradeoff
The integer function’s accuracy is a separate question from whether its execution can be proved. On WikiText-2, perplexity, a measure of how well the model predicts text, was 8.3% higher for Qwen2.5-32B-Instruct’s F_O than for its BF16 checkpoint.
That comparison bounds the accuracy claim to this model and test; it does not turn the proof into evidence about every model task.
- Tracing part of the gap
A precision test helps locate part of that WikiText-2 gap. Raising query and key precision from 8 to 12 bits removed 37% of F_O’s excess log-perplexity over BF16, where the denominator is the original excess gap.
This attributes part of the measured difference to those precisions in that evaluation. The variant was not provable as implemented, so its result is not a result for Sable’s built proof system.
Deep
- Original paper authors
- Tomer Solberg
- Submitted to arXiv
- License
- CC BY 4.0