# TorchLean: Formalizing Neural Networks in Lean

arXiv: https://arxiv.org/abs/2602.22631 · HTML: https://mlsanity.com/paper/2602.22631/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 53 references that are in the map.
- First posted on arXiv 26 Feb 2026.

## Builds on (most cited first, 23 of 23)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Error bounds for approximations with deep ReLU networks](https://mlsanity.com/paper/1610.01145/) (2016)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Certified Defenses against Adversarial Examples](https://mlsanity.com/paper/1801.09344/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results](https://mlsanity.com/paper/2512.19007/) (2025)
- [Verification for Machine Learning, Autonomy, and Neural Networks Survey](https://mlsanity.com/paper/1810.01989/) (2018)
- [Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees](https://mlsanity.com/paper/2403.07308/) (2024)
- [No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks](https://mlsanity.com/paper/2506.01054/) (2025)
- [Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion](https://mlsanity.com/paper/2506.01356/) (2025)
- [Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq](https://mlsanity.com/paper/2301.12893/) (2023)
- [Floating-Point Neural Networks Are Provably Robust Universal Approximators](https://mlsanity.com/paper/2506.16065/) (2025)
- [An Empirical Study on Tensor Shape Faults in Deep Learning Systems](https://mlsanity.com/paper/2106.02887/) (2021)
- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)

## Built on by (most cited first, 4 of 4)

- [Lazy Arithmetic using Systolic Arrays for Closing the Verification Gap on Embedded Systems](https://mlsanity.com/paper/2607.15328/) (2026)
- [PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs](https://mlsanity.com/paper/2608.12762/) (2026)
- [Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees](https://mlsanity.com/paper/2608.17070/) (2026)
- [Finite-Sample Probabilistic Safety Certification for AI-Based Grid-Edge Coordination](https://mlsanity.com/paper/2609.28182/) (2026)

## Abstract (arXiv)

Neural networks are increasingly deployed in scientific, safety critical, and mission critical pipelines, yet verification and analysis are often performed outside the programming environment that defines and runs the model. This creates a semantic gap between the executed network and the analyzed artifact: guarantees can depend on implicit conventions about operator semantics, tensor layouts, preprocessing, floating-point behavior, graph transformations, accelerated kernels, and external certificates. We present TorchLean, a unified framework for formalizing, executing, and verifying neural networks in Lean 4. TorchLean treats learned models as executable programs and mathematical objects with a shared semantics for computation, verification, and theorem proving. The framework provides a PyTorch style API for typed tensors, layers, objectives, optimizers, automatic differentiation, and graph programs, with eager and compiled execution paths that lower to a common computation-graph representation. TorchLean supports exact and finite-precision tensor semantics, verified reverse-mode differentiation, interval and affine bound propagation, CROWN/LiRPA style certificate checking, import/export workflows, and CUDA-backed execution through explicit FFI boundaries. It also includes semantic layers for attention and FlashAttention, state-space sequence models, diffusion and sampling processes, probability kernels, reinforcement-learning objectives and Markov decision processes, and self-supervised objectives such as masked autoencoding, JEPA-style predictive views, and variance/correlation-based anti-collapse losses. Together, these components provide a semantic foundation for verified machine learning, where executable neural network artifacts, verification procedures, runtime boundaries, and mathematical claims can be stated and related inside one theorem-proving environment.