Pith. sign in

REVIEW 4 major objections 5 minor 2 cited by

Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read GRPO systematically neglects rare correct proofs; a rank-aware reward restores large-N sampling gains.

desk verdict A solid, practical paper: GRPO's rank bias is a real phenomenon worth addressing, and the unlikeliness reward works; the main curves need error bars and the diagnostic metric needs bin counts. read the letter →

arxiv 2506.02355 v2 pith:EOQZGMUF submitted 2025-06-03 cs.LG

Andre He , Daniel Fried , Sean Welleck This is my paper
classification cs.LG
keywords reinforcementlearningGRPOrankbiasdistributionsharpeningunlikelinessrewardpass@NformaltheoremprovingLean
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper asks whether GRPO, the default reinforcement learning algorithm for improving language-model reasoning, merely sharpens the model around problems it can already solve. In formal theorem proving, where a verifier gives exact reward, the authors find that GRPO boosts single-sample and small-N accuracy but ends up worse than the base model at large N: it reinforces already likely proofs while neglecting rare correct ones. They call this rank bias and introduce an unlikeliness reward that discounts correct proofs by their probability rank within the sampled group, upweighting rare but correct proofs. This lifts pass@N across a wide range of N, preserves sample diversity, and reaches performance comparable to the paper's open RL-trained prover baseline on miniF2F-test. They also show that increasing the number of PPO updates per batch is a second, complementary way to mitigate the same bias.

What carries the argument

The carrying object is the unlikeliness reward, a reward shaping term applied to GRPO's group-relative advantage: each correct proof's reward is multiplied by a factor that decreases linearly with its probability rank within the group, so rare correct proofs receive a relatively larger share of the advantage. The rank is defined under the sampling policy $\pi_{\theta_{\text{old}}}$, and the strength is fixed by $\beta_{\mathrm{rank}}=0.25$. It does the work of counteracting rank bias without changing the GRPO objective itself. A second mechanism is the clipping in the importance ratio: with more PPO epochs per batch, high-probability samples hit the clip threshold first, forcing later gradient steps onto unclipped low-probability samples.

What would settle it

Run the Appendix A toy environment with GRPO across at least 16 random seeds and recompute the uplift-rate curve using exact action probabilities grouped into deciles rather than within-group ranks; if the curve is flat or non-monotone, or if it becomes flat under exact probabilities, the rank-bias claim does not survive.

Watch

Extended reading notes

Core claim

The central discovery is a degenerate bias in how GRPO assigns group-relative advantages: correct samples that already have high probability under the current policy receive most of the reinforcement, while correct samples in the long tail — exactly the ones that matter for pass@N at large N — are almost never uplifted. The paper verifies this by measuring an uplift rate: within groups of 32 proofs ranked by their old-policy probability, the chance that GRPO increases a proof's probability rises monotonically with rank, so the rarest correct proofs are rarely reinforced. This makes GRPO sharpen the distribution instead of broadening it. The proposed fix changes the reward to $r_i = R(x, y_i)\left(1 - \beta_{\mathrm{rank}}\frac{G - \mathrm{rank}(y_i)}{G}\right)$ with $\beta_{\mathrm{rank}}=0.25$, where rank $0$ is the highest-probability proof, so already-likely correct answers are discounted and rare correct answers gain relative advantage. GRPO training with this reward improves pass@N at large N, avoids monotone diversity collapse, and stays competitive with the paper's open RL-trained prover baseline. A second finding is that increasing the number of PPO epochs per batch weakens rank bias, because high-probability samples saturate at the clipping bound and later gradient steps fall on low-probability samples.

Load-bearing premise

The rank-bias diagnosis assumes that ranking a proof within a group of 32 by its old-model probability is a faithful proxy for its true probability, and that the binary 'did GRPO increase this probability' indicator is not dominated by noise, so the monotone uplift pattern in Figure 4 is genuine signal rather than a measurement artifact.

Editorial extensions

