ProofEvolve：用于形式化自动定理证明的神经符号进化

# ProofEvolve：用于形式化自动定理证明的神经-符号演化方法
来源：https://arxiv.org/html/2608.26334

**作者**  
管子维  
隶属：Meta AI  
核心贡献者  
谢毅航  
隶属：弗吉尼亚大学  
刘博涵  
隶属：弗吉尼亚大学  
Shivani Modi  
隶属：Meta AI  
张博云  
隶属：Meta AI  
温文俏  
隶属：Meta AI  
Henry Kautz  
隶属：弗吉尼亚大学  
张安东  
隶属：弗吉尼亚大学  

###### 摘要
自动定理证明为科学发现中的递归自我改进提供了天然基础。然而，现有的神经证明器未能完全保留这种递归结构，即学习过程应随时间自我改进。现有方法要么通过昂贵的权重更新将证明经验嵌入模型参数，要么仅将验证的中间推导保留在当前问题内。此外，这些方法还严重依赖稀疏的整体证明反馈，即使失败的局部尝试中也包含有用的发现。为弥补这一差距，我们提出了 ProofEvolve，一种神经-符号框架，它将显式的、经过形式验证的符号证明结构与神经模型相结合，以确定性地扩展知识边界。在此框架中，神经模型提出变体算子，包括分解、修复和模式重组。符号化的 Lean 内核验证每一次证明迁移。在演化循环中，ProofEvolve 计算由此生成的证明有向无环图（DAG）上的已验证闭包。在每个问题内部，ProofEvolve 在行为索引的存档中演化部分 AND-OR 证明 DAG。跨问题时，经过内核检查的模式提取将新证明的子 DAG 添加到持久的模式库中。证明 DAG 通过类型化的模式重组继承已解决的结果，将每个剩余的前提作为新的子目标暴露出来。这一演化过程保留了来自不完整尝试的已验证结果，并使其可供后续证明使用，而不会削弱形式可靠性。在三个竞赛级别的 Lean 基准测试中，ProofEvolve 在所评估的证明系统中实现了最高的平均求解率。

††日期：2026年8月10日††通信作者：温文俏和张安东，邮箱：[{wenqian, aidong}@virginia.edu](mailto:[email protected],[email protected])

