{"id":"7e1720df-484a-4b49-a581-25e8f0e75297","arxiv_id":"2506.02355","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"GRPO's rank bias reinforces likely answers and neglects rare correct proofs; an unlikeliness reward that down-weights likely correct samples improves pass@N in formal theorem proving.","lead":"Standard reinforcement learning for language models tends to strengthen answers the model already finds likely, while neglecting rare but correct ones. This paper shows this 'rank bias' in theorem proving and introduces a simple reward adjustment that improves performance when many proof attempts are sampled.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The rank-bias diagnosis and the claimed pass@N gains rest on a single run without error bars; the low-rank tail of Figure 4 may be too sparse and noisy to support the mechanism.","rationale":"The reader's weakest assumption points to the same metric, so I agree. The concern is load-bearing because the paper's novelty is the mechanism (rank bias) and the remedy (unlikeliness reward). The theoretical model in Section 3.4 is explicitly heuristic, so it cannot independently establish that low-probability uplift is the operative channel; the empirical demonstration is Figure 4, which is a single-run aggregate. The absence of counts and confidence intervals matters precisely because the tail of the distribution is where the claimed failure occurs. A bootstrap or probability-binned replication is cheap and would settle whether the monotonic pattern is real. I do not think the paper is wrong on its face; the central claim is plausible and supported by a controlled toy in the appendix, but the appendix currently omits the quantitative evidence. Hence the verdict should remain conditional: the paper should be accepted only after the diagnostic is verified with error bars and repeated seeds.","tokens_in":13081,"tokens_out":7056,"duration_ms":74337,"concrete_test":"Recompute the uplift-rate analysis using absolute log-probability bins rather than within-group ranks, report per-bin positive-sample counts, and add bootstrap or Wilson confidence intervals; also rerun GRPO-Default and GRPO-Unlikeliness-2 with at least three seeds and report pass@N curves with error bands. If low-probability bins contain fewer than roughly 50 positive samples, if the monotone decline in u_j disappears once binned by probability, or if the pass@N advantage over GRPO-Default is below seed variance for N ≥ 64, the rank-bias mechanism and the claimed improvement are not supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central mechanism—GRPO's rank bias (Section 3.5) and its reversal by unlikeliness reward (Section 5.2)—rests on the uplift-rate metric u_j, computed from a single training run over the first 800 training problems. The rank proxy is defensible as an ordinal within-group measure, but the metric has two unsecured properties. (1) It averages a binary indicator π_GRPO > π_0 over positive samples in each rank bin, and the paper never reports how many positive samples fall in each bin; with 800 problems and G=32, 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 rate. (2) The binary outcome measures the final result of the whole optimization—including the KL penalty, clipping, and competition from other samples—not whether GRPO supplied a positive advantage to that sample, so a monotone curve is consistent with rank bias but also with low-probability correct samples being crowded out by high-probability updates; the paper does not distinguish these. The main pass@N comparison in Figure 5 also has no error bars or repeated seeds, so the claimed improvement across N is not separated from run-to-run variance. The toy-environment confirmation (Appendix A) is described qualitatively, without reported numbers, so it does not yet validate the diagnostic.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":13408,"tokens_out":5102,"duration_ms":47400,"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":[{"comment":"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.","section":"Section 3.5, Figure 4"},{"comment":"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.","section":"Section 5.1, Figures 2 and 5"},{"comment":"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.","section":"Section 3.4"},{"comment":"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).","section":"Appendix A"}],"minor_comments":[{"comment":"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.","section":"Section 4.1, Eq. (1)"},{"comment":"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.","section":"Appendix C"},{"comment":"The figure and caption show 'Proof 2' twice; this looks like a typo and should be corrected.","section":"Figure 1"},{"comment":"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.","section":"Table 3"},{"comment":"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.","section":"Section 5.3"}],"recommendation":"major_revision","confidential_remarks":"I recommend major revision rather than rejection: the central claim is plausible and the paper includes useful controls and an open release, but the evidence for the mechanism and for the headline pass@N improvements needs to be placed on firmer statistical footing. The requested additions are feasible within the scope of the manuscript."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this paper identifies a specific failure mode in GRPO for formal theorem proving—rank bias, where already-likely correct proofs get reinforced and rare-but-correct ones are neglected—and offers a simple fix, the unlikeliness reward, that genuinely improves pass@N at large N. The open pipeline is competitive with DeepSeek-Prover-V1.5-RL. The main caveats are that the headline curves come from a single run without error bars, and the supporting diagnostic is coarser than it looks.\n\nWhat's new and good: the rank-bias diagnosis via uplift rates is a concrete, testable mechanism, and the unlikeliness reward is a minimal change that reverses the bias in their Figure 6. The KL-only control in Appendix D is the right check: raising KL alone doesn't produce the gain. The PPO-epochs observation is a nice bonus and separately validated. They also release code and data, which is genuinely useful.\n\nThe soft spots are real but not fatal. The stress-test note is partly right: Figure 4's u_j is computed on a single run over 800 problems, and low-rank bins necessarily have few positive samples, so the declining tail could be noisy. The paper doesn't report bin counts, which would settle that. The binary indicator (π_GRPO > π_0) is a blunt instrument, and the monotone curve is consistent with other mechanisms—but the toy environment and diversity curves give the rank-bias story more support than a single figure. The bigger issue is experimental: Figure 5 has no error bars or repeated seeds, so the pass@N gains are not separated from run-to-run variance. Hyperparameters (beta_rank, KL, epochs) are selected on Dval, which is also the main evaluation set; that's a mild overfitting risk, though the final recipe is confirmed on miniF2F-test. The analytic model in Section 3.4 is explicitly heuristic and not load-bearing.\n\nDespite these caveats, the central claim holds: unlikeliness reward improves pass@N at large N across settings, and the mechanism is plausible. This paper is for anyone working on RL for verifier-based tasks, especially theorem proving or code. A serious referee should ask for seeds, error bars, and bin counts, not a redesign. I'd send it to review, and I'd cite it in my own work.","headline":"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.","tokens_in":13877,"tokens_out":2209,"would_cite":true,"duration_ms":21997,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"GRPO systematically neglects rare correct proofs; a rank-aware reward restores large-N sampling gains.","keywords":["reinforcement learning","GRPO","rank bias","distribution sharpening","unlikeliness reward","pass@N","formal theorem proving","Lean"],"falsifier":"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.","tokens_in":12881,"feed_emoji":"🧮","tokens_out":13379,"duration_ms":109393,"temperature":0.7,"pith_summary":"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.","feed_headline":"Reward the unlikely: a rank-aware reward fixes GRPO's blind spot","feed_subtitle":"Penalizing the likeliest correct proofs lifts pass@N at large N and matches a top open prover.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"introduces GRPO, the algorithm whose rank bias and sharpening behavior are the paper's target.","marker":"Shao et al. (2024)"},{"why":"supplies the base SFT prover model, the training hyperparameters, the Lean REPL wrapper, and the RL-trained baseline the paper compares against.","marker":"Xin et al. (2024)"},{"why":"provides prior evidence that verifier-based RL concentrates the distribution rather than adding capability, motivating the sharpening question.","marker":"Yue et al. (2025)"},{"why":"defines the miniF2F benchmark used for the final large-scale evaluation.","marker":"Zheng et al. (2021)"},{"why":"contributes the Lean Workbook statement collection from which the training and validation sets are drawn.","marker":"Ying et al. (2024)"},{"why":"identifies the solvable 10K subset of Lean Workbook statements used as the main training set.","marker":"Wu et al. (2024)"},{"why":"provides the larger 11k solved theorem dataset used in the large-scale experiment.","marker":"Lin et al. (2025b)"},{"why":"introduces the Lean proof assistant, whose verifier supplies the binary reward signal the whole study depends on.","marker":"de Moura et al. (2015)"}],"fun_headline_variants":["Unlikeliness reward lifts GRPO beyond distribution sharpening","Rewarding rare correct proofs beats GRPO's rank bias","GRPO rank bias fixed by up-weighting unlikely correct answers","How to push GRPO past sharpening: reward the unlikely","Uplift rare proofs to fix GRPO's distribution sharpening"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Unlikeliness reward lifts GRPO beyond distribution sharpening","Rewarding rare correct proofs beats GRPO's rank bias","GRPO rank bias fixed by up-weighting unlikely correct answers","How to push GRPO past sharpening: reward the unlikely","Uplift rare proofs to fix GRPO's distribution sharpening"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000461,"raw_usage":{"total_tokens":2384,"prompt_tokens":1099,"completion_tokens":1285,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":715,"completion_tokens_details":{"reasoning_tokens":1200}},"tokens_in":715,"tokens_out":1285,"duration_ms":10127,"temperature":1.0,"reasoning_tokens":1200,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:25:46.461154+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"introduces the Lean proof assistant, whose verifier supplies the binary reward signal the whole study depends on."}],"review_version":1}