Leanstral 1.5 发布：为所有人提供丰富证明

背景

形式化验证（formal verification）通过数学证明确保软件和定理的正确性，长期以来被认为门槛高、成本昂贵。传统的证明助手如 Lean 4 需要专家手动构造冗长的证明链，限制了其在实际开发中的普及。2023 年发布的 Leanstral 模型首次将语言模型引入 Lean 4 的证明工程，提供了开放、实用的方案。如今，团队推出 Leanstral 1.5，以 Apache-2.0 许可证免费开源，参数规模达 119B（仅 6B 活跃参数），在多项形式化基准上实现性能跃升，并展示了在真实代码仓库中发现隐藏 Bug 的能力，旨在让形式化验证对所有人更加可及。

核心内容

Leanstral 1.5 是一个基于 Apache-2.0 许可证的开源模型，总参数 119B，每次推理仅激活 6B 参数。训练采用三阶段流程：mid-training（中间训练）、supervised fine-tuning（有监督微调）和 reinforcement learning with CISPO（基于 CISPO 的强化学习）。其中强化学习在两个环境中进行：

• 多轮交互环境：模型获得定理陈述后，需要证明或证伪。它提交证明，接收 Lean 编译器反馈，然后迭代修正，直到编译通过或用完预算。
• 代码代理环境：模型直接操作原始文件系统，可编辑文件、运行 bash 命令、调用 Lean 语言服务器实时查看目标、错误和类型信息。这使它能够完成长期推理任务，如补全仓库中的局部证明、构建辅助引理，并支持多轮上下文压缩。最终通过 SafeVerify 的派生版本验证正确性。

评估结果：

• miniF2F：完全饱和（100%），验证集和测试集均达满分。
• PutnamBench（672 道 Putnam 数学竞赛题）：解决 587 题，超过 Seed-Prover 1.5 high 设置 7 题，且成本显著降低——每道问题约 4 美元，而 Seed-Prover 每道问题估计花费 300 美元以上（10 个 H20 天）。
• FATE-H / FATE-X（抽象代数研究生/博士级问题）：分别达到 87% 和 34% 的准确率，创下新 SOTA。更高排名的证明器要么依赖自然语言指导，要么成本极高（如 Aleph Prover 每道题 54–68 美元）。
• FLTEval（基于费马大定理仓库实际 PR 的基准）：Pass@1 从 21.9 提升至 28.9，Pass@8 从 31.9 提升至 43.2，超越 Opus 4.6 的 39.6，且成本仅为后者的七分之一。

测试时扩展性：Leanstral 1.5 表现出最强的测试时扩展能力——将每次尝试的 token 预算从 25k 提高到 4M，PutnamBench 上的 Pass@8 从 44 题（50k token）单调增长到 587 题（4M token），证明其能在长 token 链中持续推理、编辑文件、修正，而不轻易放弃。

代码验证案例研究：

1. AVL 树时间复杂度证明：Leanstral 1.5 为实际实现证明了 O(log n) 的插入与删除时间复杂度，使用了结构归纳、单子时间追踪和穷举情况分析，经过 270 万 token 和 22 次压缩后成功完成。证明中系统地展开 TimeM 单子层，建立每个高度单位约 48 步加上常数的紧确界，并通过对数关系关联高度与树大小。
2. Bug 发现：团队构建自动流水线——Aeneas 将 Rust 代码翻译为 Lean，Leanstral 推断用户意图并生成正确性属性，然后用四次机会尝试证明每个属性；若全失败，再用四次尝试证明其否定。在 57 个仓库中标记出 47 个违规属性，其中 11 个指向真实 bug，5 个此前未被报告。例如 datrs/varinteger 库的 zigzag 解码符号函数，在输入 Std.U64.MAX 时 (value + 1) 溢出，导致 debug 模式崩溃、release 模式静默破坏——测试和 fuzzing 通常错过此边界情况。

获取方式：模型权重托管于 Hugging Face，同时提供免费 API 端点 leanstral-1-5。推荐通过 Mistral Vibe 使用，安装步骤包括获取 API Key、配置环境、安装 Lean LSP MCP（可选）等。

关键要点

• 模型规格：总参数 119B，活跃参数仅 6B，Apache-2.0 完全开源，免费 API 可用。
• 训练三阶段：mid-training → supervised fine-tuning → reinforcement learning with CISPO；两个强化学习环境（多轮证明 + 代码代理）覆盖完整证明工程工作流。
• 基准表现：miniF2F 100% 饱和；PutnamBench 解决 587/672；FATE-H 87%、FATE-X 34% 创 SOTA；FLTEval 上 Pass@1 28.9、Pass@8 43.2。
• 成本优势：PutnamBench 每道题约 4 美元，仅为 Seed-Prover 1.5 high 的 1/75，远低于 Aleph Prover 等竞品。
• 测试时扩展：token 预算从 50k 到 4M，性能单调提升，最长证明使用 270 万 token 和 22 次压缩。
• 代码验证能力：成功证明 AVL 树 O(log n) 时间复杂度；在 57 个开源仓库中自动发现 5 个新 bug，涵盖边界溢出等难以捕捉的缺陷。
• 开放性：权重、API、评估基准 FLTEval 全部开放，支持通过 Mistral Vibe 直接使用。

意义与影响

Leanstral 1.5 标志着形式化验证从学术象牙塔走向工业实践的关键一步。首先，其极低的推理成本（每道复杂问题仅数美元）打破了此前只能依赖昂贵算力或专家手工的壁垒，使中小团队甚至个人也能将形式化验证纳入日常开发。其次，模型不仅擅长纯数学证明，还在真实代码仓库中展现出实用价值——自动发现传统测试和 fuzzing 遗漏的边界条件 bug，验证复杂数据结构的时间复杂度，这为安全关键系统（如加密库、操作系统、区块链）提供了低成本的正确性保障。第三，Apache-2.0 许可证和开放 API 降低了二次开发门槛，社区可以基于 Leanstral 1.5 构建更高效的证明工具或垂直领域代理。最后，其测试时扩展性表明，通过赋予模型更长的推理预算，可以系统性地提升证明能力，这为未来形式化模型的 scaling law 提供了实证。总体而言，Leanstral 1.5 让“证明丰裕”从口号变为现实，有望加速形式化方法在软件工程中的大规模落地。