思考
摘要
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 由 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)。
Bug 发现：寻找隐藏缺陷
为了测试 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-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 处理一个定理、调试一个证明，或为一个仓库做出贡献。就这么简单。