欧洲人工智能企业Mistral AI近日正式推出面向数学形式化证明的专用模型Leanstral 1.5。该模型专为Lean4 程序语言打造，总参数规模达119B，但实际推理时仅激活6B参数，以极低的计算开销实现了惊人的证明能力，并以Apache-2. 0 许可完全开源。

在核心基准测试上，Leanstral 1. 5 交出了一份近乎完美的答卷。它在miniF2F形式数学基准的验证集和测试集上均实现了100%完成率，在PutnamBench数学竞赛 672 道Lean4 问题中成功解决 587 道。对于抽象代数领域的FATE系列基准，硕士级FATE-H达成率87%，博士级FATE-X达成率34%，两项成绩均为当前最佳。

解题成本仅为竞品百分之一

更令人瞩目的是Leanstral 1. 5 的成本优势。在PutnamBench数据集上，该模型平均每题解题开支仅需 4 美元，而字节跳动的Seed-Prover 1. 5 需要超过 300 美元，Aleph Prover也需要 54 至 68 美元。这意味着同等工作量下，Leanstral 1. 5 的推理成本仅为最强竞品的约百分之一，为数学形式化证明的大规模应用扫清了经济障碍。

在实际工程场景中，Leanstral 1. 5 同样展现了不俗的实战价值。模型在测试的 57 个代码库中标记了 47 个违规属性，其中 11 个指向真实的代码缺陷，更有 5 个是此前从未在GitHub上被报告过的全新问题。从纯粹的数学竞赛到真实的软件工程验证，这款模型正在证明一个事实：参数规模不再是能力的唯一门槛，高效激活才是将AI推理能力推向实用的关键路径。