沙丘社区
论文

GDEPO：面向样本受限强化学习、提升训练数据利用率的组双重动态与等权优势策略优化

GDEPO: Group Dual-dynamic and Equal-right-advantage Policy Optimization with Enhanced Training Data Utilization for Sample-Constrained Reinforcement Learning

Zhengqing Yan, Xinyang Liu, Yi Zhang, Fan Guo, Yao Liu, Junchen Wan, Kang Song
模型训练强化学习RLVR

摘要

自动定理证明（ATP）是人工智能（AI）中的一项基础性挑战，需要在Lean等形式语言中构造机器可验证的证明，以评估AI的推理能力。强化学习（RL），尤其是高性能的组相对策略优化（GRPO）算法，已成为该任务的主流方法。然而，在ATP场景中，GRPO面临两个关键问题：当使用复合奖励时，其相对优势估计可能与形式验证器的二值反馈相冲突；同时，其静态采样策略可能在未找到有效证明时丢弃整批数据，导致对模型更新零贡献并造成显著的数据浪费。为解决这些局限，我们提出组双重动态与等权优势策略优化（GDEPO），该方法包含三个核心机制：1）动态额外采样，对无效批次重采样，直到发现有效证明；2）等权优势，将优势函数的符号（基于正确性）与其幅值（由辅助奖励调制）解耦，以确保稳定且正确的策略更新；3）动态额外迭代，对最初失败但最终成功的样本施加额外的梯度步，以加速在具有挑战性案例上的学习。在三个不同难度数据集（MinF2F-test、MathOlympiadBench、PutnamBench）上进行的实验证实了GDEPO的有效性，消融研究验证了其各组件协同的必要性。所提方法提升了数据利用率与优化效率，为ATP提供了一种新的训练范式。

GDEPO：面向样本受限强化学习、提升训练数据利用率的组双重动态与等权优势策略优化 配图
图 1：LLM 充当自动定理证明器：接收包含 G 个相同问题实例的标准化提示，生成整证明补全，并通过 Lean4 服务器 [20] 进行验证。如果组内所有输出都不正确，则该样本被判为无效。对于同一提示，采样持续进行至最大尝试次数，直到获得至少一个正确证明。当组内准确率低于预定阈值时，验证器给出的正确性反馈为优势函数贡献一个符号项，而其他信号决定其大小。对于最初被判为无效、但随后通过继续采样得到有效证明的样本，会执行一次额外的反向传播来精炼模型参数。