[Submitted on 18 Sep 2026 (v1), last revised 19 Sep 2026 (this version, v8)]
Title:Exact Execution Verification of Cached GPT-2 in Lean and WebAssembly
Abstract: LeanExe aims to execute an algorithm written in Lean with a checked proof that the emitted program computes the source result. This work applies that goal to pretrained GPT-2 inference, where floating-point arithmetic, packed tensors, cached state, and memory management must agree across a complete sequence of token calls. We present a checked proof connecting a WebAssembly artifact of 19,083 bytes to a Lean specification of cached GPT-2 with 124,439,808 parameters and a 128-token context. In the semantics of the WebAssembly interpreter and proof library Talos, written in Lean, the decoded artifact terminates and returns exactly the cache and logit bytes of the Lean token-step recurrence for every weight array of the required length and every valid token sequence of length at most 128. The proof establishes binary decoding, validation, and equality with the execution model, then composes initialization, packed input representation, all twelve transformer blocks, vocabulary projection, allocation sufficiency, and buffer releases. Our Talos extensions define binary32 and binary64 arithmetic through integer operations and explicit rounding. Arithmetic lemmas connect Lean’s logical Float32 operations to Talos for all input words. The standalone WebAssembly runtime Wasmtime executes the module with arithmetic NaN canonicalization enabled. Tests against CPU PyTorch compare 6,432,896 logits across all supported context lengths, with a maximum observed absolute difference of 0.001450, and produce text completions. The final theorem uses three standard logical axioms. Applying the formal result to native execution relies on the interpretation of the formal semantics, the host’s byte I/O, and Wasmtime. Automatic checks of the command-line artifact’s identity and the combined theorem’s axiom policy remain open.
| Comments: | 13 pages, 2 tables |
| Subjects: | Programming Languages (cs.PL); Machine Learning (cs.LG) |
| Cite as: | marXiv:2609.00011 [cs.PL] (or marXiv:2609.00011v8 [cs.PL] for this version) |
Submission history
[v1] Sat, 19 Sep 2026 03:02:00 UTC (300 KB)
[v2] Sat, 19 Sep 2026 03:05:52 UTC (300 KB)
[v3] Sat, 19 Sep 2026 03:09:48 UTC (300 KB)
[v4] Sat, 19 Sep 2026 03:14:01 UTC (300 KB)
[v5] Sat, 19 Sep 2026 03:26:18 UTC (308 KB)
[v6] Sat, 19 Sep 2026 14:51:41 UTC (317 KB)
[v7] Sat, 19 Sep 2026 15:02:10 UTC (317 KB)
[v8] Sat, 19 Sep 2026 16:05:12 UTC (321 KB)
Related work
- marXiv:2609.00005
- Applies the per-compilation correspondence method to cached GPT-2 inference with packed FP32 runtime weights.
Named by
- marXiv:2609.00014
- Combines and expands the CPU GPT-2 verification report.
- marXiv:2609.00012
- Extends the parent GPT-2 WebAssembly verification with per-compilation WGSL certificates and a conditional hybrid session theorem.