Program Learning with Verifiable Rewards: Symbolic Backpropagation for Post-Training LLMs

Vishvesh Bhat

cs.AIAug 28, 2026

Program Learning with Verifiable Rewards: Symbolic Backpropagation for Post-Training LLMs

Authors: Vishvesh Bhat

Organizations: CoreThink AI

Abstract

Post training a language model to reason means updating its weights. Supervised finetuning and reinforcement learning both place the acquired capability inside the model where it cannot be inspected cannot be checked step by step and cannot be moved to another model. We argue that for tasks whose intermediate steps admit verification, reasoning is better placed outside the base models weights as an explicit program composed from deterministic and neural primitives. We introduce PLVR (Program Learning with Verifiable Rewards): a post training method that learns such programs directly from input-output examples. Its mechanism is symbolic backpropagation: each program layer carries a typed ontology a loss is computed at the output against ground truth and required input ontologies are propagated backward by type inference over primitive signatures: an analogue of the chain rule in which credit assignment is a derivation rather than an estimate. Where RLVR verifies a terminal outcome, PLVRs reward is a per step contract verdict dense over program structure. On LiveCodeBench v6 and Tau2Bench, 30B base models with PLVR outperform RL at matched budget by 27.8 points on average and frontier models an order of magnitude larger by 13.6 points. A single primitive library serves two benchmarks, so the marginal cost of a new task is 100 examples of program search and no new finetuning data. Replacing the loss guided search with uniform sampling over the same type admissible space at equal budget collapses the median program from 65.6 to 17.5, identifying the backward pass rather than the type system as the source of the advantage. We release the symbolic backpropagation library and a conformance checker so the method can be applied to primitive libraries other than our own.

Figures & tables

Primitive	Base model	Total	Train	Val
Decompose	Granite 4.1 3B	6,910	6,218	692
Check-Prerequisites	Granite 4.1 8B	4,867	4,376	491
Elaborate	Granite 4.1 3B	2,000	1,800	200
Get-Order	Granite 4.1 8B	2,000	1,800	200
Match-Func	Granite 4.1 8B	1,600	1,440	160
Denote	Qwen 3.6 27B	1,125	1,011	114

Table 1: Fine-tuning corpora and base models. Corpora are synthetic throughout, split 90/10.

Panel of Figure 1 — Figure 1: Top-1 accuracy of the leading indifference class against training-set prefix length. The unshuffled run reaches its final accuracy at $n=10$ and does not move thereafter, but is leading with a program other than $p^{*}$ until $n=100$ . The red line marks $n=70$ , where $p^{*}$ lies in the leading class under every permutation.

Panel of Figure 2 — Figure 2: Top-1 loss of the leading indifference class against training-set prefix length. The band collapses onto the $p^{*}$ loss floor at $n=70$ . The unshuffled run’s non-monotonicity—improving at $n=10$ , degrading through $n=30$ , recovering by $n=50$ —is a property of that ordering and is absent from the mean.

Base models, vanilla prompting
	$\tau^{2}$ -Bench
System	Airline	Retail	Telecom	LCB	Avg
Gemma 12B	47.3	0 5.3	0 5.2	28.7	21.6
GPT-OSS-20B	40.0	21.1	23.1	48.8	33.2
Nemotron 3 Nano	46.7	33.9	28.1	55.9	41.2
Muse Glimmer 30B	69.3	43.3	65.2	67.9	61.4

Table 2: Accuracy (%) by benchmark. PLVR rows wrap the reasoning layer around the base model directly above their group. Average is over the four columns; † marks an average over the columns available.

Base model	$\tau^{2}$ Airline	$\tau^{2}$ Retail	$\tau^{2}$ Telecom	LCB v6(Mar-Apr)	Avg
Gemma 12B	$+8.0$	$+22.8$	$+80.7$	$+56.3$	$+42.0$
GPT-OSS-20B	$+36.0$	$+48.2$	$+68.4$	$+41.2$	$+48.5$
Nemotron 3 Nano	$+34.0$	$+44.7$	—	$+13.8$	$+30.8^{\dagger}$
Muse Glimmer 30B	$+16.0$	$+21.0$	$+32.4$	$+21.3$	$+22.7$
Inkling 975B	$+16.0$	$+35.9$	$+21.1$	$+48.7$	$+30.4$

