A model is asked for the probability that two dice sum to at least ten. It writes four lines of clean reasoning and enumerates the favorable outcomes as 6+4, 5+5, 5+5, 6+5, 6+6, 6+6 — silently dropping 4+6 and 5+6, and double-counting two others to make up the difference. Six outcomes over 36, so 1/6. The answer is correct. The reasoning is garbage, and the errors happened to cancel. Your outcome-based verifier reads the final line, compares it to the gold label, and returns 1.0. You have just taught your selection system that this kind of reasoning is good, and the next time the errors do not cancel you will ship the answer with total confidence.
Lesson 2 ended with the finding that selection, not sampling, is what caps the parallel axis. This lesson is about the component that does the selecting: outcome versus process reward models and what each costs to train, generative verifiers that turn scoring back into a generation problem you can scale, the much larger world of verifiers that are not learned models at all, the LLM-modulo architecture that puts a sound checker in the loop, and how to design a verification stage that does not quietly become your bottleneck or your biggest vulnerability.
An outcome reward model (ORM) takes a problem and a complete solution and predicts the probability that the final answer is correct. Training data is cheap to the point of being free: roll out your policy many times on problems with known answers, label each trajectory 1 or 0 by comparing the final answer to the gold, and train a classifier head on the trace. Cobbe et al. (2021) did exactly this for GSM8K and reported the result that started the field — verifier-reranked sampling from a smaller model outperformed fine-tuning a model 30x larger.
ORMs have two structural weaknesses, and both come from the same root: a single scalar attached to a 2,000-token trace.
ORMs are still the correct default when labels are plentiful, the answer space is large enough that lucky guesses are rare, and you mostly care about ranking complete candidates. They are the wrong tool the moment you want to steer a search, because a search needs to score partial solutions and an ORM has never seen one.
A process reward model (PRM) scores every step. Given a problem and a reasoning prefix, it emits a per-step probability that the step is correct, so a partial solution has a score and a search has something to follow.
The landmark study is Lightman et al. (2023), Let's Verify Step by Step. The team collected PRM800K — around 800,000 step-level human correctness labels over solutions to MATH problems — trained a PRM on it, and used it to rerank large candidate pools. Three results are worth carrying around. First, the PRM beat both an ORM and plain majority voting, solving 78.2% of a representative MATH test subset when selecting from 1,860 samples. Second, the gap widened as the number of samples grew: outcome supervision degrades under selection pressure faster than process supervision does, because it is a looser proxy. Third, process supervision was more reliable specifically because it penalizes the right-answer-wrong-reasoning case that an ORM cannot see.
The obvious objection is cost — 800,000 human step labels is not a budget line most teams have. The field's answer is automated step labeling by rollout: take a reasoning prefix, complete it many times from that point, and estimate the step's value as the fraction of completions that reach the correct answer. That is a Monte Carlo estimate of the step's value under the current policy, it needs no humans, and it is the approach behind Math-Shepherd-style PRM training. It costs generation compute instead of annotation dollars, which for most teams is the far easier trade. Once you have per-step scores you must aggregate them into one number for ranking, and the choice matters:
| Aggregation | Behavior | Use when |
|---|---|---|
min over steps | One bad step condemns the trace | Chains where any error is fatal (proofs, arithmetic) |
| product of step probabilities | Penalizes length; long correct traces score low | Fixed-length reasoning; rarely a good default |
| score of the last step | Approximates an ORM | When later steps genuinely subsume earlier ones |
| mean over steps | Forgiving; a recovered error still ranks well | Agent trajectories with legitimate backtracking |
For math and proofs, min is the usual winner and matches the
intuition that a chain is as strong as its weakest link. For agent
trajectories it is a poor fit, because a good agent does take bad
steps and recover from them, and min punishes exactly the
recovery behavior you want to encourage.
Classical reward models are discriminative: a transformer with a scalar
head, trained with a ranking or classification loss. That throws away the
one thing the base model is best at — generating text. Zhang et al.
(2024), Generative Verifiers: Reward Modeling as Next-Token
Prediction, reframed verification as generation. The verifier is
asked a question in natural language — "Is this solution correct?
(Yes/No)" — and the reward is the probability it assigns to the token
Yes.
# A generative verifier, as a scoring function you can drop into best_of_n.
VERIFY_PROMPT = '''Problem:
{problem}
Proposed solution:
{solution}
Is this solution correct? Answer with a single token: Yes or No.'''
def genrm_score(client, problem, solution):
r = client.completions(prompt=VERIFY_PROMPT.format(problem=problem,
solution=solution),
max_tokens=1, logprobs=True)
lp = r.top_logprobs[0] # token -> logprob at position 0
import math
yes = math.exp(lp.get("Yes", -20.0))
no = math.exp(lp.get("No", -20.0))
return yes / (yes + no + 1e-9) # a calibrated-ish scalar in [0,1]
This looks like a trick and is a structural advantage. It unifies the stacks — same architecture, same serving path, same fine-tuning pipeline as your generator, no separate reward-model infrastructure to maintain. It can be trained jointly on generation and verification, and the two tasks help each other: a model that has practiced solving problems verifies them better.
Third, and most important for this course, the verifier can now spend test-time compute too. Ask it to produce a chain of thought before the Yes/No token — critique first, then score — and it catches errors a single forward pass misses. Sample that critique several times and average the resulting probabilities and you have majority voting on the verification side. The whole toolkit from Lesson 2 applies recursively to the verifier, and GenRM-CoT with majority voting over critiques was the strongest configuration in Zhang et al.'s results.
CRITIQUE_PROMPT = '''Problem:
{problem}
Proposed solution:
{solution}
Check the solution step by step. Point out the first error you find, if
any. Then, on the final line, write exactly 'VERDICT: Yes' or
'VERDICT: No'.'''
def genrm_cot_score(client, problem, solution, k=4):
'''Critique-then-score, averaged over k sampled critiques.'''
votes = []
for _ in range(k):
text = client.completions(
prompt=CRITIQUE_PROMPT.format(problem=problem, solution=solution),
temperature=0.7, max_tokens=400).text
votes.append(1.0 if "VERDICT: Yes" in text else 0.0)
return sum(votes) / len(votes)
The literature's focus on learned reward models obscures a fact that matters enormously in production: the best verifier available to you is usually not a model at all. It is a program that is right by construction.
| Verifier | What it proves | Sound? | Cost |
|---|---|---|---|
| Execution against tests | Behavior on the tested inputs | Yes, within coverage | Milliseconds |
| Property-based tests | Invariants over generated inputs | Yes, probabilistically thorough | Seconds |
| Type checker / linter | Absence of a class of errors | Yes for that class | Milliseconds |
| Schema / contract validation | Structural well-formedness | Yes | Microseconds |
| SMT solver (Z3 and kin) | Satisfiability of constraints | Yes (may time out) | Milliseconds to forever |
| Proof assistant (Lean, Coq) | The theorem, absolutely | Yes | Seconds; needs formalization |
| Domain simulator | Feasibility under a model of the world | As sound as the model | Varies |
| Learned PRM / ORM | Nothing; it estimates |
def llm_modulo(generate, hard_critics, soft_score, max_rounds=5):
'''Generator plus sound critics, with back-prompting. The output either
satisfies every hard critic or is explicitly reported as unsolved.'''
feedback, best = [], None
for round_ix in range(max_rounds):
candidate = generate(feedback)
reasons = []
for critic in hard_critics:
ok, why = critic(candidate)
if not ok:
reasons.append("%s: %s" % (critic.__name__, why))
if not reasons:
score = soft_score(candidate)
if best is None or score > best[1]:
best = (candidate, score)
return {"ok": True, "candidate": best[0],
"score": best[1], "rounds": round_ix + 1}
feedback = reasons # back-prompt with concrete objections
return {"ok": False, "candidate": None, "reasons": feedback,
"rounds": max_rounds}
Two properties make this worth the plumbing. It fails loudly: when no candidate passes, you get an explicit unsolved result with the objections attached, instead of a plausible wrong answer presented with confidence. And the guarantee it provides is exactly as strong as your critics and no stronger — which is an honest contract you can reason about, unlike "the model checked it".
A verification stage has three ways to ruin your system, and you should design against all three from the start.
It becomes the bottleneck. If verification costs as much as generation, best-of-8 costs 16x rather than 8x and the economics collapse. Budget for verification to be a small fraction of generation — the arithmetic in Lesson 1 assumed a small scoring model at under a tenth of the generator's price, and that is the right target. Order your checks from cheap to expensive and short-circuit: schema validation, then linting, then unit tests, then the expensive learned scorer only on what survives. A cascade also parallelizes trivially, since candidates are independent.
It becomes the leak. Any verifier you optimize against hard enough becomes a target. You watched this in Lesson 2's simulation: at n=64, selection actively sought out the 3% of wrong candidates that scored well. The same dynamic in RL training is covered in Model Specialization: Fine-Tuning & Agentic RL under reward hacking; at inference time the pressure is milder but the mechanism is identical, and it grows as . Defenses: cap n at the measured peak rather than the budget; ensemble two verifiers with different failure modes; keep a sound check in front of the learned one so gaming candidates must also be valid; and sample selected outputs for human review, because drift shows up there first.
It becomes the eval. The subtlest failure. If you select candidates with the same tests you report accuracy against, your reported accuracy is selection performance on the training signal and it will not survive contact with production. Keep three disjoint sets: tests visible to the agent, tests used for selection, and a held-out set used only for measurement. When someone reports a large jump from adding a verifier, the first question is always which set the numbers came from.
| No |
| One forward pass |
Property-based testing is the most underused of these with agents. Rather than asserting specific input-output pairs, you assert invariants — the sorted output is a permutation of the input, the serialize-then-deserialize round trip is the identity, the discount is never negative — and let a generator like Hypothesis hunt for counterexamples. Invariants are far harder for a model to satisfy accidentally than a handful of example tests, which makes them a much stronger selection signal. Differential testing is the other cheap win: if you have any independent implementation — an old rules engine, a slow reference function, a second model — run both on generated inputs and keep the candidate that agrees. No ground-truth labels required, only a second opinion that fails differently.
Solvers and proof assistants mark the far end of the spectrum. When you can formalize the problem, Z3 or Lean gives you soundness in the mathematical sense: no false positives, ever. The cost is the formalization itself, which is often harder than the original problem — which is precisely why the LLM is useful there. It is the translator; the solver is the judge.
Your agent generates Terraform plans. You have 40 labeled examples and a plan-validation CLI that catches malformed and policy-violating plans in about 200 ms. A teammate proposes training a PRM on the 40 examples to rank candidates. The better first move is:
Kambhampati and colleagues formalized the architecture this all points at, under the name LLM-Modulo. The claim behind it is deliberately deflationary: LLMs are excellent generators of candidate ideas and terrible guarantors of correctness, so stop asking them to be both. Pair the model with a bank of external critics that are sound in their domain, and let the loop run.
The shape is: the LLM proposes a candidate; every critic evaluates it; any critic that rejects returns a reason; the reasons are back-prompted into the LLM, which proposes again; repeat until all critics pass or a budget is exhausted. Critics come in two flavors — hard critics that are sound and whose verdict is final (a simulator, a solver, a type checker), and soft critics that express preference (style, cost, a learned reward model) and only rank among candidates that already passed the hard ones.
Work down this list and stop at the first row that describes your situation.
| Situation | Verifier to build |
|---|---|
| Output is executable and you can generate inputs | Execution plus property-based tests. Sound, cheap, no labels. |
| Output must satisfy explicit constraints | Schema or solver check as a hard critic; LLM-modulo loop around it. |
| Discrete answers, plenty of labeled outcomes, ranking only | ORM, or weighted self-consistency with it. |
| You need to prune partial solutions during a search | PRM, with rollout-based step labels if human labels are out of reach. |
| No labels, no checker, free-form output | Generative verifier with critique-then-score; calibrate against human labels before trusting it. |
| Stakes are high and the domain is formalizable | Solver or proof assistant. Slow, and the only thing that actually proves anything. |
You can now specify a verification stage the way you would specify a database: what it guarantees, what it costs per call, how it fails, and what happens when it is wrong. That specification is the prerequisite for everything in the next section, because search is only as good as the signal it follows — and a search with a bad verifier is just an expensive way to find the candidate that fools it.