https://leandojo.org/torchlean.html

LeanDojo
Home LeanDojo LeanAgent LeanCopilot LeanProgress LeanIDE TorchLean 
BRIDGE
TorchLean logo

Formalizing Neural Networks in Lean

Robert Joseph George  ^1, Jennifer Cruden^1, Xiangru Zhong^2, Huan
Zhang^2, Anima Anandkumar^1
^1California Institute of Technology; ^2University of Illinois
Urbana-Champaign
PDF Code (coming soon)

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.