✳flâneur — a map of the web's best reading

[2602.22631] TorchLean: Formalizing Neural Networks in Lean

arxiv.org · 742 words · saved by 1 readers

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.

[2602.22631] TorchLean: Formalizing Neural Networks in Lean --> Computer Science > Mathematical Software arXiv:2602.22631 (cs) [Submitted on 26 Feb 2026 ( v1 ), last revised 24 May 2026 (this version, v2)] Title: TorchLean: Formalizing Neural Networks in Lean Authors: Robert Joseph George , Jennifer Cruden , Will Adkisson , Xiangru Zhong , Huan Zhang , Anima Anandkumar View a PDF of the paper titled TorchLean: Formalizing Neural Networks in Lean, by Robert Joseph George and 5 other authors View PDF HTML (experimental) Abstract: Neural networks are increasingly deployed in scientific, safety cr

Explore this link on the map →

saved by

related reading