Mistral AI 发布 Leanstral 1.5：6B 激活参数的 Lean 4 形式化证明模型

Thinking

Summary

Leanstral 1.5，一个免费的 Apache-2.0 许可模型，拥有 6B 活跃参数，在形式化验证方面带来了重大性能升级，使 miniF2F 饱和，解决了 587/672 个 PutnamBench 问题，并在 FATE-H（87%）和 FATE-X（34%）上取得了最先进的结果。通过中期训练、监督微调和 CISPO 强化学习进行训练，它在智能体证明工程和真实世界代码验证方面表现出色，在测试的 57 个代码库中发现了 5 个此前未知的漏洞。Leanstral 1.5 完全开源，可通过 Hugging Face 和免费 API 获取，现在可用于 Lean 4 中的实际证明工程。

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

Leanstral 1.5 使 miniF2F 饱和，解决了 587/672 个 PutnamBench 问题，并在 FATE-H 上达到 87%、在 FATE-X 上达到 34% 的新最先进水平。除基准测试外，它还能验证复杂的代码属性，并在开源代码库中发现此前未知的漏洞——证明严格的形式化方法对真实世界应用既有效又实用。

训练 Leanstral

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

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

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

评估

我们在以下基准上评估 Leanstral：

• miniF2F 是一个跨系统的形式数学基准，范围从初等数学问题到 IMO 级别的挑战，测试代数、组合数学和数论等领域的多种证明能力。

• PutnamBench 包含来自 Putnam 数学竞赛的 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 预算从 25k 提高到 4M：性能一路平稳单调攀升，从 50k 时解决的 44 个问题到 200k 时的 244 个，1M 时的 493 个，以及 4M 时的 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 在代码验证方面表现出强大的能力。我们提出 2 个关键案例研究来展示其影响。

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 个指向真实存在的 bug——其中 5 个此前未在 GitHub 上被报告过。

其中一个 bug 出现在 datrs/varinteger 库 zigzag 解码的 sign 函数中。当输入为 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. 启动 agent

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 去攻克一个定理、调试一个证明，或为一个代码库做贡献。就这么简单。