思考摘要 Leanstral 1.5 是一个开放的 Apache-2.0 许可模型，具有 60 亿个活跃参数，提供了正式验证的重大性能升级，饱和了 miniF2F，解决了 587/672 个 PutnamBench 问题，并在 FATE-H (87%) 和 FATE-X (34%) 上达到了最先进的结果。通过中期训练、监督微调以及与 CISPO 的强化学习进行训练，它在主动证明工程和现实世界代码验证方面表现卓越，发现在测试的 57 个仓库中有 5 个之前未知的漏洞。Leanstral 1.5 完全开源，可通过 Hugging Face 和免费 API 获取，如今可以在 Lean 4 中进行实用的证明工程。自发布以来，Leanstral 提供了一种开放、实用的证明工程方法。今天，我们发布 Leanstral 1.5，这是一个免费的 Apache-2.0 许可模型，具有总计 1190 亿的参数，仅有 60 亿个活跃参数，提供了一个性能升级，使正式验证比以往任何时候都更加强大和可获取。Leanstral 1.5 饱和了 miniF2F，解决了 587/672 个 PutnamBench 问题，并在 FATE-H 和 FATE-X 上取得了新的最先进的成绩，分别为 87% 和 34%。除了基准测试之外，它还验证了复杂的代码属性，并发现在开源仓库中的之前未知的漏洞——证明严谨的正式方法在实际应用中既有效又实用。 训练 Leanstral Leanstral 1.5经历了一个三阶段的过程：中期训练、监督微调以及与 CISPO 的强化学习。Leanstral 1.5 在两个强化学习环境中进行了广泛训练：在多轮环境中，模型得到定理陈述，并必须证明或反驳它。模型提交证明，接收 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 展现了我们在正式推理模型中看到的最强测试时间扩展能力。下图跟踪了将每次尝试的令牌预算从 25K 提高到 4M 时，PutnamBench 上的 Pass@8：性能平稳且单调上升，从 50K 时解决的 44 个问题到 200K 的 244 个，1M 时的 493 个，最终在 4M 时解决 587 个。当证明运行时间较长时，Leanstral 不会放弃，而是继续推理，编辑文件，并在数百万个令牌中进行修订，将该预算直接转化为已解决的问题——这与下方 AVL 树证明的行为相同，该证明跨越 22 次压缩运行超过 270 万个令牌。随着这一版本的发布，我们也完全开源了 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 展现了强大的。