Table 3: Gain from PLVR over the same base model, in accuracy points. † average over available columns.

$N$	search pool	random pool	gap
5	77.6%	37.4%	$+40.2$
10	79.9%	44.3%	$+35.5$
20	81.2%	51.8%	$+29.4$
40	81.6%	62.6%	$+19.0$
60	81.6%	73.9%	$+7.6$

Table 4: Expected best-found at equal

N

, where

N

is the number of programs drawn from each pool. Mean over 200 draw orders, so neither arm benefits from a fortunate ordering.

	$n$	best	top quartile	median	bottom quartile	$\geq 70\%$
search	213	81.6%	76.1%	65.6%	40.2%	96/213 (45%)
random	64	76.6%	35.2%	17.5%	0 0.0%	0 1/64 0 (2%)

Table 5: Pool quality distributions. Quartiles are reported by value: the top quartile is the accuracy exceeded by the best 25% of programs in the pool, the bottom quartile the accuracy exceeded by the best 75%.

set	$n$	type err	RMS loss	accuracy	solved
selection set (in-sample)	60	2	0.352	82.3%	40/60
BFCL	30	2	0.412	74.7%	14/30
LCB	30	0	0.279	90.0%	26/30
held-out (unseen)	73	2	0.389	77.6%	43/73
BFCL	42	2	0.381	74.6%	19/42
LCB	31	0	0.399	81.7%	24/31

Table 6: In-sample and held-out performance of the selected program.

benchmark	in-sample	held-out	pool-wide drop
LCB	63.9%	56.9%	$-7.0$
BFCL	58.5%	50.2%	$-8.3$

Table 7: Pool-wide accuracy drop, measured across all 23 distinct behaviours in the retained pool rather than the winner alone.

required type	raw candidates	admissible at layer 1	reduction
[ToolCall]	533	21	$25\times$
[Code]	248	63	$4\times$
Scratch	534	28	$19\times$
Text	134	134	none
[Text]	1,037	1,037	none

Table 8: Type-correct compositions per required type at

d_{\max}=3

over the primitive library, before and after availability filtering at layer 1, where the program must close against

\Omega_{0}

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Parameter	Value	Role
layers ( $N$ )	4	program depth
d_max	3	composition depth within one layer
layer_k	8	partial programs surviving each depth (beam width)
per_key_k	8	candidates retained per key of $\Omega_{\text{req}}$
max_plans	60	layer plans emitted, heap-ordered by summed rank
batch	3	examples the scoring function averages over

Appendix

Table 9: Backward search settings. layer_k is the parameter that makes the search finite (§ 6.1 ); max_plans dominated wall-clock cost, and raising it from 60 to 200 made the search phase unfinishable within our budget.

Parameter	During search	Reported evaluation
assume	True while layers_below $>0$	False
execution	lookahead against library closure	real, from $\Omega_{0}$
tests	3-test prefix (LCB)	full public suite
timeout	3 s per test	15 s per test
limit_pool	—	200

Appendix

Table 10: Scoring configurations. assume permits a required type to be treated as reachable while layers remain to be built; at layer 1 it is disabled and the program must close against

\Omega_{0}

. Every number reported in § 5 uses the right-hand column.

Parameter	Value
alignment	CONTENT (not KEY )
Code policy	TESTS : $\text{val\_err}=1-\text{pass rate}$
ToolCall policy	PARTIAL
inversion_weight	0.5 (order penalty)
score	$(\text{type\_count},\ \text{val}_{L_{2}})$ , lexicographic
ranking key	$(\textsc{unmet},\ \text{type\_errors},\ \text{val}_{L_{2}},\ \text{deviation},\ \text{size},\ \text{label})$

Appendix

Table 11: Loss and ranking configuration. The score is a property of an output; the ranking key adds search-control terms that are properties of a candidate’s relation to the search state (§ 3.5 ).

Tolerance	Value	Quantity
$\tau_{\text{loss}}$	$\pm 0.10$	RMS loss
$\tau_{\text{acc}}$	$\pm 1.5$	accuracy points
$\tau_{\text{terr}}$	$\pm 1$	type errors

Appendix

Table 12: Indifference-class tolerances, applied in analysis only.

$n$	acc (%)	loss	$\|{\cdot}\|$	acc (%)	loss	$\|{\cdot}\|$	$p^{*}$ in top-1
	top-1			top-3
