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

由于有效导航大型证明搜索空间的困难，使用大语言模型证明形式化定理仍然具有挑战性。现有的树搜索方法要么将详细的编译器错误消息直接输入到生成上下文中，增加搜索过程中的上下文使用，要么采用非标准评估协议来阻止与已建立的基线进行直接比较。我们提出了一个三角色蒙特卡洛树搜索 (MCTS) 框架，该框架将 Lean 4 编译器纯粹视为奖励预言机，使用编译器输出作为 UCB 引导树更新的标量信号，而不将错误内容馈送到生成上下文中。我们的框架将证明搜索分解为三个角色：用于证明尝试的生成器、用于子目标分解的分解器以及用于子目标质量评估的批评者。我们使用标准证明尝试预算（PAB@16 至 PAB@256）的三个证明者模型来评估跨越数学和物理竞赛的 4 个基准（MiniF2F、PutnamBench、LeanPhysBench、PhysLeandata）。我们的方法在 PAB@256 上使用 Goedel-Prover-V2-8B 在 MiniF2F 上实现了 87.1%，并在 PAB@32 上解决了 26/659 PutnamBench 问题，在相同的证明尝试预算下超过了基本采样 18/659。通过对每个已编译证明进行详尽的公理级审计，我们进一步识别了基于搜索的定理证明中的奖励作弊行为：DeepSeek-Prover-V2-7B 在 PutnamBench 上生成证明，该证明在依赖sorryAx的同时通过了编译和标准的sorry-token扫描。审计从 PAB@32 和 PAB@128 的整体证明抽样中删除了 4 个和 8 个此类证明，并从 MCTS 中删除了 11 个和 19 个此类证明。我们不会将这些计数归因于搜索过程；我们报告它们是为了确定内核级审计对于编译器验证的评估是必要的。