PaperlayerView exact revision on arXiv

Source-linked AI summary

Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening

Andre He, Daniel Fried, Sean Welleck

arXiv:2506.02355v2cs.LG

TL;DR

The paper asks whether GRPO develops new reasoning solutions or mainly sharpens probability around solutions already present in the base model. In formal theorem proving, it analyzes GRPO’s rank bias, introduces unlikeliness reward and a complementary PPO-epoch adjustment, and reports stronger pass@N with an open pipeline competitive with DeepSeek-Prover-V1.5-RL.

  • Problem

    The paper investigates whether GRPO merely sharpens the base model’s distribution around already solvable problems rather than improving access to unlikely correct solutions.

  • Method

    The paper analyzes rank bias in GRPO for formal theorem proving and introduces unlikeliness reward plus PPO-epoch tuning to reinforce low-probability correct solutions.

  • Results

    The revised recipe improves pass@N across a range of N, outperforms standard expert iteration, and produces an open pipeline competitive with DeepSeek-Prover-V1.5-RL.

  • Takeaways & Limitations

    Improving multi-sample theorem proving requires addressing GRPO’s tendency to neglect rare but correct solutions.

  • Takeaways & Limitations

    Whether amplifying rare but correct solutions similarly improves exploration and generalization in reasoning models remains future work.

Abstract

from arXiv · show

Reinforcement learning is emerging as a primary driver for improving language model reasoning capabilities. A fundamental question is whether current reinforcement learning algorithms -- such as Group Relative Policy Optimization (GRPO), the de facto standard algorithm used to improve language model reasoning -- merely sharpen the base model's distribution around problems it can already solve. We investigate this question in the context of formal theorem proving, which has access to a perfect verifier. We identify a degenerate rank bias in GRPO in which highly probable trajectories are reinforced and rare ones are neglected. This results in distribution sharpening: the model can solve some problems with fewer samples, but underperforms simply sampling more solutions from the original model. To overcome GRPO's rank bias we introduce unlikeliness reward, a simple method for explicitly up-weighting rare but correct solutions. We show that unlikeliness reward mitigates rank bias and improves pass@$N$ across a large range of $N$ in both synthetic and real theorem proving settings. We also uncover an unexpected link between rank bias and a seemingly mundane hyperparameter -- the number of updates per batch -- that leads to a second, complementary mitigation. We combine our insights into a revised GRPO training recipe for formal theorem proving, yielding an open pipeline that achieves competitive performance to DeepSeek-Prover-V1.5-RL on the miniF2F-test benchmark. We release our implementation at https://github.com/AndreHe02/rewarding-unlikely-release

1 Introduction

The paper studies whether GRPO improves reasoning beyond concentrating probability on already likely solutions. It identifies rank bias and proposes unlikeliness reward plus PPO-epoch tuning to improve multi-sample theorem-proving performance.

  • Formal theorem proving provides an ideal RL testbed because Lean-like systems verify mathematical proofs step-by-step and reject spurious solutions.
  • GRPO can improve single-sample accuracy while failing to improve, or even impairing, pass@N at larger N.This limits settings where many candidates can be sampled and automatically verified.
  • GRPO exhibits rank bias by reinforcing high-likelihood correct responses while neglecting rare correct ones, reducing diversity and degrading multi-sample performance.
  • Unlikeliness reward up-weights less likely correct outputs, increasing output diversity and pass@N across a range of N values.
  • Increasing PPO epochs per batch provides a complementary mitigation by adding gradient steps that amplify learning on low-likelihood sequences after high-likelihood sequences saturate.
  • The revised training recipe substantially improves pass@N across N values, outperforms standard expert iteration, and yields an open Lean pipeline competitive with DeepSeek-Prover-V1.5-RL.

2 Problem Setup

The paper formulates formal theorem proving as training a prover model against a binary Lean verifier and evaluates performance through repeated independent proof sampling. GRPO supplies the reinforcement-learning foundation for these experiments.

  • The task is to fine-tune a language model to generate valid Lean proofs for theorem statements in a dataset.
  • Lean acts as a fully automated verifier that returns reward 1 exactly when a candidate proof proves the theorem.
  • pass@N measures the probability that at least one of N independently sampled proof attempts succeeds.The metric matches the use case of generating and verifying many candidates per theorem.
  • The experiments use GRPO, an extension of PPO that omits a critic and samples groups of outputs from the current policy.
  • GRPO computes advantages by normalizing rewards within each sampled group rather than subtracting a critic-predicted baseline.
  • When all or none of a group’s samples solve the problem, GRPO advantages are zero and no model-parameter gradient is produced except from the KL term.

3 Does GRPO Improve Pass@N?

