Mistral AI 发布 Leanstral1.5：开源数学证明模型，成本大幅降低

Mistral AI 正式发布了为 Lean 4 形式化证明语言设计的开源模型 Leanstral1.5。该模型采用 Apache-2.0 许可，参数总量 119B，激活参数 6B，在兼顾高性能的同时使用成本大幅优化。

在 miniF2F 形式数学基准测试中，Leanstral1.5 在验证集和测试集上均达成 100% 的完成率。面对 PutnamBench 数学竞赛题库，它从 672 道 Lean 4 问题中成功解答 587 道。抽象代数领域的 FATE 系列基准测试中，硕士级别的 FATE-H 测试达成率高达 87%，博士级别的 FATE-X 测试达成率也有 34%，创下同类模型的新纪录。

成本是另一个突出点。使用 Leanstral1.5 求解 PutnamBench 题目的平均成本仅为 4 美元，对比模型 Seed-Prover1.5 的开销超过 300 美元，Aleph Prover 的成本也在 54 至 68 美元之间。这一成本压缩，有望让高精度数学证明辅助技术走出实验室，服务更广泛的科研群体。

在代码缺陷检测方面，Leanstral1.5 也表现积极。对 57 个代码库的实测中，它识别出 47 个违规属性，其中 11 个经核实为真实缺陷。有 5 个漏洞此前从未在 GitHub 上被报告过，这显示了 AI 在程序验证与安全审查上的潜力。

Leanstral1.5 的开源为数学与计算机科学界提供了一个更低门槛、更高效的证明辅助工具。通过降低算力与经济成本，它有望加速数学形式化证明的普及，让科研人员从繁琐的计算与核对中解脱，聚焦核心科学问题。