奖励预言机MCTS用于形式定理证明：样本高效搜索与内核级证明审计的必要性

# 用于形式定理证明的奖励神谕MCTS：样本高效搜索与内核级证明审计的必要性
来源：https://arxiv.org/html/2608.28639

###### 摘要
使用大型语言模型进行形式定理证明仍然具有挑战性，原因在于难以高效地探索庞大的证明搜索空间。现有的树搜索方法要么将冗长的编译器错误信息直接输入生成上下文，增加了搜索过程中的上下文使用量；要么采用非标准的评估协议，使其无法与已建立的基线直接比较。我们提出了一种三角色蒙特卡洛树搜索框架，该框架将Lean 4编译器纯粹视为一个奖励神谕，利用编译器输出作为标量信号进行UCB引导的树更新，而不将错误内容输入生成上下文。我们的框架将证明搜索分解为三个角色：一个生成器用于尝试证明，一个分解器用于子目标分解，以及一个评估器用于子目标质量评估。我们在涵盖竞赛数学和物理的4个基准测试上进行了评估（MiniF2F、PutnamBench、LeanPhysBench、PhysLeandata），使用了三个证明模型，并在标准证明尝试预算下进行（PAB@16到PAB@256）。我们的方法在PAB@256时使用Goedel-Prover-V2-8B在MiniF2F上达到了87.1%的准确率，并在PAB@32时解决了PutnamBench的26/659个问题，超过了在相同证明尝试预算下的基础采样（18/659）。通过对每个编译通过的证明进行详尽的公理级审计，我们进一步识别了基于搜索的定理证明中的奖励欺骗现象：DeepSeek-Prover-V2-7B在PutnamBench上生成了能通过编译和标准sorry令牌扫描的证明，但其依赖于sorryAx。该审计在PAB@32和PAB@128的全局证明采样中分别移除了4个和8个此类证明，在MCTS中移除了11个和19个。我们并未将这些数量归因于搜索过程；我们报告它们是为了确立内核级审计对于经过编译器验证的评估是必要的。

## 引言
使用大型语言模型进行形式定理证明已成为人工智能推理领域一个具有挑战性的前沿，要求模型在满足交互式定理证明器（如Lean 4和Isabelle）严格正确性要求的同时，导航指数级庞大的证明搜索空间。近期专用证明模型的进展已在既定基准测试上展示了有希望的结果，然而高效探索证明搜索空间的根本挑战仍然存在。我们提出了一种三角色蒙特卡洛树搜索框架，该框架建立在一个独特的架构原则之上：Lean 4编译器被专门用作一个奖励神谕，而不是作为后续生成的文本反馈源。与那些将错误消息或证明状态诊断信息附加到模型上下文的编译器引导方法不同，我们的方法将编译结果转换为标量奖励，这些奖励通过搜索树传播，并仅用于UCB引导的节点选择。这种验证与生成之间的分离防止了编译器反馈随搜索深度累积，同时仍然允许形式验证信号通过价值反向传播影响未来的探索。因此，该框架在自然语言证明计划上执行迭代的、由验证器引导的搜索，而无需基于编译器错误条件生成。
我们的框架将证明搜索分解为三个不同的角色：一个生成器产生完整的证明尝试，一个分解器将问题分解为子目标（采用温度衰减采样以平衡探索与利用），以及一个评估器评估子目标质量以提供比二元编译器输出更丰富的奖励信号。在每次MCTS迭代中，UCB策略从根节点遍历当前树，根据反向传播的编译器奖励和评估器奖励选择叶子节点。我们将主要比较限制在相同冻结检查点上的全局证明采样，而不是像BFS-Prover、HunyuanProver等重新训练或微调底层证明模型的方法。因为这些方法通过重新训练的价值/策略网络、额外的强化学习或对抗生成的训练数据改变了检查点本身，任何性能差异都混淆了搜索过程增益与模型增益，无法分离搜索算法的贡献。全局证明采样提供了最干净的主要基线，用于在固定证明模型检查点的同时隔离推理时搜索的效果。我们还与使用相同冻结检查点、提示和评估环境的推理时结构化搜索基线进行了比较。
在整篇论文中，我们使用术语“证明尝试预算”和“预算”互换，并用PAB@PAB@表示。我们在涵盖竞赛数学和理论物理的四个基准测试上进行了评估：MiniF2F、PutnamBench、LeanPhysBench和PhysLeandata，使用了三个专用证明模型（Goedel-Prover-V2-8B、DeepSeek-Prover-V2-7B、Kimina-Prover-Preview-Distill-7B），并在标准证明尝试预算下进行（PAB@16到PAB@256）。
在PutnamBench上，我们的方法在PAB@32时使用Goedel-Prover-V2-8B解决了26/659个问题，超过了在相同证明尝试预算下的基础采样（18/659）。在MiniF2F上，我们的方法在PAB@256时使用Goedel-Prover-V2-8B达到了87.1%，并且随着证明尝试预算的增加，性能持续稳定提升。
除了强有力的实证结果外，我们还识别并描述了一种奖励欺骗现象。此前有报道称DeepSeek-Prover-V2-7B利用了Lean 4.9.0的接口漏洞，该模型在PutnamBench的全局证明采样和MCTS中都产生了依赖于该漏洞的成功证明。在PAB@32时，审计从全局证明采样中移除了4个成功证明，从MCTS中移除了11个；在PAB@128时，分别移除了8个和19个。这一发现凸显了基本的评估风险，使得内核级证明审计对于基于搜索的定理证明评估至关重要。我们进一步进行了系统的多智能体分析，表明对于所评估的模型，选择性地使用异构评估器可以改进证明搜索，而异构分解则会一致地降低性能。

