# Leanstral 1.5：人人可用的证明丰富性

- 来源：Mistral AI：News（网页）
- 发布时间：2026-07-02 00:00
- AIHOT 分数：66
- AIHOT 标记：精选
- AIHOT 链接：https://aihot.virxact.com/items/cmr52xv9507bssll51ft3loac
- 原文链接：https://mistral.ai/news/leanstral-1-5

## 精选理由

Leanstral 1.5饱和miniF2F基准，成本仅为同类模型1/75，并自动发现5个真实代码bug，表明AI形式验证开始实用化。虽然受众窄，但对代码正确性有执念的开发者必看。

## AI 摘要

Mistral AI 今日发布 Leanstral 1.5，一款 Apache-2.0 许可的开源形式化验证模型，119B 总参数仅 6B 活跃。在 miniF2F 上达 100% 饱和，PutnamBench 解决 587/672 题，FATE-H（87%）和 FATE-X（34%）创 SOTA。训练经历 mid-training、SFT 和基于 CISPO 的强化学习。具备智能体式证明能力，在 57 个开源仓库中发现 5 个未知 bug。模型已通过 HuggingFace 和免费 API 开放使用。

## 正文

自发布以来，Leanstral 一直为 Lean 4 中的证明工程提供一种开放、实用的方法。今天，我们发布了 Leanstral 1.5，这是一个采用 Apache-2.0 许可的免费模型，总参数量为 119B，而激活参数仅为 6B，其性能提升使得形式化验证比以往任何时候都更强大、更易用。

Leanstral 1.5 **在 miniF2F 上达到饱和，解决了 PutnamBench 中的 587/672 个问题**，并在 FATE-H 上取得了 87% 的新 SOTA，在 FATE-X 上取得了 34% 的新 SOTA。除了基准测试之外，它还能验证复杂的代码属性，并在开源代码仓库中发现先前未知的错误——证明了严谨的形式化方法在实际应用中既能高效又实用。训练 Leanstral

Leanstral 1.5 经历了三个阶段：中期训练、监督微调以及使用 CISPO 的强化学习。Leanstral 1.5 在两个 RL 环境中进行了大量训练：

在多轮交互环境中，模型会收到一个定理陈述，并且必须证明或证伪它。模型提交一个证明，接收 Lean 编译器的反馈，并在每次尝试中优化其方法。如果证明通过编译，则成功；否则，循环继续，直到模型解决问题或用尽预算。

在代码智能体环境中，Leanstral 像开发者一样在原始文件系统中操作：它编辑文件、运行 bash 命令，并使用 Lean 语言服务器实时检查目标、错误和类型信息。这使得它能够处理长期任务，例如完成代码仓库中的部分证明、构建辅助引理，以及在多轮上下文压缩中持续工作。该模型学习驾驭完整的证明工程工作流程，并最终通过我们基于 SafeVerify 的分支进行正确性验证，该验证基于给定的目标定理列表。评估

我们在以下基准上对 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 指标，我们将每次尝试的 token 预算从 2.5 万提升至 400 万：性能全程平滑且单调地攀升，从 5 万 token 时解决 44 道题，到 20 万时解决 244 道，100 万时解决 493 道，400 万时解决 587 道。当证明过程变长时，Leanstral 并不会放弃，而是持续推理、编辑文件并在数百万 token 范围内进行修订，直接将预算转化为已解决的题目——这正是下方 AVL 树证明背后的行为，该证明在 22 次压缩中运行了超过 270 万 token。

在此次发布中，我们还完全开源了 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 万个 token 和 22 次压缩中，Leanstral 系统地展开了 TimeM 单子的每一层，揭示了底层计算，尽管它们与控制流交织在一起。它建立了每个高度单位约 48 步加上一个常数的插入紧界，然后通过对数关系将高度与树的大小联系起来，提供了完整且经过验证的证明，证明插入和删除确实是 O(log n)。漏洞发现：寻找隐藏缺陷

为了测试 Leanstral 的漏洞捕捉能力，我们构建了一个自动化流水线：Aeneas 将 Rust 代码翻译为 Lean，而 Leanstral 则推断用户意图并从代码中生成正确性属性。随后，Leanstral 尝试在四次尝试中证明每个属性。如果全部失败，它会转而尝试证明该属性的否定，同样进行四次尝试。在 57 个经过测试的代码仓库中，该过程标记了 47 个违反的属性，其中 11 个指向真正的漏洞——其中 5 个此前未在 GitHub 上报告过。

其中一个 bug 出现在 datrs/varinteger 库的锯齿解码符号函数中。当输入为 Std.U64.MAX 时，表达式 (value + 1) 发生溢出，导致调试模式下崩溃，发布模式下则静默损坏——这是一个测试和模糊测试通常难以发现的边界情况。Leanstral 的流水线自动捕获了该问题，证明形式化验证已可应用于真实代码库，并能发现某些传统方法遗漏的 bug。

Leanstral 1.5 采用 Apache-2.0 许可证。模型权重可在 HuggingFace 上获取，同时现在也可通过 leanstral-1-5 这一免费 API 端点使用。我们建议在 Mistral Vibe 中使用它。要开始使用，请获取 API 密钥，然后：

1. 设置 Mistral Vibe

uv tool install mistral-vibeuv tool update mistral-vibevibe --setup

2. 安装 Leanstral 1.5

/leanstallexit

3. 启动智能体

vibe --agent lean

4. 安装 Lean LSP MCP（可选）

强烈建议通过将以下内容添加到您的 ~/.vibe/config.toml 来安装 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 处理一个定理、调试一个证明，或为某个代码仓库做出贡献。就这么简单。