If this is right

  • Under default GRPO, gains in pass@1 can come at the cost of large-N coverage, so evaluations of reasoning RL should report pass@N curves across a wide range of N rather than only pass@1 or pass@32.
  • The unlikeliness reward preserves sample diversity during training, so the policy retains a broader set of strategies instead of collapsing onto a few popular proofs.
  • Increasing the number of PPO epochs per batch is a second, slower mitigation for rank bias and can be combined with the unlikeliness reward.
  • On the held-out validation set and on miniF2F-test, the revised recipe reaches pass@128 comparable to the paper's open RL-trained prover baseline.
  • For formal theorem proving, where verifying many samples is cheap, the recipe makes RL training compatible with the natural large-N test-time regime.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: rank bias should appear in any outcome-reward RL that normalizes advantages within a group and clips importance ratios, not only in theorem proving; a cheap test would compare pass@128 of an RL-trained model against base-model sampling on a code or math benchmark.
  • Editorial inference: the unlikeliness reward's penalty depends on group size $G$, so the fixed coefficient $\beta_{\mathrm{rank}}=0.25$ may need recalibration when $G$ changes; sweeping $\beta_{\mathrm{rank}}$ as a function of $G$ is a testable extension.
  • Editorial inference: the PPO-epoch effect acts through clipping saturation, so a more compute-efficient implementation might apply a gradient mask to skip samples already at the clip bound, isolating the same mechanism without extra epochs.
  • Editorial inference: because the paper studies a perfect verifier, transfer to settings with learned reward models is not automatic; directly penalizing high-probability responses could interact with reward-model bias or reward hacking.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper studies GRPO for formal theorem proving in Lean. It observes that GRPO improves pass@N only for small N and underperforms simply sampling from the base model at large N, a phenomenon it attributes to 'rank bias': GRPO preferentially reinforces high-probability correct samples while neglecting rare correct ones. To address this, it introduces unlikeliness reward, which down-weights high-probability correct rewards, and shows that increasing the number of PPO epochs per batch also mitigates the bias. The method is evaluated on a held-out set Dval and on miniF2F-test, where the final recipe is reported to be competitive with DeepSeek-Prover-V1.5-RL. The paper releases its implementation and includes a toy-environment appendix and a KL-only control.

Significance. If the results hold, this is a useful contribution to the study of RL for formal reasoning: it identifies a concrete failure mode of GRPO in verifier-based domains, proposes a simple and easy-to-implement reward modification, and provides an open pipeline with competitive results on miniF2F-test. The paper has several strengths: it evaluates on held-out sets, includes a KL-only control (Appendix D) that helps attribute the gains to the proposed mechanism rather than to stronger regularization alone, and ships code. The main weaknesses are statistical: the central mechanism is established from a single training run and the toy-environment validation is qualitative, so the claimed findings are plausible but not yet fully secured.

major comments (4)
  1. [Section 3.5, Figure 4] The rank-bias diagnosis rests on a single training run over the first 800 problems, and the paper does not report how many positive samples fall into each rank bin. The low-rank bins are precisely where positive samples are rarest, so the declining tail of Figure 4 could be driven by a handful of problems rather than a stable effect. Since Figure 6 is the main evidence that unlikeliness reward works through the stated mechanism, please report per-bin counts, bootstrap confidence intervals, and ideally results from multiple seeds or a statistical test of monotonicity.
  2. [Section 5.1, Figures 2 and 5] The pass@N comparisons have no error bars reflecting run-to-run variance. Appendix C describes chunking a single set of 512 samples per problem into trials, which measures sampling noise conditional on one trained model, not the stochasticity of training; pass@512 has only one trial and no variance at all. The central claim that unlikeliness reward improves pass@N across a large range of N should be supported by multiple independent training runs or bootstrap intervals over problems, especially since the training-time gains in Table 2 (+153 to +358 out of 9600 solved) should be demonstrated to exceed run-to-run variance.
  3. [Section 3.4] The theoretical motivation assumes each positive sample's probability ratio independently reaches the clipping bound and ignores the group-relative advantage normalization in GRPO. Under group normalization, whether a low-probability correct sample receives a positive advantage depends on the other samples in the group, so the conclusion that improving pass@N at large N requires uplifting low-probability solutions does not strictly follow from the per-sample clipped objective alone. This is acknowledged as a simplification, but the paper should validate it quantitatively (e.g., on the toy environment) or present it explicitly as heuristic motivation rather than as a derivation.
  4. [Appendix A] The toy-environment validation is described only qualitatively. No numbers are given for pass@N, uplift rates, or entropy before and after adding the unlikeliness reward, so the reader cannot verify the claimed reversal of rank bias or the deterioration of default GRPO at tau=5.0. Since the toy environment is presented as controlled confirmation of the mechanism, please include tables or plots with quantitative results and the experimental details (number of seeds, runs, and error bars).
