Mistral AI 发布 Leanstral1.5：为数学形式化证明注入新动能
Mistral AI 近期推出了专为 Lean4 数学证明语言设计的开源模型 Leanstral1.5。该模型参数总量达119B，激活参数为6B，在保证卓越性能的同时，显著优化了运行成本，并遵循 Apache-2.0 许可协议发布。
Leanstral1.5 在数学推理任务上表现出色，于权威的 miniF2F 形式数学基准测试中，在验证集与测试集上均实现了100% 的完成率。面对极具难度的 PutnamBench 数学竞赛题库，该模型从672道 Lean4 问题中成功解答了587道。此外，在抽象代数领域的 FATE 系列基准测试中，Leanstral1.5 同样表现出领先地位，在硕士级别的 FATE-H 测试中达成率高达87%，甚至在博士级别的 FATE-X 测试中也达到了34%，创造了此类模型的新纪录。
显著降低使用成本是 Leanstral1.5 的另一大核心亮点。Mistral AI 强调，与现有解决方案相比，该模型极大地减少了科研过程中的试错成本。例如，在 PutnamBench 问题求解中，Leanstral1.5 的平均成本仅需4美元，远低于对比模型 Seed-Prover1.5 的300美元以上以及 Aleph Prover 的54至68美元。这种成本的大幅削减，有望推动高精度数学证明辅助技术走出实验室，惠及更广泛的科研群体。
在实际的代码开发与验证环节，Leanstral1.5 也展现了其强大的“故障探测”能力。通过对57个代码库的测试，该模型成功识别出47个违规属性，其中11个被确认为真实缺陷。尤为引人注目的是，其中有5个漏洞此前从未在 GitHub 上被公开披露，这充分证明了 AI 在辅助程序验证和安全审查方面蕴藏的巨大潜力。
Leanstral1.5 的开源不仅降低了数学形式化证明的门槛，也极大地提升了效率。通过减少计算和经济上的负担，该模型有望加速数学形式化证明的普及，让科研人员得以从繁琐的计算和核实工作中解放出来，更专注于核心科学问题的探索与突破。
Leanstral1.5 的出现，标志着 AI 在形式化证明领域迈出了坚实一步。其在数学推理上的优异表现，加之显著的成本优势，使得更复杂的数学问题得以被探索，并为软件安全审计提供了新的可能性。对于研究人员而言，这意味着一个更易于获取、更经济高效的辅助工具，有望加速科学发现的进程。