Leanstral 1.5：为所有人提供丰富的证明

# Leanstral 1.5：人人可用的丰富证明 来源：https://mistral.ai/news/leanstral-1-5/ Leanstral 1.5 是一款免费、Apache-2.0 许可的模型，拥有 60 亿活跃参数，在形式验证方面实现了重大性能提升：它饱和了 miniF2F，解决了 PutnamBench 上 587/672 的问题，并在 FATE-H（87%）和 FATE-X（34%）上取得了最先进的结果。通过中期训练、监督微调以及使用 CISPO 的强化学习，该模型在代理式证明工程和真实代码验证中表现出色，在 57 个测试仓库中发现了 5 个此前未知的错误。Leanstral 1.5 完全开源，可通过 Hugging Face 和免费 API 获取，现已可用于 Lean 4 中的实际证明工程。 自发布以来，Leanstral 为 Lean 4（https://leanprover.github.io/）提供了一种开放、实用的证明工程方法。今天，我们发布了 **Leanstral 1.5**，这是一款免费、Apache-2.0 许可的模型，总参数量 1190 亿，仅 60 亿活跃参数，其性能升级使得形式验证比以往任何时候都更强大、更易用。 Leanstral 1.5 **饱和了 miniF2F**，**解决了 PutnamBench 上 587/672 的问题**，并在 **FATE-H 上达到 87%**、**FATE-X 上达到 34%** 的新最先进水平。除了基准测试，它还能验证复杂的代码属性，并**发现开源仓库中此前未知的错误**——证明严谨的形式方法在现实应用中既能高效又实用。 ## **训练 Leanstral** Leanstral 1.5 经历了三个阶段：中期训练、监督微调和基于 CISPO 的强化学习。Leanstral 1.5 在两个强化学习环境中进行了大量训练： 在**多轮环境**中，模型会得到一个定理陈述，需要证明或证伪它。模型提交一个证明，接收 Lean 编译器的反馈，并在每次尝试中改进方法。如果证明编译成功则通过；否则循环继续，直到模型解决问题或耗尽预算。 在**代码代理环境**中，Leanstral 像开发者一样操作原始文件系统：编辑文件、运行 bash 命令，并使用 Lean 语言服务器实时检查目标、错误和类型信息。这使得它能够处理长期任务，例如完成仓库中的部分证明、构建辅助引理，以及在多次上下文压缩中持续工作。模型学会驾驭完整的证明工程工作流程，并最终由我们的 SafeVerify（https://github.com/mistralai/LeanstralSafeVerify）分支验证其正确性，目标定理列表由用户提供。 ## **评估** 我们在以下基准上评估 Leanstral： - **miniF2F** 是一个跨系统的形式数学基准，涵盖从初等问题到 IMO 级别的挑战，测试代数、组合学和数论方面的多种证明能力。 - **PutnamBench** 包含 672 个来自普特南数学竞赛的问题，需要深度推理和长证明链来解决数学难题。 - **FATE-H 和 FATE-X** 分别是研究生和博士级别的抽象代数基准，测试群论、环论和模论等领域的高级推理能力。 - **FLTEval** 基于费马大定理仓库的真实拉取请求，测试具有现实复杂性的实用证明工程。 我们完全饱和了 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 展示了我们所见过的形式推理模型中最强的测试时扩展能力。下图追踪了 PutnamBench 上的 Pass@8，同时我们将每次尝试的令牌预算从 25k 提高到 4M：性能在整个过程中平稳且单调地提升，从 50k 时解决的 44 个问题，到 200k 时的 244 个，1M 时的 493 个，以及 4M 时的 587 个。当证明过程较长时，Leanstral 不会放弃，而是继续推理、编辑文件，并跨数百万令牌进行修正，将预算直接转化为已解决的问题——这是下面 AVL 树证明背后的相同行为，该证明跨 22 次压缩运行了超过 270 万令牌。 在此次发布中，我们还完全开源了 FLTEval（https://github.com/mistralai/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 主要针对数学进行训练，但它在代码验证方面也展现出强大的能力。我们提供两个关键案例研究来展示其影响。 ### **AVL 树：证明时间复杂度** AVL 树是自平衡二叉搜索树，通过插入和删除时的重平衡来维持 O(log n) 的高度。Leanstral 1.5 为一个实际实现证明了这些时间复杂度保证——这项任务需要结构归纳来反映树的递归结构，仔细处理单子时间追踪，并对重平衡路径进行穷举案例分析。在 270 万令牌和 22 次压缩中，Leanstral 系统地展开了 TimeM 单子的每一层，尽管与控制流交织，仍暴露了底层计算。它建立了插入操作每单位高度 48 步再加上一个常数的几乎紧致上界，然后通过对数关系将高度与树大小联系起来，提供了完整、经过验证的证明，证明插入和删除确实是 O(log n)。 ### **漏洞发现：发现隐藏缺陷** 为了测试 Leanstral 的漏洞捕获能力，我们构建了一个自动化流水线：Aeneas 将 Rust 代码翻译为 Lean，而 Leanstral 推断用户意图并从代码生成正确性属性。然后 Leanstral 尝试在四次尝试中证明每个属性。如果全部失败，它会尝试证明否定，也是四次尝试。在 57 个经过测试的仓库中，这个过程标记了 47 个被违反的属性，其中 11 个指向真正的错误——其中 5 个此前未在 GitHub 上报告。 其中一个错误出现在 datrs/varinteger（https://github.com/datrs/varinteger）库的锯齿解码符号函数中。在输入 Std.U64.MAX 时，表达式 (value + 1) 发生溢出，导致调试模式下崩溃，发布模式下静默损坏——这是一个测试和模糊测试通常无法发现的边界情况。Leanstral 的流水线自动捕获了它，证明形式验证已经可以应用于现实代码库，并发现一些传统方法忽略的错误。 ## **快速开始** Leanstral 1.5 采用 **Apache-2.0** 许可。权重可在 Huggingface（https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B）上找到，同时也可通过免费 API 端点（https://docs.mistral.ai/models/model-cards/leanstral-1-5）以 `leanstral-1-5` 名称使用。我们建议在 Mistral Vibe 中使用它。要开始你的旅程，请获取一个 API 密钥，然后： **1. 设置 Mistral Vibe** `` uv tool install mistral-vibe uv tool update mistral-vibe vibe --setup `` **2. 安装 Leanstral 1.5** **3. 启动代理** **4. （可选）安装 Lean LSP MCP** 强烈建议通过将以下内容添加到你的 `~/.vibe/config.toml` 来安装 Lean LSP MCP（https://github.com/oOo0oOo/lean-lsp-mcp）： `` [[mcp_servers]] name = "lean-lsp" transport = "stdio" command = "uvx" args = ["lean-lsp-mcp"] tool_timeout_sec = 600 `` 如果没有现有的 MCP 服务器，你可能需要移除 `mcp_servers = []`。 **5. 开始证明** 让 Leanstral 处理一个定理、调试一个证明，或为仓库做出贡献。就是这么简单。