5	76.2	0.419	3	67.5	0.497	4	no
10	81.4	0.356	1	78.0	0.402	3	no
20	79.0	0.385	2	72.4	0.459	4	no
30	76.6	0.414	1	76.2	0.419	3	no
40	79.0	0.385	2	72.4	0.459	4	no

Appendix

Table 13: The unshuffled run: the training order the search actually saw, with the candidate pool gated by discovery. Top-1 accuracy reaches its final value at

n=10

and does not move, but the leading class does not contain

p^{*}

until

n=100

$n$	acc (%)	loss	acc (%)	loss	$P(p^{*})$
	top-1		top-3
5	75.9 [68.8, 79.9]	0.424 [.375, .487]	70.8 [58.4, 77.4]	0.477 [.412, .589]	0.73
10	78.2 [74.0, 81.5]	0.397 [.356, .450]	75.3 [70.8, 78.2]	0.432 [.403, .479]	0.62
20	80.0 [76.6, 81.6]	0.374 [.355, .414]	77.2 [74.3, 79.9]	0.410 [.375, .438]	0.72
30	80.8 [77.9, 81.6]	0.364 [.355, .409]	77.6 [74.3, 79.9]	0.405 [.375, .438]	0.84
40	81.0 [78.7, 81.6]	0.362 [.355, .394]	77.6 [74.3, 79.9]	0.404 [.375, .438]	0.85

Appendix

Table 14: Mean with 5–95% band over 109 permutations of the training order, pool fixed.

P(p^{*})

is the probability that the leading class contains

p^{*}

Panel of Figure 3 — Figure 3: Accuracy of the leading class against the three leading classes pooled, over 109 permutations. Top-3 sits 3–4 points below top-1 from $n=20$ onward and converges to a stable deficit rather than closing.

Panel of Figure 4 — Figure 4: Loss of the leading class against the three leading classes pooled, over 109 permutations. Both converge; the top-3 floor at 0.403 is above the top-1 floor at 0.356 by construction, since pooling admits programs the leading class excludes.

Panel of Figure 5 — Figure 5: Probability that the leading class contains $p^{*}$ , over 109 permutations. The dip at $n=10$ occurs because a wide class at small $n$ contains $p^{*}$ by inclusion rather than discrimination; as the class narrows, $p^{*}$ is briefly excluded before being placed back on merit.

Model	Benchmark	Mean	$\pm$ SD	$n$	Runs, oldest $\rightarrow$ newest (%)
INTELLECT-3 PrimeIntellect/INTELLECT-3
	$\tau^{2}$ Airline	58.7	5.0	3	58.0, 54.0, 64.0
	$\tau^{2}$ Retail	59.9	2.7	3	62.3, 57.0, 60.5
	$\tau^{2}$ Telecom	23.4	2.2	3	21.1, 23.7, 25.4
DeepCoder-14B-Preview agentica-org/DeepCoder-14B-Preview
	LCB v6	55.0	2.5	3	55.0, 52.5, 57.5

Appendix

Table 15: Per-run scores for the post-training baselines. Cells left blank in Table 2 are omitted here rather than reported as zero: DeepCoder-14B is a coding checkpoint and we do not evaluate it on

\tau^{2}

-Bench

Model	Benchmark	Mean	$n_{\text{prob}}$	Wilson 95%	Bootstrap 95%
INTELLECT-3	$\tau^{2}$ Airline	58.7	0 50	[44.9, 71.2]	[44.0, 72.0]
	$\tau^{2}$ Retail	59.9	114	[50.8, 68.5]	[50.9, 68.4]
	$\tau^{2}$ Telecom	23.4	114	[16.6, 32.0]	[15.8, 31.6]
DeepCoder-14B	LCB v6	55.0	0 80	[44.1, 65.4]	[43.8, 66.2]
Nemotron-Cascade-2	$\tau^{2}$ Airline	60.0	0 50	[46.2, 72.4]	[46.0, 74.0]
	$\tau^{2}$ Retail	67.8	114	[58.7, 75.6]	[58.8, 76.3]

Appendix

Table 16: Marginal 95% intervals over problems. Wilson intervals are computed from the pooled success rate; bootstrap intervals are 20,000 resamples of the problem set. The two agree to within a point in every cell, as expected for a binomial proportion, and we report both so that the bootstrap figure can be checked against a closed form.

