arXiv cs.AI· Zhengqing Yan, Fan Guo, Xinyang Liu, Yi Zhang, Yao Liu, Qi Liu, Jihao Huang, Kang Song·· 3 天前AI 评分20
GDEPO：面向样本高效强化学习的组双动态与等权优势策略优化
GDEPO: Group Dual-dynamic and Equal-right Advantage Policy Optimization for Sample-Efficient Reinforcement Learning
AI 导读
针对 GRPO 在自动定理证明中相对优势估计与二元验证反馈冲突、静态采样丢弃无效批次造成数据浪费的问题，研究者提出 GDEPO，通过动态补充采样、等权优势（解耦优势函数的符号与幅度）和动态额外迭代三项机制提升数据利用率。在 MinF2F-test、MathOlympiadBench 和 PutnamBench 上的实验验证了其有效性，消融研究确认各组件协同作用。
正文 · AI 翻译
摘要：自动定理证明（ATP）是一项基础性的人工智能挑战，要求在 Lean 等形式化语言中提供机器可验证的证明来评估推理能力。强化学习（RL），尤其是组相对策略优化（GRPO），是主流方法。然而，GRPO 在 ATP 中面临两个关键问题：在复合奖励下，其相对优势估计可能与二元验证器反馈相冲突；其静态采样策略会丢弃没有有效证明的批次，造成数据浪费。对已掌握问题的重复训练也会浪费计算资源。为解决这一问题，我们提出了组双动态与等权优势策略优化（GDEPO），包含三个核心机制：1）动态额外采样，对无效批次重新采样，直到找到有效证明；2）等权优势，将优势函数的符号（正确性）与其幅度（辅助奖励）解耦，以确保策略更新稳定，同时增加有效计算量；3）动态额外迭代，对最初失败但最终成功的样本施加额外的梯度步骤，以加速学习。在 MinF2F-test、MathOlympiadBench 和 PutnamBench 上的实验证实了 GDEPO 的有效性，消融研究验证了其各组件之间的协同作用。该方法提高了数据利用率和优化效率，为 ATP 提供了一种新的训练范式。
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2601.06795 [cs.AI] |
| （或 arXiv:2601.06795v4 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2601.06795 arXiv 颁发的 DOI，通过 DataCite |
提交历史
来自：Zhengqing Yan [查看电子邮件]
[v1]
2026年1月11日星期日 07:34:41 UTC（2,146 KB）
[v2]
2026年1月21日星期三 02:58:47 UTC（2,146 KB）
[v3]
2026年1月22日星期四 14:58:18 UTC（2,146 KB）
[v4]
2026年10月12日星期一 13:47:23 UTC（2,103 KB）
来源：arXiv cs.AI · arxiv.org