On formal theorem proving, GRPO improves performance at small sample budgets but can degrade pass@N at larger N. The analysis attributes this pattern to insufficient uplift of low-probability correct solutions and a rank bias toward already likely responses.

  • 3.1 Dataset: The study applies GRPO to Lean theorem proving using a curated solvable dataset, miniF2F-valid, and an IID held-out validation set.The combined data leave 9.6K training theorems and 200 validation theorems; miniF2F-test is reserved for final large-scale experiments.
  • 3.3 GRPO Fails to Improve Pass@N: GRPO substantially improves pass@1 through pass@16 on Dval, but gains diminish at larger N and can fall below the base model.The evaluation extends to pass@512.
  • 3.4 Can RL Optimize Pass@N?: Improving pass@N at large N requires increasing the probability of correct solutions whose initial probability is approximately 1/N.The toy analysis predicts small gains at pass@512 when initial p0 is large, but negligible pass@1 gains when p0 is small.
  • 3.5 Does GRPO Reinforce Unlikely Solutions?: The empirical analysis compares initial and final GRPO probabilities for training solutions, using within-group rank and binary uplift as a more stable proxy than raw probability ratios.Raw ratios contain extreme outliers and vary widely across problems.
  • 3.5 Does GRPO Reinforce Unlikely Solutions?: GRPO exhibits rank bias: it more often uplifts already high-probability correct solutions while rarely uplifting low-probability correct samples.The latter samples are identified as especially important for improving pass@N at large N.

4 Improving GRPO for Multi-Sample Performance

The paper introduces unlikeliness reward to counteract GRPO’s empirical rank bias, and identifies additional PPO epochs as a complementary mitigation for multi-sample performance.

  • Motivation: GRPO empirically reinforces high-probability correct solutions while rarely reinforcing low-probability correct solutions.This rank bias is attributed to optimizer biases rather than the GRPO loss itself.
  • 4.1 Unlikeliness Reward: Unlikeliness reward directly counteracts rank bias by up-weighting correct outputs that are less likely than other group samples.The reward modification discourages reinforcing already high-probability solutions.
  • 4.1 Unlikeliness Reward: Incorrect solutions remain unaffected by the unlikeliness perturbation, and βrank is fixed at 0.25 in the experiments.Samples with zero advantage are skipped before perturbation, preserving the verifier reward’s optimization direction.
  • 4.2 Effects of PPO Epochs: Increasing ppo-epochs mitigates rank bias because early updates saturate high-rank solutions, leaving later updates to emphasize still-unclipped low-rank samples.This provides a complementary optimization-based mitigation to unlikeliness reward.
  • 4.2 Effects of PPO Epochs: Increasing ppo-epochs makes training substantially slower and potentially unstable, so the paper prefers unlikeliness reward as the more direct and efficient solution.The trade-off limits the practical appeal of using additional optimization steps alone.

5 Experiments

Experiments show that unlikeliness reward and additional PPO epochs improve large-N pass@N, mitigate rank bias, and increase proof diversity, with PPO epochs carrying a stability and runtime cost.

  • 5.1 Results: Pass@N: Unlikeliness reward substantially improves pass@N at large N, with a minor tradeoff in pass@1 and pass@2.Additional PPO epochs also improve pass@N but significantly increase training time.
  • 5.1 Results: Pass@N: All GRPO variants outperform the static model on training problems, with GRPO-Unlikeliness-2 solving the most problems.Training runs for one epoch, so each example is effectively unseen when sampled.
  • 5.2 Analysis: Rank Bias: GRPO-Unlikeliness-2 reverses the original uplift pattern and becomes more likely to reinforce low-probability solutions.GRPO-Epochs-2 and GRPO-Epochs-3 retain the bias but increase overall reinforcement enough to uplift low-probability solutions.
  • 5.3 Analysis: Sample Diversity: GRPO-Unlikeliness-2 initially reduces proof diversity but later recovers, unlike variants whose diversity declines monotonically.The passage suggests that penalizing dominant solutions allows low-probability correct solutions to resurface.
  • 5.3 Analysis: Sample Diversity: Higher PPO epochs consistently increase sample diversity until ppo-epochs = 4, where training becomes unstable.The paper links this diversity increase to indirect amplification of rare solutions and mitigation of distribution sharpening.
  • 5.4 Large-Scale Experiment: GRPO-Unlikeliness-2 achieves competitive results with DeepSeek-Prover-V1.5-RL on MiniF2F-test and Dval.The large-scale experiment trains on an 11k-theorem Lean-Workbook subset excluding Dval theorems.

6 Related Work

Related work spans automated theorem proving, expert iteration, reinforcement learning, and multi-sample performance; this paper positions itself as the first to attribute poor multi-sample performance to failure to reinforce low-probability samples.

  • Automated Theorem Proving: Automated theorem provers generate either individual proof steps or complete proofs using formal systems such as Lean and Isabelle.Full-proof models reduce interaction overhead by producing complete proofs autoregressively.
  • Automated Theorem Proving: Recent theorem-proving research explores inference-time proof discovery, informal reasoning, novel test-time context, and long chain-of-thought strategies.These directions complement the paper’s focus on reinforcement-learning posttraining.
  • Expert Iteration for Theorem Proving: Expert iteration alternates between search and learning and has become a dominant theorem-proving paradigm.Recent work applies best-first search and related search-based data-collection methods.
  • RL for Theorem Proving: GRPO has been applied to theorem proving with theorem statements and verifier rewards, while other work adapts AlphaZero and direct preference optimization.The paper studies a less explored use of general RL algorithms relative to expert iteration.
  • RL for Multi-Sample Performance: Prior work reports that verifier-reward RL improves pass@N at small N but can deteriorate it at large N by concentrating outputs around existing correct answers.The paper contrasts this literature with its attribution to insufficient reinforcement of low-probability samples.

