Leanstral 1.5：让所有人都能拥有充足的证明

中文精读

原文约 1,402 词 · 8 节

1. Leanstral 1.5：人人可享的证明丰盈

   • 发布方为 Mistral 的 Leanstral 团队，日期为 2026 年 7 月 2 日，阅读时长约 6 分钟。
   • 摘要称 Leanstral 1.5 是 Apache-2.0 免费许可模型，激活参数仅 6B，在形式化验证上大幅提升。
   • 具体成绩：刷满（saturate）miniF2F，解出 PutnamBench 672 题中的 587 题，FATE-H 达 87%、FATE-X 达 34%，均为最新最优。
   • 训练经过中训练（mid-training）、监督微调与 CISPO 强化学习，擅长智能体式证明工程与现实代码验证。
   • 文中称其在测试的 57 个仓库中发现 5 个此前未知的 bug；模型完全开源，可在 Hugging Face 与免费 API 使用，面向 Lean 4 的实际证明工程。
   • 文章开头说明：自发布以来 Leanstral 为 Lean 4 提供了开放、实用的证明工程途径，此次 1.5 版总参数 119B、激活 6B，性能升级让形式化验证更强、更易获得。

2. 训练 Leanstral

   • 训练分三阶段：中训练、监督微调、使用 CISPO 的强化学习。
   • 强化学习在两类环境中进行。多轮环境里，模型拿到定理陈述，须证明或证伪；提交证明后获得 Lean 编译器反馈，据此改进，编译通过即成功，否则循环直到解出或耗尽预算。
   • 代码智能体环境中，模型像开发者一样在原始文件系统里操作：编辑文件、运行 bash 命令、用 Lean language server 实时查看目标、错误与类型信息。
   • 该环境用于长程任务，如补全仓库中的部分证明、构建辅助引理、经历多轮上下文压缩（compaction）坚持下去。
   • 模型学习完整的证明工程流程，最后由 Mistral 分叉的 SafeVerify（LeanstralSafeVerify）在给定目标定理列表下检验正确性。

3. 评测

   • 评测基准：miniF2F 是跨系统的形式数学基准，从初等题到 IMO 级问题，覆盖代数、组合、数论。
   • PutnamBench 含 672 道 Putnam 数学竞赛题，需要深度推理与长证明链。
   • FATE-H 与 FATE-X 是抽象代数基准，分别对应研究生与博士水平，涉及群论、环论、模论。
   • FLTEval 基于费马大定理仓库的真实拉取请求，测试真实复杂度的实用证明工程。
   • miniF2F 在验证集与测试集均达 100%。PutnamBench 与 FATE-H/X 上对比 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 美元。

4. 评测（续）

   • 测试时扩展（test-time scaling）表现最强：PutnamBench 的 Pass@8 随每题 token 预算从 25k 升到 4M 单调平滑上升，50k 解 44 题、200k 解 244 题、1M 解 493 题、4M 解 587 题；证明变长时不放弃，持续推理、编辑文件、修订。
   • 同时完全开源 FLTEval：Leanstral 1.5 将其 pass@1 从 21.9 提升到 28.9，pass@8 从 31.9 提升到 43.2，超过 Opus 4.6 的 39.6，成本仅为其七分之一，并拉大对 3–10 倍规模开源模型的领先。

5. 代码验证案例研究

   • Leanstral 1.5 主要面向数学训练，但在代码验证上表现出较强能力。
   • 文中给出两个关键案例研究，用以展示其实际影响。

6. AVL 树：证明时间复杂度

   • AVL 树是自平衡二叉搜索树，通过插入、删除时的再平衡维持 O(log n) 高度。
   • Leanstral 1.5 为真实实现证明了这些时间复杂度保证，需要结构归纳对应树的递归结构、谨慎处理单子式时间追踪、并对再平衡路径做穷尽分情况分析。
   • 过程耗用超过 270 万 token、22 次上下文压缩，逐层展开 TimeM 单子，暴露与控制流交织的底层计算。
   • 它给出每个高度单位约 48 步加常数的近乎紧的界（用于插入），再把高度与树规模以对数关系连接，给出完整的已验证证明：插入与删除确为 O(log n)。

7. 缺陷发现：找出隐藏瑕疵

   • 为测试找 bug 能力，团队搭建自动化流水线：Aeneas 将 Rust 代码翻译为 Lean，Leanstral 推断用户意图并从代码生成正确性属性。
   • 随后它对每个属性尝试证明四次；若全部失败，再尝试证明其否定，同样四次。
   • 在 57 个测试仓库中，该流程标出 47 个被违反的属性，其中 11 个指向真实 bug，5 个此前未在 GitHub 报告过。
   • 示例：datrs/varinteger 库 zigzag 解码的符号函数中，输入 Std.U64.MAX 时 (value + 1) 溢出，调试模式崩溃、发布模式静默损坏，属于测试与模糊测试通常漏掉的边界情形，被该流水线自动捕获。

8. 开始使用

   • Leanstral 1.5 采用 Apache-2.0 许可；权重发布在 Hugging Face，同时以 `leanstral-1-5` 名义提供免费 API 端点，推荐在 Mistral Vibe 中使用。
   • 第一步用 uv 安装并更新 mistral-vibe，然后运行 `vibe --setup` 完成配置。
   • 第二步在 Vibe 中执行 `/leanstall` 安装模型，再 `exit` 退出。
   • 第三步以 `vibe --agent lean` 启动智能体。
   • 第四步（可选但强烈推荐）安装 Lean LSP MCP：在 `~/.vibe/config.toml` 中加入对应的 MCP 服务器配置（stdio 传输、uvx 运行 lean-lsp-mcp、工具超时 600 秒）；若原本没有 MCP 服务器，需删掉 `mcp_servers = []`。
   • 最后即可让 Leanstral 证明定理、调试证明或为仓库做贡献。
   toml

   [[mcp_servers]]
   
   name = "lean-lsp"
   
   transport = "stdio"
   
   command = "uvx"
   
   args = ["lean-lsp-mcp"]
   
   tool_timeout_sec = 600