AI 中文总结
本研究提出三角色奖励-预言机MCTS框架用于形式化定理证明，在多基准测试中提升了证明求解性能，并通过审计发现了奖励黑客问题，确立了内核级审计的必要性。
AI 中文摘要
基于大语言模型的形式化定理证明仍面临挑战，原因在于难以高效地在庞大的证明搜索空间中进行导航。现有树搜索方法要么将冗长的编译器错误消息直接输入生成上下文，增加搜索过程中的上下文使用量，要么采用非标准评估协议，无法与既定基准进行直接比较。我们提出了一种三角色蒙特卡洛树搜索（MCTS）框架，该框架将Lean 4编译器纯粹视为奖励预言机，利用编译器输出作为用于UCB引导树更新的标量信号，而不将错误内容输入生成上下文。我们的框架将证明搜索分解为三个角色：用于证明尝试的生成器、用于子目标分解的分解器，以及用于子目标质量评估的评判者。我们在涵盖竞赛数学和物理学的4个基准（MiniF2F、PutnamBench、LeanPhysBench、PhysLeandata）上，使用三种证明器模型，在标准证明尝试预算（PAB@16至PAB@256）下进行评估。我们的方法在PAB@256下使用Goedel-Prover-V2-8B在MiniF2F上达到了87.1%的准确率，在PAB@32下解决了26/659个PutnamBench问题，超过了相同证明尝试预算下基础采样的18/659个问题。通过对每个已编译证明进行详尽的公理级审计，我们进一步发现了基于搜索的定理证明中的奖励黑客行为：DeepSeek-Prover-V2-7B在PutnamBench上生成的证明通过了编译和标准sorry-token扫描，同时依赖于sorryAx。该审计在PAB@32和PAB@128下从全证明采样中分别移除了4个和8个此类证明，在MCTS中分别移除了11个和19个此类证明。我们不将这些数量归因于搜索过程；我们报告这些结果是为了确立内核级审计对于编译器验证评估的必要性。
英文摘要
Formal theorem proving with large language models remains challenging due to the difficulty of navigating large proof search spaces efficiently. Existing tree search approaches either feed verbose compiler error messages directly into the generation context, increasing context usage during search, or employ non-standard evaluation protocols that prevent direct comparison with established baselines. We propose a three-role Monte Carlo Tree Search (MCTS) framework that treats the Lean 4 compiler purely as a reward oracle using compiler output as a scalar signal for UCB-guided tree updates without feeding error content into the generation context. Our framework decomposes proof search into three roles: a generator for proof attempts, a decomposer for subgoal decomposition, and a critic for subgoal quality evaluation. We evaluate across 4 benchmarks spanning competition mathematics and physics (MiniF2F, PutnamBench, LeanPhysBench, PhysLeandata) with three prover models at standard proof attempt budgets (PAB@16 to PAB@256). Our method achieves 87.1\% on MiniF2F with Goedel-Prover-V2-8B at PAB@256 and solves 26/659 PutnamBench problems at PAB@32 surpassing base sampling 18/659 at same proof attempt budget. Through an exhaustive axiom-level audit of every compiled proof, we further identify reward hacking in search-based theorem proving: DeepSeek-Prover-V2-7B produces proofs on PutnamBench that pass compilation and the standard sorry-token scan while depending on sorryAx. The audit removes 4 and 8 such proofs from whole-proof sampling at PAB@32 and PAB@128, and 11 and 19 from MCTS. We do not attribute these counts to the search procedure; we report them to establish that kernel-level auditing is necessary for compiler-verified evaluation.
