GDEPO提升自动定理证明中的数据利用率，解决奖励冲突与无效样本浪费问题。
GDEPO: Group Dual-dynamic and Equal-right Advantage Policy Optimization with Enhanced Training Data Utilization for Sample-Constrained Reinforcement Learning
- 动态重采样+等权优势分解，避免验证失败导致的数据浪费
- 在三个难度递增的数据集上，胜率较GRPO提升12.7%~23.4%
- 适合资源受限的强化学习场景，尤其对证明类任务有显著优化
自动定理证明（ATP）是人工智能领域的基础挑战，需在如Lean等形式语言中构建机器可验证的证明以评估AI推理能力。强化学习（RL），特别是高性能的组相对策略优化（GRPO）算法，已成为主流方法。然而，在ATP场景中，GRPO面临两大关键问题：复合奖励下相对优势估计与形式验证器的二值反馈存在冲突；静态采样策略若某批次无有效证明，则整批数据被丢弃，导致零贡献且严重浪费。为此，我们提出组双动态均权优势策略优化（GDEPO），包含三项核心机制：1）动态额外采样，对无效批次持续重采样直至发现有效证明；2）等权优势，解耦优势函数符号（基于正确性）与幅值（由辅助奖励调节），确保策略更新稳定准确；3）动态额外迭代，对初始失败但最终成功的样本追加梯度步数，加速困难案例的学习。在三个难度递增的数据集（MinF2F-test、MathOlympiadBench、PutnamBench）上的实验验证了GDEPO的有效性，消融研究证实各组件协同必要性。该方法显著提升数据利用率与优化效率，为ATP提供新型训练范式。
原文摘要 · Abstract (English)
Automated Theorem Proving (ATP) represents a fundamental challenge in Artificial Intelligence (AI), requiring the construction of machine-verifiable proofs in formal languages such as Lean to evaluate AI reasoning capabilities. Reinforcement learning (RL), particularly the high-performance Group Relative Policy Optimization (GRPO) algorithm, has emerged as a mainstream approach for this task. However, in ATP scenarios, GRPO faces two critical issues: when composite rewards are used, its relative advantage estimation may conflict with the binary feedback from the formal verifier; meanwhile, its static sampling strategy may discard entire batches of data if no valid proof is found, resulting in zero contribution to model updates and significant data waste. To address these limitations, we propose Group Dual-dynamic and Equal-right-advantage Policy Optimization (GDEPO), a method incorporating three core mechanisms: 1) dynamic additional sampling, which resamples invalid batches until a valid proof is discovered; 2) equal-right advantage, decoupling the sign of the advantage function (based on correctness) from its magnitude (modulated by auxiliary rewards) to ensure stable and correct policy updates; and 3) dynamic additional iterations, applying extra gradient steps to initially failed but eventually successful samples to accelerate learning on challenging cases. Experiments conducted on three datasets of varying difficulty (MinF2F-test, MathOlympiadBench, PutnamBench) confirm the effectiveness of GDEPO, while ablation studies validate the necessity of its synergistic components. The proposed method enhances data utilization and optimization efficiency, offering a novel training paradigm for ATP.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。