Whatever Remains Must Be True: Filtering Drives Reasoning in LLMs, Shaping Diversity
Authors: Germán Kruszewski
Pierre ERBACHER
Jos Rozen
Marc Dymetman
Venue: ICLR 2026 Poster (2026)
Keywords: Large Language Models
LLMs
Post-Training
Reasoning
theorem proving
Lean
f-divergences
Amari $\alpha$-divergences
Distributional Matching
diversity
Primary area: foundation or frontier models, including LLMs
TL;DR: We propose using a family of divergences that span mode seeking to mode covering to balance between precision and diversity in training LLMs for reasoning tasks

Abstract: Reinforcement Learning (RL) has become the _de facto_ standard for tuning LLMs to solve tasks involving reasoning.
However, growing evidence shows that models trained in such way often suffer from a significant loss in diversity.
We argue that this arises because RL implicitly optimizes the "mode-seeking" or "zero-forcing" _Reverse KL_ to a target distribution causing the model to concentrate mass on certain high-probability regions of the target while neglecting others. 
In this work, we instead begin from an explicit target distribution, obtained by filtering out incorrect answers while preserving the relative probabilities of correct ones.
Starting from a pre-trained LLM, we approximate this target distribution using the $\alpha$-divergence family, which unifies prior approaches and enables direct control of the precision–diversity trade-off by interpolating between mode-seeking and mass-covering divergences.
On a Lean theorem-proving benchmark, our method achieves state-of-the-art performance along the coverage–precision Pareto frontier, outperforming all prior methods on the coverage axis.

Published as a conference paper at ICLR 2026
WHATEVER REMAINS MUST BE TRUE: FILTERING DRIVES REASONING IN LLMs, SHAPING DIVERSITY
Germán Kruszewski', Pierre Erbacher', Jos Rozen' & Mare Dymetman
Naver Labs Europe
IIndependent Researcher
{german. kwwszewski, erbacherr,bacer,, harraacceer.os.rroneeeeeeeeeeeee rww.rroeeeeeeeeaaatte. com ma rc. gymetman@@maai com
ABSTRACT
Reinforcement Learning (RL) has become the de facto standard for tuning L.LMs to solve tasks involving reasoning. However, growing evidence shows that models trained in such way often suffer from significant loss in diversity. We argue that this arises because RL implicitly optimizes the "mode-secking" or "zero-forcing" Reverse KL to a target distribution causing the model to concentrate mass on cer- tain bigh-probability regions of the target while neglecting others. In this work, we instead begin from an explicit target distribution, obtained by filtering out in- correct answers while preserving the relative probabilities of correct ones. Start- ing from a pre-trained L.M,, we approximate this target distribution using the a-divergence family, which unifies prior approaches and enables direct control of the precision-diversity tradc-off by interpolating between modc-seeking and mass-covering divergences. On LEAN theorem- theorem-proving benchmark, our method achieves state-of state-of-the-ar the-art art performance along the coverage preccsiorecnnnn Pareto fron- tier, outperforming all prior methods on the coverage axis.
INTRODUCTION
"How often have said to you that when you have eliminated the impossible, whatever remains, however improbable, must be the truth?"
Arthur Conan Doyle, The Sign of Four
Large Language Models (LLMs) have made striking progress reasoning tasks. A leading approach is Reinforcement Learning from Verifiable Rewards (RLVR) (Lambert et al. 2025 2017
DeepSeck-Al et al. 2025). where policy-gradies methods such PPO (Schulman al.
or GRPO (Shao et al. (024) optimize against a reward that combines a binary verifier of correctness with KL penalty to keep the tuned model close to its base distribution.
While RLVR has been credited with enabling exploration new solutions DeeepSeek-Al et al,, 2025). recent studies challenge this view. In particular, they find that base models already contain these solutions given a sufficient sampling budget, and that tuned models often exploit additional
samples less effectively due reduced output diversity (Yue al. 2025b He et al.) [025 Dang
ct al. 2025 Wu et al. (202).. Earlier, with RLHF (Christiano et al. 2017 Ziegler et al. 2020
similar diversity reductions were observed, sometimes described as "mode collapse" Kirk et al.
2024 O' O'Mahony et al. 2024).
We argue that this loss of diversity stems from the implicit objective of RL-based training: opti- mizing the Reverse KL divergence to target distribution that favors correct answers (Korbak et al.) 20226). Reverse KL is "mode-seeking" or "zero-forcing." emphasizing precision on subset of so-
lutions while ignoring others (Bishop) 2006; Huszár 2015 Li & Farnia 2023). This explains why RLVR models become accurate but less diverse.
"Equal contribution

---

Published as a conference paper at ICLR 2026
Prediion
Famco fonder welich
16-m Vede Sorking by
4O0 13-1
GRPO
Vode Serbuter
Pow
Inteol
PC
Mearowwaryy TRi Sharsiyy
eit jand 17)
Diversity
To00
Sazo
Ado 6.0
600
444
Illustration of our method. RLVR policy-gradient approaches (e.g. GRPO, PPO) concentrate probability on narrow region of the target distribution, while methods like KL-DPG increase diversity but allocate mass to low-quality regions. a-DPG balances these extremes. Right: Model precision (pass@) 1) and coverage (pass @ 256). The Pareto frontier is the upper-right bound- ary of the convex hull; the shaded band shows one bootstrap standard deviation. a-DPG and baseline models lie along the frontier. with c- c-DPG achieving the highest coverage and precision for low and high values of a, respectively.
Figure 1: Left:
To address this, we explicitly define the desired target distribution: one that always outputs correct solutions while remaining as close as possible to the base model, thus preserving any solution in- cluded therein (Khalifa et al.) |021 Kim et al. 2025). Direct sampling is infcasible, but we can approximate it with an autoregressive policy using Distributional Policy Gradient Algorithms (DPG Parshakova et al. 2019 Khalifa et al. 202 Go et al. 2023). Concretely, we apply f-DPG (Go et al. 2023), which minimizes an f f-divergence (Polyanskiy & Wu 2025) to this target. Different divergences trade off precision (probability of sampling a correct solution) and coverage (probabil- ity of sampling at least one correct solution given a sufficiently large sampling budget): Reverse KL emphasizes the former, Forward KL the latter (Bishop) 2006). To interpolate between them, we introduce a-DPG, based on a-divergences (Rényi 1961 Cressie & Read 1984] Amari 1985). No- tably, this method unifies RLVR (Reverse KL) and both KL-DPG (Parshakova et al. [019]]
et al. 2021; Go et al.) 2023) and Rejection Sampling Fine-Tuniig (Forward KL) (Zelikman et al.
2022
2023) under single umbrella. We call this approach Distributional Matching with Verifiable Rewards (DMVR), positioning it under the general framework of Distributional Match-
Yuan et 2
ing (Khalifa et al. 2021 Korbak et al. 2022a b).
We evaluate a-DPG in LEAN, proof assistant that automatically verifies formal mathematical proofs. this setting, success requires not only correct candidates but also diversity across proof attempts, since harder theorems may be solvable only through rare derivations. We find that DPG achieves statc-of-the-at performance, producing models that lic on the Parcto fronticr between precision (pass31) 1) and coverage (pass@255) and that surpass prior methods in coverage
Contributions.
We introduce the DMVR framework, which trains models by approximating an explicitly defined verifier-based target distribution.
We clarify how the implicit dynamics of RL-based methods lead to reduced diversity.
We highlight the role of the divergence family in trading off precision and diversity, and propose a-DPG smoothly interpolate between Forward and Reverse KL.
We show on the LEAN benchmark that a-DPG achieves results along a Pareto coverage- precision frontier, with the a parameter allowing to trade-off between precision and cover- age. Moreover, a-DPG achieves the best coverage results among all considered methods when using low values of a.
We make the code available
dpg
2

---

