[Submitted on 24 Sep 2026 (v1), last revised 24 Sep 2026 (this version, v2)]
Title:Quantized GPT-2 Inference with Exact WebAssembly Proofs: Arithmetic, Cached Execution, and Numerical Evidence
Abstract: Quantization changes a language model’s arithmetic, storage, and output, while deployment adds obligations about compiled instructions and retained state. We extend LeanExe’s GPT-2 124M example with signed eight-bit weights and projection inputs, 32-bit integer accumulation, and binary32 operations elsewhere. A Lean-checked theorem connects the exact 28,315-byte WebAssembly binary to the specified quantized cached-inference algorithm, including validation, termination, allocation, and buffer release for sessions of at most 128 tokens. The specification fixes scale selection, nearest-even rounding, saturation, and the order of all rescaling operations. An initial scale per activation row caused severe output degradation. Scales for consecutive groups of 64 coordinates improved greedy agreement with the binary32 implementation from 87 to 120 of 128 retained prefixes. The deployed grouped model matches its independent reference bit for bit on 6,432,896 logits, 128 complete caches, and nine completions. Its checkpoint occupies 74.3% less storage. A controlled resident-session benchmark measures a 3.59-fold median speedup and a 34.7% reduction in warm WebAssembly memory. Across 302 evaluated positions, including prefixes of six held-out prompts, greedy choices agree at 263 positions. Separate certificates derived from observed logit pairs establish 232 individual choices after removing a common offset. Conditional numerical theorems propagate quantization and floating-point errors through the complete cached recurrence, but their evaluated forward bounds certify zero token choices. We give the theorem boundary, data identities, measurement procedures, and remaining assumptions, including native checker execution and the identity of captured operands with source intermediates.
| Comments: | 20 pages. Source, theorem map, measurement records, and reproduction instructions accompany the report. |
| Subjects: | Programming Languages (cs.PL); Computation and Language (cs.CL) |
| Cite as: | marXiv:2609.00018 [cs.PL] (or marXiv:2609.00018v2 [cs.PL] for this version) |
Submission history
[v1] Thu, 24 Sep 2026 13:25:18 UTC (383 KB)
[v2] Thu, 24 Sep 2026 13:32:41 UTC (385 KB)
Related work
- marXiv:2609.00011
- Extends the cached binary32 GPT-2 execution proof with grouped quantized inference.
- marXiv:2609.00014
- Uses the LeanExe GPT-2 artifact-verification architecture and adds quantized CPU execution and numerical evidence.