Elamur Research⌕
☰
home / papers / 2025 / Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening

Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening

Paper · 2025 · Andre Wang He, Daniel Fried and Sean Welleck

Summary

The authors ask whether GRPO, the standard reinforcement learning algorithm for improving LLM reasoning, teaches models to solve new problems or only concentrates probability on solutions the base model already finds. They study this in Lean 4 theorem proving, where a verifier gives exact binary rewards. Starting from DeepSeek-Prover-V1.5-SFT and a training set built from Lean Workbook and miniF2F-valid, they find that standard GRPO raises pass@N for small N. For large N, however, it falls behind simply sampling more from the base model.

They trace this to a "rank bias": GRPO updates mostly strengthen proofs that are already probable and largely ignore rare correct ones. As a fix, they propose an unlikeliness reward that gives extra weight to correct but low-probability samples. They also show that using more PPO epochs per batch helps for a related reason. Combining both changes yields a fully open training pipeline that roughly matches DeepSeek-Prover-V1.5-RL on miniF2F-test. This matters because verifier-backed domains depend on drawing many samples at test time.

Key points

  • Data: About 10K solvable theorems were taken from the ~140K-statement Lean Workbook and combined with the 244 miniF2F-valid problems. From this pool, 200 theorems were held out as an i.i.d. validation set (D_val), leaving 9.6K for training. miniF2F-test was used only for the final evaluation because results on it were noisy.
  • Setup: GRPO was implemented on the verl framework with the Lean REPL providing rewards. Settings were 32 samples per problem, KL coefficient 0.02, learning rate lowered to 1e-6, responses capped at 512 tokens, and one pass over the training data.
  • Diagnosis: Default GRPO improves pass@1 through pass@16 but underperforms the base model at large N (evaluated up to pass@512). This is consistent with Yue et al. (2025).
  • Fixes: The unlikeliness reward up-weights rare correct proofs and increases sample diversity. Raising the number of PPO epochs per batch adds gradient steps on low-likelihood sequences once the likely ones saturate.
  • Results (pass@32 / pass@128):
    • miniF2F-test: the new model scores 48.8% / 50.6%, versus 49.2% / 51.2% for DeepSeek-Prover-V1.5-RL and 47.1% / 49.2% for SFT.
    • D_val: the new model scores 84.3% / 88.8%, versus 84.8% / 87.5% for V1.5-RL.
    • Code is released at github.com/AndreHe02/rewarding-unlikely-release.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Carnegie Mellon UniversityPittsburgh · United States539 works · 179,533 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 works

Cite

Cite as Andre Wang He, Daniel Fried and Sean Welleck. 2025. Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening. Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2025.emnlp-main.1298