minor comments (5)
  1. [Section 4.1, Eq. (1)] The text says rank(y_i) is in {1,...,G} and then says rank 0 corresponds to the highest-probability sample; this is inconsistent, since presumably rank 1 should correspond to the highest-probability sample. Please clarify the indexing.
  2. [Appendix C] The chunking procedure for pass@n appears to divide the Nmax samples into Nmax/n chunks; for n values that do not divide Nmax, or for pass@512, the result is a single trial, and the reported 'standard deviation across trials' is not a confidence interval. Please clarify how non-divisible cases are handled.
  3. [Figure 1] The figure and caption show 'Proof 2' twice; this looks like a typo and should be corrected.
  4. [Table 3] The differences between the proposed model and V1.5-RL on MiniF2F-test are within the reported standard errors; the text should state explicitly whether the comparison is statistically distinguishable or should be framed as statistically indistinguishable at this scale.
  5. [Section 5.3] The claim that 'higher PPO epochs consistently increases sample diversity, up to ppo-epochs = 4 where training becomes unstable' is not accompanied by data for ppo-epochs=4; please add the result or qualify the claim.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the rank-bias diagnosis is an empirical measurement, the unlikeliness reward is a designed intervention evaluated on held-out sets, and no load-bearing self-citation or definitional reduction appears.

full rationale

The paper's central claims are empirically grounded rather than derived from their own definitions. The rank-bias diagnosis (Section 3.5) is an observational measurement of a defined uplift-rate metric on training samples; it is not assumed in the GRPO objective. Section 3.4 is explicitly an estimate ('we can make estimates by assuming...'), not a derivation, and the pass@N improvements in Figures 5 and Table 3 are evaluated on held-out Dval and miniF2F-test with fixed hyperparameters (β_rank = 0.25 is fixed, not tuned on test). The unlikeliness reward is purpose-built to increase the relative advantage of low-rank correct samples, so the later confirmation that it changes the uplift-rate curve is a mechanism check rather than an independent prediction; the paper does not present this reversal as an unexpected empirical discovery, and the reward uses current-policy ranks rather than the initial-model ranks used in the diagnosis, so the mapping is not identity by construction. All supporting citations to the authors' prior work appear only in related-work context and are not load-bearing for the method's validity. No equation reduces to its input by construction, and no fitted parameter is renamed as a prediction. Therefore no significant circularity is present.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

The central claim depends on a few hand-chosen hyperparameters (beta_rank, KL penalty, number of PPO epochs) and on two modeling assumptions: the perfect verifier setup, and the rank-as-proxy assumption for measuring and correcting rank bias. No new physical or conceptual entities are introduced beyond the 'rank bias' label, which is an empirical pattern rather than a postulated mechanism.

free parameters (3)
  • beta_rank = 0.25
    Strength of the unlikeliness reward penalty; fixed by hand without a sensitivity study (Section 4.1).
  • PPO epochs K = 2 or 3
    Number of optimization steps per batch; chosen based on Dval improvements (Section 5, Table 1).
  • KL coefficient beta_KL = 0.10
    Increased from the default 0.02 to prevent pass@N deterioration; a hyperparameter selected on Dval (Section 5).
assumptions (4)
  • domain assumption The Lean verifier provides a perfect binary correctness signal (R(x,y)=1 if y proves x)
    Used throughout; correctness is fully automated, so rewards are noise-free.
  • domain assumption The KL penalty in GRPO keeps the policy close to the reference model, preserving the base distribution
    Invoked in Section 3.2 and Appendix D; the reference is the base model.
  • ad hoc to paper In the simplified analysis, each positive sample's probability ratio reaches the clip bound (1+epsilon) independently
    Section 3.4; this neglects normalization coupling and the possibility of discovering new correct proofs.
  • ad hoc to paper The rank of a sample within a group of 32 is a valid proxy for its probability under the model
    Section 3.5; used for the uplift-rate analysis and the unlikeliness reward computation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening." pith.science (2026). https://pith.science/paper/EOQZGMUF

@misc{pith2026250602355,
  author       = {Pith},
  title        = {Pith review of: Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EOQZGMUF}},
  note         = {Machine review of arXiv:2506.02355}
}
abstract

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

Figures

Figures reproduced from arXiv: 2506.02355 by the authors.