Published as a conference paper at ICLR 2026
2 BACKGROUND
Reinforcement Learning with Verifiable Rewards (RLVR) Let (T(112) y + R be an LLM with parameters 0 defining probability distribution over sequences y E Y' conditioned I. A verifier uy. E {0. 1 is a binary function that discriminates between correct and incorrect responses to æ. Given dataset D of prompts (and, optionally, ground-truth answers for the verifier), RLVR uses a standard reinforcement learning objective derived from previous work on Reinforce- ment Learning from Human Feedback (RLHF) (Christiano et al.
prompt
2017 Ziegler al. 2020
JRLVR arg max (1) Re (y,
where the "pseudo-reward" Korbak et al. 2022b) Rg is defined as follows:
Te (y)z))
Ro(y, x) = u(y, x) - log
(2)
Tbase [/)=z)
Here, Thase is the base LLM and | is tunable parameter that controls the trade-off between max- imizing the reward and minimizing divergence from the original model. Some authors fall back to setting 3 = 0. just optimizing the expected verifier reward (Liu et al. 2025 Mistral-AI et al. 2025
Yu et al. 2025
Policy Gradient (PG) Algorithms We can maximize Eq. 2 following multiple algorithms. One of the simplest ones KL-Control (Todorov 2006 Kappen et al 2012). with the following gradient
V & (0) Eg-DD.yr A(y. V log (v(2)))
(3)
where A(y, .z) Ro (y, x)- B(x) is the advantage function and (xx) is baseline that doesn't 't de-
pend on y/ to keep the objective unbiased used for variance reduction (Sutton & Barto 2020, Chapter
2. Sectioin 7). Some options for an unbiased baseline could include constant, critic (Sutton al.
1999). or leave-one-out average in a batch of rewards (RLOO; Kool 2019 Ahmadian et al. 2024
When 3 0, Eq. reduces the original policy gradient algorithm REINFORCE (Williams) 1992).
Another popular choice is PPO (Schulman et al. 2017). which optimizes the following clipped sur- rogate objective:
lvv
JiPO (8) EEND.y
Σ
min (plualz, ye Bcr)) (wt.dppppppppppppp (p(yd)2, c, c,1 A(y.z))
(4)
where p(ye J2, Uet) = To To(ui (2r, (ct) no (Vel x. Vee) is the ratio between the current and the previ- ous policy token probabilities and is small hyperparameter. PPO discourages large policy updates that would move p outside the interval [1 [1-e, [+e], which improves training stability by constraining the new policy to be close to the old one. GRPO (DeepSeek-Al et al. 2025) and other recent meth- ods use the same clipping strategy, but differ in the form of the baseline. While PPO is commonly understood to use critic model as baseline, GRPO uses the group-level reward average.
Distribution Matching (DM) DM Khalifa et al. 2021 Korbak et al., 2022a Go et al. 2023
Kim al.; 2025) is a family of techniques for aligning LLMs to meet certain constraints. For instance, let's 's suppose that we want to constrain the LM so that all sequences meet r(æ, w) for some binary filter r(x, y) E {0, 1] The method expresses this target distribution want to approximate, which in this case is given by
P=(y) Thase (ylz) r(y,z).
(5)
This distribution is the only distribution p' that fulfills the following two desirable conditions: (i) satisfies the constraint r r(y,z) = 1, Vy E Supp(p'(-Iz)), and (ii) is the closest to Thase in terms of DKL (p' (-|2r) [ (-12)). The second condition guarantees the preservation of all the
diversity contained in the original model. In information geometric terms, Pz. is the I-projection of Touse (-12:) into the manifold of all distributions that satisfy the constraint given by (Csiszár &
Shields 2004).
NNoe that the average of samples, as used GRPO, is biased instead.
'If the reader notices strong similarity between constraint r(x, y) and verifier v( v), this is no coincidence: It is exactly this connection that will exploit in this paper.
3

---

Published as a conference paper at ICLR 2026
Distributional Policy Gradient (DPG) Algorithms Given a target distribution, we can optimize
an autoregressive policy Te to approximate it. Khalifa et al. (202I) used for this the DPG algo-
rithm (Parshakova al.) 2019 Korbak et al.) 2022a b), later denoted KL-DPG (Go et al. 2023),
which minimizes the Forward KI. DKL (Px (T)) ) to the target distribution px:
Pr(
VoL (0) Vo (px|I = -
-1)
Vo log (yll))) (6)
To(y)>
The negative term acts constant bascline. Computing (=r(y(z) requires estimating nor- malization constant denoted as the partition function, Zz, which can be estimated by importance sampling (Owen 2013). Note that in the case of binary constraint, Ze is the acceptance rate of the constraint when sampling from the base model (Kim et al. 2025): Ze Evey a(ylz)r(y,
By>a((1n)) = P y-aa(->))) (1)a(()))[((), x) = 1]. (See App. for additional details.)
Later, Go al., (2023) introduced f-DPG, effectively generalizing this technique to any f-
divergence by minimizing
Px):
VoLT-DPG(0) (0) = VeDDND (D, (To(-1=))1P22) = Ex (.grvro-1))) [- A (w, V log To (ulz)) (7)
is "pseudo-reward", B(x) is context-dependent baseline, and ʃ a convex function that parametrizes the f-divergence where f: (0) + I s.t. f(1) = O. If (v()) O, then, Rg (v.x) = -f' -f'(co) (oo), where f fox) = lim tf(?).
where A (v, = Rg (v,x)~ B(x), Ri (v, = -f [T((ll))
DISTRIBUTIONAL MATCHING WITH VERIFIABLE REWARDS (DMVR)
Here, adopt the DM framework, and propose that the ideal target distribution for tuming lan- guage model Trase (- (z) to solve problems x ~ D by means of a verifier v(y, x) E {0, 1] is simply the result of applying the verifier as binary constraint, i.e. r(y,2) v(y, x). as follows:
Py(y) & Thmse (y) ())y, x) Vx E D.
(8)
This distribution filters out all incorrect responses, leaving out only correct ones with the same relative probabilities as the reference LLM. This is the single distribution that (i) always answers
correctly to I, and (ii) it is closest to the base model hese as measured by DKL base) bose) (Khalifa let al. 2021). In the following discussion, we argue that (I) the distribution approximated by RLVR closely related, becoming equivalent ps in the limit 8 O, (2) for any fixed B > 0. RLVR optimizes the Reverse KL to target distribution, which has mode-seeking behavior, incentivizing the policy to put high probability mass in small regions of high reward at the cost of diversity, and (3) we propose an alternative based on f-DPG parametrized with a-divergences to trade-off precision and diversity. Of these, points (1) and (3) are original to our work, whereas point (2) reproduced from Korbak et al. (2022b). Moreover, the target distribution and the f-DPG technique to approximate were defined in prior art (Khalifa et al. 2021 Go al. 2023).
3.1 FROM RLVR TO DMVR
Consider the following lemma, reproducing the argument from Korbak et al. (2022b):
Lemma 1. Define
Pv) (3) Thase (y ax) x/)3)
Σ
Thase (y ax) xx)()().x)/3))
Then,
1 B (0(y. x)) log
To (y (x)
Vo [KL [1] = -EEND.y
Va log (2(2)
(9)
Thase (w) xx)
To (v x))
E Ean
e(y, x) - 3 log
Ve log To (0(2)
(10)
B
Thase (y x))
REVR pseudl-rewwrd
(Proof in App. B
4

---

Published as a conference paper at ICLR 2026
see that the gradient of the KL-Control's objective (right-hand-side, optimiz- ing the expected RLVR pseudo-reward) is proportional to the gradient of the Reverse KL of To to Pz.8 (left-hand-side up negative constant that flips the direction of optimization. Therefore, maximizing the regularized reward implies minimizing the divergence, and vice versa.
From Eq. 10
Furthermore, note that the distribution Pz.8 is smooth approximation to the ideal distribution defined in Eq. 8 Pz. converging to it as 3 + 0+: Lemma 2.
lim Pr. = Pv- B 8-+
(11)
(Proof in App.
C
However, the gradient of the Reverse KL dominated by - Volywaa [v(y, (Eq. revealing why minimizing Reverse KL becomes an increasingly aggressive medk-s proxy for maximiz- ing expected reward, at the cost of diversity even if the diversity of responses is well-captured by the target Pa- In the limit, with 3 = O, the Reverse KI. becomes undefined, the KL--Cntrool algorithm reduces plain REINFORCE, and safeguard remains preserve diversity.
3.2 AND BACK (AS SPECIAL CASE OF a-DPG)
Having defined the target distribution Pz. we are left with the task of picking a divergence to train a
policy xy approximate it. As we have seen, the Reverse KL DRL (To [p) implicitly employed by
RLVR, is a mode-seeking or zero-forcing divergence (Bishop) 2006 Huszár 2015 Li et al. 2025).
This means that it will penalize placing probability mass in regions where p assigns little or none, but it is relatively indifferent to ignoring modes of altogether. As a result, the learned policy tends to concentrate on a small subset of high-prood probbabbbbbit modes while disregarding other plausible regions of the target distribution, which can reduce diversity and lead to brittle or degenerate behavior.
In contrast, the Forward KL, (KL Te), mass-covering. Here, the divergence becomes large whenever Ty assigns insufficient probability to regions where p has support, encouraging the policy to cover all modes of the target distribution. While this can improve diversity and robustness, often comes at the cost of assigning non-negligible probability mass to low-reward or unlikely regions, leading to less precise approximations of the target.
This tension between mode-seeking and mass-covering behavior motivates considering broader family divergences. The a-divergences family (Rényi) 1961; Cressie Read, 1984 Amari 1985) subfamily of f-divergences- provides exactly such continuum, interpolating smoothly between the Forward KL (as a + 0) and the Reverse KL (as a + 1). In between (for a = 0.5) lies the squared Hellinger distance (Hellinger) 1909). By tuning a, mode-seeking versus mass-covering behavior, potentially capturing the benefits both extremes while mitigating their drawbacks. We refer to Table [T for full characterization. We denote the parametrization of of fDDG with a-divergences as a-DPG, which has the following pseudo-reward:
balance the degree of
Roly, xx) - (TT(Ulle)
Pa Pe(()) <o(y)a)) ((
-
-1)
(12)
Because for low values of a, peaks in the p/ ratios can induce large variance in Rg. we clip the parenthetical factor maximum M. We also rescale by discounting the constant 1/(1 //)1-)):
Roly, .r) = min ((
(=(3) To (v(x))
1-a
M
(13)
Finally, we use the gradient formula in Eq.
setting the baseline ((x) to the leave-one-out per-
context average of the pseudo rewards (Kool 2019: Ahmadian et al. 2024).
is interesting to note its behavior when setting a e (i.c., close to the Reverse KL), Then, ()(() P&
V VoDio (To(11)))))) EowD
V log (1((
(14)
Eg Dayne
V ()(()
(15)
Te (y/lz)
EewD.y u(v. Vo log T (v)z))
(16)
5

---

Published as a conference paper at ICLR 2026
Parameter
NameeCooespooneecc
Generator fa( (generic)
E. (generic)
0,1 a a-divergence (f-div)
F" ot [I-
(p)
0 <<1 1
ala- 1] lim Ia(t) = Fogg - ++1
Q-1
1
0 0>> 1: +.00
Reverse KI. ((()T)))
lim 1.(0 = logt
log
4.00
Forward KL K)
1m fu(1) = logt +t-1
lim (2())
p/p/Tt
1
Hellinger (exact)
-2/D/T
2
Table 1: Parametrization of the a-divergence as f-divergence (T.(p)
by discounting for simplicity the scaling constant and the baselines in Eq. 15 and noting that for 0 c < 1 and if |æ|] is bounded then x' I[ # and (v) * 0 + ely, x) in the last step. Thus, for a that is lower but very close to 1, we are again recovering the REINFORCE learning rule. In contrast, when a = O, then D, becomes exactly the Forward KI., and thus we recover the original KL-DPG algorithm (Parshakova et al. [209 Khalifa et al. 2021). which conserves more diversity from the original distribution sacrificing some precision:
(v)
VoDy. (==(1)>>)) D.y..y
V log (y(az)
(17)
TT(2)
Notably, it is easy to see that if a fixed amount of samples are obtained just from Thase instead of Te. KL-DPG reduces RS-FT (Zelikman al.) 2022 Yuan et al. 2023). as it optimizes the cross-entropy to samples from the base model filtered by the verifier (see App. Dj more details).
Finally, while the general formal properties of a-divergences are well-studied, our specific setup, with a target distribution that has a restricted support (over verifiable outputs only) has some inter- esting novel formal properties that we describe in App.
EXPERIMENTS
Informal vs Formal Mathematics Informal mathematics has become a common paradigm for training large language models (LL.Ms) on reasoning tasks, with widely used benchmarks such as MATH (Hendrycks et al., 2021) and AIME (Sun et al., 2025). These methods have achieved im- pressive performance (Gemini team 2025), but they also face inherent challenges. Informal proofs and solutions often lack guarantees of rigor, making large-scale verification difficult and requiring heuristics like majority voting rather than provable correctness. While effective in many scenarios, these approaches may be less suited for tasks that aim to explore novel results or a wide variety of solutions. Formal methods provide a promising alternative (Tao] 2025). Proof assistants such as
LEAN (de Moura al. 2015), COQ (Barras al. 1997), and ISABELLE (Nipkow al. 2002) represent statements and proofs in a formally verifiable language. This not only allows for effi cient and rigorous proof generation but also reduces dependence on labeled data. At inference, the paradigm shifts from achieving consensus over a large pool of candidates (eg., via majority voting) to ensuring sufficient diversity among them to guarantee larger coverage. Theorem provers must therefore go beyond producing single correct proof but should generate diverse candidate proof's to more fully explore the solution space. Prior work LEAN has applied reinforcement learning (e.g., GRPO (Wang et al. 2025 Xin et al. 2025 Ren et al. 2025 ). but such methods can result in decreased diversity (He et al. 2025). In this work, we present an approach to formal theorem proving in LEAN that seeks to improve both precision for better efficiency and diversity to guarantee high coverage, highlighting the potential of formal reasoning for scalable discovery.
For these experiments consider CrepSeek-Proveet Prover-V..5----- V1.5-SFT (Xin al. 2025 7B parameters models based on DeepSeek model and further pre-trained on high-quality mathematics and code data, with focus on formal languages such as LEAN, ISABELLE, and METAMATH, and finetuned on LEAN4 code completion datasets (Xin et al. 2025).
Models
Dataset
The training set is composed of 10K solvable LEAN problems extracted and filtered from the LEAN Workbook dataset (Ying al. 2024 Wu et al. 2024), from which 200 problems are kept unseen as test set.
We follow the experimental setup introduced in prior work (He et al. 2025
Reward function and LEAN4 Verifier The reward function extracts the last LEAN4 code block in the generated sequence and verifies it automatically by the LEAN proof assistant. The sequence is

---

Published as a conference paper at ICLR 2026
given reward of it is verified correct and 0 otherwise. In our experiments used the same LEAN4 and Mathlib4 version (lean4:v4.9.0) as used in DeepSeek-Proot ProverV1.5 (Xin et al. 2025).
Baselines We compare against several baselines, focusing on critic-free methods, which have be- come standard thanks to not requiring an additional copy of the model: GRPO (DeepSeek-Al et al.)
2023 for which we only consider its unbiased instantiation, Dr. GRPO (Liu at. 2025) and other variants with inversity-preservinn regularization: High-KL with a strong KL penalty( = 0.1), Rw- 0.25, and Pass @k k training (Chen 2025b; Tang et al. (025) directly optimizes pass @k via lcave-one-out advantage formula-
Ulkly (He al. 2025) with rank bias promoting diversity
ct al.
tion that reduces variance. We further include in our comparison GPG (Chu et 2025), ReMax (Li 2024) and RLOO (Ahmadian et al. 2024). For reference, Base-SFT is the model used as
ct al.
base for all methods.
Training All trainings are done on single node of 4xA with 28 CPUs dedicated for running proof assessment in parallel. Due to the high variance in LEAN compilation and verification time, the reward function is executed asynchronously. All training scripts are based on VERL (Sheng
ct al. 2024). By default, since we use a verifiable reward, we follow Mistral-AI et al. (2025); Liu ct al. (2025) and disable advantage normalization while setting the KL divergence penalty to = D. For all a-DPG training, we set the clipping value to M 10, train on float16 following et al. (2025), and constrain the partition function on the lower side Zu 2 with 1
The partition function is computed online using the sampled responses for each problem, thus not incurring any additional computational cost with respect baseline methods. See App. E for more details on the estimation of Z and an ablation experiment using more samples to compute the partition function. Across all methods, we fix the maximum response length to 1024 tokens and use 512 generated sequences per step for 200 iterations (<2 3 epochs), See App. F for additional details on hyperparameters.
To evaluate model performance on reasoning and generation tasks, we report pass@k (Chen al. [02T], a standard metric widely used code generation and problem-solving benchmarks. The metric measures the probability that at least one correct solution is found within the top-k sampled outputs of the model. For a problem with n generated outputs with n 2 k, of which correct, an unbiased estimate of the probability that at least one of k sampled outputs is correct is (Chen et al. 2021)
Evaluation Metric
pass@k =
Averaging over problems gives the overall pass@k. generate responses using temperature T = 1 and nucleus sampling (Holtzman et al. (2020) with parameter p 0.99.
4.1 RESULTS
Coverage vs. precision analysis We analyze models along the trade-off between coverage, mea- sured by pass@256, and precision, measured by pass@l (Fig. [ The results reveal clear pre- cision-coverage frontier. The base SFT model attains relatively broad coverage but low precision, indicating the ability to solve diverse problems but with low single-sample success probability, placing it far from the frontier. @ass@k training improves coverage while leaving precision largely unchanged. Training strategies such as GRPO with KL regularization and GRPO-Rw-UIi im- prove precision without substantially affecting coverage, still shifting performance toward a more favorable region of the trade-off space. In contrast, RLOO, GRPO without KL regularization, and GPG achieve high precision at the cost of reduced coverage. Across D-DPG variants, lower-a set- tings (e.g., a = 0.25) achieve the highest coverage while still considerably improving precision over SFT. Increasing further improves precision, reaching parity with RI-bbased methods at large val- ues (c.g., a 2 0.995), while typically retaining higher coverage. Importantly, most a-DPG models lie near the Pareto frontier, demonstrating that the method provides controllable and effi- cient trade-off between precision and coverage, outperforming or matching competing RL baselines across much of the spectrum.
Pass @k curves Figure 2 illustrates the pass@k performance on the test set measured over 256 samples for a few chosen models. First, looking the left panel, we note that have
7

---

Published as a conference paper at ICLR 2026
Feridrctt modes
Fouid fo vodes
Paodee EPPt orited
Rea
Figure 2: Pass @ curves on the test set for the Base-SFT model tuned with different methods.
Figure 3: Problem Difficulty Transition Matrices showing the number of problems that transition from an initial difficulty classification under the base model (Base-SFT) (y-axis) to a final difficulty after post- fest-training (x-axis). The results highlight a polarizing effect: a-DPG (a 0.999) and GRPO exhibit similar behavior, improving performance on a majority of medium-ddfffccul problems by making them easy, but also degrading performance on hard problems, causing many of them to become unsolved. a-DPG (a 0.25) and GRPO (High-KL, KL)) are more conservative, improving sample efficiency on fewer problems but harder problems remain solvable.
produced the results reported by He al. 2025), where the GRPO model starts with much higher pass@1 score, but then the base model overpasses it as it reaches pass 1 6. Furthermore, there is no single model that dominates all others across all values of indicating Pareto trade-off between precision (pass@1) 1) and coverage (pass@255) Nonetheless, a-DPG (a 0.999) generally dom- inates GRPO and other pure RI.-based techniques, with the only exception of ReMax that has better coverage albeit somewhat lower precision. On the other hand, = 0.25 dominates the base model and other prenssiiyp baselines such as Pass @k training and GRPO with KL regularization, achieving the best performance
pass@256 Rw-UIkly, in turn, starts with higher pass@l, 1,, but a = 0.25 outperforms for & 2 4. The middle panel highlights the RL-based baselines, confirming that KL regularization helps prevent diversity collapse and Pass@k training and Rw-Ulkly baselines offer competitive results. The rightmost panel is comparing different variants of a-DPG in relation to the base model. While the base model surpasses and matches models with a 2 0.75, models with lower values of alpha dominate the base model.
Problem difficulty analysis In this section, we examine how training affects problem solvabil- ity. We categorize problem difficulty based model performance, measured as the proportion of correctly solved sequences. A problem is considered easy for a given model if at least 80% of the sampled sequences are correct, medium if 20-80% are correct, and hard if fewer than 20% cor- rect. This notion of difficulty has a direct relation with the efficiency of the model at solving a given problem as the number of samples until generating one correct solution follows geometric distri- bution whose parameter is the model's sampling accuracy. In Figure 3 we plot how the problems difficulties evolve after having trained the Base SFT model using various methods. Problems on the diagonal (grey) remain unaffected by training. Elements in the lower-left triangle (blue) represent problems for which solving efficiency improved, while elements in the upper-right triangle (red) indicate problems where sampling efficiency decreased. As we can see, many problems that were medium or hard for the base model became easy after training both for GRPO and a = 0.999. How- ever, this came at the cost of other problems in these same categories becoming unsolvable given the same sampling budget. a- a-DGP (a = 0.25) and GRPO (High-KI. on the other hand, improve sample efficiency fewer problems at the cost of just three problems becoming unsolvable.
8

---

Published as a conference paper at ICLR 2026
Premice Diversky (Shannen dstrapyl Model
Nepploxity unier Basel untdd
172
Nece Conersing Soldee
State
Figure 4: Left: Relationship between premise diversity measured by Shannon index and model performance (pass@) @1 1 and puss$226), The regression lines computed for c-DPG models. The left y-axis shows pass@1 performance, and the right y-axis shows pass@ 256 performance. Right: Perplexity analysis showing the distribution of perplexity for responses single problem sampled from various models under the base SFT model distribution.
Diversity Analysis We investigate the relationship between proof diversity and model perfor- mance. We split this analysis into two components: the tactics and premises used candidate LEAN proofs. A tactic is a command that transforms a proof goal into simpler subgoals (c.g.. intro, apply, y, rw), while a premise proof (e.g., mu mul_comm, mul mul_ the Gini-Simpson index. For each problem, we evaluate 256 generated proof sequences. At every proof state, compute both the Simpson index and Shannon entropy over the choices of tactics and premises. Concretely, for a given problem, we count the occurrences of each premise and tactic, and compute the Simpson index as D = Σi= where p. is the relative abundance of premise or tactic and S is the total number of premises or tactics. These metrics are then aggregated across all problems to capture the overall diversity of can- didate sequences. Higher diversity tactics and premises in candidate proofs generally correlates with improved cass@256 performance, whereas it is anticorrelated with pass@1 as shown on the left panel of Figure 4 (and, additionally, in Appendix Figure 10p.
lemma or previously proven theorem that can be used within
As measures of diversity, we employ the Shannon index and
i=1 př and the Shannon index as H = - -E
i=1 In ps
Perplexity Analysis Recent work on RLVR (Yue et al. 2025a) shows that RL-trained models do not truly discover new solutions, instead the solutions they generate are already likely under the base model. To further investigate whether a-DPG stays close to the base model, we conduct a perplexity analysis. We sample single problem from the test and have each model generate 16 solutions. For each solution, we compute perplexity both under the model that generated it (sell-perplcxity) and under the base model (Base SFT). As shown in the right panel of Figure across all models, the generated sequences are already highly probable according to the base model, with very similar perplexities. Note also that for this particular problem, GRPO collapsed and produces 16 identical sequences, which were also highly probable under the base model.
OTHER RELATED WORK
Improving test-time scaling (passek) Popular RL-based post-training methods, such as PPO (Schulman et al. (017)) or GRPO (Shao et al. 2024) optimize inherently mode-seeking ob- jectives, which can lead to mode collapse. The resulting models often achieve high accuracy, but exhibit very low entropy, generating less diverse sequences ( (uue et al.) 2025b). This issue is partic- ularly pronounced when scaling test-time compute for solution search, with the SFT models often achieving better performances due to higher diversity (He et al. 2025 Chen et al., 2025al Tang et al. 2025 Zhu et al., 2025 Yue et al. 2025a). Multiple approaches try to overcome this issue, mainly by adapting the advantage function. (He al. (025) proposed to add rank bias penalty, that increases the advantage of unlikely sequences. (Chen et al. 20256) modify the reward from pass@1 equivalent to pass@k: allowing better sampling efficiency. They obtain better pass @k

---

Published as a conference paper at ICLR 2026
at inference than training with entropy regularization. Tang et al. (2025) propose a leave one out strategy to reduce variance and therefore improving pass k at test-time.
Reinforcement Learning from Proof Assistant Feedback Significant efforts in the community have focused on training LLMs integrated with interactive proof assistants such as LEAN (de Moura
al.
2013), CoQ (Barras al., 1997), and ISABELLE (Nipkow et al.) 2002). Early approaches
leveraged LLMs to generate the next proof step or tactic (AlphaProof and AlphaGeometry teams, Polu et al. [023] Wu et al.) 2024), often combined with explicit search strategies (Lample et al. 2022p. More recent work has shifted towards training models to generate complete proofs directly (Xin et al., 2025 Ren et al.) 2025 Wang et al., 2025) where the last training stage relies on reinforcement learning from proof assistant feedback (RLPAF), where the proof assistant veri- fication serves as a reward signal. However, RLPAF algorithms such as GRPO are mode-secking, strongly truncating/fiterrig the original distribution, which inherently limits the diversity of gener- ated proofs and introduces significant inefficiencies in inference scaling (Zhu et al. 2025).
2024
6 FINAL REMARKS AND CONCLUSIONS
We have introduced DMVR, a general framework for optimizing a policy to produce only correct answers according verifier function. This perspective casts RLVR training in new light and helps diagnose its failure modes. In particular, building on the work of Korbak et al. (2022b), we established that RLVR methods optimize toward a filtered version of the original distribution, even if they do it in a way that especially focuses on certain regions of high verifier reward. From this viewpoint, we can revisit recent debates on whether RL alone can create new skills (DeepSeek- Al et al. 2025 He et al. 2025 Yue et al., 2025b Wu et al.. 2025 and understand why RLVR does not generate fundamentally new capabilities but instead reweights and amplifies behaviors already present in the base model. Moreover, because RLVR is tied to a mode-seeking divergence, sacrifices distributional breadth, leading models to forget solutions that the base model could originally provide.
However, the core principle of filtering the base model is sound and can be independently motivated; it enforces correctness while preserving the multiplicity of valid responses. The true source of diver- sity loss, therefore, lies not in the target distribution itself, but in the divergence used to approximate it with gradient descent within a restricted parametric family.
By explicitly defining the target distribution, DMVR enables optimization with divergences that bal- ance the two competing goals: correctness and diversity. In particular, explored a-divergences, which smoothly interpolate between Forward and Reverse KI.. This approach generates a Pareto frontier of models: setting a near the Reverse KL recovers models that match or exceed the per- formance of RL-based alternatives, while low values of a produce models that preserve substantial diversity while still improving sampling precision over the base model.
The choice of divergence impacts the resulting models in at least two different ways: On one hand, loss landscapes associated with different divergences can produce different training dynamics. On the other hand, within a restricted parametric family, each divergence can induce different optima. To disentangle the contribution that each of these factors has in the resulting models we could adopt curriculum in which we gradually increase during training, thus encouraging coverage at the beginning of training, and precision towards the end. If the resulting models preserve more diversity, this could be an indication that training dynamics matter. If, on the contrary, they reach as much coverage as using a high value a from the start, then this would be an indication that it is the optima for the given parametric family that dominates. We leave these questions for future work.
Known Limitations Without clipping, o-DGG is unstable for small values of a (e.g., S 0.5). Khalifa et al. (202I) use an offline version of DPG where the sampling policy is only updated from the training policy if the divergence to the target probability is estimated to have improved. Here, we avoided keeping in memory a second copy of the model, and preferred to manage variance by clipping the pseudo rewards. Also, the evidence for the effectiveness of a aDDPG centers on the Lean task using the DeepSeek Prover base model. Generalization to other tasks (e.g., code generation) and larger model families remains limited and is acknowledged as future work.
10

---

Published as a conference paper at ICLR 2026
ETHICS STATEMENT
LLMs tuned using verifier feedback have attracted considerable attention from the research com- munity and the general public because of their strong problem-solving abilities. The techniques introduced in this paper aim to preserve more of a model's initial diversity than existing RL-based approaches at the cost of less strict adherence to the verifier's feedback.
In the specific setting we risk of harm. In broader applications, however, such as attempts to "aliin"" language models with specific policies or behaviors, weaker adherence to constraints could be more concerning. We note that recent proposals within the distributional matching framework may help address this issue (Kim) et al. 2025), even though they rely the availability of verifier at inference time.
models to prove theorems- this trade-off carries little
More importantly, the distributional perspective makes explicit the central choice of a target distri- bution to optimize. Although the training techniques used for approximation also influence model behavior, we believe that making the choice of target distribution open and transparent can promote accountability and clarity. We therefore encourage this practice when tuning models for specific goals.
REPRODUCIBILITY STATEMENT
We will make publicly available all the code to reproduce our experiments after publication. The LEAN Workbook dataset we used in our experiments already open (Ying al., [002] Wu al. 2024), as so it is the base model
Propeeek-roove--II....
we use for training (Xin et al.] 2025).
In addition to the experiment details we describe in Section 4 we report additional details such as hyperparameter choices in in App.
ACKNOWLEDGEMENTS
We thank Thibaut Thonet for the very helpful comments this paper and the anonymous reviewers for suggestions that helped improve this work.
REFERENCES
Arash Ahmadian, Chris Cremer, Matthias Gallé, Marzieh Fadaee, Julia Kreutzer, Olivier Pietquin, Ahmet Üstün, and Sara Hooker. Back to Basics: Revisiting REINFORCE Style Optimization for Learning from Human Feedback in LLMs, February 2024. URL http: http://arxiv.org//eeet
2402.14744 arXiv:2402.14744 [cs].
AlphaProof and AlphaGeometry teams.
AI achieves silver-medal stan-
dard July
solving
International
Mathematical Olympiad problems.
Blog post,
htwp:/iiiinnnnoooooeeeooooommmee gwwgle/ sccoer//bb/ ai www.-ooo---ooeeeemeemoemme at -edveer-eedallleeee
2024.
URL:
Shun-ichi Amari. a a-Divergence and a-Projection in Statistical Manifold. In Shun-ichi Amari (ed.), Geometrical Methods in Statisties,, pp. 66-103. Springer, New York. NY, 1985. ISBN 978-1-4612-50565 doi: 10. 1111007997---4412-55555
DifferettalGeemmericall
Bruno Barras, Samuel Boutin, Cristina Comes, Judicaël Courant, Jean-Christophe Filliåtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, César Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq Proof Assistant Reference Manual Version 6.1. Research Report RT-0203, INRIA, May 1997. URL https::/inni.... Projet COQ.
hal www.ciienceee iineiiiiiiaa 00069968
Christopher M. Bishop. Pattern recognition and machine learning. Information science and statis- tics. Springer, New York, 2006. ISBN 978-0-387-31073-2
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri,
11

---

Published as a conference paper at ICLR 2026
Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder. Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavar- ian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plap- pert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss: William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang. Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Joshua Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Pe- ter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojciech Zaremba. Evaluating large language models trained on code. CoRR, abs/2107.03374. 2021. URL http://db> p. uni mrri-trier.com deciierreeeeeeee http//////oooaassseeeeaa
html
Zhipeng Chen, Xiaobo Qin, Youbin Wu, Yue Ling, Qinghao Ye, Wayne Xin Zhao, and Guang Shi. Pass@k training for adaptively balancing exploration and exploitation of large reasoning models. arXiv preprint arXiv:2508. 2025a.
Zhipeng Chen, Xiaobo Qin, Youbin Wu, Yue Ling, Qinghao Ye, Wayne Xin Zhao, and Guang Shi. @ass@k Training for Adaptively Balancing Exploration and Exploitation of Large Reasoning Models, August 2025b. URL [cs] version: 1.
wttp://..rggbbb/b/////e 10751 10i5:
Paul F Christiano, Jan Leike, Tom Brown, Miljan Martic, Shane Legg, and Dario Amodei. Deep Reinforcement Learning from Human Preferences. In Advances in Neural In- formation Processing Systems, volume 30. Curran Associates, Inc., 2017. URL
html
Xiangxiang Chu, Hailang Huang. Xiao Zhang, Fei Wei, and Yong Wang. GPG: A Simple and Strong Reinforcement Learning Baseline for Model Reasoning, May 2025. URL http: /tttpp//arxiv.
org/abs/ /504. 02546 17Xiv:2504.02544 [cs].
Andrzej Cichocki and Shun-ichi Amari Families of alpha-, beta- and gamma- gamma-divergences: Flexible and robust measures of similarities. Entropy, 153))1532-1566 2010. doi: 123390/e12061555
URL http::ttt://// //ww wwww mdpi. wwt./10999430011225555555
Noel Cressic and Timothy R. C. Read. Multinomial Goodncss-of-Fil Tests. Journal of the Royal
Statistical Society, Series B (Methodological), 46(3):400464, 1984. ISSN 0035-9246. URL
https://wwwt //ttt/////ww///oo.roooo.oo wttp:/taale/e///5eo5.. ford University Press).
Publisher: [Royal Statistical Society, Ox-
I. Csiszár and C. Shields. Information Theory and Statistics: A Tutorial. Foundations and Trends@ in Communications and Information Theory, 1(4):417-528, December 2004. ISSN 1567-2190, 1567-2328. doi: 10.1551/0100000004,, URL/https:/ /tww///wwww.. nowpublishers. com/ haam/aaaccceeeeeass/cccc-
Publisher: Now Publishers, Inc.
Xingyu Dang, Christina Baek, J. Zico Kolter, and Aditi Raghunathan. Assessing Diversity Col- lapse in Reasoning. February 2025. URL
wwtp:/ewwwwwe...r.oeeeee net/forum?id
AMi KMijsh
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In CADE, 2015. URL httpp:://pppp.
lemanticscholle www.oollrrrrrr///oooo Cttpgg//oooouuuo 232990
DeepSeck-AL, 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, Aixin Liu, Bing Xue, Bingxuan Wang, Bochao Wu, Bei Feng, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Damai Dai, Deli Chen, Dongjie Ji, Erhang Li, Fangyun Lin, Fucong Dai, Fuli Luo, Guangbo Hao, Guanting Chen, Guowei Li. H. Zhang, Han Bao, Hanwei Xu, Haocheng Wang, Honghui Ding, Huajian Xin, Huazuo Gao, Hui Qu, Hui Li, Jianzhong Guo, Jiashi Li, Jiawei Wang, Jingchang Chen, Jingyang Yuan, Junjie Qiu, Junlong Li, J. L. Cai, Jiaqi Ni, Jian Liang, Jin Chen, Kai Dong, Kai Hu, Kaige Gao, Kang Guan, Kexin Huang, Kuai Yu. Lean Wang, Lecong Zhang, Liang Zhao, I Litong Wang, Liyue Zhang, Lei Xu, Leyi Xia, Mingchuan Zhang, Minghua Zhang,
12

---

Published as a conference paper at ICLR 2026
Minghui Tang, Meng Li, Miaojun Wang, Mingming Li, Ning Tian, Panpan Huang, Peng Zhang, Qiancheng Wang, Qinyu Chen, Qiushi Du, Ruiqi Ge, Ruisong Zhang, Ruizhe Pan, Runji Wang, R. J. Chen, R. L. Jin, Ruyi Chen, Shanghao Lu, Shangyan Zhou, Shanhuang Chen, Shengfeng Ye, Shiyu Wang, Shuiping Yu, Shunfeng Zhou, Shuting Pan, S. S. Li, Shuang Zhou, Shaoqing Wu, Shengfeng Ye, Tao Yun, Tian Pei, Tianyu Sun, T. Wang, Wangding Zeng, Wanjia Zhao, Wen Liu, Wenfeng Liang, Wenjun Gao, Wenqin Yu. Wentao Zhang, W. L. Xiao, Wei An, Xiaodong Liu, Xiaohan Wang, Xiaokang Chen, Xiaotao Nie, Xin Cheng, Xin Liu, Xin Xie, Xingchao Liu, Xinyu Yang, Xinyuan Li, Xuecheng Su, Xuheng Lin, X. Q. Li, Xiangyue Jin, Xiaojin Shen, Xi- aosha Chen, Xiaowen Sun, Xiaoxiang Wang. Xinnan Song, Xinyi Zhou, Xianzu Wang, Xinxia Shan, Y. K. Li, Y. Q Wang. Y. X. Wei, Yang Zhang. Yanhong Xu, Yao Li, Yao Zhao. Yaofeng Sun, Yaohui Wang, Yi Yu, Yichao Zhang, Yifan Shi, Yiliang Xiong, Ying He, Yishi Piao, Yisong Wang, Yixuan Tan, Yiyang Ma, Yiyuan Liu, Yongqiang Guo, Yuan Ou, Yuduan Wang, Yue Gong, Yuheng Zou, Yujia He, Yunfan Xiong, Yuxiang Luo, Yuxiang You, Yuxuan Liu, Yuyang Zhou, Y. X. Zhu, Yanhong Xu, Yanping Huang, Yaohui Li, Yi Zheng, Yuchen Zhu, Yunxian Ma, Ying Tang, Yukun Zha, Yuting Yan, Z. Z. Ren, Zehui Ren, Zhangli Sha, Zhe Fu, Zhean Xu, Zhenda Xie, Zhengyan Zhang, Zhewen Hao, Zhicheng Ma, Zhigang Yan, Zhiyu Wu, Zihui Gu, Zijia Zhu, Zijun Liu, Zilin Li, Ziwei Xie, Ziyang Song, Zizheng Pan. Zhen Huang, Zhipeng Xu, Zhongyu Zhang, and Zhen Zhang. DeepSeek-RI: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning, January 2025. URL http: /ttp:///axxiv.o org wtwpg/abs//5a00 wws.////............. 12948 arXiv:2501.12948 [es].
Gemini team. Advanced version of gemini with deep think officially achieves gold medal standard at the international mathematical olympiad. URL: http:://eeemmttt.ooogg//////oo//
Blog
post, July 2025.
delanced-versionn of gemini -tt.a:aawwatrrgeeeee-ooooooooaaa
-oress-oolll goldd - standard
Dongyoung Go, Tomasz Korbak, Germán Kruszewski, Jos Rozen, Nahyeon Ryu, and Marc Dymet-
man. Aligning Language Models with Preferences through f-divergence Minimization, June
2023. URL (RLpttpp//aaxxx>
orgoorgg///sss /230g C8215 arXiv:2302.08215 [cs].
Andre He, Daniel Fried, and Sean Welleck. Rewarding the Unlikely: Lifting GRPO Be- yond Distribution Sharpening, June 2025. URL http::///xxxv.oo///////
02355
arXiv:2506.0233 [cs].
E. Hellinger. Neue Begründung der Theorie quadratischer Formen unendlichvielen Veränderlichen. Journal für die reine und angewandte Mathematik, 1909(136::10-271) July 1909. ISSN 1435-5345, 4075-4102 doi:
URL https:: 1909..........11 136. 210 0/html
degruyter.comm wtw.tterrcoomeooo wtt.c/////ww.c/cc/tc//coc /tt///o///00/
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring Mathematical Problem Solving With the MATH Dataset, November 2021. URL
03874 arXiv:2103.0387 [cs].
Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. The Curious Case of Neural Text Degeneration. arXiv:I90 1904.09757) [cs], February 2020. htL::tt::// httt:::/aaxxv..or//aa....
1904. 09751
arXiv: 1904.09751.
Ferene Huszár. How (not) Train your Generative Model: Scheduled Sampling, Likelihood, Adver- sary?, November 2015. URL [stat].
arXiv:1511.05101
B. Kappen, V. Gomez, and M. Opper. Optimal control as graphical model inference prob- lem. Machine Learning, 87(2):159 182, May 2012. ISSN 0885-6125, 1573-0565. doi: 10. 1007//10944-22-577---7 URL http:::://axxiv..rr.oom [math].
0633 arXiv:0901.0633
Muhammad Khalifa, Hady Elsahar, and Mare Dymetman. Distributional Approach to Controlled Text Generation, May 2021. URL http:///axxv..oog//b//////0///// arXiv:2012.1 1635 [es].
Minbeom Kim, Thibaut Thonet, Jos Rozen, Hwaran Lee, Kyomin Jung, and Mare Dymetman. Guaranteed Generation from Large Language Models, July 2025. PRLattp:: //arxii////v.....//aa org/ abs/2410 2410 06716 arXiv:2410.067 [es].
13

---

Published as a conference paper at ICLR 2026
Robert Kirk, Ishita Mediratta, Christoforos Nalmpantis, Jelena Luketina, Eric Hambro, and Edward Grefenstette. Understanding the Effects of RLHF on LLM Generalisation and Diversity. 2024.
Wouter Kool. Buy 4 REINFORCE Samples, Get Baseline for Free!, July 2019. URL https:
Tomasz Korbak, Hady Elsahar, German Kruszewski, and Marc Dymetman. Controlling Conditional Language Models without Catastrophic Forgetting, June 2022a. URL httt:://axxiv.a.////////////
abs/2112. 001 arXiv:2112.00791 [cs].
Tomasz Korbak, Hady Elsahar. Germán Kruszewski, and Mare Dymetman. On Reinforce- ment Learning and Distribution Matching for Fine-Tuning Language Models with no Catas- trophic Forgetting, November 2022b. URL httt:://are org/ wwtp://////a///eeee 00761 arXiv:2206.00761 [cs].
Nathan Lambert, Jacob Morrison, Valentina Pyatkin, Shengyi Huang, Hamish Ivison, Faeze Brah- man, Lester James V. Miranda, Alisa Liu, Nouha Dziri, Shane Lyu, Yuling Gu, Saumya Ma- lik, Victoria Graf, Jena D. Hwang, Jiangjiang Yang, Ronan Le Bras, Oyvind Tafjord, Chris Wilhelm, Luca Soldaini, Noah A. Smith, Yizhong Wang, Pradeep Dasigi, and Hannaneh Ha- jishirzi. Tulu 3: Pushing Frontiers in Open Language Model Post- Training, April 2025. URL arXiv:2411. [cs].
http: / arwiv.iivvvv./.../ org/ hale/abs//// htts//211..111111
Guillaume Lample, Timothee Lacroix, Marie anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril. Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Ad- vances Neural Information Processing Systems, 2022. URL httttttss///peeeeeeeee 24
net/
Cheuk Ting Li and Farzan Farnia. Mode-Seeking Divergences: Theory and Applications to GANs. In Proceedings of The 26th International Conference on Artificial Intelligence and Statistics, pp. 8321-8350 PMLR, April 2023. URL ISSN: 2640-3498.
ngs. mlr wwwps//2sss...
Ling-1i23al html
Long Li, Jiaran Hao, Jason Klein Liu, Zhijian Zhou, Xiaoyu Tan, Wei Chu, Zhe Wang. Shirui Pan, Chao Qu, and Yuan Qi. The Choice of Divergence: Neglected Key to Mitigating Diversity Collapse in Reinforcement Learning with Verifiable Reward, September 2025. URL http:
0000//2309000000 arXiv:2509.07430 [cs] version: 1.
Yingzhen Li and Yarin Gal. Dropout inference in bayesian neural networks with alpha-divergences, 2017. /Rl//ttss//arxvv..cr///bb///////
02914
Ziniu Li, Tian Xu, Yushun Zhang, Zhihang Lin, Yang Yu, Ruoyu Sun, and Zhi-Quan Luo. ReMax: A Simple, Effective, and Efficient Reinforcement Learning Method for Aligning Large Language Models, May 2024. /ttp:tttt///xxxi.. org/ abs/ 2310 O. 10505 arXiv:2310. 1055055 [cs].
Friedrich Liese and Igor Vajda. On divergences and informations in statistics and information theory. IEEE Transactions on Information Theory, 52(10):43944442, 2006. doi: 10.1109/TT1.2066.
881731.
Zichen Liu, Changyu Chen, Wenjun Li, Penghui Qi, Tianyu Pang, Chao Du Wee Sun Lee, and
Min Lin. Understanding rl- rl-zero-like training: A critical perspective. In Conference on Language Modeling (COLM), 2025.
Mistral-AI, Abhinav Rastogi, Albert Q. Jiang, Andy Lo, Gabrielle Berrada, Guillaume Lample, Jason Rute, Joep Barmentlo, Karmesh Yaday, Kartik Khandelwal, Khyathi Raghavi Chandu, Léonard Blier, Lucile Saulnier, Matthieu Dinot, Maxime Darrin, Neha Gupta, Roman Soletskyi, Sagar Vaze, Teven Le Scao, Yihan Wang, Adam Yang, Alexander H. Liu, Alexandre Sablay- rolles, Amélie Héliou, Amélie Martin, Andy Ehrenberg, Anmol Agarwal, Antoine Roux, Arthur Darcet, Arthur Mensch, Baptiste Bout, Baptiste Rozière, Baudouin De Monicault, Chris Bam- ford, Christian Wallenwein. Christophe Renaudin, Clémence Lanfranchi, Darius Dabert, Devon Mizelle, Diego de las Casas, Elliot -hane-Sane, Emilien Fugier, Emma Bou Hanna, Gauthier Delerce, Gauthier Guinet, Georgii Novikov, Guillaume Martin, Himanshu Jaju, Jan Ludziejewski,
14

---

Published as a conference paper at ICLR 2026
Chabran, Jean-Malo Delignon, Joachim Studnia, Jonas Amar, Josselin Somerville Roberts, Julien Denize, Karan Saxena, Kush Jain, Lingxiao Zhao, Louis Martin, Luyu Gao, Lélio Renard Lavaud, Marie Pellat, Mathilde Guillaumin, Mathis Felardos, Maximilian Augustin, Mickaël Seznec, Nikhil Raghuraman, Olivier Duchenne, Patricia Wang, Patrick von Platen, Pa- tryk Saffer, Paul Jacob, Paul Wambergue, Paula Kurylowicz, Pavankumar Reddy Muddireddy, Philomène Chagniot, Pierre Stock, Pravesh Agrawal, Romain Sauvestre, Rémi Delacourt, San- chit Gandhi, Sandeep Subramanian, Shashwat Dalal, Siddharth Gandhi, Soham Ghosh, Srijan Mishra, Sumukh Aithal, Szymon Antoniak, Thibault Schueller, Thibaut Lavril, Thomas Robert, Thomas Wang. Timothée Lacroix, Valeriia Nemychnikova, Victor Paltz, Virgile Richard, Wen- Ding Li, William Marshall, Xuanyu Zhang, and Yunhao Tang. Magistral, June 2025. URL http://wwwrrabb//...b/b /2066 10910 arXiv:2506.109) 10910 [es].
Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer-Verlag Berlin, Heidelberg, 2002. ISBN 3540433767.
Art B Owen. Importance Sampling. In Monte Carlo theory, methods and examples. Chapter 9,
2013. BRK_sttpp://statwebbbo wtt.::awwtttt..t.t.t.a.aaaoo.eee www/w/ww./wwnn.eeeo mc Saaee/hhvvaa-aaa pdf
Laura O' Mahonyy Leo Grinsztajn, Hailey Schoelkopf, and Stella Biderman, ATTRIBUTING MODE COLLAPSE IN THE FINE-TUNING OF LARGE LANGUAGE MODELS. 2024.
Tetiana Parshakova, Jean-Mare Andreoli, and Mare Dymetman. Distributional Reinforcement Learning for Energy-Bases Sequential Models, December 2019. URL http::t/xxx...rrgggg
abs/ /1912. 08517 arXiv: 191.08911 [cs].
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya
Sutskever. Formal mathematics statement curriculum learning. The Eleventh International Conference Learning Representations, 2023. URL httpt:ps///ppenevieee.... net. net/oruummmt/ forum?
SGs-P7GG-ddShh
Yury Polyanskiy and Yihong Wu. Information Theory: From Coding to Learning. Cambridge University Press, 2025. ISBN 978-11088322
Penghui Qi, Zichen Liu, Xiangxin Zhou, Tianyu Pang. Chao Du, Wee Sun Lee, and Min Lin. De- feating the Training-Infeer Inference Mismatch via FP16, October 2025. Utt::t/p//aaxxx org/ abs/ 2t//25100 0. 2688 arXiv:2510.26788 [es].
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. keepseek-prover--22 Advancing for- mal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025. URL
https://arxt:
wtgg/bss.... 2504 21801
Alfréd Rényi On Measures of Entropy and Information. In Proceedings of the Fourth Berkeley Symposium on Mathematical Statistics and Probabiliry, Volume 1: Con- tributions to the Theory of Statistics, volume 4.1, pp. 547-562, University of Cal- Press, January 1961. ifomia
URL htt.a/////ooooeeeeeeeeoooooaaaaa
wtt.sttitttssiait...... chapter/On Meaarrrr--eeassesseee of of anwppy--an-----eeee wnd hat.aroyyya..aaaaaaaaaaaaoaaoona
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal Pol- icy Optimization Algorithms, August 2017. arXiv:1707.06347 [cs].
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models, April 2024. URL TRLLattt://aaaa http:://xxxvvo//////
2402. 03300 arXiv:2402.0330M [es].
Guangming Sheng, Chi Zhang, Zilingfeng Ye, Xibin Wu, Wang Zhang, Ru Zhang, Yanghua Peng, Haibin Lin, and Chuan Wu. Hybridflow: A flexible and efficient rlhf framework. arXiv preprint arXiv: 2409. 19256, 2024.
15

---

Published as a conference paper at ICLR 2026
Haoxiang Sun, Yingqian Min, Zhipeng Chen, Wayne Xin Zhao, Lei Fang, Zheng Liu, Zhongyuan Wang, and Ji-Rong Wen. Challenging the Boundaries of Reasoning: An Olympiad-Lever Math Benchmark for Large Language Models, May 2025. Utthttp: wtw.a//rrgabbb/////// 21380 MrXiv:2503.2136 [es] version: 2.
Richard S. Sutton and Andrew Barto. Reinforcement learning: an introduction. Adaptive computa- tion and machine learning. The MIT Press, Cambridge, Massachusetts London, England, second edition edition, 2020. ISBN 978-0-262-03922-6.
Richard Sutton, David McAllester, Satinder Singh, and Yishay Mansour. Policy Gra- dient Methods for Reinforcement Learning with Function Approximation. In Ad-
vances Neural Information Processing Systems, volume 12. MIT Press, 1999. URL
wttp::tt.w......pcppceeeeeeeeee. 6568222883000338900000333311b0.3 www.:sofoo-bttttt.ta..a.aaao html
Yunhao Tang, Kunhao Zheng, Gabriel Synnaeve, and Remi Munos. Optimizing language mod- els for inference time objectives using reinforcement learning. In Forty-second International Conference on Machine Learning, 2025. URL https::////// hattps://operreviww wtw.:eewweeefffooreeee 2VWJ05YTZ4
Terence Tao. Micchine-assiseee proof. Notices of the American Mathematical Society, 72:1, 01 2025. doi: 10. n0.10
Emanuel Todorov. Linearly-solvable
In Advances in Neural Information Processing Systems, volume 19. MIT Press, 2006.
Markov decision problems.
URL
https: httt:s:/ppapers.ntte wttp:/ss.iips..cppppppeppppp
co/paper files/ httss/pppr/220//aas..
d 4B00allaa349aff2aeeeeeeecceeee Abstract.............. html
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, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang. Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang. Zhengying Liu, and Jia Li. Kimina-prover preview: Towards large formal reasoning models with reinforce- ment learning, 2025. URL htt.hhtss:///xiiiiie /ttp://aavvve/ee//ee//eeeeeaeeee org/ abs 2504 11354
Ronald J. Williams. Simple statistical gradient algorithms for connectionist reinforce- ment learning. Machine Learming, 8(3):229-256, May 1992. ISSN 1573-0565. doi: 10.1007/ BF00992696.
1007 1000///000000//0009226559
Fang Wu, Weihao Xuan, Ximing Lu, Mingjie Liu, Yi Dong, Zaid Harchaoui, and Yejin Choi. The Invisible Leash: Why RLVR May or May Not Escape Its Origin, September 2025. http::
arXiv:2507.1488 [cs].
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang. Dahua Lin, and Kai Chen. Internlm2.5 stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems, 2024. URL httpt:tt///aaatt www.lvoorrgaaaae abs///a///// aataabb//1.... 15700
Huajian Xin, Z.Z. Ren, Junxiao Song. Zhihong Shao, Wanjia Zhao. Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. Deepseck-prover-.e 1.:: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. The Thirteenth International Conference Learning Representations, 2025. URLhttps:: URL/https:/oppeeevvee opp.revieeeeeeeeeeeeeeeeee net forum?
Hid=I4YAIree
Huaiyuan Ying, Zijian WU, Yihan Geng, Jayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. In The Thirty- eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024. URL htt.ttttp///ppeee
net. wew.rorwmmmmm.ww.wwar jHDb
16

---

Published as a conference paper at ICLR 2026
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, Jinhua Zhu, Jiaze Chen, Jiangjie Chen, Chengyi Wang, Hongli Yu, Weinan Dai, Yuxuan Song, Xiangpeng Wei, Hao Zhou, Jingjing Liu, Wei Ying Ma, Ya-Qin Zhang. Lin Yan, Mu Qiao, Yonghui Wu, and Mingxuan Wang. DAPO: An Open- Source LLM Reinforcement Learning System at Scale, March 2025. URL http: //stpi arXiv:2503. 14476 [cs] version: 1.
org/abs 2503. 14476
Zheng Yuan, Hongyi Yuan, Chengpeng Li, Guanting Dong, Keming Lu, Chuanqi Tan, Chang Zhou, and Jingren Zhou. Scaling Relationship on Learning Mathematical Reasoning with Large Language Models, September 2023. URI. httt:://aaaxe.. http:///aaaww...o/aa///////ss/// arXiv:2308.0 0000000082550 [es].
Yang Yue, Zhiqi Chen, Rui Lu, Andrew Zhao. Zhaokai Wang, Yang Yue, Shiji Song, and Gao Huang. Does reinforcement learning really incentivize reasoning capacity Ilms beyond the base model? arXiv preprint arXiv:2504. 13837, 2025a.
Yang Yue. Zhiqi Chen, Rui Lu, Andrew Zhao, Zhaokai Wang, Yang Yue, Shiji Song, and Gao Huang. Does Reinforcement Learning Really Incentivize Reasoning Capacity in LLMs Beyond the Base Model?, May 2025b. URL http::/ /ttp:///arxvv http::://axxvvoo/g////// www.orgg/bbbar/oeeee 13837 arXiv:2504. 13837 [es].
Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah D. Goodman. STaR: Bootstrapping Reasoning With Reasoning, May 2022. URL [cs].
2tbb//20033 14465. arXiv:2203.14465
Xinyu Zhu, Mengzhou Xia, Zhepei Wei, Wei-Lin Chen, Danqi Chen, and Yu Meng. The surprising effectiveness of negative reinforcement in Iim reasoning. arXiv preprint arXiv:2506.013477 2025.
Daniel M. Ziegler, Nisan Stiennon, Jeffrey Wu, Tom B. Brown, Alec Radford, Dario Amodei, Paul Christiano, and Geoffrey Irving. Fine-Tuming Language Models from Human Preferences, Jan- uary 2020. URL http:://axxiv.orr/aa/////////
08593 1rXiv:190..0859) [cs].
A LLM USAGE
We have required the assistance from LLMs (ChatGPT, Gemini) in the production of this paper on many stages during its development. The most prevalent usage has been on writing code and debugging, but we have also discussed research directions and mathematical statements, used them to simplify and format mathematical proofs, proof-reading of the paper and improving the flow of the text, and they even assisted us in producing the cartoon illustrating our method. The authors take full responsibility for the contents in this paper.
B PROOF OF THE CORRESPONDENCE BETWEEN RLVR AND REVERSE KL
We work in the contextual setting where contexts x are drawn from p(z),, the policy is To(y | x), the reward is v(y, æ), and the prior (reference policy) Tref(y x)). Define for each context ar and inverse temperature 3 > 0
(v)
Zz( Trer(y
1
=))(v()x))88)
Za(3)
Σ Trorly x) exp(v(1,xx/0)
Fix context x. The reverse KL divergence (from To(. xx) to pr,e) is
Ps.s) = Bymr log To ax) pr)
<-( x))
Substituting Pa,s(v) (v) = Z. (y (v.2/)) gives
KI(TolPPo.o) E Bynsr
Toy x)) log
1 Z=(3) Zroo Fror( =())
To(y [x) 1
Bynss
log
Treel (y) x) u(y,,) log (3).
17

