TorchLean
TorchLean is the first unified Lean 4 framework for neural-network specification, execution, and verification.
A Lean 4 framework for building neural networks and mathematically proving properties about how they behave.
TorchLean is a framework built in Lean 4, a programming language designed for writing mathematical proofs that a computer can check for correctness, and it applies that idea to neural networks. Instead of just building and running neural networks the usual way, TorchLean lets researchers write, run, inspect, and mathematically verify neural network programs, so claims about how a model behaves can be checked with the same rigor as a mathematical proof rather than only tested through examples.
The framework provides typed tensors, which are the multi-dimensional arrays of numbers neural networks are built from, along with APIs for building models, a shared internal representation of a model's computation graph, support for running models and computing gradients during training, and tools for checking certificates, meaning formal evidence that a specific property about a model holds true. It also handles the boundary between this proof-focused code and lower-level runtime and CUDA graphics card execution, and includes examples spanning both typical machine learning use cases and scientific computing applications.
Getting started involves cloning the repository and using Lake, the build tool for Lean projects, to build the project and run a small example, such as training a simple multi-layer perceptron on the CPU for a set number of steps. The README notes the project is pinned to a specific Lean 4 toolchain version. Other Lean projects can depend on TorchLean directly through Lake by pointing to its Git repository or a local path, and most downstream code is expected to start from a documented public entry point module.
The repository is organized into folders covering the public interface, mathematical specifications, the runtime and training code, the internal graph representation, formal proofs, finite-precision number handling, learning theory, and verification tooling, along with the source for its documentation website. A companion academic paper describes the project in more detail, and TorchLean is released under the MIT license, a permissive open source license.
Where it fits
- Formally verify mathematical properties of a neural network's behavior.
- Build and train neural network models with typed tensors inside Lean 4.
- Import or export models between TorchLean and PyTorch.
- Use certificate checkers to confirm a model satisfies specific proven guarantees.