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

作为一款专注于数学推理的智能工具，Leanstral1.5的表现相当亮眼。在权威的 miniF2F 形式数学基准测试中，该模型在验证集和测试集上均达成了100% 的完成率。面对极具挑战性的 PutnamBench 数学竞赛题库，它能够从672道 Lean4问题中成功解答587道。此外，在抽象代数领域的 FATE 系列基准测试中，它同样展现了统治力:在硕士级别的 FATE-H 测试中达成率高达87%，即便是面对博士级别的 FATE-X 测试，其达成率也达到了34%，创下了该类模型的新纪录。

成本优势是此次模型发布的另一大核心亮点。Mistral AI 强调，相比于市面上的其他方案，Leanstral1.5极大地降低了科研试错成本。以 PutnamBench 中的题目为例，使用 Leanstral1.5进行求解的平均成本仅为4美元，而对比模型 Seed-Prover1.5的开销超过300美元，Aleph Prover 的成本也处于54至68美元之间。这一显著的成本压缩，有望让高精度的数学证明辅助技术走出实验室，服务于更广泛的科研群体。

在实际的代码开发场景中，Leanstral1.5也展现了极强的“找茬”能力。在对57个代码库的实测中，该模型成功识别出47个违规属性，其中11个经核实为真实缺陷。尤为值得一提的是，其中有5个漏洞此前从未在 GitHub 上被报告过，证明了 AI 在辅助程序验证与安全审查方面的巨大潜力。

随着 Leanstral1.5的开源，数学界与计算机科学界正迎来一个更低门槛、更高效的证明辅助工具。通过降低算力与经济成本，该模型有望加速数学形式化证明的普及，助力科研人员从繁琐的计算与核对工作中解脱出来，专注于核心科学问题的突破。