arXiv: DeepSeek@Zeynel A. Uluşan, Burak S. Akbudak, Can S. Erer, Gözde Gül Şahin
45
推荐理由：该基准填补了形式化定理证明中奖励模型评估工具的空白，揭示专用定理证明模型在评估任务上的不足，为改进RL训练信号提供了明确方向。
全部 AI 动态
AI 相关资讯全量信息流
5月12日
19:11
近期神经定理证明器使用基于可验证奖励的强化学习（RLVR），但面临稀疏奖励问题：困难问题中部分进展无法获得信号。为此，研究者提出学习奖励模型以评估证明质量，但比较不同奖励模型通常需要昂贵的RL训练消融实验。FormalRewardBench是首个专门评估Lean 4形式化定理证明中奖励模型的基准，包含250个偏好对，每个正确证明通过5种专家设计的错误注入策略生成错误变体。评估包括前沿LLM（如Claude Opus 4.5）、判别型LLM（如CompassJudger-1-14B）、通用LLM（如Qwen2.5-72B-Instruct）以及专用定理证明模型（如DeepSeek-Prover-V2-7B）。结果显示前沿LLM表现最佳（59.8%），而专用定理证明器表现最差（24.4%），表明定理证明能力并未迁移到证明评估任务。