Mistral AI发布Leanstral 1.5：数学证明模型以百分之一推理成本实现顶尖性能

欧洲人工智能公司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%，两项成绩都是当前最佳。

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

成本优势同样明显。在PutnamBench数据集上，Leanstral 1.5平均每题解题开支只需4美元。字节跳动的Seed-Prover 1.5需要超过300美元，Aleph Prover则需要54至68美元。同等任务下，Leanstral 1.5的推理成本仅为最强竞品的约百分之一，扫清了数学形式化证明大规模应用的经济障碍。

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