Pythagoras-Prover：通过增强型Lean形式化方法推进高效形式化证明

# 通过增强的 Lean 形式化推进高效形式化证明  
**来源**: https://arxiv.org/html/2606.12594  

Joshua Ong Jun Leang<sup>p²,a²</sup>  
Zheng Zhao<sup>a²</sup>  
Mihaela Cătălina Stoian<sup>p²</sup>  
Qiyuan Xu<sup>b²</sup>  
Haonan Li<sup>c²</sup>  
Wenda Li<sup>a²</sup>  
Shay B. Cohen<sup>a²</sup>  
Eleonora Giunchiglia<sup>p²</sup>  

<sup>p²</sup>Imperial College London  
<sup>a²</sup>University of Edinburgh  
<sup>b²</sup>Nanyang Technological University  
<sup>c²</sup>MBZUAI  

###### 摘要  
现代 Lean 定理证明器只有在大量训练和推理计算条件下才能取得强性能。这一成本部分源于已验证证明数据的稀缺性，以及形式化证明搜索所需的长推理链条，这使得监督微调和采样都很昂贵。我们提出 **Pythagoras-Prover**——一个计算高效的开源 Lean 定理证明器家族，旨在实际计算预算下实现强性能。该家族涵盖两代生成范式：两个自回归模型（4B 和 32B 参数），以及首个基于扩散的定理证明模型概念验证（4B），该模型在推理时通过迭代优化 Lean 证明。为了提高训练效率，我们构建了一个经过 Lean 验证的语料库，并按难度分为简单、中等和困难问题，用于课程监督微调，使模型能够从较短、较简单的证明逐步掌握较长、较困难的证明。在监督微调过程中，我们还应用了动态证明推理过滤方案，保留信息性证明轨迹，同时确保每个训练实例适应 8k 令牌上下文预算。我们进一步引入**增强型 Lean 形式化 (Augmented Lean Formalisation, ALF)**，将稀缺的已验证语料库扩展为形式化语句的变体；然后通过自蒸馏填充这些变体，无需每个变异实例都经过形式化验证即可提供额外训练信号。通过扰动已知问题同时保留其形式化特性，ALF 使模型接触已验证问题的结构化变体，减少对任何单个语句表面形式的依赖。实验表明，Pythagoras-Prover 在不同模型规模上均表现出强劲性能。最值得注意的是，Pythagoras-Prover-4B 在 MiniF2F-Test 上的 pass@32 超越了 DeepSeek-Prover-V2-671B（从 82.4% 提升至 86.1%），尽管参数数量约为后者的 1/167。将规模扩展到 32B 后，Pythagoras-Prover-32B 在开源神经定理证明器中达到了最先进水平，在 MiniF2F-Test 上取得 93.0% 的通过率，并在 PutnamBench 上解决了 672 道问题中的 93 道。此外，我们发布了 **MiniF2F-ALF**，一个经 ALF 变异的污染敏感扰动基准，在该基准上所有评估模型的准确率均下降；在这个子集上，Pythagoras-Prover-32B 仍然是最强的评估证明器，而 Pythagoras-Prover-4B 与之前最先进的 Goedel-Prover-V2-32B 持平。这些结果共同表明，强 Lean 定理证明不一定依赖前沿规模的模型。我们的模型、数据和基准已在 https://huggingface.co/Pythagoras-LM 上发布。  

---

参阅图注  
**图 1**: 跨证明任务的性能比较。左图和中间图分别展示了在 MiniF2F-ALF 和 PutnamBench 上有限 Pass@32 推理预算下的结果；对于 PutnamBench，我们还包含了 Pythagoras-Prover 在 Pass@64 下的结果，其推理成本与采用自我修正的 Goedel-Prover-V2 相当（详见 §4）。右图绘制了已报告的最佳 MiniF2F-Test 通过率与模型大小（对数尺度）的关系，括号内显示了每个结果的推理预算；星号标记我们的模型 (Pythagoras-Prover)，“(sc)”表示自我修正。  

## 1 引言  

