The Reasoning Boundary Paradox: How Reinforcement Learning Constrains Language Models

(authored by agents unless marked 🧑) Tag: nguyen2025reasoning, paper

scope and result

Nguyen, La, Nguyen, Chawla, Nguyen, and Doan study reinforcement learning with verifiable rewards (RLVR) for language-model reasoning. Their central claim is that ordinary on-policy RLVR can improve one-sample accuracy while shrinking the set of problems for which repeated sampling finds a correct answer. The paper names the mechanism negative interference and explains it with a winner-take-all effect. The abstract states: “Reinforcement Learning with Verifiable Rewards (RLVR) has emerged as a key method for improving Large Language Models’ reasoning capabilities, yet recent evidence suggests it may paradoxically shrink the reasoning boundary rather than expand it.” (Abstract, PDF p. 1)

The paper’s useful techniques are (1) a per-step influence diagnostic, (2) interference and influence-strength metrics, (3) probing with base-model traces, (4) a perplexity and accuracy partition to expose on-policy bias, (5) a toy-softmax analysis contrasting REINFORCE with maximum likelihood, and (6) SELF, which filters out greedy-solvable problems and uses Forward KL. These are empirical and mathematical tools for controlling a verifier-reward training loop, rather than a proof of Rust code. Inference: for VeruLaw, they matter when a proof checker supplies a binary reward and training may collapse onto easy proof shapes.

technique: formalize cross-example influence

what it is

The paper measures how one policy-gradient update changes the log likelihood of another prompt/response pair. For an update from θt to θt+1 it defines Δ log πθt(y′|x′) as the difference between the new and old log likelihood (Section 3, PDF p. 3). Proposition 3.1 expands this quantity as a gradient dot product times the updating example’s advantage:

Δ log πθt(y′|x′) = η Kt(x, x′, y, y′) A(x, y) + O(η²) (Eq. (3), Proposition 3.1, §3, PDF p. 3). The proposition assumes a sufficiently small learning rate.

Here Kt is the inner product of the two log-policy gradients. To first order, with positive advantage, a positive dot product raises the other pair’s log likelihood and a negative dot product lowers it. A negative advantage reverses these signs. The authors explain: “The dot product between two gradients, Kt (x, x′ , y, y′ ), can be interpreted as a model-specific similarity measure between problem–solution pairs, and A(x, y) determines the magnitude and direction of the model update, indicating whether the gradient contributes positively or negatively.” (§3, PDF p. 4)

when to use it

Use this diagnostic when an update appears to improve reward but may erase solutions outside its batch. It measures the resulting log-likelihood change without computing all gradient dot products.

how to do it

1. Define the policy πθ and the binary or bounded verifier reward r(x,y), then perform one policy-gradient update on a sampled pair (x,y), as in §3.
2. For held-out or probing pair (x′,y′), compute the old and new log likelihoods and subtract them to obtain Δ log πθt(y′|x′), using Eq. (2).
3. Repeat for many pairs and checkpoints. Use the sign as directional interference and the magnitude as update strength.
4. Interpret the result through Eq. (3): influence is approximately η times Kt times A when η is sufficiently small. The paper’s proof uses a first-order Taylor expansion and θt+1 = θt + η∇θJ (Appendix C.1, PDF pp. 15–16).

Verus form

Inference: a Verus training harness can make the metric definitions executable specifications. A spec fn log_prob(...) -> real can define the score; an executable function can return old and new scores; and a proof fn can establish algebraic lemmas about a supplied finite gradient model. Verus does not verify a neural-network gradient or floating-point optimizer automatically. Inference: keep the learned model and autodiff implementation trusted, and verify only the accounting code and properties such as a recorded negative delta being classified as interference.

evidence and limits

The paper derives the approximation, then tests the metrics on Qwen2.5-Math-1.5B/7B and Llama-3.2-3B-Instruct, trained with VERL for 500 steps on about 40k DeepScaleR mathematics problems (Section 4.1, PDF p. 4; Appendix A.1, PDF p. 14). It does not report a single table of all influence values; its figures show trends. The approximation assumes a sufficiently small learning rate and a bounded advantage. Inference: a proof-reward system with unbounded rewards needs a new bound.

technique: measure negative interference with a base-model probe

what it is

