基于编译器引导的自适应证明搜索与跨模型协同在上下文依赖定理证明中的应用

# 上下文相关定理证明中基于编译器引导与跨模型协同的自适应证明搜索

来源：https://arxiv.org/html/2608.18084
罗切斯特大学刘卓（[email protected]）& 罗切斯特大学丁宇（[email protected]）& 罗切斯特大学何杭锋（[email protected]）

###### 摘要

现实世界 Lean 4 项目中的定理证明颇具挑战性，因为证明往往依赖于项目特定上下文。虽然迭代精修可以利用编译器错误修复失败的证明，但复用失败尝试则需要精细的搜索控制：某些证明提供了更好的起点，而后续修订可能损害一个部分正确的证明。我们提出了一种编译器引导的证明搜索框架，该框架平衡了探索与利用。它通过双模型生成与停滞触发重采样来探索多样化的起点，同时利用经编译器验证的成对比较来指导当前最优精修，从而利用有前景的证明状态。在来自 miniCTX-v2 的七个现实世界 Lean 4 项目上的实验表明，与 pass@k 基线相比，我们的方法在效果与效率之间实现了更好的权衡。在 pass@32 的预算内，我们的方法将平均通过率提高了 12.8 个百分点，同时将大型语言模型调用次数减少了 21.9%。

基于编译器引导与跨模型协同的自适应证明搜索用于上下文相关定理证明

罗切斯特大学刘卓（[email protected]）罗切斯特大学丁宇（[email protected]）罗切斯特大学何杭锋（[email protected]）

## 1 引言