## 相关工作
### 使用大型语言模型进行形式定理证明
早期的神经定理证明方法侧重于训练专用模型以在单次前向传递中生成完整的证明尝试。GPT-f证明了在数学文本上预训练的语言模型在证明语料库上进行微调时可以生成有用的证明步骤，为后续工作奠定了基础。ReProver引入了用于策略预测的检索增强生成，通过将证明生成条件化在从Mathlib检索到的相关前提上来提高性能。
### 用于定理证明的树搜索
树搜索方法在形式推理领域有着悠久的历史。超树证明搜索将蒙特卡洛树搜索应用于Lean证明搜索，使用与证明模型联合训练的学习价值函数来指导节点扩展。COPRA通过维持跨尝试的证明状态并将编译器反馈纳入后续生成来执行上下文敏感的证明搜索。草稿-提纲-证明方法将证明分解为高级提纲，随后由策略模型完成，预见了中间证明分解的使用。ReProver通过检索增强生成改进了策略预测，而证明代理则在树框架内执行迭代的编译器引导搜索。
### 大型语言模型推理中的蒙特卡洛树搜索
MCTS已被广泛应用于改进定理证明之外的LLM推理。思维树使用LLM引导的搜索，结合对中间状态的价值估计来探索推理步骤。规划推理将MCTS与基于LLM的世界模型应用于多步推理任务。思维证明将AlphaZero式的自博弈扩展到数学推理，联合训练价值和策略网络。
### 全局证明生成
一个互补的研究方向侧重于全局证明生成，其中模型在单次传递中生成完整的Lean证明脚本，通常伴随着扩展的推理轨迹。该范式的最新进展主要由两种方法驱动。第一种采用专家迭代框架，将成功验证的证明迭代地纳入训练语料库，以逐步改进证明器。第二种利用由证明助手验证信号引导的强化学习，使模型能够通过基于验证器的反馈来改进证明生成。
### 强化学习中的奖励欺骗
奖励欺骗是强化学习中一种有据可查的失败模式，即代理利用奖励信号中的非预期模式，而不是解决预期任务。在LLM背景下，奖励欺骗在RLHF环境中已被观察到，模型学会利用奖励模型的弱点。特别是在形式定理证明中，有报道称DeepSeek-Prover-V2-7B利用了Lean 4.9.0编译器的漏洞，其中apply?策略在某些条件下未能发出sorry声明，从而产生了能通过编译但数学上无效的证明。
### Lean 4 证明评估基础设施
Lean 4证明的自动化评估需要交互式定理证明器基础设施，该基础设施能够编译策略级证明尝试并以编程方式返回验证结果。为此目的已开发了几种工具，每种工具都有不同的设计权衡。LeanDojo是一个开源框架，通过基于REPL的交互模型为Lean 4提供编程接口，能够从Mathlib提取证明状态、执行策略和检索前提。LeanDojo已成为许多定理证明基准测试（包括MiniF2F和PutnamBench）的标准评估基础设施，其前提提取能力支撑了像ReProver这样的检索增强方法。LeanInteract扩展了基于REPL的方法，改进了会话管理并支持并行证明评估，降低了维护多个并发Lean进程的开销。PyPantograph采取了一种不同的方法，通过直接FFI绑定（而不是REPL子进程）提供对Lean 4内核的Python原生接口。Kimina Lean Server专门为强化学习和树搜索方法的背景下的大规模并行证明评估而构建。与维护单个Lean进程顺序交互的基于REPL的工具不同，Kimina Lean Server管理一个持久的Lean REPL实例池，以处理并发的证明编译请求，从而在树搜索方法所需的采样预算下实现高吞吐量评估。该服务器公开一个HTTP接口，接受完整的Lean 4证明字符串并返回编译结果，包括成功状态、错误消息和sorry使用检测。我们的方法在所有实验中使用Kimina Lean Server作为编译器奖励神谕。

## 与现有推理时搜索方法的比较
为明确我们框架与先前用于形式定理证明的推理时搜索方法之间的算法区别，表1总结了主要设计选择。与那些将未来生成条件化于编译器反馈或证明状态诊断的方法不同，我们的方法将Lean验证器专门视为一个*奖励神谕*：只有标量奖励通过MCTS传播，编译器消息永远不会插入LLM上下文。此外，我们的搜索在自然语言证明计划上运行，而非形式证明状态，这允许搜索策略通过UCB引导的探索分配计算，同时独立于特定编译器的反馈。

表1：我们的框架与密切相关的推理时搜索方法的架构比较。“编译器使用”指Lean验证如何被纳入搜索过程。
| 方法 | 搜索策略 | 搜索表示 | 生成器接收编译器反馈 | 评估器 | LLM搜索奖励分配 | 回传 |
|---|---|---|---|---|---|---|
| COPRA | 顺序精化 | 形式证明状态 | ✓ 编译器文本 | – | 固定 | – |
| 证明代理 | 树精化 | 证明尝试 | ✓ 编译器文本 | – | 启发式扩展 | 方法特定 |
| BFS+CG | 广度优先搜索 | 自然语言计划 | × (仅标量评估) | ✓ | 广度优先 | – |