Leanstral 1.5：人人可用的形式化证明工具

Leanstral 自发布以来，一直为 Lean 4 提供开放、实用的证明工程方法。今天，我们发布 Leanstral 1.5，这是一款免费、Apache-2.0 许可的模型，拥有 119B 总参数，但仅激活 6B 参数，其性能提升使形式化验证比以往更强大、更易用。

Leanstral 1.5 在 miniF2F 上达到饱和（验证集和测试集均为 100%），解决了 PutnamBench 中 587/672 的问题，并在 FATE-H（87%）和 FATE-X（34%）上创下新纪录。在基准测试之外，它还能验证复杂代码属性，并在开源仓库中发现先前未知的 bug，证明严谨的形式化方法在实际应用中同样有效且实用。

训练过程 Leanstral 1.5 经过三个阶段：中期训练、监督微调和基于 CISPO 的强化学习。它利用两个强化学习环境进行广泛训练：

• 多轮环境：模型被给予一个定理陈述，需要证明或证伪。模型提交证明，接收 Lean 编译器反馈，并在每次尝试中改进方法。如果证明编译成功，则成功；否则循环继续，直到模型解决问题或耗尽预算。
• 代码代理环境：Leanstral 像开发者在原始文件系统中一样操作：编辑文件、运行 bash 命令，并使用 Lean 语言服务器实时检查目标、错误和类型信息。这使其能够处理长期任务，如补全仓库中的部分证明、构建辅助引理，并在多轮上下文压缩中持续工作。模型学会导航整个证明工程工作流，并最终通过我们的 SafeVerify 分支验证正确性。

评估结果 在 miniF2F 上，Leanstral 1.5 完全饱和。在 PutnamBench 和 FATE-H/X 上，与 Goedel-Architect（无自然语言引导）、Seed-Prover 1.5（高设置）和 AxProverBase 相比，Leanstral 1.5 在 FATE-H/X 上达到新纪录（分别解决 87 和 34 个问题）。在 PutnamBench 上，它以远低于 Seed-Prover 的成本（每个问题约 4 美元 vs. Seed-Prover 的 300 美元以上）多解决了 7 个问题。排名更高的证明器要么使用自然语言证明指导，要么运行成本更高（如 Aleph Prover 每个问题 54-68 美元）。

Leanstral 1.5 展示了我们所见过的形式化推理模型中最强的测试时扩展能力。随着每次尝试的 token 预算从 25k 增加到 4M，PutnamBench 上的 Pass@8 平滑单调增长：从 50k 时的 44 个问题增加到 200k 时的 244 个、1M 时的 493 个和 4M 时的 587 个。当证明运行时间较长时，Leanstral 不会放弃，而是继续推理、编辑文件和修订，将预算直接转化为已解决的问题。

此外，我们还完全开源了 FLTEval 基准。Leanstral 1.5 将基准上的 pass@1 从 21.9 提升到 28.9，pass@8 从 31.9 提升到 43.2，以七分之一的成本超过了 Opus 4.6 的 39.6，并扩大了与 3-10 倍大小的开源模型的差距。

代码验证案例研究

• AVL 树时间复杂度证明：Leanstral 1.5 使用结构归纳法和细致的单子时间跟踪，证明了真实实现中 AVL 树的 O(log n) 时间复杂度。经过 270 万 token 和 22 次压缩，它系统性地展开 TimeM 单子的每一层，揭示了与控制流交织的底层计算，建立了近乎严格的界限，并连接了高度与树大小，最终完整验证了插入和删除操作的时间复杂度。
• 漏洞发现：通过自动化流水线（Aeneas 将 Rust 代码翻译为 Lean，Leanstral 推断用户意图并生成正确性属性），在 57 个测试仓库中标记了 47 个违反属性，其中 11 个指向真实 bug，5 个先前未在 GitHub 上报告。例如，在 datrs/varinteger 库的 zigzag 解码符号函数中，输入 Std.U64.MAX 时表达式 (value + 1) 溢出，导致调试模式崩溃和发布模式静默损坏——这种边缘情况通常会被测试和模糊测试遗漏。

如何开始 Leanstral 1.5 采用 Apache-2.0 许可。权重可在 Hugging Face 上获取，同时也可通过免费 API 端点 leanstral-1-5 使用。推荐在 Mistral Vibe 中使用。获取 API 密钥后，按步骤设置：安装 Mistral Vibe、安装 Leanstral 1.5、启动代理，并可选安装 Lean LSP MPC。即可开始证明定理、调试证明或贡献代码。