FormalRewardBench：形式化定理证明奖励模型基准

近期的神经定理证明器采用可验证奖励强化学习（RLVR），由证明助手提供二元正确性信号。虽然可验证奖励廉价、可扩展且不存在奖励破解问题，但其贡献归因稀疏：在部分进展得不到奖励的困难问题上，模型无法获得学习信号。这促使人们研究能够超越二元验证、评估证明质量的习得型奖励模型。然而，比较奖励模型颇具挑战，因为通常需要昂贵的强化学习训练消融。为此，我们提出FormalRewardBench，首个用于评估Lean 4形式化定理证明中奖励模型的基准。该基准包含250个偏好对，其中正确证明与通过五种专家设计的错误注入策略生成的错误变体配对：强迫性错误、最小单点变动、冗长的错误证明、自然语言论证以及Python代码注入。我们评估了前沿LLM（如Claude Opus 4.5）、评审型LLM（如CompassJudger-1-14B）、通用LLM（如Qwen2.5-72B-Instruct）以及专用定理证明模型（如DeepSeek-Prover-V2-7B）。结果显示，前沿LLM表现最佳（59.8%），而专用定理证明模型表现最差（24.4%），表明定理证明能力并不能迁移到证明评估上。我们对各类错误注入机制提供了进一步洞见，凸显了大多数注入机制的挑战性。我们公开发布FormalRewardBench，以鼓励更多关于形式化数学奖励模型开发的研究。