Figure 1
Figure 1. We identify a rank bias in GRPO in which model updates only reinforce already probable solutions and fail to surface new ones. This sharpens the distribu￾tion and impairs pass@N performance for large N. Our unlikeliness reward addresses rank bias by explicitly encouraging uplifting low-probability correct solutions. ation, RL has been applied at scale to elicit com￾plex reasoning behaviors using only problem in￾stan… view at source ↗
Figure 2
Figure 2. Finetuning DeepSeek-Prover-V1.5-SFT with [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 4
Figure 4. Uplift rate uj as a function of rank j among positive samples. GRPO rarely increases the probability of lowest-ranked (i.e. rarest) correct samples. suggest that GRPO may not be effectively uplifting low-probability correct solutions. To verify this, we examine training samples for the first 800 prob￾lems, computing their probabilities under the initial model and final GRPO-trained model. Let xi be the i-th training… view at source ↗
Figures from the paper (4 more)
Figure 5
Figure 5. Figure 5: Performance of GRPO variants on Dval. Both the unlikeliness reward and additional PPO epochs improve pass@N. Appendix C details how we compute these metrics. 0 5 10 15 20 25 30 Rank of Sample in Group 0.0 0.1 0.2 0.3 0.4 0.5 0.6 Uplift Rate GRPO-Default GRPO-Epochs-2 G…
Figure 7
Figure 7. Figure 7: Number of unique proofs generated at each [PITH_FULL_IMAGE:figures/full_fig_p007_7.png]
Figure 8
Figure 8. Figure 8: Performance of GRPO variants including GRPO-High-KL on Dval. For readability, we omit some variants. 0 5 10 15 20 25 30 Rank of Sample in Group 0.0 0.1 0.2 0.3 0.4 0.5 Uplift Rate GRPO-Default GRPO-Unlikeliness-1 GRPO-Unlikeliness-2 GRPO-High-KL [PITH_FULL_IMAGE:figur…
Figure 9
Figure 9. Figure 9: Uplift rates of GRPO variants including GRPO-High-KL. increased sampling, up to hundreds of thousands of passes (Lin et al., 2025b). This suggests that the distribution of the base model is highly diverse and crucial to preserve during fine-tuning. Prior work addressed…

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Beyond the Sampled Token: Preserving Candidate Support in RLVR

    cs.AI 2025-10 conditional novelty 6.0 of 10

    SimKO, an asymmetric top-K token-level regularizer for RLVR, improves pass@K on math/logic benchmarks across K=1..256 without lowering pass@1 relative to GRPO.

  2. Representation-Based Exploration for Language Models: From Test-Time to Post-Training

    cs.LG 2025-10 conditional novelty 6.0 of 10

    Representation-based elliptical bonuses improve inference-time and post-training pass@k for LLM reasoning, but the headline AIME result is tainted by validation/test overlap.

Reference graph

Works this paper leans on

36 extracted references · 4 canonical work pages · cited by 2 Pith papers

  1. [1]

    Thomas Anthony, Zheng Tian, and David Barber. 2017. https://arxiv.org/abs/1705.08439 Thinking fast and slow with deep learning and tree search . Preprint, arXiv:1705.08439

    arXiv 2017

  2. [2]

    Yinlam Chow, Guy Tennenholtz, Izzeddin Gur, Vincent Zhuang, Bo Dai, Sridhar Thiagarajan, Craig Boutilier, Rishabh Agarwal, Aviral Kumar, and Aleksandra Faust. 2024. https://arxiv.org/abs/2412.15287 Inference-aware fine-tuning for best-of-n sampling in large language models . Preprint, arXiv:2412.15287

    arXiv 2024

  3. [3]

    Xingyu Dang, Christina Baek, Kaiyue Wen, Zico Kolter, and Aditi Raghunathan. 2025. https://arxiv.org/abs/2504.10478 Weight ensembling improves reasoning in language models . Preprint, arXiv:2504.10478

    arXiv 2025

  4. [4]

    Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. https://api.semanticscholar.org/CorpusID:232990 The lean theorem prover (system description) . In CADE

    work page 2015

  5. [5]

    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. 2025. https://arxiv.org/abs/2501.12948 Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement lea...

    arXiv 2025

  6. [6]

    Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. 2024. https://openreview.net/forum?id=kk3mSjVCUO ABEL : Sample efficient online reinforcement learning for neural theorem proving . In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS'24

    work page 2024

  7. [7]

    Jiewen Hu, Thomas Zhu, and Sean Welleck. 2024. minictx: Neural theorem proving with (long-) contexts. arXiv preprint arXiv:2408.03350

    arXiv 2024

  8. [8]

    Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample

    Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. 2023. https://arxiv.org/abs/2210.12283 Draft, sketch, and prove: Guiding formal theorem provers with informal proofs . Preprint, arXiv:2210.12283

    arXiv 2023

Show all 36 references
  1. [9]

    Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. 2022. https://arxiv.org/abs/2205.11491 Hypertree proof search for neural theorem proving . Preprint, arXiv:2205.11491

    2022 arXiv

  2. [10]

    Haohan Lin, Zhiqing Sun, Sean Welleck, and Yiming Yang. 2025 a . https://arxiv.org/abs/2407.10040 Lean-star: Learning to interleave thinking and proving . Preprint, arXiv:2407.10040

    2025 arXiv

  3. [11]

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. 2025 b . https://arxiv.org/abs/2502.07640 Goedel-prover: A frontier model for open-source automated theorem proving . Preprint, arXiv:2502.07640

    2025 arXiv

  4. [12]

    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 oth...

    2024 arXiv

  5. [13]

    Lawrence C. Paulson. 1994. Isabelle: A Generic Theorem Prover. Springer Verlag

    1994

  6. [14]

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. 2022. https://arxiv.org/abs/2202.01344 Formal mathematics statement curriculum learning . Preprint, arXiv:2202.01344

    2022 arXiv

  7. [15]

    Stanislas Polu and Ilya Sutskever. 2020. https://arxiv.org/abs/2009.03393 Generative language modeling for automated theorem proving . Preprint, arXiv:2009.03393

    2020 arXiv

  8. [16]

    Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn. 2023. https://openreview.net/forum?id=HPuSIXJaa9 Direct preference optimization: Your language model is secretly a reward model . In Thirty-seventh Conference on Neural Infor...

    2023

  9. [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. https://arxiv.org/abs/2504.21801 Deepseek-prove...

    2025 arXiv

  10. [18]

    John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. 2017. https://arxiv.org/abs/1707.06347 Proximal policy optimization algorithms . Preprint, arXiv:1707.06347

    2017 arXiv

  11. [19]

    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. https://arxiv.org/abs/2402.03300 Deepseekmath: Pushing the limits of mathematical reasoning in open language models . Preprint, arXiv:2402.03300

    2024 arXiv

  12. [20]

    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

    2024 arXiv

  13. [21]

    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. https://arxiv.org/abs/1712.01815 Mastering chess and shog...

    2017 arXiv

  14. [22]

    Zhiqing Sun. 2024. Gpt-accelera: Simple and efficient pytorch-native transformer training and inference (batched). https://github.com/Edward-Sun/gpt-accelera

    2024

  15. [23]

    Yunhao Tang, Kunhao Zheng, Gabriel Synnaeve, and Rémi Munos. 2025. https://arxiv.org/abs/2503.19595 Optimizing language models for inference time objectives using reinforcement learning . Preprint, arXiv:2503.19595

    2025 arXiv

  16. [24]

    Terence Tao. 2025. https://doi.org/10.1090/noti3041 Machine-assisted proof . Notices of the American Mathematical Society, 72(1):6--15

    2025 doi

  17. [25]

    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...

    2025 arXiv

  18. [26]

    Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. https://arxiv.org/abs/2410.15700 Internlm2.5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems . Preprint, arXiv:2410.15700

    2024

  19. [27]

    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. https://arxiv.org/abs/2408.08152 Deepseek-prover-v1.5: Harnessing ...

    2024 arXiv

  20. [28]

    Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. 2025. https://arxiv.org/abs/2502.03438 Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving . Preprint, arXiv:2502.03438

    2025

  21. [29]

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. 2024. https://arxiv.org/abs/2412.16075 Formal mathematical reasoning: A new frontier in ai . Preprint, arXiv:2412.16075

    2024 arXiv

  22. [30]

    Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. https://arxiv.org/abs/2406.03847 Lean workbook: A large-scale lean problem set formalized from natural language math problems . Preprint, arXiv:2406.03847

    2024 arXiv

  23. [31]

    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. https://arxiv.org/abs/2503.1...

    2025 arXiv

  24. [32]

    Yang Yue, Zhiqi Chen, Rui Lu, Andrew Zhao, Zhaokai Wang, Yang Yue, Shiji Song, and Gao Huang. 2025. https://arxiv.org/abs/2504.13837 Does reinforcement learning really incentivize reasoning capacity in llms beyond the base model? Preprint, arXiv:2504.13837

    2025 arXiv

  25. [33]

    Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. 2025. https://arxiv.org/abs/2504.06122 Leanabell-prover: Posttraining scaling in formal reasoning . Preprint, arXiv:2504.06122

    2025 arXiv

  26. [34]

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2021. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110

    2021 arXiv

  27. [35]

    online" 'onlinestring :=

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint eprinttype howpublished institution journal key month note number organization pages publisher school series title type volume year doi pubmed url lastchecked label extra.label sort.label short.list...

  28. [36]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.