该模型专为数学形式化证明语言设计，以 119B 总参数与 6B 激活参数架构在多项基准测试中取得最佳成绩，同时将单题求解成本压缩至 4 美元，并以 Apache-2.0 协议开源。
欧洲人工智能企业 Mistral AI 于当地时间 7 月 2 日正式推出面向数学形式化证明程序语言 Lean 4 的专用模型 Leanstral 1.5。该模型采用稀疏架构设计，总参数量达到 119B，实际激活参数为 6B，并以 Apache-2.0 许可协议向公众开源，旨在降低数学证明与代码验证的技术门槛和使用成本。
在基准测试表现方面，Leanstral 1.5 在 miniF2F 形式数学基准测试的验证集和测试集中均实现了 100% 的完成率。针对 PutnamBench 数学竞赛问题集包含的 672 道 Lean 4 题目，该模型成功解决了其中 587 道。在抽象代数领域的 FATE 系列测试中，模型在硕士级 FATE-H 任务上的达成率为 87%，在博士级 FATE-X 任务上达到 34%，上述指标均为当前同类模型中的最优表现。成本效益是本次发布的另一核心数据点：处理 PutnamBench 数据集问题时，Leanstral 1.5 的平均开销仅为 4 美元，而对比方案 Seed-Prover 1.5 需超过 300 美元，Aleph Prover 的成本区间则在 54 至 68 美元之间。
实际应用测试显示，该模型在 57 个代码库的扫描中标记了 47 个违规属性，经核实有 11 个属于真实缺陷。其中包含 5 个此前未在 GitHub 平台上被报告过的问题，证明了其在程序验证与漏洞挖掘方面的实用价值。随着该模型的开源，数学研究与计算机科学领域的形式化验证工具将因算力成本的大幅降低而更易普及，有助于推动相关技术在更广泛科研群体中的应用。
此次发布标志着 Mistral AI 在垂直领域大模型上的进一步深入，通过特定于 Lean 4 的优化架构与极低的推理成本，为学术界和工业界提供了一套高效的数学证明辅助方案。相较于传统需要高算力资源或昂贵 API 调用的替代工具，该模型的出现可能改变形式化验证领域的资源分配模式。