TorchLean: Formalizing Neural Networks in Lean

How could this lend insight into why Fast Fourier Transform approximates self-attention?

> Because self-attention can be replaced with FFT for a loss in accuracy and a reduction in kWh [1], I suspect that the Quantum Fourier Transform can also be substituted for attention in LLMs.

[1] "Fnet: Mixing tokens with fourier transforms" (2021) https://arxiv.org/abs/2105.03824 .. "Google Replaces BERT Self-Attention with Fourier Transform: 92% Accuracy, 7 Times Faster on GPUs" https://syncedreview.com/2021/05/14/deepmind-podracer-tpu-ba...

"Why formalize mathematics – more than catching errors" (2025) https://news.ycombinator.com/item?id=45695541

Can the QFT Quantum Fourier Transform (and IQFT Inverse Quantum Fourier Transform) also be substituted for self-attention in LLMs, and do Lean formalisms provide any insight into how or why?

TorchLean logo

2University of Illinois Urbana-Champaign

Abstract

Neural networks are increasingly deployed in safety- and mission-critical pipelines, yet many verification and analysis results are produced outside the programming environment that defines and runs the model. This separation creates a semantic gap between the executed network and the analyzed artifact, so guarantees can hinge on implicit conventions such as operator semantics, tensor layouts, preprocessing, and floating-point corner cases. We introduce TorchLean, a framework in the Lean 4 theorem prover that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification. TorchLean unifies (1) a PyTorch-style verified API with eager and compiled modes that lower to a shared op-tagged SSA/DAG computation-graph IR, (2) explicit Float32 semantics via an executable IEEE-754 binary32 kernel and proof-relevant rounding models, and (3) verification via IBP and CROWN/LiRPA-style bound propagation with certificate checking. We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification, alongside mechanized theoretical results including a universal approximation theorem. These results demonstrate a semantics-first infrastructure for fully formal, end-to-end verification of learning-enabled systems.

TorchLean overview

Key Contributions

PyTorch-style verified API in Lean 4 with eager and compiled modes that lower to an op-tagged SSA/DAG computation-graph IR.
Explicit Float32 semantics via an executable IEEE-754 binary32 kernel and proof-relevant rounding models.
Verification via IBP and CROWN/LiRPA-style bound propagation with certificate checking.
End-to-end validation on certified robustness, PINN residual bounds, and Lyapunov-style neural controller verification, plus mechanized theory results (including a universal approximation theorem).

System Modules

TorchLean is organized around three tightly integrated modules that share a single formal semantics end-to-end:

TorchLean (Frontend)

PyTorch-style API for defining models, layers, and training/inference code directly in Lean.
Eager execution for rapid iteration plus a compiled mode that lowers to an op-tagged SSA/DAG graph IR.
A single representation used by execution, analysis, and proof.

Runtime (Semantics)

Executable Float32 semantics via an IEEE-754 binary32 kernel (IEEE32Exec).
Proof-relevant rounding models to make numerical assumptions and trust boundaries explicit.
Eliminates “semantic gap” between what runs and what gets verified.

Verification

Native IBP and CROWN/LiRPA-style bound propagation over the shared graph IR.
Certificate checking to validate computed bounds inside Lean.
Supports robustness, PINN residual bounds, and control-oriented safety/stability (Lyapunov-style) verification.

Hacker Times