[Submitted on 19 Sep 2026 (this version), latest revision 19 Sep 2026 (v4)]
Title:Checked WGSL Compilation and Conditional GPT-2 Execution in LeanExe
Abstract: The goal of LeanExe is to run an algorithm written in Lean and obtain a checked proof that the emitted program performs that algorithm. Previous work established this connection for cached GPT-2 inference in a formal WebAssembly execution model. The WGSL work extends the approach toward GPU execution by moving matrix products to the WebGPU Shading Language (WGSL) while retaining the model controller in WebAssembly. We present a compiler for a restricted class of Lean definitions that checks each translation against an independent shader parser and a statement-execution semantics. Packed-layout proofs connect six compiled shaders to the matrix operations of a 124M-parameter GPT-2 implementation. The hybrid session theorem equates cache and logit bytes with the Lean cached-step recurrence for arbitrary weight bytes of the required length and up to 128 valid tokens, assuming completed shader execution with separate FP32 arithmetic and exact host transfers. The branch supplies a native inference runner and records a CPU WebGPU comparison in which all 6,432,896 logits match the parent WebAssembly implementation bit for bit. Runtime conformance, hybrid binary decoding, and browser execution remain separate verification or evaluation tasks.
| Comments: | 9 pages, 1 table |
| Subjects: | Programming Languages (cs.PL); Machine Learning (cs.LG) |
| Cite as: | marXiv:2609.00012 [cs.PL] (or marXiv:2609.00012v1 [cs.PL] for this version) |
Submission history
[v1] Sat, 19 Sep 2026 15:36:05 UTC (270 KB)
[v2] Sat, 19 Sep 2026 15:43:55 UTC (269 KB)
[v3] Sat, 19 Sep 2026 15:50:19 UTC (272 KB)
[v4] Sat, 19 Sep 2026 15:59:34 UTC (272 KB)
Related work
- marXiv:2609.00011
- Extends the parent GPT-2 WebAssembly verification with per-compilation WGSL certificates and a conditional hybrid session theorem.
Named by
- marXiv:2609.00014
- Combines and expands the WGSL verification report.