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

TL;DR

This work tackles the inefficiencies of reinforcement learning in automated theorem proving by identifying three core bottlenecks of GRPO: misalignment between composite rewards and binary verifier feedback, poor data utilization from batches with mostly incorrect trajectories, and uniform update schedules. It introduces GDEPO, a three-pronged framework featuring dynamic sampling, equal-right advantage, and dynamic iterations to maximize data value and accelerate learning on hard-but-solvable proofs. Empirical results across MiniF2F-test, MathOlympiadBench, and PutnamBench show substantial improvements over state-of-the-art baselines, including an 84% gain on PutnamBench, with ablations confirming the synergy of all components. The approach advances ATP by leveraging precise verifier signals to guide adaptive exploration and targeted optimization, offering a practical path toward more efficient and robust formal reasoning with LLMs.

Abstract

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.

Figures (5)

• Figure 1: LLMs serve as auto-theorem provers by receiving a standardized prompt containing $G$ identical problem instances, generating whole-proof completions, and verifying them through a Lean4 server santos2025kimina. A sample is deemed invalid if all outputs in the group are incorrect. For the same prompt, sampling continues up to a maximum number of attempts until at least one correct proof is obtained. When the within-group accuracy falls below a predefined threshold, the correctness feedback from the verifier contributes a sign term to the advantage function, while other signals determine its magnitude. For samples initially classified as invalid but later yielding valid proofs through subsequent sampling, an additional backward pass is performed to refine the model parameters.
• Figure 2: Overall Architecture of the GDEPO Framework and Its Comparison with Conventional Paradigms.
• Figure 3: Overall Training Framework of GDEPO in Comparison with GRPO.
• Figure 4: Dae. Ad quatur autat ut porepel itemoles dolor autem fuga. Bus quia con nessunti as remo di quatus non perum que nimus. (a) Case I. (b) Case II.
• Figure 5: Relationship Between the Sign of Advantage and the Direction of Change in Trajectory Output Probabilitys.