Mistral 发布 Leanstral 1.5：6B 激活参数的形式化证明模型，Apache-2.0 完全开源

Thinking

Summary

Leanstral 1.5，一个免费的 Apache-2.0 许可模型，拥有 6B 活跃参数，在形式化验证方面带来重大性能升级，使 miniF2F 饱和，解决了 587/672 个 PutnamBench 问题，并在 FATE-H（87%）和 FATE-X（34%）上取得最先进的结果。通过中期训练、监督微调和使用 CISPO 的强化学习进行训练，它在智能体证明工程和真实世界代码验证方面表现出色，在测试的 57 个仓库中发现了 5 个此前未知的 bug。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% 的新最先进水平。除基准测试外，它还能验证复杂的代码属性，并在开源仓库中发现此前未知的 bug——证明严格的形式化方法对真实世界使用既有效又实用。

训练 Leanstral

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

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

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

评估

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

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

• PutnamBench 由 672 个来自 Putnam 数学竞赛的问题组成，需要深度推理和长证明链来解决具有挑战性的数学问题。

• 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 个指向真正的缺陷——其中 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 处理一个定理、调试一个证明，或为一个仓库做贡献。就这么简单。