[R] TorchLean: Formalizing Neural Networks in Lean

A team from Caltech and UC Irvine, led by Robert Joseph George and Anima Anandkumar, has introduced TorchLean, a novel framework that formally defines neural networks within the Lean 4 theorem prover. This work addresses a critical 'semantic gap' where safety verification of AI models is often performed separately from the code that runs them, leading to potential errors in assumptions about operator behavior, tensor layouts, and floating-point arithmetic. TorchLean treats trained models as precise mathematical objects, creating a single, shared semantics for both execution and formal proof, aiming to provide ironclad guarantees for AI systems in safety-critical applications like autonomous vehicles and medical diagnostics.

The framework unifies three key components: a verified, PyTorch-compatible API that lowers code to a shared computation graph; explicit, executable IEEE-754 binary32 (Float32) semantics to handle floating-point corner cases; and integrated verification tools using Interval Bound Propagation (IBP) and CROWN/LiRPA-style bound propagation. The team validated TorchLean end-to-end on certified adversarial robustness, bounds for Physics-Informed Neural Networks (PINNs), and Lyapunov-style stability verification for neural controllers. By providing a 'semantics-first' infrastructure, TorchLean enables fully formal, end-to-end verification, moving beyond testing and empirical validation to mathematical proof for critical AI systems.