Program Learning with Verifiable Rewards: Symbolic...

Program Learning with Verifiable Rewards: Symbolic... | AI Research

Key Takeaways

Program Learning with Verifiable Rewards (PLVR) is a post-training method that moves reasoning capabilities out of a language model’s weights and into an exp...
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.

Paper AbstractExpand

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.

Program Learning with Verifiable Rewards (PLVR) is a post-training method that moves reasoning capabilities out of a language model’s weights and into an explicit, verifiable program. By using a technique called symbolic backpropagation, the method learns programs composed of deterministic and neural primitives that can be inspected and checked at every step, rather than relying on opaque weight updates.

Reasoning Outside the Model

Current post-training methods like supervised fine-tuning and reinforcement learning (RL) store reasoning capabilities directly inside a model's weights. This makes the reasoning opaque, unverifiable during execution, and tied to a specific model checkpoint. Vishvesh Bhat of CoreThink AI argues that for tasks where intermediate steps can be verified—such as tool-calling or program generation—reasoning should instead be stored as an explicit program. In this approach, the base model remains unchanged, and the "learning" occurs by identifying the best arrangement of primitives and their parameters.

Symbolic Backpropagation

Because these programs are composed of discrete, non-differentiable primitives, they cannot be optimized using standard gradient-based backpropagation. PLVR introduces symbolic backpropagation to assign credit. Each program layer contains an "ontology"—a structured, typed representation of the computation state. When a program produces an output, a loss is calculated against ground truth. Instead of estimating gradients, the system performs type inference backward through the program’s primitive signatures. This derivation determines the required input for each preceding layer, effectively localizing failures to the specific step where they occurred.

Performance and Efficiency

In tests on LiveCodeBench v6 and τ²-Bench, 30B base models using PLVR outperformed RL-based post-training at a matched budget by an average of 27.8 points. The method also outperformed frontier models an order of magnitude larger by 13.6 points. A key finding is that the backward pass is the primary driver of this success; when the researchers replaced loss-guided search with uniform sampling, the median program quality dropped from 65.6% to 17.5%. Additionally, the method is efficient: once a primitive library is established, the marginal cost of a new task is approximately 100 examples of program search, requiring no new fine-tuning data.

Limitations and Scope

PLVR is designed specifically for tasks where intermediate outputs can be checked against a contract or specification. It is not intended for tasks that rely on subjective judgment, such as open-ended summarization or creative generation, where gradient-based post-training remains the standard. The "verification" provided by PLVR consists of contract checking and empirical validation rather than formal mathematical proof. The authors have released their symbolic backpropagation library and a conformance checker to allow others to apply this method to different primitive libraries.