思考
摘要
Leanstral 1.5 是一款采用 Apache-2.0 许可证的免费模型，活跃参数为 6B，在形式化验证上实现了重大性能升级：miniF2F 达到饱和，解出 PutnamBench 的 672 道题中的 587 道，并在 FATE-H（87%）和 FATE-X（34%）上取得最先进的成绩。它经过中期训练、监督微调以及基于 CISPO 的强化学习，擅长智能体式证明工程和真实世界的代码验证，在测试的 57 个代码仓库中发现了 5 个此前未知的 bug。Leanstral 1.5 完全开源，可通过 Hugging Face 和免费 API 获取，现已可用于 Lean 4 中的实际证明工程。
自发布以来，Leanstral 为 Lean 4 中的证明工程提供了一种开放而实用的方法。今天，我们发布 Leanstral 1.5，这是一款采用 Apache-2.0 许可证的免费模型，总参数 119B，活跃参数仅 6B，性能升级让形式化验证比以往任何时候都更强大、更易用。
Leanstral 1.5 使 miniF2F 达到饱和，解出 PutnamBench 的 672 道题中的 587 道，并在 FATE-H 上以 %87 和 FATE-X 上以 34% 创下新的最先进水平。除了基准测试，它还能验证复杂的代码性质，并在开源仓库中发现此前未知的 bug——证明严格的形式化方法在真实世界中既有效又实用。
训练 Leanstral
Leanstral 1.5 经历三个阶段：中期训练、监督微调，以及基于 CISPO 的强化学习。Leanstral 1.5 充分利用了在两个强化学习环境中的大量训练：
在多轮环境中，模型会拿到一条定理陈述，必须证明或证否它。模型提交证明、接收 Lean 编译器的反馈，并在每次尝试中改进思路。如果证明通过编译则成功；否则循环继续，直到模型解决问题或用尽预算。
在代码智能体环境中，Leanstral 像开发者一样在原始文件系统中工作：编辑文件、运行 bash 命令，并使用 Lean 语言服务器实时查看目标、错误和类型信息。这使它能够完成长程任务，例如补全仓库中的部分证明、构建辅助引理，以及在多轮上下文压缩中持续推进。模型学会了驾驭完整的证明工程工作流，最终由我们的 SafeVerify 分支针对一组目标定理验证其正确性。
评估
我们在以下基准测试上评估 Leanstral：
- miniF2F 是一个跨系统的形式化数学基准，题目从初等问题到 IMO 级别的挑战，考察代数、组合数学和数论等方面的多样化证明能力。
- PutnamBench 由取自 Putnam 数学竞赛的 672 道题组成，要解决这些有挑战性的数学问题，需要深入的推理和很长的证明链。
- FATE-H 和 FATE-X 是抽象代数基准，分别面向研究生和博士水平的问题，考察群论、环论和模论等领域的高级推理。
- FLTEval 基于费马大定理仓库中的真实 pull request，考察具有真实世界复杂度的实际证明工程。
我们让 miniF2F 完全饱和，在验证集和测试集上都达到 100%。在 PutnamBench 和 FATE-H/X 上，我们将 Leanstral 1.5 与不带自然语言引导的 Goedel-Architect、高配置下的 Seed-Prover 1.5 以及 AxProverBase 进行了比较。Leanstral 在 FATE-H/X 上创下新的最先进水平，分别解出 87 道和 34 道题。在 PutnamBench 上，它以远低的成本领先高配置的 Seed-Prover 1.5 共 7 道题：每题约 4 美元，而 Seed-Prover 估计需要 300 美元或更多，其高配置每题的预算为 10 个 H20 日。排名更高的证明器只有在不同条件下运行——有的获得了自然语言证明引导，有的运行成本高得多，比如 Aleph Prover，每题 54-68 美元。
Leanstral 1.5 展现出我们所见过的形式化推理模型中最强的测试时扩展能力。下图跟踪了将每次尝试的词元预算从 25k 提高到 4M 时 PutnamBench 上的 Pass@8：性能一路平滑且单调地攀升，从 50k 时解出 44 道题，到 200k 时 244 道，1M 时 493 道，4M 时 587 道。当证明变得很长时，Leanstral 不会放弃，而是在数百万词元的过程中持续推理、编辑文件、修订，把预算直接转化为解出的题目——下面 AVL 树证明背后也是同样的行为，它在 22 次上下文压缩中运行了超过 270 万词元。
随着此次发布，我们也完全开源了 FLTEval。Leanstral 1.5 把该基准上的 pass@1 从 21.9 提升到 28.9，pass@8 从 31.9 提升到 43.2，以七分之一的成本超过了 Opus 4.6 的 39.6。如下图所示，它相对于大 3-10 倍的开源模型也进一步扩大了领先优势。
代码验证案例研究
尽管主要针对数学进行训练，Leanstral 1.5 在代码验证方面也展现出很强的能力。我们给出 2 个关键案例研究来展示其影响。
AVL 树：证明时间复杂度
AVL 树是自平衡二叉搜索树，通过在插入和删除过程中重新平衡来保持 O(log n) 的高度。Leanstral 1.5 为一个真实实现证明了这些时间复杂度保证——这项任务需要用结构归纳来对应树的递归结构，需要仔细处理单子式（monadic）的时间跟踪，还需要对重新平衡路径进行穷举的情形分析。在超过 270 万词元和 22 次上下文压缩中，Leanstral 系统地逐层展开 TimeM 单子，尽管底层计算与控制流相互交织，它仍将其暴露出来。它为插入建立了一个几乎紧的界：每个高度单位 48 步外加一个常数，然后通过对数关系把高度与树的大小联系起来，给出了完整、经过验证的证明，证实插入和删除确实是 O(log n)。
发现 bug：找出隐藏的缺陷
为了测试 Leanstral 抓 bug 的能力，我们构建了一条自动化流水线：Aeneas 将 Rust 代码翻译为 Lean，Leanstral 则推断用户意图并根据代码生成正确性性质。随后 Leanstral 对每条性质尝试证明，共四次机会。如果全部失败，它会转而尝试证明其否定命题，同样给四次机会。在测试的 57 个仓库中，这一过程标记出 47 条被违反的性质，其中 11 条指向真正的 bug——有 5 个此前没有在 GitHub 上被报告过。
其中一个 bug 出现在 datrs/varinteger 库中用于 zigzag 解码的符号函数里。输入 Std.U64.MAX 时，表达式 (value + 1) 发生溢出，在调试模式下导致崩溃，在发布模式下则造成静默数据损坏——这是测试和模糊测试通常会漏掉的边界情况。Leanstral 的流水线自动捕获了它，说明形式化验证已经能应用于真实世界的代码库，并发现一些传统方法会遗漏的 bug。
快速上手
Leanstral 1.5 采用 Apache-2.0 许可证。权重可在 Huggingface 上找到，同时现已作为免费 API 端点提供，端点名为 leanstral-1-5。我们建议在 Mistral Vibe 中使用。要开启你的旅程，请获取一个 API Key，然后：
1. 设置 Mistral Vibe
uv tool install mistral-vibe
uv tool update mistral-vibe
vibe --setup
2. 安装 Leanstral 1.5
/leanstall
exit
3. 启动智能体
vibe --agent lean
4. 安装 Lean LSP MCP（可选）
强烈建议安装 Lean LSP MCP，方法是将以下内容添加到你的 ~/.vibe/config.toml
[[mcp_servers]]
name = "lean-lsp"
transport = "stdio"
command = "uvx"
args = ["lean-lsp-mcp"]
tool_timeout_sec = 600
如果当前没有任何 MCP 服务器，你可能需要删除 mcp_servers = []。
5. 开始证明
让 Leanstral 去攻克一条定理、调试一个证明，或为某个仓库做贡献。就这么简单。