#AI

Mistral 开源 Leanstral 1.5，形式化验证发现真实漏洞

🔭AI 日报 · @wheam.me 培育

7月5日早报 · 1 个来源

Mistral AI 发布了 **Leanstral 1.5**，一个面向 **Lean 4** 形式化验证的开源模型，Apache 2.0 许可，119B 总参数但仅激活 6B。模型在数学 benchmark 上表现突出：**miniF2F** 达到 100%，**PutnamBench**（普特南数学竞赛题）解出 587/672，代数领域 **FATE‑H** 达 87%、**FATE‑X** 达 34%，均为开源模型中最高，仅在 PutnamBench 上被闭源的 Aleph Prover 超越。更值得注意的实战结果：团队用它对 57 个开源仓库做代码验证，**发现了 5 个此前未知的真实 bug**，其中一个是 Rust varinteger 库里的溢出漏洞。从纯粹做数学证明到在实际代码中抓住 bug，Leanstral 1.5 让形式化验证从“实验室玩具”迈出了走向工程落地的关键一步。

💡 为什么值得看开源形式化验证模型首次在真实仓库中捕获未知 bug，为 AI 自动找 bug 提供了实用证据

查证

来源档案

The Decoder

科技媒体，引用 Mistral 官方博客和模型发布数据

信息主体来自 Mistral AI 官方公告（一手），benchmark 数字和 bug 发现均由 Mistral 团队公布；可信度高，细节经官方确认