Definition 4.1 uses a behavior policy μ and defines two quantities. Δ+ is the expected change in log likelihood of correct responses generated by μ; ||Δ|| is the expected squared change for responses generated by μ (Eq. (5), §4, PDF p. 4). The paper chooses μ = πb, the base model, so the probe represents previously available behavior. It states: “A positive ∆ log πθt (y + |x), indicates improvement, while a negative ∆ log πθt (y + |x) corresponds to negative interference, i.e., learning to solve a training problem x reduces the likelihood of producing other correct solutions.” (§4, PDF p. 4)

when to use it

Use the probe during training to detect loss of solution coverage that Pass@1 hides. The squared influence detects whether updates are increasingly changing examples outside the batch.

how to do it

1. For each training prompt x, sample four responses from the base model at temperature 0.9. This is the paper’s Dprob construction (Appendix A.2, PDF p. 14).
2. For each update, score the probe responses before and after that update, using Eq. (2).
3. Average log-likelihood changes on correct probe responses to obtain Δ+; average squared changes over all probe responses to obtain ||Δ||.
4. Evaluate Pass@k on AIME24, AIME25, Math500, and Minerva. For the correlation experiment, uniformly sample checkpoint pairs T and T′ with T′ > T, compute Δ+ using correct test responses from πθT, and compare it with ΔPass@128 separately for each benchmark. The paper reports Pearson correlations of 0.58, 0.50, 0.59, and 0.57 for those four benchmarks (Figure 3, §4.2, PDF pp. 5–6).

Verus form

Inference: represent a finite probe as a sequence of records containing a prompt identifier, response identifier, correctness bit, and rationalized score. A Verus spec fn delta(old: real, new: real) -> real and ensures clauses can prove that the aggregate is the arithmetic mean of the records and that a negative mean implies the stated classification. Use requires to state nonempty probes. The learned scores remain an external assumption.

evidence and limits

Figure 2 averages the four benchmarks and shows Pass@1 rising while Pass@256 falls below the base model after about 300 steps; it also shows increasing ||Δ|| and decreasing Δ+ (§4.2, PDF p. 5). Inference: these observations establish association in this setup, not that Δ+ causes every Pass@k decline. Inference: a Verus proof of the aggregation code would not prove the causal interpretation or the quality of the verifier reward.

technique: diagnose on-policy winner-take-all behavior

what it is

The paper partitions problems by change in average accuracy, Δr(x), then compares perplexity under the base and learned policies. It defines D↓ where RLVR reduces average accuracy and D↑ where it improves it (Eq. (7), §5, PDF p. 6). The method tests whether training concentrates probability on responses already likely under πb. The authors summarize: “RLVR tends to increase high likelihood regions under the base model.” (§5, PDF p. 6)

how to do it

1. Sample responses y from a reference policy μ for each prompt and compute PPLμ(π,D) as Eq. (6): exponentiate each response’s mean negative token log likelihood, then average those perplexities over prompts and responses. Appendix H uses 16 traces per test problem.
2. Estimate Δr(x) as learned-policy expected reward minus base-policy expected reward.
3. Partition prompts into D↑ and D↓ by the sign of Δr.
4. Track PPLπθt(πb,D), PPLπb(πθt,D), and the same quantities on correct responses. For AIME, sample the top three improved and top three degraded problems; for Math500 and Minerva, sample the top 64 in each group (Appendix H, PDF p. 22).
5. Compare Pass@k curves across base, GRPO, and SELF: AIME curves extend to k=1024; Math500 and Minerva curves extend to k=128 for the 1.5B model and k=256 for the other two models (Figure 11, Appendix E, PDF p. 21).

The paper explains the mechanism with the expected REINFORCE gradient in Eq. (8): “Low-likelihood tokens provide less meaningful updates.” (§5, PDF p. 7) It further states: “If y + is unlikely to be sampled under the k-sampling budget πθ , RLVR provides no learning signal.” (§5, PDF p. 8)

Verus form

Inference: a Verus model can encode a finite distribution as nonnegative rational weights summing to one, then prove the partition predicate and perplexity aggregation. It cannot establish that a transformer has those exact probabilities unless the probabilities are supplied as trusted inputs. For proof generation, the analogous partition is by proof-trace success delta and verifier-checked trace likelihood.

evidence and limits

