Leanstral 1.5: 证明的丰饶时代

Leanstral 1.5: 证明的丰饶时代

Mistral AI 发布了 Leanstral 1.5，这是一个专为 Lean 4 证明工程设计的专用模型。该模型总参数量为 119B，其中仅有 6B 为激活参数，采用 Apache-2.0 许可发布，并在形式化验证和数学推理方面提供了显著的性能提升。

性能基准测试

Leanstral 1.5 在多个关键数学基准测试中取得了最先进（state-of-the-art）的结果，展示了其处理初等和高等推理的能力。

  • miniF2F: 该模型完全饱和了这一跨系统的形式化数学基准测试，在验证集和测试集上均达到了 100%。
  • PutnamBench: Leanstral 1.5 解决了 Putnam 数学竞赛中的 672 道题目中的 587 道。其表现优于 Seed-Prover 1.5 (high setting)，并多解决了 7 道题，同时成本显著降低——每道题约 4 美元，而后者估计超过 300 美元。
  • FATE-H and FATE-X: 该模型在这些针对研究生和博士级问题的抽象代数基准测试上创下了新的最先进记录，解决了 87% 的 FATE-H 问题和 34% 的 FATE-X 问题。
  • FLTEval: Leanstral 1.5 将 pass@1 从 21.9 提升至 28.9，将 pass@8 从 31.9 提升至 43.2，以仅为 Opus 4.6 七分之一的成本超越了其 39.6 的表现。

训练方法论

Leanstral 1.5 是通过三个阶段的过程开发的：中期训练（mid-training）、监督微调（supervised fine-tuning）以及使用 CISPO 的强化学习。该模型在两个不同的 RL 环境中进行了训练：

  1. 多轮对话环境 (Multiturn Environment): 模型被要求证明或证伪一个定理陈述。它提交一个证明，接收来自 Lean 编译器的反馈，并迭代地改进其方法，直到证明通过编译或预算耗尽。
  2. 代码智能体环境 (Code Agent Environment): 模型作为一个开发者在原始文件系统中运行，编辑文件、运行 bash 命令，并利用 Lean 语言服务器来检查目标、错误和类型信息。这种环境允许模型处理长程任务，例如在仓库中完成部分证明并构建辅助引理。

测试时扩展 (Test-Time Scaling) 与推理

Leanstral 1.5 表现出强大的测试时扩展能力，这意味着随着每次尝试的 token 预算增加，其性能会单调提升。在 PutnamBench 上，Pass@8 性能从使用 50k tokens 时解决的 44 道题增加到使用 4M tokens 时解决的 587 道题。这种能力允许模型在数百万个 token 之间进行推理、编辑文件并进行修订，正如在一个复杂的 AVL-tree 证明中所示，该证明需要超过 270 万个 token 和 22 次压缩。

现实世界代码验证案例研究

Leanstral 1.5 在验证代码属性和在开源仓库中发现漏洞（bug）方面展示了实际应用价值。

AVL Tree 时间复杂度

该模型成功证明了 AVL 树真实实现的 O(log n) 时间复杂度保证。这需要结构归纳法、处理单子（monadic）时间追踪以及对重平衡路径进行详尽的案例分析。

开源软件中的漏洞发现

通过使用包含 Aeneas（用于将 Rust 代码转换为 Lean）和 Leanstral 1.5（用于推断意图并生成正确性属性）的流水线，Mistral AI 在 57 个测试的仓库中识别出了 11 个真实的漏洞，其中 5 个是之前在 GitHub 上未见报道的。一个显著的例子是在 datrs/varinteger 库的 zigzag decoding 的 sign 函数中存在一个溢出漏洞，该漏洞在输入 Std.U64.MAX 时发生。

社区反馈与分析

虽然模型的性能令人印象深刻，但 Hacker News 上的社区成员提出了几个讨论点：

"我发现漏洞发现的例子很奇怪……在这种情况下，这种边界条件案例怎么会被认为是一种‘测试……通常会漏掉’的情况？"

一些用户认为，像在 datrs/varinteger 中发现的漏洞，边界条件漏洞通常会被模糊测试（fuzzing）或仔细的测试所捕捉。其他人则指出，该漏洞在公告发布前一周就已经作为 GitHub issue 报告过，从而质疑了所谓的“发现”的有效性。

此外，一些用户质疑了基准测试的时机，认为对比的是较旧的模型，而其他人则质疑了选择 Lean 4 而非其他形式化验证工具（如 Isabelle/HOL 或 TLA+）的原因。

开始使用 Leanstral 1.5

Leanstral 1.5 可以在 HuggingFace 上作为 Apache-2.0 许可的模型下载，也可以通过免费的 API 端点 (leanstral-1-5) 使用。用户可以通过以下设置在 Mistral Vibe 中部署它：

  1. 安装 Mistral Vibe: uv tool install mistral-vibe 随后执行 vibe --setup。
  2. 安装 Leanstral 1.5: /leanstallexit。
  3. 启动智能体 (Agent): vibe --agent lean。
  4. 可选的 LSP MCP: 通过将 lean-lsp-mcp 添加到 ~/.vibe/config.toml 文件中以增强功能。

Sources