TorchLean formalizes neural networks in Lean 4, from autograd to CUDA verification
srush_nlp · x · 2026-09-16
A Caltech-led team released TorchLean, a Lean 4 codebase for specifying, executing, and verifying neural networks, selected as an ICML 2026 AI4Math Workshop Spotlight. Sasha Rush also referenced the earlier Lean Verified Transformers project, which proved a set of Transformer invariants from scratch in Lean.
- Typed tensor and layer APIs for writing neural-network programs directly in Lean, keeping tensor layouts, preprocessing, compiler boundaries, and float semantics explicit.
- Full runtime: PyTorch-style API, eager and compiled execution via an op-tagged SSA/DAG graph IR, reverse-mode autograd, and optimizers.
- CUDA/GPU backend with native kernels, CPU stubs, Compute Sanitizer checks, and Nsight profiling hooks.
- Explicit trust boundaries covering external FFI, PyTorch import/export, Python/Julia/Arb oracles, α,β-CROWN certificates, and CUDA kernels.
- Float32/IEEE-754 semantics with IBP and CROWN/LiRPA-style verification.
- A model zoo spanning MLPs, CNNs, ResNets, ViTs, GPT-2, Mamba/SSM, diffusion, MAE-style SSL, RL, PINNs, and 3D-geometry certificates.
More from Research
- Greg Brockman says OpenAI has 'significant progress' on another Millennium Prize Problem — scaling01 · 2026-09-16
- OmegAMP preprint: generative AI designs programmable antimicrobial peptides, 204 experimentally validated with in vivo efficacy — AllThingsApx · 2026-09-16
- Agent benchmark turns real incidents into tasks: cached token acted as wrong user for 40 minutes — Kind-Atmosphere9655 · 2026-09-16
- A Millennium Prize Problem, two AI labs, and a credit fight over Navier-Stokes — thursdai_pod · 2026-09-16
- MICAFlow: fast and robust MRI preprocessing pipeline bridges neuroimaging research and clinical practice — bttyeo · 2026-09-16
- Self-evolving agent framework Épi hits 120 research records, tightens Klarner's constant — my_cat_can_code · 2026-09-16