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

- 来源：Mistral AI：News（网页）
- 发布时间：2026-07-02 00:00
- AIHOT 分数：66
- AIHOT 标记：精选
- AIHOT 链接：https://aihot.news/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 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 依托在两个强化学习环境上的大规模训练：

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

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

评估

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

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

PutnamBench 由 672 道 Putnam 数学竞赛题目组成，需要深度推理和长证明链来求解这些具有挑战性的数学问题。

FATE-H 和 FATE-X 分别是面向研究生和博士级别问题的抽象代数基准，测试群论、环论和模论等领域的高级推理能力。

FLTEval 基于费马大定理代码仓库中的真实 pull request，测试具有真实世界复杂度的实用证明工程能力。

我们在 miniF2F 上完全饱和，验证集和测试集均达到 100%。在 PutnamBench 和 FATE-H/X 上，我们将 Leanstral 1.5 与无自然语言引导的 Goedel-Architect、高配置下的 Seed-Prover 1.5 以及 AxProverBase 进行了对比。

Leanstral 在 FATE-H/X 上达到新的 SOTA，分别解决了 87 道和 34 道问题。在 PutnamBench 上，它以远更低的成本以多解出 7 道问题的优势胜过高配置的 Seed-Prover 1.5：每道问题约 $4，而 Seed-Prover 估计需要 $300 或更多，其高配置每道问题的运行预算为 10 H20-days。

排名更高的证明器仅在不同的条件下运行——有些接受自然语言证明引导，另一些运行成本远更高，例如 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 解码的符号函数中。当输入为 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-vibeuv tool update mistral-vibevibe --setup

2. 安装 Leanstral 1.5

/leanstallexit

3. 启动智能体

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