大型语言模型（LLMs）越来越多地被用作代理，根据来自外部环境的反馈来修订其输出（Yang 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib24)；Chen 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib25)；First 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib2)）。形式定理证明非常适合研究这一过程：在 Lean 中（Moura 和 Ullrich，2021 (https://arxiv.org/html/2608.18084#bib.bib37)），每个候选证明都可以由编译器检查，而失败的尝试会从编译器获得结构化反馈（Chen 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib25)；First 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib2)）。

近年来，神经定理证明器在形式推理问题上取得了显著进展。诸如 DeepSeek-Prover-V2（Ren 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib3)）和 AlphaProof（AlphaProof 与团队，2024 (https://arxiv.org/html/2608.18084#bib.bib20)）等系统表明，神经证明器能够生成强有力的证明尝试，尤其是在奥数风格和基于库的基准测试中（Zheng 等人，2021 (https://arxiv.org/html/2608.18084#bib.bib12)；Tsoukalas 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib11)）。然而，在项目级 Lean 项目内证明定理会带来额外的挑战。现实世界的项目级证明通常依赖于局部定义、项目特定引理、命名约定以及分布在周围上下文中的证明模式（Tooby-Smith，2025 (https://arxiv.org/html/2608.18084#bib.bib38)）。最近在项目级 Lean 定理证明方面的努力（Hu 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib4)；Kumarappan 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib26)；Poiroux 等人，2025a (https://arxiv.org/html/2608.18084#bib.bib5)）表明，即使强大的证明器在这种设置下仍然步履维艰。

大多数现有方法依赖于独立采样：证明器生成多个完整的候选证明，成功率通过 pass@k（Chen 等人，2021 (https://arxiv.org/html/2608.18084#bib.bib1)；Ren 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib3)）来衡量，即计数是否有任何候选证明通过验证。然而，这种范式将编译器视为最终的过滤器，而非指导后续尝试的反馈来源。因此，失败的证明即使包含有用的部分进展也会被丢弃。在上下文相关的形式证明中，这些部分进展可能包括一个相关的项目特定引理、一个有前景的证明大纲或一个几乎正确的策略序列。这迫使后续的采样在很大程度上从头开始。

编译器引导的精修（First 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib2)；Zhou 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib9)）提供了一种复用失败证明的自然方式，但有效的精修并不能得到保证。执行反馈可以改进代码生成和代理问题解决（Chen 等人，2021 (https://arxiv.org/html/2608.18084#bib.bib1)；Yang 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib24)；First 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib2)），但先前的研究也表明，自我纠正通常并不一定有益（Kamoi 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib27)；Adnan 和 Kuhn，2025 (https://arxiv.org/html/2608.18084#bib.bib28)）。同样，在编译器引导的证明精修中，额外的修订不一定会改善证明状态。一次修订可能修复一个错误的同时引入另一个错误，或者损害一个部分正确的证明。此外，精修对起始证明也很敏感：有些失败的尝试接近可修复，而另一些即使经过多次精修也陷入僵局。这些观察表明，在尝试新证明和改进现有证明之间存在一个探索-利用的权衡。因此，一个有效的证明器应该探索多样化的起始证明，在精修过程中保留有用的中间证明状态，并在当前路径停止改进时重新开始。在实践中，Lean 专用的证明器和通用推理模型在项目级问题上表现出互补的优势：前者生成精确的策略序列但未能充分利用周围的项目上下文，而后者更好地利用此上下文但更经常产生类型不正确的策略（Wang 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib33)）。

为此，我们提出了一种用于上下文相关 Lean 定理证明的编译器引导自适应证明搜索框架。该框架结合了跨模型探索和受控精修。在探索阶段，它从两个互补模型中抽取候选：一个提供策略级精度的 Lean 专用证明器，以及一个能更好利用长项目上下文的通用推理模型。一个基于编译器的成对比较选择更有前景的候选作为当前最优证明状态。在利用阶段，系统使用编译器反馈精修这个当前最优证明，但仅当成对比较显示改进时才接受一次修订。当精修停止取得进展时，它会返回探索阶段，并从两个模型重新采样候选。

我们的贡献如下：

- •我们引入了一个混合证明搜索框架，该框架使用互补的专家和通用模型进行探索，并将它们与当前最优精修和停滞触发重采样相结合。
- •我们分析了上下文相关 Lean 定理证明中的证明搜索轨迹，表明成功强烈依赖于起始证明以及保留有用的中间证明状态。
- •我们在来自 miniCTX-v2 的七个 Lean 4 项目和来自 RLMEval-FLT3 的 84 个形式化问题上评估了我们的框架，表明它在通过率与大型语言模型调用次数之间实现了更好的权衡。

代码。代码可在 https://github.com/joeliuz6/lean_proof_search 获取。

## 2 相关工作

### 2.1 上下文相关定理证明

上下文相关定理证明研究的是证明依赖于周围项目上下文的问题。miniCTX（Hu 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib4)）引入了一个基于七个现实世界 Lean 项目构建的基准，突显了在长项目上下文下定理证明的难度。RLMEval（Poiroux 等人，2025a (https://arxiv.org/html/2608.18084#bib.bib5)）评估了来自 Lean 蓝图（Zhu 等人，2026 (https://arxiv.org/html/2608.18084#bib.bib32)）形式化项目的研究级定理的神经定理证明和证明自动形式化。LeanAgent（Kumarappan 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib26)）在多个 Lean 仓库中进一步研究了这一设置。我们的工作针对这一现实场景，并侧重于如何复用失败的证明尝试。

### 2.2 完整证明生成

完整证明生成一次性生成完整的证明，而不是逐个预测证明策略。最近的系统在这一方向上取得了显著进展。AlphaProof（AlphaProof 与团队，2024 (https://arxiv.org/html/2608.18084#bib.bib20)）和 AlphaGeometry（Trinh 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib21)）证明了人工智能系统可以在国际数学奥林匹克（IMO）问题上达到奖牌水平的表现，而神经证明器（Wang 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib6)；Ren 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib3)；Chen 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib8)；Lin 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib7)）在 miniF2F（Zheng 等人，2021 (https://arxiv.org/html/2608.18084#bib.bib12)）和 PutnamBench（Tsoukalas 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib11)）等奥数风格基准上取得了强劲成果。其他系统使用验证器或编译器错误来修复失败的完整证明（Zhou 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib9)；First 等人，2023 (https://arxiv.org/html/2608.18084#bib.bib2)；Wang 等人，2026 (https://arxiv.org/html/2608.18084#bib.bib39)），表明失败的尝试可以为后续精修提供有用信息。我们的工作建立在完整证明生成的基础上，但侧重于对失败的完整证明进行搜索：我们使用互补模型寻找多样化的起点，并使用基于编译器的比较来保留有前景的证明状态。

参见标题 图 1：我们框架的概览。探索（左）通过一个通用模型和一个专家模型生成两个多样化的候选。利用（右）维护一个单一的当前最优证明 s*，并驱动其走向验证：每次修复产生一个*提案*，一个大型语言模型判断器决定是否接受它。当精修连续 N 轮停滞时，系统重新进入探索阶段，从两个模型抽取新的候选。验证与反馈层（底部）提供结构化错误反馈、策略建议和验证信号。

### 2.3 基于策略搜索的证明

一条互补的研究路线是基于策略的证明搜索，其中模型根据当前证明状态预测下一个策略。许多系统使用最佳优先搜索（Xin 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib15)；Wu 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib31)；Polu 和 Sutskever，2020 (https://arxiv.org/html/2608.18084#bib.bib40)）或相关的树搜索方法（Coulom，2006 (https://arxiv.org/html/2608.18084#bib.bib30)）来指导这一过程。例如，Lample 等人（2022 (https://arxiv.org/html/2608.18084#bib.bib16)）提出了一种 AlphaZero 风格的超树证明搜索算法以提高搜索效率。LeanProgress（George 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib29)）训练一个模型来预测证明进展，并使用此信号来指导搜索。BFS-Prover（Xin 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib15)）引入了一个可扩展的最佳优先搜索框架，其中包含基于状态-策略对的偏好优化和长度归一化。我们的工作在粒度上有所不同：我们不是搜索单个策略，而是搜索完整的证明候选。这使我们能够结合来自多个证明生成器的探索与对有前景的证明状态的精修。

## 3 编译器引导的自适应证明搜索

#### 概述

给定定理陈述 s 及其周围的 Lean 4 项目上下文 C，系统生成一个已验证的证明 p。我们设计了一个编译器引导的搜索过程，该过程协调两个互补的现成模型以及基于比较的精修。

我们将完整证明生成视为一个在证明候选上的搜索问题。系统维护一个单一的*当前最优证明状态* s*，并在两个阶段之间交替，如图 1 (https://arxiv.org/html/2608.18084#S2.F1) 所示：

- •探索通过从两个具有互补优势的模型（一个通用模型和一个专家模型）抽取候选来提出多样化的起点（§3.2 (https://arxiv.org/html/2608.18084#S3.SS2)），并在搜索停滞时重新调用两者（§3.4 (https://arxiv.org/html/2608.18084#S3.SS4)）。
- •利用使用编译器反馈精修当前最优证明，将每次修复视为一个可能替代也可能不替代 s* 的提案（§3.3 (https://arxiv.org/html/2608.18084#S3.SS3)）。

成对比较在整个过程中充当搜索控制器：它在探索期间选择更强的初始证明，在利用期间决定精修的提案是否应替代 s*，并在重采样后选择新的起点（§3.3 (https://arxiv.org/html/2608.18084#S3.SS3)）。

附录 A (https://arxiv.org/html/2608.18084#A1) 中的算法 1 (https://arxiv.org/html/2608.18084#alg1) 显示了完整的搜索过程。

### 3.1 基于编译器的反馈

我们不仅将 Lean 4 编译器用作验证器，还将其用作结构化错误反馈和轻量级自动策略的来源。

#### 结构化错误反馈

当证明失败时，我们提取结构化错误：错误位置和错误消息，与产生该错误的特定策略行对齐。这为模型提供了精确的行级定位，而非文件级的噪声。错误消息被修复模型和成对比较控制器共同使用。

#### 轻量级自动求解

在我们的工作中，AutoSolve 模块尝试一组小型的自动策略：确定性的闭合策略和 Lean 内置的引理搜索来解决简单目标。更多细节可在附录 E (https://arxiv.org/html/2608.18084#A5) 中找到。通过这种方式解决的证明无需任何模型调用即可退出搜索，为更难的目标节省预算。

### 3.2 探索：双模型候选生成

单个模型在重复的失败样本中经常产生类似的错误。因此，我们从两个互补的模型中各生成一个候选以增加有意义的多样性。

#### 通用模型

我们使用一个强大的通用推理模型作为通用模型，例如 GPT-5（Singh 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib34)）。其长上下文能力使其适用于利用项目特定的定义和依赖关系，尽管它仍可能产生无效的 Lean 语法或策略用法（Wang 等人，2024 (https://arxiv.org/html/2608.18084#bib.bib33)）。

#### 专家模型

我们使用一个 Lean 专用的证明器（Wang 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib6)；Ren 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib3)）作为专家，例如 Deepseek Prover（Ren 等人，2025 (https://arxiv.org/html/2608.18084#bib.bib3)）。因为它在大规模 Lean 证明数据上训练，所以它与 Lean 语法、策略和常见证明模式更匹配，但在利用长项目级上下文方面可能效果较差。

这两个模型通常以不同的方式表现：通用模型在上下文理解方面更强，而专家模型在形式证明语法方面更强。因此，它们倾向于产生不同类型的证明尝试，而不是重复相同的错误。在我们的方法中，每个候选在生成后立即验证；如果任一证明成功，系统无需精修即返回。否则，进行成对比较。