Leanstral 1.5 是一款采用 Apache-2.0 许可证的免费模型，拥有 60 亿活跃参数，在形式化验证方面实现了重大性能升级：在 miniF2F 基准上达到饱和，解决了 PutnamBench 中 672 道题目中的 587 道，并在 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 许可证的免费模型，总参数量为 1190 亿，但活跃参数仅为 60 亿，其性能升级使得形式化验证比以往任何时候都更强大、更易用。
Leanstral 1.5 在 miniF2F 上达到饱和，解决了 PutnamBench 中 672 道题目中的 587 道，并在 FATE-H 上取得了 87%、在 FATE-X 上取得了 34% 的最新最优结果。除了基准测试之外，它还能验证复杂的代码属性，并在开源代码仓库中发现此前未知的错误——证明了严谨的形式化方法对于实际应用既有效又实用。
训练 Leanstral
Leanstral 1.5 经历了三个阶段：中期训练、监督微调以及基于 CISPO 的强化学习。Leanstral 1.5 在两个强化学习环境上进行了大量训练：
在多轮交互环境中，模型会收到一个定理陈述，必须证明或证伪它。模型提交一个证明，接收 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 高设置的成本（每个问题约 4 美元，而 Seed-Prover 高设置每个问题预算约为 10 个 H20 天，估计成本 300 美元或更多）多解决了 7 个问题。排名更高的证明器运行条件不同——有些接收自然语言证明引导，另一些运行成本则高得多，例如 Aleph Prover 每个问题成本为 54 至 68 美元。
Leanstral 1.5 展现了我们在形式化推理模型中所见过的最强测试时扩展能力。下图追踪了在 PutnamBench 上，当我们将每次尝试的 token 预算从 25k 提升至 4M 时的 Pass@8 表现：性能在整个过程中平滑且单调地上升，从 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 主要针对数学进行训练，但它在代码验证方面也展现出强大的能力。我们提供两个关键案例研究来展示其影响。
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 库的锯齿解码符号函数中。当输入为 `Std.U64.MAX` 时，表达式 `(value + 1)` 发生溢出，导致调试模式下崩溃，发布模式下则造成静默数据损坏——这是一个测试和模糊测试通常会遗漏的边界情况。Leanstral 的流水线自动捕获了它，这证明了形式化验证已经可以应用于真实世界的代码库，并发现一些传统方法会忽略的 bug。
Leanstral 1.5 采用 Apache-2.0 许可证。权重可在 HuggingFace 上找到，同时现在也可通过免费 API 端点 leanstral-1-5 获取。我们建议在 Mistral Vibe 中使用它。要开始你的旅程，请获取一个 API 密钥，然后：
- 设置 Mistral Vibe
uv tool install mistral-vibeuv tool update mistral-vibevibe --setup
- 安装 Leanstral 1.5
/leanstallexit
- 启动智能体
vibe --agent lean
- 安装 Lean LSP MCP（可选）
强烈建议通过将以下内容添加到你的 ~/.vibe/config.toml 来安装 Lean LSP MCP
[[mcpservers]]name = "lean-lsp"transport = "stdio"command = "uvx"args = ["lean-lsp-mcp"]tooltimeoutsec = 600
如果没有现有的 MCP 服务器，你可能需要移除 `mcpservers = []`。
- 开始证明
让 Leanstral 去攻克一个定理、调试一个证明，或者为一个仓库做贡献。就这么简单。