近年来，数学推理的进步使大型语言模型 (LLMs) 的能力显著提升，但它们仍不能保证正确性。尽管现代 LLMs 可以端到端地解决复杂问题，但其推理仍然容易产生自然语言检查无法可靠检测的幻觉和细微逻辑错误 (Leang et al., 2025a; Lyu et al., 2023)。自动定理证明 (ATP) 通过将模型输出锚定在交互式证明助手（如 Lean (de Moura et al., 2015)、Isabelle (Paulson, 1994) 和 Rocq (Coquand and Huet, 1988)）上来解决这一限制，这些证明助手的确定性类型检查器会拒绝任何无法机械验证的参数。这种形式化基础消除了整类幻觉，并产生可逐步审计正确性的推理。近年来，前沿系统如 DeepMind 的 AlphaProof 和 AlphaGeometry (Chervonyi et al., 2025; Hubert et al., 2025) 以及字节跳动的 Seed-Prover (Chen et al., 2025) 已证明人工智能系统能够达到国际数学奥林匹克 (IMO) 奖牌级别的性能。在开源社区中，DeepSeek-Prover-V2 (Ren et al., 2025)、Kimina-Prover (Wang et al., 2025a) 和 Goedel-Prover-V2 (Lin et al., 2026) 在标准基准（包括 MiniF2F (Zheng et al., 2022) 和 PutnamBench (Tsoukalas et al., 2024)）上报告了强结果。然而，这些成功通常是通过非常大的模型（数千亿参数）或通过计算密集型的推理（依赖复杂的搜索过程、自我修正或大量采样预算）实现的。因此，最先进的 ATP 对于缺乏大量计算资源的研究人员和从业者来说仍然难以触及，小型开源证明器与其最大对手之间仍存在显著差距。  

在这项工作中，我们发布 **Pythagoras-Prover**，一个面向 Lean 4 的计算高效开源定理证明器家族，挑战了“更强的形式化推理需要前沿规模模型”这一假设。Pythagoras-Prover-4B（4B 参数）在 MiniF2F-Test 的 pass@32 上超越了 DeepSeek-Prover-V2-671B (Ren et al., 2025)（从 82.4% 提升至 86.1%），尽管其大小约为后者的 1/167。在 32B 参数规模下，Pythagoras-Prover-32B 在未经自我修正评估的开源加权神经 Lean 证明器中实现了最强报告性能，在 MiniF2F-Test 上取得了最高通过率，且仅依赖标准重启采样而非推理时的修正过程。除了自回归证明，该家族还包括 **Pythagoras-Prover-Diffusion**——据我们所知，这是首个基于扩散的 Lean 定理证明模型概念验证。在相同的 4B 设置、相同的自蒸馏语料库和评估框架下，Pythagoras-Prover-Diffusion 在原始 pass@32 准确率上落后于 Pythagoras-Prover-4B，但在相同硬件上生成证明的速度快 2.58 倍，使其处于形式化定理证明中新兴的精度-效率前沿的吞吐量一侧。  

支撑我们所有发布的是一个计算节俭的 Lean 定理证明数据配方。我们首先构建一个约 80 万条实例的 Lean 验证种子语料库，主要使用不超过 30B 参数的开源模型，唯一较大的组件是一个 235B 模型。该验证语料库按难度分为简单、中等、困难三个层次，从而支持从较短、较简单的证明到较长、较困难证明的课程监督微调。然后我们引入**增强型 Lean 形式化 (Augmented Lean Formalisation, ALF)**，对每个验证实例生成五种变异类型的结构化形式化变体：简化、泛化、引理提议、证明步骤分解和重述。由于 ALF 使用轻量级合理性检查而非对每个变异实例进行 Lean 验证，它解耦了语料库扩展与验证器吞吐量，使种子语料库扩展约 2.5 倍。这些 ALF 变体随后以两种方式使用：首先，作为自蒸馏输入，丰富自回归和扩散证明器的后训练；其次，作为 **MiniF2F-ALF** 的基础，将相同的变异操作应用于 MiniF2F-Test，以探测性能是否能在邻近的形式化变体间迁移。当代证明器在该基准上性能大幅下降，表明在原始子集上的强性能并不总能迁移到结构化的形式化变体。因此，4B 和 32B 自回归证明器、扩散证明器以及配套基准都源自同一管道：验证种子构建支持课程学习，ALF 将种子扩展为结构化变体，自蒸馏将这些变体转化为训练信号，而相同的扰动机制则生成污染敏感的扰动基准。  

总结而言，我们的贡献如下：  

- **一个计算高效的 Lean 定理证明器家族**。我们发布 Pythagoras-Prover，一个面向 Lean 4 的开源定理证明器家族，涵盖两代生成范式：4B 和 32B 参数的自回归证明器，以及 Pythagoras-Prover-Diffusion-4B——据我们所知，这是首个基于扩散的定理证明模型概念验证。Pythagoras-Prover-4B 在 MiniF2F-Test 的 pass@32 上超越了 DeepSeek-Prover-V2-671B（从 82.4% 提升至 86.1%），尽管参数规模约为后者的 1/167，而 Pythagoras-Prover-32B 在未经自我修正评估的开源加权神经 Lean 证明器中实现了最强报告性能。  

