Automated Theorem Proving (ATP) is a fundamental AI challenge, requiring machine-verifiable proofs in formal languages like Lean to evaluate reasoning. Reinforcement Learning (RL), especially Group Relative Policy Optimization (GRPO), is a mainstream approach. However, GRPO faces two critical issues in ATP: its relative advantage estimation may conflict with binary verifier feedback under composite rewards, and its static sampling strategy discards batches without valid proofs, causing data waste. Repeated training on mastered problems also wastes computation. To address this, we propose Group Dual-dynamic and Equal-right Advantage Policy Optimization (GDEPO), incorporating three core mechanisms: 1) dynamic additional sampling, resampling ineffective batches until a valid proof is found; 2) equal-right advantage, decoupling the advantage function's sign (correctness) from its magnitude (auxiliary rewards) to ensure stable policy updates while increasing effective computation; and 3) dynamic additional iterations, applying extra gradient steps to initially failed but eventually successful samples to accelerate learning. Experiments on MinF2F-test, MathOlympiadBench, and PutnamBench confirm GDEPO's effectiveness, with ablation studies validating its synergistic components. The method enhances data utilization and optimization efficiency, offering a novel training paradigm for ATP.
Figures & tables
Figure 1: The detailed training procedure of GDEPO: 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 [ 20 ] . A sample is deemed ineffective 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 ineffective but later yielding valid proofs through subsequent sampling, multiple extra gradient update steps
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.
Model
MiniF2F-test
MathOlympiadBench
PutnamBench
Pass Rate (%)
Number of Problem Solved
DeepSeek-Prover-V2-7B
75.6
7
9
DeepSeek-Prover-V2-671B
82.4
50
22
Kimina-Prover-8B
78.3
26
15
Kimina-Prover-72B
84.0
58
24
Goedel-Prover-V2-8B
84.6
60
25
Table 1: Performance Comparison of GDEPO-Prover with Existing SOTA Models and Their Variants Across Model Sizes.
Figure 4: Performance comparison of the same base model trained with GRPO using a single binary reward versus GDEPO employing composite rewards, under varying proportions of challenging samples: (a) performances on MathOlympiadBench; (b) performances on PutnamBench.
Algorithm
MiniF2F-test
MathOlympiad Bench
Putnam Bench
Pass Rate ( % ) ↑
Tokens ↓
Simi. Rate ( % ) ↓
Prob. Solved ↑
Tokens ↓
Simi. Rate ( % ) ↓
Prob. Solved ↑
Tokens ↓
Simi. Rate ( % ) ↓
Goedel-Prover-V2-8B with GRPO (Single Binary Reward)
84.8
9640.89
49.29
61
28692.96
81.84
27
30148.48
85.23
Goedel-Prover-V2-8B with GRPO
83.2
7903.04
46.99
59
14906.10
75.59
24
26215.64
80.76
δ Perf.
-1.6
-1737.85
-2.30
-2
-13786.86
-6.25
-3
-3932.84
-4.47
Goedel-Prover-V2-8B with Equal-Right Advantage
85.3
9008.35
48.22
62
15632.41
77.33
31
28510.36
83.87
δ Perf.
+0.5
-632.54
-1.07
+1
-13060.55
-4.51
+4
-1638.12
-1.36
Table 2: Performance Comparison of the Equal-Right Advantage Module Against GRPO with Single Binary Reward and GRPO with Composite Reward Functions.
Module
MiniF2F-test
MathOlympiadBench
PutnamBench
D.A.S.
E.R.A.
D.A.I.
Pass Rate (%)
Number of Problems Solved
–
–
–
84.6
60
25
✓
–
–
84.9 (+0.3)
63 (+3)
36 (+11)
–
✓
–
85.3 (+0.7)
62 (+2)
31 (+6)
✓
–
✓
85.8 (+1.2)
64 (+4)
41 (+16)
✓
✓
✓
86.2 (+1.6)
65 (+5)
46 (+21)
Table 3: Ablation study results, showing the impact of each component on overall performance.
Figure 5: Relationship between the sign of advantage and the direction of change in trajectory output probabilities.
Group Relative Policy Optimization (GRPO) effectively scales LLM reasoning but incurs prohibitive computational costs due to its extensive group-based sampling requirement. While recent selective data utilization methods can mitigate this overhead, they could induce estimation bias by altering the underlying sampling distribution, compromising theoretical rigor and convergence behavior. To address this limitation, we propose Dynamic Pruning Policy Optimization (DPPO), a framework that enables dynamic pruning while preserving unbiased gradient estimation through importance sampling-based correction. By incorporating mathematically derived rescaling factors, DPPO significantly accelerates GRPO training without altering the optimization objective of the full-batch baseline. Furthermore, to mitigate the data sparsity induced by pruning, we introduce Dense Prompt Packing, a window-based greedy strategy that maximizes valid token density and hardware utilization. Extensive experiments demonstrate that DPPO consistently accelerates training across diverse models and benchmarks. For instance, on Qwen3-4B trained on MATH, DPPO achieves 2.37× training speedup and outperforms GRPO by 3.36% in average accuracy across six mathematical reasoning benchmarks.
Haodong Zhu, Yangyang Ren, Yanjing Li +6
Beihang University · Zhongguancun Academy · Rakuten Singapore +3
Reinforcement learning with verifiable rewards (RLVR), particularly Group Relative Policy Optimization (GRPO), has advanced LLM reasoning. However, GRPO suffers from three credit assignment failures: uniform token-level granularity that ignores heterogeneous informational value, uniform polarity that penalizes correct steps and rewards incorrect ones, and zero-variance collapse that erases outcome-driven gradients. We systematically quantify these failures, revealing highly non-uniform token informativeness, widespread step-level polarity misalignment, and substantial training waste. To address these limitations, we propose Entropy-Progress Aligned GRPO (EP-GRPO), a framework that mines the model's intrinsic information flow for dense, self-supervised guidance. EP-GRPO integrates entropy-gated modulation to prioritize high entropy decision pivots, implicit process signals from policy divergence anchored to outcome advantages for directional token-level feedback without external reward models, and cumulative entropy mapping that enables progress-aligned advantage normalization, naturally maintaining gradient flow under zero reward variance. Extensive experiments on mathematical reasoning benchmarks demonstrate that EP-GRPO achieves superior accuracy and efficiency compared to GRPO and its variants. The code will be available.
Song Yu, Li Li, Wenwen Zhao +1
School of Computer and Information Science, Southwest University, Chongqing 400715, China
Reinforcement learning improves LLM reasoning, but PPO/GRPO typically use fixed clipping and decoding temperature, which makes training brittle and tuning-heavy. We propose Adaptive Group Policy Optimization (AGPO), a critic-free refinement of GRPO that uses group-level statistics to control both update magnitude and exploration. AGPO uses a shared probe-derived statistical state to drive two controllers: (i) adaptive clipping, which sets the trust-region size from reward dispersion and skewness, probe vote entropy, policy entropy, and step-wise KL drift; and (ii) bidirectional adaptive temperature sampling, which heats or cools decoding around a base temperature according to centered uncertainty relative to a running baseline. On nine English and Chinese math/STEM benchmarks, Qwen2.5-14B trained with AGPO outperforms PPO/GRPO under the same generated-token budget, reaching 67.3% on GSM8K and 40.5% on MATH. Gains transfer to Llama-3-8B and Gemma-2-9B, and ablations confirm both modules are complementary. Our implementation is publicly available at https://github.com/wandugu/paper_agpo.
Miaobo Hu, Shuhao Hu, Bokun Wang +5
Institute of Information Engineering, Chinese Academy of Sciences, Beijing 100092, China · School of Cyber Security, University of Chinese Academy of Sciences, Beijing 100049, China · School of Artificial Intelligence, University of Chinese Academy of Sciences, Beijing 100049, China