@inproceedings{he2025rewarding,
  title = {{Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening}},
  author = {Andre Wang He, Daniel Fried and Sean Welleck},
  booktitle = {Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing},
  year = {2025},
  doi = {10.18653/v1/2025.emnlp-main.1298},
  url = {https://doi.org/10.18653/v1/2025.emnlp-main.1298}
}

References

35 references, 15 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Thomas Anthony, Zheng Tian, and David Barber. 2017. Thinking fast and slow with deep learning and tree search. Preprint, arXiv:1705.08439. find
  2. Yinlam Chow, Guy Tennenholtz, Izzeddin Gur, Vincent Zhuang, Bo Dai, Sridhar Thiagarajan, Craig Boutilier, Rishabh Agarwal, Aviral Kumar, and Aleksandra Faust. 2024. Inference-aware fine-tuning for best-of-n sampling in large language models. Preprint, arXiv:2412.15287. 2025. Deepseek-r1: Incentivizi…
  3. Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. 2024. ABEL: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24. find
  4. Jiewen Hu, Thomas Zhu, and Sean Welleck. 2024. minictx: Neural theorem proving with (long-) contexts. arXiv preprint arXiv:2408.03350. find
  5. Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. 2023. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. Preprint, arXiv:2210.12283.
  6. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. 2022. Hypertree proof search for neural theorem proving. Preprint, arXiv:2205.11491.
  7. Haohan Lin, Zhiqing Sun, Sean Welleck, and Yiming Yang. 2025a. Lean-star: Learning to interleave thinking and proving. Preprint, arXiv:2407.10040. find
  8. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. 2025b. Goedel-prover: A frontier model for open-source automated theorem proving. Preprint, arXiv:2502.07640. find
  9. OpenAI, :, Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, Alex Iftimie, Alex Karpenko, Alex Tachard Passos, Alexander Neitz, Alexander Prokofiev, Alexander Wei, Allison Tam, and 244 others. 2024. Openai o1 sy…
  10. Lawrence C. Paulson. 1994. Isabelle: A Generic Theorem Prover. Springer Verlag. find
  11. Xingyu Dang, Christina Baek, Kaiyue Wen, Zico Kolter, and Aditi Raghunathan. 2025. Weight ensembling improves reasoning in language models. Preprint, arXiv:2504.10478. find
  12. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. 2022. Formal mathematics statement curriculum learning. Preprint, arXiv:2202.01344.
  13. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In CADE. find
  14. Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. Preprint, arXiv:2009.03393.
  15. DeepSeek-AI, Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, and 181 others. find
  16. Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn. 2023. Direct preference optimization: Your language model is secretly a reward model. In Thirty-seventh Conference on Neural Information Processing Systems.
  17. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. 2025. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinfo…
  18. John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. 2017. Proximal policy optimization algorithms. Preprint, arXiv:1707.06347. find
  19. Rulin Shao, Shuyue Stella Li, Rui Xin, Scott Geng, Yiping Wang, Sewoong Oh, Simon Shaolei Du, Nathan Lambert, Sewon Min, Ranjay Krishna, Yulia Tsvetkov, Hannaneh Hajishirzi, Pang Wei Koh, and Luke Zettlemoyer. 2025. Spurious rewards: Rethinking training signals in rlvr. Preprint, arXiv:2506.10947. find
  20. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. 2024. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. Preprint, arXiv:2402.03300.
  21. Guangming Sheng, Chi Zhang, Zilingfeng Ye, Xibin Wu, Wang Zhang, Ru Zhang, Yanghua Peng, Haibin Lin, and Chuan Wu. 2024. Hybridflow: A flexible and efficient rlhf framework. arXiv preprint arXiv: 2409.19256.
  22. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy Lillicrap, Karen Simonyan, and Demis Hassabis. 2017. Mastering chess and shogi by self-play with a general reinforcement learning alg…
  23. Zhiqing Sun. 2024. Gpt-accelera: Simple and efficient pytorch-native transformer training and inference (batched). https://github.com/Edward-Sun/ gpt-accelera. ↗
  24. Yunhao Tang, Kunhao Zheng, Gabriel Synnaeve, and Rémi Munos. 2025. Optimizing language models for inference time objectives using reinforcement learning. Preprint, arXiv:2503.19595. — [arXiv:2503.19595](https://arxiv.org/abs/2503.19595) find
  25. Terence Tao. 2025. Machine-assisted proof. Notices of the American Mathematical Society, 72(1):6–15. find
  26. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, and 21 others. 2025. Kimina-prover preview… find
  27. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Internlm2.5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. Preprint, arXiv:2410.15700. find
  28. Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. 2024. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and…
  29. Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. 2025. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. Preprint, arXiv:2502.03438. find
  30. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. 2024. Formal mathematical reasoning: A new frontier in ai. Preprint, arXiv:2412.16075. find
  31. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Lean workbook: A large-scale lean problem set formalized from natural language math problems. Preprint, arXiv:2406.03847. find
  32. Qiying Yu, Zheng Zhang, Ruofei Zhu, Yufeng Yuan, Xiaochen Zuo, Yu Yue, Tiantian Fan, Gaohong Liu, Lingjun Liu, Xin Liu, Haibin Lin, Zhiqi Lin, Bole Ma, Guangming Sheng, Yuxuan Tong, Chi Zhang, Mofan Zhang, Wang Zhang, Hang Zhu, and 16 others. 2025. Dapo: An open-source llm reinforcement learning sys…
  33. Yang Yue, Zhiqi Chen, Rui Lu, Andrew Zhao, Zhaokai Wang, Yang Yue, Shiji Song, and Gao Huang. 2025. Does reinforcement learning really incentivize reasoning capacity in llms beyond the base model? Preprint, arXiv:2504.13837.
  34. Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. 2025. Leanabell-prover: Post-training scaling in formal reasoning. Preprint, arXiv:2504.06122. find
  35. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2021. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/he-2025-rewarding-unlikely-lifting-grpo-beyond/