TorchLean: Formalizing Neural Networks in Lean
3 days ago
- #TorchLean
- #Formal Verification
- #Neural Networks
- Neural networks are critical in safety- and mission-critical applications but often verified outside their execution environment, creating a semantic gap.
- TorchLean is introduced as a framework in Lean 4 to unify execution and verification under a single precise semantics.
- TorchLean features a PyTorch-style verified API, explicit Float32 semantics, and verification via bound propagation methods like IBP and CROWN/LiRPA.
- The framework supports certified robustness, physics-informed residual bounds, and neural controller verification.
- TorchLean demonstrates a semantics-first approach for formal, end-to-end verification of learning-enabled systems.