Mistral发布开源Lean 4证明智能体Leanstral 1.5

Mistral AI 发布了名为 Leanstral 1.5 的开源代码智能体模型，专门面向 Lean 4 形式化证明与定理证明场景。该模型规模为 119B（6B 激活参数），基于 Apache-2.0 协议开源，旨在将大语言模型的代码生成能力与严格的形式化数学验证深度结合，推进数学推理的自动化。

关键细节与性能表现

Leanstral 1.5 在多个权威数学基准测试中取得了当前最优（SOTA）的表现。据 Sophia Yang 提供的数据，该模型在 miniF2F 基准上取得了 100% 的通过率；在 PutnamBench 测试中，成功解决了 672 道题中的 587 道（平均成本约 4 美元/题）；同时在 FATE-H 测试中达到 80% 的准确率，并在研究生代数基准测试上拿下 SOTA。

工作原理与应用价值

Sophia Yang 在解析文章中指出，Leanstral 的核心价值在于区分了传统的“测试”与“证明”。测试仅能验证有限输入，而用 Lean 语言书写并由计算机检验的证明，可以断言某性质对所有输入均成立。作为一套证明写作系统，Leanstral 能够自主编辑证明代码、读取 checker（检验器）报错并进行反复重试，从而大幅提升形式化证明的自动化效率。

2026-07-03 ~ 2026-07-05 · 5 条相关

一手来源