# Leanstral 1.5：让所有人都能拥有充足的证明 - 原标题：Leanstral 1.5: Proof Abundance for All - 类型：博客 - 来源：Mistral AI - 发布时间：2026-07-02 - 首次精选：2026-10-28 16:25 - 分级：值得看 - 学习层级：深入 - 主题：[ai-mathematics-proofs]()（第 6 位）、[moe-model-architecture]()（第 18 位）、[reinforcement-alignment]()（第 39 位） - 原文链接：[https://mistral.ai/news/leanstral-1-5]() - 本站页面：[https://oplearnx.com/resources/pk\_e5a617b77fe9]() ## 摘要 Mistral 发布的 Lean 4 形式化证明模型 Leanstral 1.5，采用 Apache-2.0 许可，总参数 119B、激活参数 6B。文中称其在形式验证任务上有大幅提升：miniF2F 达到饱和，PutnamBench 解决 587/672 题，FATE-H 达 87%、FATE-X 达 34%；训练经过中期训练、监督微调与基于 CISPO 的强化学习，并在测试的 57 个代码仓库中发现 5 个此前未知的缺陷。模型已开源，可通过 Hugging Face 和免费 API 使用。 ## 中文精读 ### 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 ``` --- 来源：LearnMap · 学径（https://oplearnx.com）