7 Conclusion

The paper identifies GRPO’s preference for already likely solutions as a source of poor large-N performance and proposes unlikeliness reward to shift reinforcement toward rare correct samples.

  • Conclusion: The study connects degraded pass@N at large N with GRPO’s failure to reinforce low-probability solutions.The analysis focuses on formal theorem proving.
  • Conclusion: Unlikeliness reward shifts reinforcement toward rare samples, improving large-N pass@N and sample diversity compared with existing methods.The revised recipe also produces a model competitive with DeepSeek-Prover-V1.5-RL and is released publicly.

Limitations

The paper leaves open whether rare-solution amplification generalizes from formal theorem proving to more diverse reasoning settings. It also identifies inference-aware reinforcement learning as an unresolved direction.

  • Limitations: Developing efficient inference-aware reinforcement learning algorithms remains an open direction.The paper also points to directly optimizing performance under specific inference-time algorithms.
  • Limitations: Future work should test whether amplifying rare but correct solutions improves exploration and generalization in reasoning models.The authors specifically note that planning, backtracking, and self-critique may change GRPO behavior.
  • A.1 Environment Design: The diagnostic toy environment uses a fully observable 10-dimensional state space and 128 discrete actions with hidden fixed action vectors.Its binary reward is threshold-based, with τ varied during evaluation to simulate different difficulty levels.

A.3 GRPO Training and Diagnosis

The toy diagnosis evaluates GRPO across sampling budgets and difficulty levels, revealing rank bias and deteriorating multi-sample performance. Unlikeliness reward restores diversity and improves difficult-setting pass@32.

  • A.3 GRPO Training and Diagnosis: GRPO is trained for 200 steps and evaluated at pass@N values of 1, 4, 8, 16, and 32.At training difficulty τ = 1.0, initial evaluations suggest improved pass rates across all tested N.
  • A.3 GRPO Training and Diagnosis: GRPO preferentially reinforces already high-probability solutions, exposing a rank bias.This diagnosis links the training behavior to the observed multi-sample degradation.
  • A.3 GRPO Training and Diagnosis: Unlikeliness reward makes uplift rates more uniform by neutralizing GRPO’s rank bias.It changes how the toy training procedure reinforces less likely solutions.
  • A.3 GRPO Training and Diagnosis: At τ = 5.0, unlikeliness reward substantially improves pass@32 while default GRPO declines to near chance levels.The comparison is specific to the difficult evaluation setting.
  • A.3 GRPO Training and Diagnosis: Unlikeliness reward substantially increases the entropy of the predicted action distribution.The entropy change is consistent with a less concentrated action distribution in the toy environment.

B Training Setup

The main experiments use multi-GPU Lean infrastructure and measure theorem-proving performance with chunked pass@n estimates from large response samples. Policy-update time increases with PPO epochs.

  • B Training Setup: The main experiments use 4 NVIDIA L40S GPUs, 500GB of RAM, and 48–64 CPUs for parallel Lean REPL instances.This infrastructure supports the theorem-proving experiments described in the paper.
  • B Training Setup: Each training step comprises sequence generation, proof verification, and policy-model updates.Generation and verification take approximately 120 seconds per batch of 16 problems and 32 attempts.
  • B Training Setup: Policy-update time rises from approximately 70 seconds with 1 PPO epoch to approximately 210 seconds with 3 epochs.The reported times are approximately 70, 140, and 210 seconds for 1, 2, and 3 epochs, respectively.
  • B Training Setup: Pass@n evaluation generates Nmax = 512 responses per problem and averages binary chunk rewards across trials.Each chunk is rewarded according to whether it contains at least one valid proof; pass@512 has one trial.

D Effects of KL Penalty

The paper increases KL regularization to preserve the base distribution, but treats it as supportive rather than sufficient. The reported figures compare GRPO variants and their uplift rates.

  • D Effects of KL Penalty: Figure 8 reports performance for GRPO variants including GRPO-High-KL on Dval.Some variants are omitted for readability.
  • D Effects of KL Penalty: Figure 9 reports uplift rates for GRPO variants including GRPO-High-KL.The figure is intended to compare how the variants uplift sampled solutions.
  • D Effects of KL Penalty: Increasing the KL loss coefficient to 0.1 is used to better preserve the original distribution.This modification is motivated by evidence that theorem-prover pass rates can keep improving with increased sampling.
  • D Effects of KL Penalty: The KL-only control prevents pass@N deterioration but does not substantially improve over the base model.The authors attribute this to RL updates still failing to uplift low-rank samples and therefore treat KL regularization as supporting.
Loading 2506.02355v2…