Mistral AI·· 2026-07-02
Mistral 发布 Leanstral 1.5：6B 激活参数形式化验证模型
Leanstral 1.5: Proof Abundance for All
SI 导读
Mistral 发布 Leanstral 1.5，一个 Apache-2.0 许可、119B 总参数 6B 激活参数的形式化验证模型，在 miniF2F 上达到 100%，解出 PutnamBench 672 题中的 587 题，并在 FATE-H 取得 87%、FATE-X 取得 34%。
精选SI 评分66
推荐理由
原文给出 Leanstral 1.5 在形式化验证基准上的具体成绩与每道题成本对比，读者可据此判断开源证明模型的性价比。
来源：Mistral AI · mistral.ai