降低数学科研门槛：Mistral AI 发布开源模型 Leanstral 1.5

近日，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 个经核实是真实缺陷。更值得关注的是，这 11 个缺陷里有 5 个此前从未在 GitHub 上被报告过。这说明 AI 在程序验证与安全审查方面，已经不只是“锦上添花”，而是能切切实实发现未知隐患。 随着 Leanstral1.5 的开源，数学界和计算机科学界正在迎来一个更低门槛、更高效的证明辅助工具。算力成本降下来，经济压力小下去，数学形式化证明的普及速度自然就提上来了。科研人员终于能从繁琐的计算与核对中抽身，把更多精力投入到核心科学问题的突破上。