Explore similar work

Jun 22, 2026cs.LG

Provable Benefits of RLVR over SFT for Reasoning Models: Learning to Backtrack Efficiently

Recent advances in large language models (LLMs) have demonstrated that reinforcement fine-tuning of pretrained base models can lead to significant gains in reasoning performance at inference time. In this work, we theoretically analyze why reinforcement fine-tuning induces better reasoning ability than purely supervised fine-tuning (SFT) methods. We model chain-of-thought (CoT) reasoning as a pathfinding problem on graphs and compare the popular method of reinforcement learning with verifiable rewards (RLVR) against traditional SFT. We prove that SFT, when trained on golden shortest paths without negative examples, fails to learn how to efficiently backtrack. In contrast, an RLVR-trained model can learn how to efficiently backtrack from dead ends using only outcome reward. This leads to an exponential separation in inference-time compute between the two methods, and demonstrates that RLVR leads the model to learn the location of difficult decisions in a reasoning chain, ultimately allowing for better allocation of inference-time compute. Finally, we show that the reasoning traces of an RLVR model can be distilled to train a base model to backtrack efficiently as well.

Stanley Wei, Juno Kim

1Princeton University · University of California, Berkeley.

Large Reasoning Models Reinforcement Learning With Verifiable Reward Reasoning Chain Reinforcement Fine-Tuning Provable Guarantees

Ask PDF

Jul 16, 2026cs.LG

Non-vacuous Generalization Bounds for Reinforcement Learning with Verifiable Rewards

While reinforcement learning with verifiable rewards (RLVR) is widely used to improve the reasoning capabilities of large language models (LLMs), the generalizability of the resulting models remains poorly understood. In this work, we establish the first non-vacuous generalization bounds for parameter-efficient RLVR fine-tuning at the billion-parameter scale. Our approach adapts PAC-Bayes compression bounds to this setting, and addresses the inherent stochasticity of token generation by applying the Gumbel-max reparameterization trick. To operationalize these bounds, we propose the Progressive RLVR framework, which integrates RLVR with on-policy distillation, TinyLoRA, and model quantization. Progressive RLVR empirically retains 84-97% performance of standard LoRA fine-tuning while producing models that are 14,796x more compressible. We show that this framework yields non-vacuous generalization bounds in four domains: mathematical problem-solving, programming, general-knowledge reasoning, and Text-to-SQL. Our bounds exceed the accuracy of the base model by 9-51% and lie within 6-11% of the accuracy of the fine-tuned models.

Yuxuan Zhu, Rohan Alur, Daniel Kang

UIUC · MIT · Bridgewater AIA Labs

Reinforcement Learning With Verifiable Reward Verifiable Rewards Generalization Bounds

Ask PDF

Apr 28, 2026cs.AI

JURY-RL: Votes Propose, Proofs Dispose for Label-Free RLVR

Reinforcement learning with verifiable rewards (RLVR) enhances the reasoning of large language models (LLMs), but standard RLVR often depends on human-annotated answers or carefully curated reward specifications. In machine-checkable domains, label-free alternatives such as majority voting or LLM-as-a-judge remove annotation cost but can introduce false positives that destabilize training. We introduce JURY-RL, a label-free RLVR framework that decouples answer proposal from reward disposal: votes from model rollouts propose a candidate answer, and a formal verifier determines whether that candidate can receive positive reward. Concretely, only rollouts matching the plurality-voted answer are rewarded when that answer is successfully verified in Lean. When verification is inconclusive, we invoke ResZero (Residual-Zero), a fallback reward that discards the unverified plurality proposal and redistributes a zero-mean, variance-preserving signal over the residual answers. This design maintains a stable optimization gradient without reinforcing unverifiable consensus. Across three backbone models trained on mathematical data, JURY-RL consistently outperforms other label-free baselines on mathematical reasoning benchmarks and transfers competitively to code generation and general benchmarks. It attains pass@1 performance comparable to supervised ground-truth training, with superior generalization demonstrated by higher pass@k and response diversity.

Xinjie Chen, Biao Fu, Jing Wu +4

Tongyi Lab, Alibaba Group, Hangzhou, China

Reinforcement Learning With Verifiable Reward Verifiable Rewards Process-Level Supervision Majority Voting

Ask PDF