告别盲测Bug：Mistral推出Lean 4形式化验证模型Leanstral

aftahi_ai · x · 2026-08-08

传统代码测试和模糊测试只能靠运气发现 Bug，而 LLM 也仅能进行模式匹配，无法保证代码绝对正确。Mistral 团队为此推出了 Leanstral 系列代码模型。

该模型专门针对 Lean 4 语言进行训练。Lean 4 是一种形式化验证语言，通过受信任的数学内核来证明代码属性。只要证明编译通过，就能确保该属性对任何可能的输入永远成立。Leanstral 能够自动化生成这些原本极其耗时的数学证明，让形式化验证终于有望走出学术界，实现大规模工程应用。