Source-linked AI summary
Program Learning with Verifiable Rewards: Symbolic Backpropagation for Post-Training LLMs
Vishvesh Bhat
TL;DR
Existing post-training methods store reasoning capabilities in model weights, making them opaque, difficult to verify step by step, and tied to one model. PLVR instead learns explicit typed programs with symbolic backpropagation and per-step contract verdicts; its loss-guided search substantially outperforms uniform sampling under matched conditions.
Problem
Current supervised fine-tuning and reinforcement learning place acquired capabilities in opaque weights that cannot be inspected step by step or transferred directly between models.
Method
PLVR leaves base-model weights untouched and learns explicit programs of deterministic and neural primitives using symbolic backpropagation over typed contracts.
Results
65.6% to 17.5%: replacing loss-guided search with uniform sampling over the same type-admissible space collapses the median program under equal budget.
Takeaways & Limitations
Typed, contract-verified program construction provides a checkable alternative substrate for reasoning when intermediate outputs can be verified.
Takeaways & Limitations
PLVR requires checkable intermediate outputs and does not claim applicability to judgment-based tasks such as summarisation or open generation.
Abstract
from arXiv · showhide
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.
1 Introduction
PLVR places verifiable reasoning in an explicit typed program rather than only in base-model weights, using symbolic backpropagation to derive credit through discrete compositions. The method reports stronger matched-budget results than RL, lower task-amortized data costs, and an ablation attributing its advantage to loss-guided backward search.
- Motivation: Post-training stores learned reasoning in weights, making intermediate capabilities opaque, progress unverifiable, and adaptation bound to the trained model.These properties motivate moving reasoning into an explicit artifact.
- Approach: PLVR learns an explicit program of deterministic and neural primitives while leaving the base model’s weights unchanged.The program specifies primitive selection, arrangement, and parameters.
- Approach: Symbolic backpropagation derives required input ontologies backward from primitive signatures, replacing rollout-based credit estimates with deterministic type inference.Value search remains bounded within declared primitive ranges, while contracts localise failures to producing steps.
- Approach: PLVR makes verifiable rewards dense over program structure by checking typed output contracts at every step rather than only terminal outcomes.This extends the checkable-signal premise of RLVR inward to intermediate computation.
- Evidence: 65.6% to 17.5% is the median-program collapse when loss-guided search is replaced by uniform sampling over the same type-admissible space.Because both arms retain the type system and other constraints, the passage attributes the advantage to the backward pass.
- Evidence: ≈100 program-search examples and no new fine-tuning data are needed at the margin for a new task using the shared primitive library.One library of 19,627 synthetic examples serves both benchmarks.
- Scope: The broader substrate claim remains untested with a third-party construction method, although it is intended to be checkable by other compositional pipelines.The released library and conformance checker support application beyond the authors’ primitive set.
2 Related Work
PLVR extends verifiable and process-level feedback by deriving per-step structural signals from typed contracts rather than learning or estimating them from trajectories. It shares explicit program structure with workflow-optimization systems but differs in using typed, execution-enforced intermediate verification.
- Verifiable feedback: RLVR replaces learned reward models with programmatic terminal checks, while PLVR adds typed contract verdicts at every program step.PLVR therefore makes the verifiable signal dense over program structure rather than scalar and terminal.
- Process supervision: Process reward models judge steps with learned verifiers and step-level supervision, whereas PLVR checks contracts derived from primitive signatures without step-level annotation.The distinction is between predicted judgments and programmatic structural checks.
- Textual optimization: ProTeGi, TextGrad, and Trace use language-model-generated critiques, suggestions, or reflections as gradient analogues, unlike PLVR’s type-inferred backward signal.PLVR’s required inputs follow from declared signatures rather than generated feedback.
- Textual optimization: GEPA also uses reflective feedback but searches instructions, whereas PLVR obtains per-step attribution structurally from types and contracts.The papers share a diagnosis concerning sparse scalar rewards but propose different remedies.
- Workflow synthesis: ADAS and AFlow search explicit workflow structure using coarse whole-trajectory scores over untyped LLM calls, unlike PLVR’s typed contracts enforced during execution.The comparison isolates both the optimization signal and intermediate verification regime.
- Scope: PLVR splits agentic reasoning between deterministic structural invariants and learned semantic decisions bounded by empirically validated contracts.Agentic tool-calling includes semantic judgments that resist complete formal specification.
3 Methodology
PLVR represents computation as a layered typed program whose ontologies are inspected, scored, and connected through tokenizer boundaries and primitive contracts. Symbolic backpropagation resolves admissible structure backward, while bounded value search and lexicographic ontology loss guide synthesis without updating the base model.
- Ontologies and layers: A PLVR program is an N-layer composition of primitives in a typed DSL, with each layer carrying an inspectable ontology of computation state.Learning selects the primitives and operators that produce each layer’s required ontology.
- Ontologies and layers: An ontology is a keyed collection of nested typed objects containing both structural types and instance values for the current example.The representation uses the knowledge-representation sense of ontology while populating each layer with realized values.
- Tokenizer: Tokenizers convert raw instances and answers into ontologies of the same format, allowing the ontology loss to apply at both program boundaries.The schema detects different object types at inputs and outputs, including turns, tools, code, and tool calls.
- Tokenizer: The hybrid tokenizer combines learned structure identification with symbolic well-formedness and grounding checks.This division gives the boundary both semantic flexibility and deterministic validation.
- Contracts: Every text field must be a verbatim source span, while references and bindings must resolve and type-check against declared schemas and signatures.Only semantic attribution is validated empirically.
- Contracts: Tokenizer errors become invisible to downstream contracts, and tokenizer granularity determines which objects the loss can score separately.This makes boundary correctness a central assumption of the pipeline.
- Primitives: ELABORATE pairs learned expansion choices with exhaustive symbolic checks that enforce subsequence and fixed-dictionary insertion constraints.The hybrid design constrains invented, dropped, or reordered content without directly constraining the learned expansion decision.
- Operators: WRAP lifts a value into a singleton list, enabling composition with FOREACH and APPEND and deriving α as the required input for output [α].This supplies a route to collection types without a direct collection-producing primitive.
4 Experiments
The experiments test PLVR across two benchmarks, multiple base models, and comparisons designed to separate program learning from prompting, scaffolding, and post-training scale. They also examine primitive training, convergence, and methodological boundaries.
- Evaluation design: LiveCodeBench v6 and τ 2-Bench were selected for distinct verification characters: code execution against tests and policy-constrained dialogue.
- Evaluation design: The evaluated base models are Gemma 3 12B, Muse Glimmer 30B, GPT-OSS-20B, and Nemotron-3-Nano 30B, while neural primitives range from 3B to 27B.All primitives remain resident at inference; the composed system has approximately 57B total parameters and 3–27B active per forward pass.
- Primitive fine-tuning: Primitives are trained on synthetic, operation-specific structured-JSON examples rather than benchmark tasks, using exact-match validation and 90/10 train-validation splits.This task-agnostic setup is intended to let one primitive library serve multiple tasks without benchmark-specific fine-tuning data.
- Baselines: PLVR is compared with vanilla prompting, a token-matched agentic harness, and published RL checkpoints rather than newly trained supervised or reinforcement-learning baselines.The published checkpoints are selected for data-matched and parameter-matched comparisons, which are explicitly treated as non-interchangeable.
- Baselines: The claimed comparison is bounded: PLVR is assessed against RL post-training at matched data and at comparable parameters while using a fraction of task-specific data.The paper makes no claim relative to supervised fine-tuning.
- Protocol boundaries: Published baseline repetitions measure inference variance only, because the authors did not control or vary those checkpoints’ training seeds.The paper does not attempt FLOP-matched comparison or report latency, instead reporting raw compute components, token counts, and memory footprint.
5 Results
PLVR improves performance across models and benchmarks, outperforming RL post-training and larger prompted systems while showing that loss-guided search, rather than typing alone, drives program quality. Results also show rapid program identification, limited evidence of selection overfitting, and important benchmark-specific caveats.
- Benchmark results: 13.8 to 80.7 points: PLVR improves every measured model and benchmark, with the largest gains on weaker base models.GPT-OSS-20B gains 48.5 points on average, while Gemma 12B gains 80.7 points on Telecom from a 5.2 baseline.
- Benchmark results: 83.1 average: the best PLVR configuration exceeds the reported frontier vanilla systems, while PLVR also outperforms the evaluated token-matched harness.PLVR averages 63.9 on Gemma 12B, 78.4 on GPT-OSS-20B, and 80.6 on Muse Glimmer 30B; the harness reaches 47.9.
- Benchmark results: 27.8 points: Muse Glimmer 30B with PLVR leads the three RL baselines on shared columns, and exceeds the frontier-system mean by 13.6 points.The gaps are +30.7 against INTELLECT-3, +30.0 against DeepCoder-14B on LiveCodeBench, and +22.6 against Nemotron-Cascade-2 on the τ 2 domains.
- Benchmark caveats: 2.6-point margin: PLVR leads least comfortably on τ 2 Retail, and the Telecom gain is partly recovery from a collapsed 5.2% vanilla baseline.The authors report that three runs cannot resolve the Retail margin confidently and would not rest the claim on Telecom alone.
- Convergence and identification: 70 examples: identification of the leading program is reliable when results are averaged over permutations, whereas a single unshuffled run requires 100 examples.Accuracy alone appears converged from n = 10 in the unshuffled run, before the leading class contains the target program.
- Ablation: removing the loss-guided search: 65.6% versus 17.5%: loss-guided search produces a much stronger program pool than uniform sampling over the same type-admissible space.The guided pool has 45% of programs above 70% accuracy versus 2% for the null, while every constraint other than scoring is retained.
- Generalization: 0.1 points: the selected program’s BFCL performance drops from 74.7% to 74.6%, while the pool average drops 8.3 points on unseen tool tasks.On LiveCodeBench, accuracy drops from 82.3% in-sample to 77.6% held-out because the held-out set includes harder contest problems.
6 Discussion
The discussion separates the roles of types, beam search, and loss-guided derivation, while interpreting convergence and transfer results with explicit limits.
- Search space: 1027 well-typed four-layer programs show that types alone do not make exhaustive search tractable.The search scored roughly 14,400 candidates and retained 213, about 10^-23 of the space.
- Search space: Beam width makes search finite, while types make candidates well-formed and availability mainly constrains final closure against Ω0.Availability filtering acts severely only at layer 1, where the program must close against the initial ontology.
- Search settings: Width dominates depth computationally: increasing max plans from 60 to 200 made search unfinishable, while dmax = 3 remained affordable.A layer requiring six types multiplies the space by roughly 10^9.
- Ablation: 45% of guided-search programs exceed 70% accuracy versus 2% under the null, making the distributional comparison stronger than best-of-N curves.The best-of-N gap narrows as the finite null pool is exhausted, whereas medians compare where procedures land in the space.
- Ablation: 65.6% versus 17.5% median accuracy shows loss-guided search reaches a different program-space distribution than uniform sampling.The comparison uses identical type-admissible spaces, equal budgets, and retained constraints.
- Transfer: 0.1 points is the selected program’s BFCL drop, versus 8.3 points for the pool average, while LiveCodeBench drops 4.7 points in-sample to held-out.The BFCL result indicates transfer robustness relative to the candidate pool; the held-out split reflects harder problem families rather than an i.i.d. generalisation estimate.
- Limits: The evidence does not separately isolate the loss design from the backward pass, and held-out data are not i.i.d.The supported claim is that target-directed derivation beats other proposal mechanisms under the fixed loss.
7 Conclusion
The paper introduces PLVR as post-training that leaves base-model weights untouched and learns explicit programs with typed, contract-verified primitives. Its conclusion emphasizes dense symbolic credit assignment and a substrate-level claim for future testing.
- 7 Conclusion: PLVR leaves the base model’s weights untouched and learns an explicit program composed from deterministic and neural primitives.Symbolic backpropagation derives required lower-layer ontologies from primitive signatures and localises contract failures.
- 7 Conclusion: The proposed substrate-level claim is that program construction over typed, contract-verified primitives outperforms the same procedure over raw model calls.The authors present this as a claim for others to test, not as a benchmark result established by a third-party method.
Reproducibility Statement
The reproducibility statement identifies the released implementation resources and separates final-run scoring configurations from search settings.
- Resources: The symbolic backpropagation library and conformance checker are slated for release following peer review.The paper also specifies the method and run settings across the main text and appendices.
- Settings: Final-run settings use 109 examples, with search and evaluation deliberately separated into different scoring configurations.Only the evaluation configuration is used for reported numbers.
- Settings: The backward-search configuration uses layer k to make search finite, while max plans dominate wall-clock cost.Increasing max plans from 60 to 200 made the search phase unfinishable within the stated budget.
A.2 Scoring: search versus evaluation
The appendix distinguishes inexpensive search scoring from the configurations used for reported evaluation and documents how losses, ranking, and convergence classes are interpreted.
- Scoring: Search scoring is intentionally cheap, whereas every reported number uses the separate evaluation configuration.Conflating them could allow an approximate scorer to inflate reported results.
- Loss: Content alignment compares matched content before the inversion weight applies an order penalty to correctly matched calls in the wrong order.Key alignment would give maximum loss when correct calls are displaced by a setup call.
- Convergence analysis: Indifference-class tolerances are applied only in convergence analysis, while search ranks candidates strictly.Classes pool programs whose scores lie within specified RMS-loss, accuracy, and type-error tolerances.
- Convergence analysis: The convergence appendix reports both top-1 and pooled top-3 classes for an unshuffled run and 109 permutations with the candidate pool fixed.The all-example best program p∗ scores 81.6% accuracy and 0.355 loss.
B.1 Unshuffled run
The unshuffled search reaches final top-1 accuracy at n = 10, while the leading class contains p∗ only at n = 100. This motivates reporting identification separately from accuracy.
- Top-1 accuracy reaches its final value at n = 10 but the leading class does not contain p∗ until n = 100.
- Accuracy stabilises early while p∗ remains outside the leading class, separating performance from identification.
- Permutation summaries report the mean and 5–95% band over 109 training-order permutations with the candidate pool fixed.
B.4 Reading the top-3 curve
Top-3 remains consistently below top-1 in accuracy and loss, while its wider band reflects continued contestation among later classes. The displayed top-1 anomaly at n = 70 and n = 80 is rounding, not distributional behavior.
- Top-3 trails top-1 by 3–4 accuracy points and 0.047 loss from n = 20 onward.
- The top-3 band is wider at every n because the third class remains contested after the leader stabilises.
- At n = 70 and n = 80, the reported top-1 mean of 81.4 falls below its 5–95% lower bound of 81.5 because of rounding.
C Post-training baselines: per-run scores
The post-training baseline appendix excludes failed zero-score or scoreless runs, reports valid-run counts, and treats three-run deviations as descriptive rather than confidence intervals. Coverage excludes DeepCoder-14B-Preview from τ 2 domains and averages only available columns.
- Zero-score or scoreless runs are excluded from score lists, means, and standard deviations, with valid-run counts reported per cell.
- Three-run standard deviations describe run-to-run variation, not training variance or interval estimates.
- DeepCoder-14B-Preview is not evaluated on τ 2 domains because its coding specialization would make that comparison uninformative.
- Averages marked † use available columns only, without imputing missing cells.
C.1 Intervals over problems
Problem-level intervals are the primary uncertainty measure because finite task sets dominate run-to-run variation. τ 2 Airline is especially underpowered for small margins, while paired bootstrap intervals can be substantially tighter than marginal intervals.
- Problem-level uncertainty is primary because τ 2 Airline has 50 tasks, Retail and Telecom 114 each, and LiveCodeBench v6 80.
- At 50 Airline tasks, a 95% interval spans roughly 26 points, so margins below about 13 points are not resolvable from marginal intervals.
- PLVR on Gemma 12B reaches 56.0 on Airline against INTELLECT-3’s 58.7 and Nemotron-Cascade-2’s 60.0, with substantially overlapping intervals.
- Paired bootstrap resamples per-problem outcomes and yields substantially tighter intervals than marginal intervals by removing shared between-problem variance.
- INTELLECT-3’s Airline scores span 54.0 to 64.0 across three runs, making its mean more cautionary than other baseline cells.
- Wilson and bootstrap marginal intervals agree within one point in every cell, while paired intervals use actual per-problem outcome vectors.