AI BriefingLeanstral 1.5: Proof Abundance for Everyone
Key point
Leanstral 1.5, an open-source model based on Lean 4 specialized for Formal Verification, has been released.
Details
Released under the Apache-2.0 license, Leanstral 1.5 is a model that uses 6B active parameters out of a total of 119B parameters, demonstrating overwhelming performance in the field of Formal Verification.
Key achievements include:
- Achieved saturation on the miniF2F benchmark
- Solved 587/672 problems on PutnamBench
- Recorded SOTA (State-of-the-art) with FATE-H 87%, FATE-X 34%
- Found 5 previously undiscovered bugs by testing 57 real open-source repositories
This model was trained through a 3-stage process of Mid-training, SFT (Supervised Fine-Tuning), and RL (Reinforcement Learning) using CISPO. In particular, through training in Multiturn environments and Code Agent environments, it has gained the ability to perform complex proof engineering workflows, such as revising proofs based on compiler feedback or editing files and executing Bash commands.
It is currently available via Hugging Face and a free API, and can be used as a practical proof engineering tool in Lean 4 environments.
This summary was generated automatically by AI. Check the original for the author's claims and context. Copyright belongs to the original author.
Our guide explains how the AI works. Report summary errors, attribution issues, or removal requests via Contact.
Related
Trail of Bits Uses AI Agents to Build Custom Security Tooling and Formal Proofs for Miden zkVM Audit