## 1 引言
定理证明为科学推理铺平了道路，使其能在正确性形式保证下发现新知识。一个证明所贡献的往往不止其声明的结论。它可以产生可重用的引理，揭示隐藏的结构，并暴露新的假设。即使是未成功的证明程序也能推动重要进展。几个世纪以来，数学家们试图从欧几里得剩余的公理中推导出**欧几里得平行公理**。然而，考察该公理不成立的几何学，反而催生了非欧几何的发展（Bonola, 1955 (https://arxiv.org/html/2608.26334#bib.bib6)）。类似的模式也出现在理论计算机科学（TCS）中。希尔伯特的**判定问题**询问是否存在一个通用程序来确定一阶逻辑中任何命题的有效性（Hilbert and Ackermann, 1928 (https://arxiv.org/html/2608.26334#bib.bib16)）。随后，在这个问题悬而未决时，丘奇和图灵证明了不存在这样的通用程序（Church, 1936 (https://arxiv.org/html/2608.26334#bib.bib9); Turing, 1937 (https://arxiv.org/html/2608.26334#bib.bib46)）。图灵的分析还引入了一个计算的形式模型，后来成为TCS的基础。因此，证明从根本上将个体结果转化为可重用的知识，支持后续的发现。

图1：ProofEvolve概览。在某个目标内，一个证明DAG存档保留结构多样的候选证明，并根据从内核接受的子目标计算出的已验证闭包ρ\\rho进行排序。跨目标时，经过检查的提取将新证明的结果添加到持久的模式库中，而类型化的重组在后续的DAG中实例化它们，同时将所有剩余前提暴露为子目标。

近期，AI系统已开始自动化科学发现的部分流程。经过训练的神经模型与自动评估相结合，已产出新的算法、数学构造和结构模式（Romera-Paredes et al., 2024 (https://arxiv.org/html/2608.26334#bib.bib39); Novikov et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib31); Davies et al., 2021 (https://arxiv.org/html/2608.26334#bib.bib10)）。演化搜索也前景广阔，因为它可以通过重复生成、评估和选择来随时间改进候选方案。然而，当前基于语言的神经定理证明器仍然只使用了已验证结构的一小部分。基于训练的系统主要将经验存储在模型参数中，因此新结果只能在下一轮训练周期后才影响后续问题（Hubert et al., 2026 (https://arxiv.org/html/2608.26334#bib.bib17); Ren et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib38); Lin et al., 2025b (https://arxiv.org/html/2608.26334#bib.bib25)）。智能体系统利用多智能体协作，在推理时处理带有子目标的问题（Jiang et al., 2023 (https://arxiv.org/html/2608.26334#bib.bib19); Varambally et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib47)）。一项最新工作 LEAP（Kung et al., 2026 (https://arxiv.org/html/2608.26334#bib.bib22)）也在证明DAG的分支间共享中间引理，但这种记忆仍然绑定于当前目标。因此，当前系统仍然主要关注根定理是否被解决。

Lean 4（de Moura and Ullrich, 2021 (https://arxiv.org/html/2608.26334#bib.bib11)）中的形式化定理证明为累积演化提供了可靠环境，因为每一个接受的证明步骤都经过严格验证。然而，当前的神经定理证明器并未完全保留已验证的进展。基于训练的方法主要将经验存储在模型参数中（Hubert et al., 2026 (https://arxiv.org/html/2608.26334#bib.bib17); Ren et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib38); Lin et al., 2025b (https://arxiv.org/html/2608.26334#bib.bib25)），而智能体方法主要在当前问题内重用信息（Jiang et al., 2023 (https://arxiv.org/html/2608.26334#bib.bib19); Varambally et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib47); Kung et al., 2026 (https://arxiv.org/html/2608.26334#bib.bib22)）。因此，来自部分和已完成证明的有用结构很少在搜索之间被继承。这是演化搜索的一个核心限制，它要求有用的结构能在不成功的候选方案中存活下来，并传递给后续的世代。一个小的文本修改就可能使一个完整的证明失效，即使其大部分已验证的论证仍然是正确的（Nagashima, 2019 (https://arxiv.org/html/2608.26334#bib.bib30)）。因此，一个自我改进的证明器应该演化已验证的部分结构，而不仅仅是完整的证明文本，并保存它们以便在不同问题间进行重组。

为了解决这些不足，我们提出了 **ProofEvolve**，一个神经-符号演化框架，其中改进在一个由经验证的符号结构组成的显式体系中生长，并由神经提案驱动。如图1所示（https://arxiv.org/html/2608.26334#S1.F1），ProofEvolve 通过内核验证的迁移为每个定理构建一个证明DAG。在每一步，语言模型提出一个分解、修复或模式重组，Lean 4内核接受或拒绝它。一个行为索引的存档（Mouret and Clune, 2015 (https://arxiv.org/html/2608.26334#bib.bib29)）保留结构多样的部分证明，并按 ***verified closure***（一个基于内核的评分，通过AND-OR结构聚合已证明的子目标）进行排序，因此选择作用于分级的进展，而非单一的通过/失败判定。跨问题时，ProofEvolve 将已封闭的子DAG提取为定理模式。类型化的重组随后在一个匹配的目标上实例化一个模式，将任何剩余的前提作为新子目标暴露出来，并用内核重新检查结果。因此，来自早期问题的已验证结果扩大了后续问题的可达搜索空间。

为了展示其有效性，我们在三个竞赛级基准测试（PutnamBench、IMO-LeanProofBench 和 CombiBench）上评估了我们的框架，使用前沿 LLM（Claude Opus 4.8）作为基础模型，并在匹配的每目标预算下进行；同时在分离的 Lean Workbook 数据集划分上使用前沿开源模型 Qwen3.5-397B-A17B-FP8 进行了评估。ProofEvolve 达到了 57.8% 的平均求解率，而 LEAP 为 50.5%，Hilbert 为 45.9%。消融和测试时缩放研究进一步分析了该方法的组成部分及其在每目标预算增长时的行为。一项单独的评估分离了库本身的效果：在与来源流的 9,968 条定理不相交的 744 条 Lean Workbook 定理上，证明器自身的 546 个经内核检查的证明比零样本求解率提高了约四个百分点，而从同一库中随机检索则没有带来任何改进。

总之，我们的主要贡献如下：
- ∙\bullet 我们将定理证明形式化为一个基于结构化符号知识的演化过程，通过 Lean 验证的定理模式库实现持久遗传，其中神经模型提出新的方向以扩展知识边界。
- ∙\bullet 我们引入了基于内核的已验证闭包（verified closure）作为适应度度量，以及类型化模式重组（typed schema recombination）作为实现跨目标已验证子证明的机制。
- ∙\bullet 在三个竞赛级 Lean 基准测试上，将 ProofEvolve 与最先进的神经模型和智能体基线进行了广泛实验，展示了该框架的显著有效性；并且在与其库不相交的 744 条 Lean Workbook 定理上，证明器自身的已验证证明比零样本提高了约四个百分点，而从同一库中随机检索则毫无增益。

## 2 相关工作
### 2.1 神经定理证明器
神经定理证明器训练一个 LLM 策略来提出策略或用形式语言完成证明。GPT-f（Polu and Sutskever, 2020 (https://arxiv.org/html/2608.26334#bib.bib35)）和 PACT（Han et al., 2021 (https://arxiv.org/html/2608.26334#bib.bib15)）建立了用于策略生成的语言模型策略。其他工作（Yang et al., 2023 (https://arxiv.org/html/2608.26334#bib.bib52); Lample et al., 2022 (https://arxiv.org/html/2608.26334#bib.bib23); Xin et al., 2025a (https://arxiv.org/html/2608.26334#bib.bib50); Xin et al., 2025b (https://arxiv.org/html/2608.26334#bib.bib51)）将学习的提案与检索或树搜索相结合。近期系统通过合成证明、监督微调和强化学习获得了更强的策略（Ren et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib38); Lin et al., 2025b (https://arxiv.org/html/2608.26334#bib.bib25); Wang et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib49); ByteDance Seed, 2025 (https://arxiv.org/html/2608.26334#bib.bib8); Ji et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib18)）。AlphaProof（Hubert et al., 2026 (https://arxiv.org/html/2608.26334#bib.bib17)）在经内核检查的自生成经验上进行大规模训练，并在困难目标上进行测试时适应。检索增强证明器在推理时重用现有的库引理（Shen et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib40)），而自博弈系统则从成功和失败的证明树中学习（Poesia et al., 2024 (https://arxiv.org/html/2608.26334#bib.bib34)）。ProofEvolve 则相反，保持模型固定，并将新证明的结果存储为显式的、经验证的模式。

### 2.2 智能体定理证明器
智能体系统使用多个语言模型，通过分解、检索和验证器反馈来结构化证明搜索。Draft-Sketch-Prove（Jiang et al., 2023 (https://arxiv.org/html/2608.26334#bib.bib19)）将非形式化论证转化为形式化草图。COPRA（Thakur et al., 2024 (https://arxiv.org/html/2608.26334#bib.bib41)）通过重复的策略执行来构造证明。Hilbert（Varambally et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib47)）递归分解困难目标并修复失败的证明，而 LEAP（Kung et al., 2026 (https://arxiv.org/html/2608.26334#bib.bib22)）使用 AND-OR 证明 DAG 在分支间共享中间引理。AlphaProof Nexus（Tsoukalas et al., 2026 (https://arxiv.org/html/2608.26334#bib.bib45)）将编译器引导的智能体应用于研究问题，而 AlphaGeometry（Trinh et al., 2024 (https://arxiv.org/html/2608.26334#bib.bib43)）将神经提案与几何中的符号演绎相结合。这些方法强化了在单一目标内的搜索。相比之下，ProofEvolve 额外提取了经验证的子DAG，以便跨目标重用，这使该框架具备了递归演化的能力。

### 2.3 符号知识演化
演化程序搜索，包括 FunSearch（Romera-Paredes et al., 2024 (https://arxiv.org/html/2608.26334#bib.bib39)）和 AlphaEvolve（Novikov et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib31)），交替进行语言模型生成、自动评估和选择，而 MAP-Elites 在行为生态位中保留多样的高质量候选方案（Mouret and Clune, 2015 (https://arxiv.org/html/2608.26334#bib.bib29)）。LEGO-Prover 扩展了引理库（Wang et al., 2023 (https://arxiv.org/html/2608.26334#bib.bib48)），尽管仅存储并不能保证重用（Berlot-Attwell et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib5)）。DreamProver 最接近我们的场景，因为它保持模型固定，并通过清醒-睡眠抽象构建一个可迁移的 Lean 库（Zhang et al., 2026 (https://arxiv.org/html/2608.26334#bib.bib57); Ellis et al., 2021 (https://arxiv.org/html/2608.26334#bib.bib12)）。其他方法重新训练检索器（Kumarappan et al., 2024 (https://arxiv.org/html/2608.26334#bib.bib21)），蒸馏证明策略（Fang et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib13)），或使用经验适应度修改智能体代码（Zhang et al., 2025 (https://arxiv.org/html/2608.26334#bib.bib56)）。形式化证明演化很困难，因为验证是二值的，且微小的编辑可能使有用的候选方案失效（Nagashima, 2019 (https://arxiv.org/html/2608.26334#bib.bib30)）。ProofEvolve 则将已验证闭包和类型化模式重组结合在单个推理时过程中。部分证明 DAG 通过内核接受的子目标进行选择，而新封闭的子DAG 成为在后续候选方案中重用的模式，且无需修改模型。根据 Kautz 关于神经-符号 AI 的分类法（Kautz, 2022 (https://arxiv.org/html/2608.26334#bib.bib20)），ProofEvolve 是一个 **Neuro\[Symbolic\]** 系统，其中 Lean 内核和已验证闭包算子被嵌入到神经生成过程中，以实现随时间的递归改进。

## 3 预备知识
我们首先定义 ProofEvolve 操作的符号结构。每个状态都是一个 Lean 4 产物，搜索过程保留每一个部分结果而非丢弃它。一个尝试的封闭片段是一个有效的、可重用的结果，即使该尝试尚未封闭其根目标（公式 \(5\) (https://arxiv.org/html/2608.26334#S3.E5)）。正是这一特性使得后续搜索能够积累和转移已验证的工作（第4节 (https://arxiv.org/html/2608.26334#S4)）。

#### Lean 验证。我们在一个固定的 Lean 4 环境E\\mathcal{E}中工作，该环境导入了一个匹配的 Mathlib 版本（The mathlib Community, 2020 (https://arxiv.org/html/2608.26334#bib.bib42)）。当项p在局部上下文Γ下进行精化，并且不包含未解析的元变量或占位符时，我们写作E;Γ⊢Kp:g\\mathcal{E};\\Gamma\\vdash\_\\{\\mathcal{K}\\}p:g。