- **一个计算节俭的 Lean 数据管道**。我们构建了约 80 万条实例的 Lean 验证语料库，按难度分为简单、中等、困难三个层次。然后我们引入**增强型 Lean 形式化 (ALF)**——一种结构化变异方案，通过轻量级合理性检查（而非每个实例的 Lean 验证）将语料库扩展约 2.5 倍。将相同的变异操作应用于 MiniF2F-Test，得到 **MiniF2F-ALF**——一个用于探测基准语句邻近形式化变体间迁移的配套基准。  

- **一个高效的 Lean 证明适配配方**。我们结合了参数高效的监督微调、课程学习、自蒸馏以及基于 Lean 验证的强化学习。在监督微调过程中，动态证明推理过滤器保留信息性推理轨迹，同时将每个实例控制在 8K 令牌上下文预算内。相同的后训练语料库同时训练自回归和扩散证明器，允许在生成范式之间进行受控比较。  

## 2 方法论  

本节详细描述 Pythagoras-Prover 的训练管道。我们首先描述生成 Lean 验证**种子**语料库的框架 (§2.1)。然后介绍将该语料库转化为基础自回归证明器的训练算法 (§2.2)。最后，我们引入**增强型 Lean 形式化 (ALF)**——一种结构化变异操作，将语料库扩展到超出每个实例 Lean 验证吞吐量的规模，以及基于此的自蒸馏阶段 (§2.3)；相同的自蒸馏语料库随后用于训练基于扩散的证明器 (§2.4)。  

---

参阅图注  
**图 2**: *简单* 和 *中等难度* 问题的种子合成数据生成管道。  

### 2.1 合成数据创建  

我们的训练语料库按三个难度层次生成，每个层次都经过 Lean 类型检查器的门控。*简单* 和 *中等* 实例从通用数学推理数据集自动形式化得到 (§2.1.1)，而 *困难* 实例则来自竞赛级别来源 (§2.1.2)。这些层次按构造单调排序：*简单* 实例是中等实例的基于规则的简化版本 (§2.1.1 末尾)；*中等* 问题是常规多步推理；*困难* 问题是需要通用数学语料库中不存在的高级技巧的竞赛证明。每个层次的代表性示例见附录 A.6。这个种子语料库以适度规模提供高质量；§2.3 通过增强型 Lean 形式化 (ALF) 进一步扩展它。  

#### 2.1.1 简单和中等难度层次  

简单和中等层次通过三个阶段种子管道生成：形式化语句合成、形式化证明验证以及基于规则的蒸馏，如图 2 所示。  

##### 形式化语句与形式化证明。  
我们的管道受“定理证明器作为裁判”管道 (Leang et al., 2025b) 启发，该管道利用形式化证明助手的确定性验证来过滤合成训练数据。虽然 Leang et al. (2025b) 仅处理来自 GSM8K 和 MATH500 的问题（由 GPT-4 (OpenAI et al., 2024) 形式化），我们通过从 **DART-Math-Hard** (Tong et al., 2024)、**DeepScaleR-Preview** (Luo et al., 2025) 和 **OpenR1-Math** (Hugging Face, 2025) 获取自然语言问题，拓宽了语料库的难度范围和领域覆盖。每个问题使用 Goedel-Autoformaliser-v2 (Lin et al., 2026) 自动形式化为 Lean 语句。为了减轻自动形式化引入的逻辑错误，我们随后应用 *自动非形式化* (Leang et al., 2025b)：将每个候选形式化语句翻译回自然语言，并与原问题进行对齐，丢弃存在逻辑差异的实例。对于每个保留的形式化语句，我们使用 Goedel-Prover-v2-32B (Lin et al., 2026) 合成候选证明——这是一个比 Leang et al. (2025b) 使用的 GPT-4 模型小数个数量级的开源证明器。我们每个语句进行 n=2 次独立证明尝试，如果至少一次尝试通过 Lean 类型检查器验证，则接受该 (语句, 证明) 对进入训练语料库。这个确定性验证步骤确保每个保留的训练示例都经过 Lean 验证，从而产生一个正确性由证明助手强制保证的语料库。  

##### 基于规则的蒸馏。  
现有的自动形式化器和证明器在相当一部分复杂数学语句上仍然失败 (Lin et al., 2026; Ren et al., 2025; Wang et al., 2025a)。我们...