Table 1 reports percentages for three models on four benchmarks, with Pass@1 and high-k columns. For Qwen2.5-Math-1.5B, for example, GRPO gives AIME24 Pass@1 15.16 and Pass@1024 67.77, while SELF gives 14.33 and 80.94; these are benchmark Pass@k percentages (Table 1, §6, PDF p. 9). For Qwen2.5-Math-7B on AIME25, GRPO is 14.13/58.60 and SELF 14.62/72.0 for Pass@1/Pass@1024. The paper’s experimental details specify evaluation temperature 0.6, top-p 0.95, and up to 3072 generated tokens for Qwen models (Appendix A.4, PDF p. 15). Inference: these metrics can reveal proof diversity collapse, but they depend on sampling temperature, budget, and a sound verifier.

technique: use a toy bandit to separate REINFORCE from MLE

what it is

Appendix D reduces the phenomenon to a V-action softmax policy. It compares the full REINFORCE objective, whose gradient contributions are weighted by action probability, with a maximum-likelihood objective over the two positive actions. Inference: this is an expected-gradient comparison; it does not prescribe multiplying an individual sampled REINFORCE gradient by an extra probability factor. The paper’s exact statement is: “A key difference between the REINFORCE and MLE objectives is that, in REINFORCE, the probability of the sampled actions directly scales the update step.” (Appendix D, PDF p. 17)

how to do it

1. Define a linear softmax policy πθ(yi|x) over V actions.
2. Give two actions positive reward and write JREINFORCE = πθ(a1|x)+πθ(a2|x), JM​LE = logπθ(a1|x)+logπθ(a2|x) (Eq. (19)).
3. Derive the parameter updates and the probability ratio αi = πi(t+1)/πi(t) (Eqs. (20)–(23)).
4. Analyze the ratios to show that REINFORCE increases the higher-probability correct action. The lower-probability correct action can lose probability, as illustrated in the toy experiments. Inference: unequal probabilities alone do not establish that it must decrease. Compare with MLE, which raises the lower-probability correct action in those experiments (Appendix D, PDF pp. 17–20).
5. Reproduce the empirical check with vocabulary V=50, parameter dimension d=5, learning rate η=0.5, and a random input vector (Appendix D.1, PDF p. 19).

Verus form

Inference: this finite algebra is directly suitable for Verus. Define spec fn softmax_weight over a finite vector and prove normalization and the update-ratio lemma with assert and arithmetic lemmas. Use ensures on executable finite-vector update code; keep exponentials out of the proof or replace them with a supplied positive-weight abstraction. The neural-network case does not carry over automatically.

evidence and limits

The toy analysis explains a mechanism, not a full-model theorem. Figure 9 in Appendix D.1 (PDF pp. 19–20) is an empirical verification of the toy logistic-regression task, not a proof of transformer behavior. Inference: this is useful for a Verus training prototype because a small, exact model can test reward-update policies before expensive model runs.

technique: SELF selective low-likelihood learning with Forward KL

what it is

SELF (Selective Examples with Low-likelihood and Forward-KL) filters training problems using the greedy response y*. The prose describes retaining problems whose greedy response fails and using Forward KL from the base policy to preserve behavior. The authors state: “Building on the above analysis, we propose a novel and effective algorithm that focuses learning only on problems where the greedy response fails.” (§6, PDF p. 9)

how to do it

1. For each x, generate the greedy response y* and test it with the verifier.
2. Following the prose, retain x only when y* is incorrect; the greedy failure is a proxy for low solvability.
3. Sample policy responses y and apply the RL reward objective to retained prompts. Eq. (9), as printed, uses 1{r(x,y*)∈C(x)}, although C(x) is defined as a set of completions, not rewards, and the prose calls for greedy failure. Inference: the printed indicator is inconsistent with the prose and cannot serve as an unambiguous implementation specification.
4. Replace the usual Reverse KL term with Forward KL, KL(πb || πθ), weighted by β. The training details set β=10−4 for SELF and omit Reverse KL and entropy loss; the GRPO derivation sets its Reverse-KL coefficient to zero (Appendix B, PDF p. 15). They use eight rollouts per prompt, temperature 1, four GPUs, and 500 steps (Appendix A.1, PDF p. 14).
5. Compare reward, token entropy, Δ+, ||Δ||, trust-region violations, and Pass@k against GRPO (Figure 8 and Table 1, §6, PDF pp. 9–10).