---

Published as a conference paper at ICLR 2026
Equivalently (rearranging signs).
To x)
[L TT 1P2,8)
Bynna 3 uly. x) log
+ log (z))).
Trel (y x))
Now take the gradient with respect to 0 and average over contexts x ~ μ.. Since (g) depends only on rref and (not on 0), Ve log Z. O. Thus
B (l(,,) - log To x) Tee (y/ x))
Vo Eazny KT [Tolll)) Vo Beza By-no(ll)
To proceed we use the score-function (REINFORCE) identity: for any function h(y, x)) independent of 0,
Vo (y =>] (-) (h(,, Vo log to =)]
Applying this identity (and noting the dependence of the log गH term must be handled consistently) yields the explicit gradient form
Va E Eznp (KL(TTllPa.S)) = Baen E By-ro(((a)) [ - log
To (y x)) Tret (y x))
V log To xx)
(18)
This is the standard oolicy-gradien// / score-function expression for the gradient of the reverse-Ki KL objective in the contextual case.
Finally, an equivalent compact form is obtained by moving the Va inside the expectation and notic- ing the factor 1/3:
To x))
Vo Eg [L
B Vo E Eawy, yozza u(y. x) - 99 log
Teet (y x))
Maximizing the expected reward under the conditional policy:
B (e.gr--(l((,,a)) Blog To(y x) Tret (3/ x)
is equivalent (up constants) to minimizing:
Ezep(() [DKI((TOC) w)) |l Pa,a(y x))]
C PROOF THAT P3 BECOMES p 3 0
Proposition 1.
lim Pz.0 = Pas B 8-50
(19)
in the formal sense that || Pa PalITV a $ O. In particular Pv,o(y) Pa(y) for every fixed
Proof. The proof is a direct adaptation, for a context x, of the following Lemma.
Lemma 3. Let Thase be a probability distribution countable set Y, let Y - {0, 1} and
assume % = En Toase (y)r()) E (0, 1]. Define
p(y) Abase (v)r(v)
Po(u)= Tbase (a)as(()e (1))
Zg
Σ Tbase (w1/8
ZB
Then [|pa -pllTv - 0 as B O. In particular pa (v) - p(v) for every fixed y E Y.
18

---

Published as a conference paper at ICLR 2026
Proof. Set Su Er())= (baee Z and e- e - Z). A short computation gives ZB = el/B2 Z + So and hence, after multiplying numerator and denominator by e1//8
bbsse (v)
r(y) 1,
+ Thase (3)
p>(y)
1/8
r(y) =
Z +
Therefore
Σ (ps(v) - p(v)
E Z +
ps(y) - p(y) = E
Z 7+
=1
r(y)=0
2c and
so Ey (ps()) - -((u) =
llpo p||TV
Σ 2
1
(P(())
p(y)
e e-1/8(1-) -I-
Z E
Z+e e 118
Z)
Since e11/8 + 0 as 4. O, the right-hand side tends to proving total-variation convergence. The
pointwise pointwisecoonverg convergence py(y) + p(y) follows immediately because (ps(v) -p(y) < Ey (p((')
p(y/1 = 2||p3 - pllTv.
D RS-FT OPTIMIZES THE FORWARD KL
Rejection sampling fine tuning Zelikman et al. 2022 Yuan al. 2023) generates a sample set from the base model Misse S ~ base (-1z). filters them using the verifier to obtain S {y v(y,
1, y/ E S), and then trains the policy using standard cross-entropy on this filtered set:
RS-FT = Eyyss Vo log To To(((x))
(20)
Now, starting from KL-DPG, we note that:
Pa(y)
-1)
V VoDKL(PelITO) = - Eynaao (+1a)
Vo log log
(21)
TT(y)
P=(v)
Eywaoo (s1xz)
Ve log (v(lx)
(22)
Te Te( (z)
-- Reyaaol- T basse (2/x²)
Ps (v)
Vo log To(lx>)
(23)
Tuuse (2)(z) (b)
De (v)
--yymmoul (-1n)
V log (y(l)>)
(24)
Tbasc
Those (y) 2 ( Vo log (o(y)>)
7, B (yy
(25)
Thase (yl (r)
(-y uly 2:) Vo log (o(
(26)
which exactly corresponds the objective in Eq. 20 There two erucial differences between the two: One is their sample efficiency: whereas RS-FT is limited to using samples from the base model. many which may be rejected from the verifier, KL-DPG makes use the updated policy
which has higher acceptance rate. The second one is that whereas RS-FT uses finite pool of samples, and thus can over-fit them, KL-DPG uses an unbounded number of samples.
E ESTIMATION OF THE PARTITION FUNCTION
Define
(v( buse (b) (u),))((,,)) x:).
(27)
19

---

Published as a conference paper at ICLR 2026
discrete space V, with partition function Z
Zx = Σ Pa(y).
(28)
BEV
Using importance sampling (Owen 2013 we can estimate Ze by using samples [VilsE(o...N) generated from proposal distribution with Supp(P) S Supp(q), as follows.
Z Σ PL(V) Σ NEY
(v(a) (yya
Pa (v) Byra( (m) q(1/2))
Pz(U)
1
Σ (u(
(29)
N
q(3) (x)
Note that in the specific case that use o T. buse: then
2e E (1)x)(1xx)
Tbase (y a (z)) x))
E Byyatt (x)
Σ e(y,,z). N
1
(30)
Thase (3) (r)
E. ABLATION EXPERIMENT: ROLE OF PARTITION FUNCTION CALCULATION
To analyze whether more precise calculation of the partition function affects the results, we com- pared the reported results using an online- computed partition function based on just sampled re- sponses with pre-computed partition function using 128 samples from the base model. The results are displayed on Fig. 5 showing no clear advantage for pre-computing the partition function. As result, we favored the online computation as it offers drop-in replacement for GRPO and other similar variants without any additional computational burden.
Feddbor (hang
Figure 5: Comparison of a-DPG with Z. computed online on the basis of just samples per problem versus using 128 samples to compute the partition function offline.
F ADDITIONAL EXPERIMENTAL DETAILS AND HYPERPARAMETERS
20

---

Published as a conference paper at ICLR 2026
Method
Learning Rate
Batch Size
Rollout Size (N)
KI. Penalty
@ass@k
1 X 10 6
16
32
0.001
Rwrd. Unlkly (rank plty=0.25)
10 6
16
32
0.001
Dr. GRPO
2 x 10-6
128
4
0.0
RLOO
2 10
128
4
0.0
GPG
2 10-6
128
4
0.0
ReMax
2 x 10-6
128
4
0.0
Dr. GRPO with High KL.
2 x 10
128
4
0.1
a-DPG
10
128
4
Table 2: Summary of key hyper parameters for different training runs.
Figure 6: Training curves of both a-DPG and dr-GRPO, Sequence entropy on the right and reward on the left
Figure 7: Training curves of a- D-D for various alpha values. Sequence entropy on the right and reward on the left. (Truncated curves are runs that have been stopped and resumed)
Aw
Figure 8: Training curves various dr-grpo baselines (dr-grpo, thigh KL, +entropy). Sequence en- tropy on the right and reward on the left. (Truncated curves are runs that have been stopped and resumed
G ADDITIONAL EXPERIMENTAL RESULTS
21

---

Published as a conference paper at ICLR 2026
12
Figure 9: Problem Difficulty Transition Matrix from the Base-SFT to GRPO. The matrix shows the number of problems that transition from an initial difficulty classification under the base model (Base-SFT) (y-axis) to a final classification after post-training (x-axis).
0000
3100
-30
+3677
+141
TWOBLD
-15
450
-24
-15
-35
Bole
493
+137
-3
-1.
415
430
+35
35
430
+11
420
420
-14
400
1363
1157
K1.
23
12.3
TERBLE
(1883
430
-35
455
-43
<22
+68
43
31
43
.13
43
423
459
438
440
443
435
40
mockimatte m)
100
1126
410
34
143
4M
11
MARLS
130
115
100
115
100
a (klloaenn))
194
1164
191
131
164
165
154
164
WA815
a3K0nat X5
4361
4181
453
411
444
435
413
48
433
J10
45
-3
450
434
453
415
200
400
3 639
+156
441
Table 3: Pairwise performance comparison. Diagonal: Absolute Pass@1 / Pass 256 scores (%).
Upper Triangle: Pass 256 differences (Row Column). Lower Triangle: Pass @1 differences (Row Column). Bold indicates statistical significance (p < 0.05) via paired bootstrap.
22

---

Published as a conference paper at ICLR 2026
Premise Diversity (Simpson Index) vs Model Passgk
Tactic eiversity (Simpson Index) vs Model Passgg
431
540
340
0/1
Paries hrw Inde
PM
Premise Diversity (Shamen Entropy) Model Passerk
Tactic Diversity (Shannon Model Passigk
Lie Aguusstaco
Sharsee Extryy
Teclk Swwventrecy
Figure 10: Diversity index vs Pass
Premise Simpson Index
Tactic Simpson Index
Tactic Entropy Index
Premise Entropy Index
pass 6P556
pass
Model
Base SPT
0.884013
0.793399
2.814039
4.138613
0,865000
0.553008
HRPPOPPss@k
0,893146
0.793183
2. 2.840828
4,271897
0.875000
0.558867
GRPO
0.608813
0.558731
1 1.641007
2.597491
0.810000
0,700332
GRPO KL.
0,867052
0.775942
2. 2.665062
3.936221
0.870000
0.607383
GRPO-Rw-Ulliy
0,794
0.6865 14
2.1 1227
3,231985
0.860000
0
ReMax
0.712695
0.6142204
1.861515
2.920214
0.845000
0.695762
RLOO
0,651459
0.557749
1 1.614147
24482766
0.815000
0.705332
GPG
0.670303
0,550061
1 1.607887
2.538284
0,810000
0,718320
o-DPG (o=0)
0.775301
2.63658
3899748
0.800000
0.617969
a-DPG (o=0.25)
0. 0.864668
0.776839
2 2.655524
3.873548
0.855000
0.620527
DDDPG(o-0.5
0,864517
0.770372
2 11666779
3,855339
0,860000
0.6280066
D.
0,849480
0.759164
2.519318
3.678993
0,865000
0.647949
PD-PG(n-03
0,8261 29
0.735853
2. 344282
3.433220
0. 06000000
0.670332
a-DPG (u=0.95)
0,795030
0.699298
2.144001
3,191290
0.845000
0.686562
(o=0.66
0.792300
0.670038
2.035
355578
0,860000
0.696621
a-DPG
0.731704
0.635556
884774
2.848510 16
0,815000
0,703691
a-DPG (o=0.98)
0.635610
2.881272
0.835000
0.697891
a-DPG (o=0.99)
0.718106
0.584643
1 1.99220
2.735522
0,825000
0.706055
a-DPG (o5).995)
0.683162
0,554934
1 1.603550
2,593344
0.825000
0,720449
a-DPG (o-7..997)
0,702118
0.584954
6633736
2.687643
0,835000
0.722520
o.DPG (a=0.999)
0.662599
0.546542
1.573962
2.536636
0.815000
0,717402
Table 4: Diversity and performance metrics across models. For each problem statement, we evaluate 256 generated proof sequences. At every proof state, compute the Simpson Index (SI) and Shannon entropy over both tactic choices and premise selections. The metrics are then aggregated across all problems to capture the overall diversity of candidate sequences. Higher diversity in tactics and premises generally correlates with improved pass@ 256 performance.
23

---

Published as a conference paper at ICLR 2026
H FORMAL COMPLEMENTS ON a-DIVERGENCE
H.1 SMOOTHNESS OF G-DIVERGENCE, BEHAVIOUR FOR + 0 AND a +
The fact that Dy. (T, p) a continuous function of and that it converges the forward K K for a - 0 and to the reverse ([pp])p) for - 1 including cases where these KL-divergences may be infinite - is well-known in the literature, e.g. Cichocki & Amari (2010).
In our specific situation, while typically the autoregressive policy is full-support (T(y) >> 0, Vy E V). the support 4 = {y p(y) > 0} of p is a proper subset of V. In such cases, while (L [)] is (typically) finite KL ((T((plp) is infinite.
H.2 COMPARING DIFFERENT POLICIES, ILLUSTRATION
In order to provide "non gradient" interpretation of what happens at the edges, it is instructive to compare D (T.,) with D,, (æ', p) for different candidate policies π and x².
Illustration We provide an illustration in Fig. on toy example with small finite sample space V. with A Ç y; and with three policies. The policy is more "covering" than Te and m3. with lower forward K (pl IT), but
less "focussed" on the valid region A than either IT or T3+ which are both concentrated on A (with 22 (A) (A) 0.9), but with different peaks. Despite the fact that the reverse KTL [=(=lbb [=]pp) is infinite for the three policies, the divergences, for a close to 1 while large (and tending to infinity) than D,, (T3,P). which in turn is slightly higher than Ds_ (TT.
still show a clear order, with Dj, (T1.P) much higher
More in detail, we consider the discrete space y {ui, 1/2 Ja over which the base model Those has an (almost) uniform distribution Thase = (0.33, 0.34, 0.33), and where the binary verifier v(y) takes the values (1, 0, 1), i.e. accepts y1 and y/3 and rejects 1/- This results in the target distribution:
(0.5, 0, 0.5).
We study three alternative policies, with distributions:
Ji = Tasse = (0.33, 0.34, 0.33), T2 = (0.8, 0.1, 0.1),
Ty = (c, 0.1, 1-
taking e = 0.01. ni is the more diverse/covering of the three, but has some significant mass on the invalid point y2, while π2 and F3 waste less mass the invalid point, and are peaky the first point and the third point respectively, even more so for 73-
The endpoints recover the forward and reverse KL divergences:
lim D (T|pp) KL(PlIT), a-1
lim Dj. (Tllp) KL(T]lp),
where we adopt the usual conventions that (p[l) = +oo whenever p charges a point on which vanishes, and similarly for KL(TTIp)
In our setting, p(y2) = while each म, assigns positive mass to y2, so (T.(T:llp) +00 for
i == 1,2,3.
Numerical values. Table reports Dy, (TillP) for a range of representative a values, including the limiting cases a = 0 and 1.
Curves as function of Figure 11 shows the curves + Dy (mell)) for 1, on (0, 1).
On the left of the plot, with at O, we see that TT which is the more diverse/covering of the three relative to p. has the lowest value of forward KL, K (p, т), while Æ3. which is even more "peaky" than T2 has larger forward KL. On the right of the plot, with tending to 1, the divergences all tend to infinity, but their order stabilizes, with the divergence of Tı getting and staying much larger
In some "pathological" situations, and for an infinite sample space Y, K KT. (q) can he infinite even when the supports coincide.
24

---

Published as a conference paper at ICLR 2026
Distribution
->
a = 0.1
a 0.5
a 0.7
a
0.9
0.99
at -
T1 (0.33, 0.34, 0.33)
0.4155
0,4522
0.7504
1.2018
3,4666
34.0658
00
22 (0.8, 0.1, 0.1) 3 = (0.01, 0.1, 0.89)
0.5697
0.5585
0.5758
0.6816
1.3252
10.3160
1.6677
1,4693
1.0488
1.1827
1.7766
10.5828
00
Table 5: Values of Dy, (T<llp) for p (0.5, 0, 0.5) and #i, 72, #3 selected a values. For -+ and a + 1 we recover the forward and reverse KL divergences, respectively.
than both those of i22 and T3- we will see in Theorem [ and equation 32 below, the relative behaviour of the policies for close to 1 is determined predominantly by their relative values of π (A), and here, with 72 (A) = (A) = 0.9 > (A) 0.66, т "loses" relative to #2 and mT. For two policies, such T2, Ts. which have exactly the same "valid" mass, their order is determined by a secondary term, the one appearing to the right of '+' in equation 32
[m, with 0.01
2.00
1.25
1.00
0.50
RL-(0.33.034.033)
0.25
R,-(0.,0.1.
m...de.01... 0.1.6.00...--9)
0.00
Figure 11: The divergence D,, (T. for Tl (0.33, 0.34, 0.33), T2 (0.8,0.1,0.1) and n3 (e, 0.1, -) with 5 = 0.01.
H.3 A DECOMPOSITION THEOREM FOR THE O-DIVERGENCE FOR TARGETS WITH PARTIAL. SUPPORT
We now state useful (and apparently novel) result, which permits better understanding of what happens in the situation where the support A of the target p is strictly contained in the support of the model æ. This result says that, with (AA) the mass of A, and with æ the "renormalization" of to A. that is, (2)
(tv)/((A) for y E A. and for E (0, 1), we have the identity D (T. p) 1-x(4)- a(I-a) + 7 (A) (T..P).
This identity especially interesting for the case of a tending to In that case, with æ full support and a (AA) 1, the support of π is equal to the support of and therefore D,,, (TA p) tends to finite value KL p). and the second term of the identity tends towards a finite value. On the other hand, the first term tends to infinity at rate closer and closer to 1-=(4) meaning that n (A) > r'(A) I-a
implies that the divergence of π becomes and stays lower than the divergence of x' after a certain point ag-
In other words, when A is the subset of y for which the binary reward v(y) is equal to 1, and for sufficiently close to 1, minimizing Dj, (Te.) p) is essentially equivalent to maximizing En, u(y), the same objective pure REINFORCE.
FORMAL RESULT: THE SUPPORT DECOMPOSITION OF a-DIVERGENCE
Let π and p be probability distributions on a countable sample space Y. We consider the a- divergence defined by the generator function fa (t) ('-at((1-a) for (0, 1).
a(a-1)
25

---

Published as a conference paper at ICLR 2026
First, we establish the algebraic relationship between the divergence and the "Hellinger sum" (the discrete counterpart to the Hellinger integral (Liese & Vajda 2006), see also Appendix of (Li & Gal 2017)).
Lemma (Connection to Hellinger sum), Leta E (0, Ler A = supp(p) CY. The a-divergence satisfies:
1 1- (a.
D1a (T.
(31)
a(l-a)
where Ha( = Ewer p(y)) - is the Hellinger sum. This holds even if sup((()) g A.
Proof. We use the extended definition of -diivergence (Polynnkky & Wu 2025) which includes the boundary term for the set where p(y) but rty) O. Let A Y and let x(A)) be the "leakage" mass.
(x(()) p(y)
Ds (T.P)
Σ ply)
f2(( T(AA).
yE
1. The Boundary Term: The term to the right uses the constant (a(()) = -lim fa(t//t. For
1, t-- so: fa (00)
a(a-1) I-a See also Table
The Sum on Support A: Note that EyE T(V) = and Eyea p(y) =1
(t)
Eply)f.
Σ
T(y 1-a a(1 6) (1 aa)
p(u)
ala - 1)
yEA
UEE
[Ha(T,p) 1 ace.
a(a 1)
3. Combination: Adding the boundary term: Boundary 1-a a(a-1)" cancel perfectly:
The terms involving
Dj, (T, p) Ha(
aE
1- Ha (T,P)
ala -
a(1 aa)
Using Lemma 4 now derive the main decomposition theorem.
Theorem (Support Decomposition). Assume that A = supp(p) is strictly included in supp(r).
Let T be the renormalization of A, i.e., (T( T(v) (A) A) for y A, or, equivalently T (y) = A). The divergence decomposes as:
1- (AA)a a(1 0))
Din (T.P)
+ (A)= Dr (TA.P)
(32)
Shape Divergence
Leakage Penalty
Proof.
Since p(y) = 0 for & A, the Hellinger sum restricts to A. Substituting =(v) + (A)TA()):
H. (T. = Σ (T)))TA())) p(u)2-a = Ha
yEA
From Lemma 4 we have Ha (TA.P) = - a(1 - (.) Substituting this back into the
global divergence formula:
1- π (T..H.
Di, (T,
a(1 a)
- (AA) [1 a(1 - -01--a)D (TA.) a(1 aa)
1- ((A)
+ (AA) (TA.P).
a(1 a)
26

---

Published as a conference paper at ICLR 2026
CONSEQUENCES FOR FIXED TARGET p
We analyze the case where π has full support and has strictly partial support A. Remark (Limit a + The Strong Constraint). As a - 1, Dra converges to the Reverse KL divergence DKL(T) (T]pp) +oo. The Mass Penalty term diverges:
(A)) +o (ifx(A) < 1). a(1
lim
This acts as strong constraint, heavily penalizing support leakage.
As for the Shape divergence term (A)) (TTA.)), it remains finite, and dominated by the first term.
Remark (Limit a - 0: The Weak Constraint). As a - O, D converges to the Forward KLL divergence (pI(p) The Mass Penalty term remains finite:
1 - xA) In(xxAA)
lim
a(1
This acts soft constraint ("Surprise Penalty"), allowing trade-off between coverage (n (T(A) and conditional shape matching ( (DxL (p((aA)) The Shape divergence term T()) Dj, (T P) also remains finite and converges to Da A.
27


Reviews:
[{"review_id": "Ow3vMliDZs", "reviewer": "Reviewer_m7ni", "summary": "Building on prior works on Distributional Matching, the authors consider the target distribution $p_c$, which is essentially the I-projection of the base policy onto the space of distributions that strictly filters out incorrect responses. The authors then argue that the RLVR optimizes the reverse KL to $p_c$, which potentially reduces diversity. In order to interpolate between the reverse and forward KL behaviors, the authors propose **Amari-DPG**, which utilizes Amari's $\\alpha$-divergence for the $f$-DPG (Go et al., 2023). The efficacy of this is shown in a formal math dataset with Lean, along with extensive ablations.", "questions": "1. What may be a principled way of choosing $\\alpha$ other than doing a grid search of $\\alpha$?\n\n2. Does different value of $\\alpha$ impact the trainig stability/convergence rate?\n\n3. Albeit with extensive ablations, the authors only consider the formal math task. What other tasks may benefit significantly from the proposed approach?\n\n4. Can one think about \"tuning\" the $\\alpha$ throughout the training? Of course, this means that the partition function would have to be reevaluated, but just a random thought.\n\n5. (Minor) Very recently, there have been some issues regarding floating-point operations (https://x.com/QPHutu/status/1984258808332550245). Can the authors comment on whether this issue(?) applies to their experiments?\n\n6. (Minor) Other than Amari's $\\alpha$-divergence, there is another way of interpolating forward and reverse KL via density ratio metrics (DRMs) [1]. Could the authors comment on what would happen if such another interpolation is used?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- Paper is well-written and easy to follow, with enough background explanation\n- A simple approach with meaningful peformance gain\n- Extensive ablations", "weaknesses": "- Novelty-wise, at the end of the day, the methodology is precisely f-DPG of Go et al. (2023), with f-divergence replaced with Amari's $\\alpha$-divergence. Also, the target distribution $p_c$ is taken from Khalifa et al. (2021). But, I also concur that the simplicity of the proposed method overshadows the \"lack\" of novelty.\n- The writing can be made a bit clearer. As this is a mixture of prior works, a clearer separation of the authors' contributions and prior works in Section 3 would be helpful.\n- The computation of the partition function, $Z_c$, is not mentioned explicitly anywhere in the paper. This makes the paper not so self-contained.\n\n**minor suggestion**\n- The \"original\" reference for the alpha-divergence is [1], and thus also referred to as Renyi's alpha-divergence. But, their forms are a bit different, although they are equivalent up to reparametrization; see Appendix B of [2], for instance. Maybe good to mention this just for clarity..!\n\n\n[1] https://projecteuclid.org/ebooks/berkeley-symposium-on-mathematical-statistics-and-probability/On-Measures-of-Entropy-and-Information/chapter/On-Measures-of-Entropy-and-Information/bsmsp/1200512181\n\n[2] https://proceedings.mlr.press/v70/li17a.html", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "weTJLIctSA", "reviewer": "Reviewer_nArH", "summary": "This paper addresses the diversity loss issue in LLMs tuned via Reinforcement Learning by proposing the Distributional Matching with Verifiable Rewards (DMVR)  framework. It constructs an explicit target distribution by filtering out incorrect answers while preserving the relative probabilities of correct ones from a pre-trained base model. To approximate this target, the paper introduces Amari-DPG, which leverages Amari’s α-divergence family to enable controllable trade-offs between precision and diversity.", "questions": "1. Amari-DPG (α=0) uses on-policy sampling. Compared to RS-FT’s base model sampling, how does it perform in terms of sample efficiency (e.g., rejection rate of incorrect samples)?\n\n2. Amari-DPG (α=0.25) shows limited improvement in the efficiency of medium-difficulty problems. Can dynamically adjusting α during training balance the goals of \"preserving the solvability of hard problems\" and \"improving the efficiency of medium-difficulty problems\"?\n\n3. In Section 3.2, you argue that Amari’s α-divergence unifies Reverse KL  and Forward KL by interpolating between α→1 and α→0. However, the paper only shows gradient equivalence for these edge cases. Can you provide a formal proof (or more rigorous intuition) that the α-divergence’s interpolation smoothly preserves the \"mode-seeking to mass-covering\" transition across all $\\alpha \\in (0,1)$ ?\n\n4. You unify RLVR and RS-FT by showing Amari-DPG recovers both methods at α extremes. However, RLVR uses a KL penalty ($\\beta$) to balance reward and proximity to $\\pi_{base}$, while Amari-DPG sets $\\beta=0$ by default. Theoretically, how does Amari-DPG’s α parameter interact with RLVR’s $\\beta$ if both are used together?", "limitations": "", "rating": 4, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The theoretical analysis is rigorous, clearly attributing the diversity loss in RL-tuned LLMs to the mode-seeking behavior induced by the Reverse KL divergence.\n\n2. The paper is well-structured and addresses a meaningful research question, highlighting the significance of the accuracy–diversity trade-off in RL-aligned LLMs.", "weaknesses": "The main weakness lies in the experimental evaluation.\n\n1. The authors focus on RL algorithms in LLMs, yet RL-specific experiments are limited. It is essential to include baselines covering algorithms such as PPO and REINFORCE.\n\n2. Additionally, evaluations are confined to Lean. It would be valuable to incorporate 1–2 additional tasks (e.g., code generation or natural language mathematical reasoning) to assess the framework’s general applicability beyond formal theorem proving.\n\n3. Why doesn't Lean's testset use mainstream theorem proving benchmark, such as MiniF2F？\n\nIf these concerns are adequately addressed, I will consider raising my score.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "OFSGiMXpLD", "reviewer": "Reviewer_bJDc", "summary": "The paper presents DMVR, a distributional matching view for post training with verifiable rewards. The key idea is to form an explicit target distribution by filtering out incorrect generations with a verifier and then approximate this target with an autoregressive policy. The authors show that standard RL with verifiable rewards is equivalent to minimizing the reverse KL to a softened filtered target, which explains the loss of diversity in many RL runs. They then propose Amari DPG, which minimizes an α divergence to the filtered target and gives direct control over the precision and diversity tradeoff. Following theorem proving, the method traces a Pareto frontier between pass@1 and pass@256 and improves coverage over several GRPO style baselines.", "questions": "1. How does Amari DPG compare against two recent diversity aware baselines: pass@k training and rewarding the unlikely, when all methods receive similar compute and careful tuning. If combined, do they add or conflict.\n2. Several recent papers suggest that RL tends to reweight existing solutions rather than create new ones. Do you see evidence that α near zero brings the model closer to the base distribution in that sense, for example by recovering harder rare solutions that the base already had. Any analysis of overlap of successful trajectories would be helpful.\n3. If possible, conduct more experiments on different model families. (I know it may be too much for a rebuttal, and I will not take this into my final rating, just for the paper quality considerations.)", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The paper formalizes the filtered target distribution, pc, and proves that maximizing the usual RLVR objective equals minimizing the reverse KL to a softened filter. This clarifies why RLVR becomes mode seeking and why diversity collapses in practice. The argument is simple but convincing.\n2. The method unifies rejection sampling fine-tuning at one end and RLVR-style training at the other end, and allows smooth interpolation between mass covering and mode-seeking regimes. This aligns with prior distributional-matching insights and provides a knob practitioners can use.\n3. The paper also measures tactic and premise diversity and shows how those relate to pass@1 and pass@256, which is informative for understanding diversity effects beyond one score.", "weaknesses": "1. Evaluation is quite narrow. All main experiments are with a single base model family and a 7B scale, which is my biggest concern.\n2. The GRPO baselines use β=0 by default and add a single high KL setting. However, recent works show that reward shaping like rewarding the unlikely or optimizing pass@k can rescue coverage. A stronger baseline suite with these variants tuned as carefully as Amari DPG would make the frontier result harder to question. [1] Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "OPqMpZBVSs", "reviewer": "Reviewer_yHrP", "summary": "This paper proposes Distributional Matching with Verifiable Rewards (DMVR), a framework for training LLMs on reasoning tasks that explicitly defines a target distribution by filtering incorrect answers while preserving relative probabilities of correct ones. The authors introduce Amari-DPG, which uses Amari's α-divergence family to interpolate between mode-seeking (Reverse KL) and mass-covering (Forward KL) divergences, enabling control over the precision-diversity trade-off. Experiments on LEAN theorem proving demonstrate state-of-the-art results along the coverage-precision Pareto frontier.", "questions": "How does the method perform on other reasoning domains beyond LEAN?\n\nWhat is the computational overhead compared to GRPO in wall-clock time?\n\nCan you provide statistical significance tests for the main results?\n\nWhy not compare to other recent LEAN training methods (e.g., Kimina-prover, InternLM2.5-StepProver)?\n\nHow sensitive are results to the ε threshold for Z_c?", "limitations": "", "rating": 4, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- Clear conceptual contribution: The paper provides a unified perspective that clarifies how RLVR methods implicitly optimize Reverse KL to a filtered distribution, explaining diversity loss in a principled way.\n\n- Theoretically grounded: The connection between RLVR and distributional matching (Lemmas 1-2) is well-established, and the use of α-divergences to interpolate between objectives is mathematically sound.\n\n- Comprehensive experimental analysis: The diversity analysis using Simpson index and Shannon entropy, along with problem difficulty transitions, provides valuable insights into model behavior.", "weaknesses": "## Limited Novelty\n\nThe core technical contribution is incremental. The paper essentially applies existing f-DPG methods with Amari α-divergences to the RLVR setting. While the unification perspective is useful, the algorithmic novelty is limited:\n\n- The connection between RLVR and Reverse KL was already established by Korbak et al. (2022b)\n- f-DPG and KL-DPG are existing methods\n- Amari α-divergences are well-known in the literature\n\nThe main contribution is demonstrating that α ≈ 1 can outperform standard GRPO, but this feels more like careful hyperparameter tuning than a fundamental advance.\n\nAligning Language Models with Preferences through f -divergence Minimization.\n\nOn Reinforcement Learning and Distribution Matching for Fine-Tuning Language Models with no Catastrophic Forgetting.\n\nA Distributional Approach to Controlled Text Generation.\n\n\n## Narrow Experimental Validation\n\n- Single domain: Experiments are limited to LEAN theorem proving. The generalizability to other reasoning tasks (code generation, mathematical problem solving, multi-step reasoning) is unclear.\n\n- Single base model: Only DeepSeek-Prover-V1.5-SFT (7B) is evaluated. Scaling behavior and performance on larger models is unknown.\n\n## Overclaimed Improvements\n\n- It missed a lot of relevant baselines: such as DAPO, Dr. GRPO, GPG, etc.\n\n- Looking at Figure 2, the comparison is confusing. It seemed that Amari-DPG improved pass@1 but significantly harmed the pass@k when k becomes large (e.g., 256, 512). This can be understood as the model loses a lot of answer diversity. \n\n\n## Overlook of Relevant Papers\n\nThe authors claim in the conclusion section that RLVR does not generate fundamentally new capabilities but instead reweights and amplifies behaviors already present in the base model. However, they failed to cite the very closely related papers that discovered the same phenomenon. \n\nThe invisible leash: Why rlvr may not escape its origin.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)