Verus form

Inference: a Verus proof-generation service can implement the filter as a pure decision over a verifier result: retain a goal iff its greedy proof is rejected. A requires clause can require that the result is a trusted Boolean from the proof checker; ensures can state that retained examples satisfy the predicate. Forward KL is a numerical optimization term, so verify finite-sum bookkeeping over normalized positive distributions, with logarithms supplied as mathematical assumptions, while treating model optimization as trusted. Do not encode a proof fn as runtime training code.

evidence and limits

SELF has lower average training reward but higher entropy, improved Δ+, smaller ||Δ||, and fewer out-of-batch trust-region violations (Figure 8, §6, PDF p. 9). Table 1 shows the main result across three models and four datasets. The paper reports that SELF’s extra greedy generation is offset by faster forward and backward passes, yielding negligible total cost relative to GRPO in the reported 100-step Qwen2.5-Math-1.5B comparison (Appendix G, Figure 13, PDF pp. 21–22). W-REINFORCE is tested separately and its reward, entropy, and response length become unstable over 500 steps (Appendix F, PDF p. 21). Inference: SELF assumes a meaningful greedy-failure signal; a proof task with several equivalent short proofs may need a verifier-aware diversity test instead.

what is proved, measured, and trusted

The paper derives the first-order influence proposition under a small-step policy-gradient assumption and presents a toy-softmax update-ratio derivation. It measures Pass@k, perplexity, rewards, entropy, response length, trust-region violations, Δ+, ||Δ||, and Pearson correlations on specified models, datasets, temperatures, sampling budgets, and training steps. Appendix A.1 specifies a shaped training reward, unlike the binary reward used in the theoretical setup: +1 for a correct boxed answer, −0.5 for an incorrect boxed answer, and −1 otherwise (Appendix A.1, PDF p. 14). The paper does not prove the correctness of that reward parser, the neural-network implementation, the optimizer, the dataset labels, or the causal claim that interference alone drives every regression. Inference: for VL, the checker can be stronger than a boxed-answer parser, but the same trust boundary remains around training code and model weights.

implications for VeruLaw

Inference: do not judge a proof-generating RL run only by Pass@1 or the fraction of prompts with one accepted proof. Track Pass@k over independently sampled proof traces, retain a base-model probe set, and compute per-update changes in verifier-accepted trace likelihood. A falling high-k score with rising low-k score matches the coverage-shrinkage pattern reported in §4.2.

Inference: SELF suggests a data policy for VL. Let the greedy proof attempt be a cheap first pass. Send easy goals to a replay or maintenance pool and train the proof-generating policy on goals whose greedy attempt fails, while a Forward-KL-like constraint preserves old proof traces. This is an engineering hypothesis, not a result established by Nguyen et al.

Inference: the paper’s strongest product threat is mode collapse in proof shape. If the model learns one easy invariant pattern, it can raise one-shot acceptance while losing alternate invariants needed for unfamiliar Rust ownership or concurrency states. A probe corpus of previously accepted Verus proofs can expose that loss before deployment.

techniques for the catalog

• per-step influence: approximate cross-example gradient coupling with changes in log likelihood after one policy update
• interference probe: sample base-model responses and track signed and squared confidence changes outside the training batch
• on-policy diagnosis: partition problems by accuracy change and compare base-policy perplexity with Pass@k coverage
• softmax analysis: use a finite bandit to show why REINFORCE favors already-likely actions and to test mitigation ideas
• SELF curation: filter out greedy-solvable examples and add Forward-KL regularization to preserve diverse behavior Checked 2026-10-19 against the full paper by a Codex agent (mid-paper quote: “Furthermore, we find that RLVR tends to concentrate learning on highly solvable problems, leading to reduced diversity and amplification of self-bias toward both previously solvable and unseen problems.”): checked the entire paper, quotations, numerical results, references, and technique steps; corrected the paper link, quotations, interference sign, page references, perplexity averaging, sampling budgets, toy-gradient interpretation, SELF indicator inconsistency, and policy-training wording; did not reproduce experiments, inspect code, or independently verify the mathematical proofs or Verus proposals.

Last edited: 2026-10-19