4  Learned, Programmatic, and Hybrid Verifiers

M. C. Escher, Dolphins (1923).

4.1 Chapter Map

  • Distinguish the programmatic verifier core of RLVR from learned verifiers.
  • Explain how hybrid stacks combine checks, and the failure modes introduced.

4.2 Programmatic versus Learned Verifiers

Recall the quadratic example from Chapters 2 and 3: a model correctly finds both roots of \(x^2-5x+6=0\), then reports only \(x=2\). A programmatic checker can reject the incomplete final answer. A learned process verifier can separately assess the four correct intermediate steps. Combining them raises a different question from where to place the reward: which component checks which property, and how should their verdicts be combined?

Chapters 2 and 3 classify verifiers by whether they apply on the final artifact or on intermediate steps in the rollout. This chapter changes axes, as we discuss how the verifier itself is implemented:

Programmatic verifiers are deterministic, auditable, and brittle. Examples include: regex-based answer extraction, symbolic equivalence checking (as in Math-Verify), unit-test execution in a sandbox, static analysis and linting, proof-kernel acceptance, and format-validation rules (Kydlicek 2025; Le et al. 2022).

Learned verifiers are flexible, soft-scored, and opaque. They are not verifiable rewards in the narrow sense; instead, a model is trained or prompted to judge another model’s output. This covers ambiguity, open-endedness and edge cases, but inherits the biases and blind spots of the judge model.

4.3 Programmatic verifiers

Table 4.1: Programmatic verifiers by domain.
Domain Programmatic checks Checkable core
Math Answer extraction, canonicalization, symbolic equivalence Closed-form answers with known ground truth
Code Sandbox execution, test suites, linters, static analysis Functional behavior covered by tests
Proof Kernel acceptance (Lean, Coq, Isabelle) Validity of the submitted proof under the formal system’s assumptions
Format Regex, XML schema, JSON schema, tag-structure validation Output-contract compliance

Programmatic verifiers have explicit, auditable acceptance rules, although their implementations and test coverage can still have blind spots. For example, a symbolic equivalence checker either recognizes two expressions as equal or it does not, and a unit test either passes or fails. A passing test establishes the behavior covered by that test, not every correctness property of the program (Liu et al. 2023). In Lean, tactics construct proof terms for the kernel to check; kernel acceptance is not a separate judgment that every tactic was appropriate or that the formal statement captures the intended task.

4.4 Learned verifiers

4.4.1 LLM-as-a-Judge

The simplest form of learned verification is prompting a strong LLM to evaluate a weaker model’s output. Zheng et al. called the paradigm LLM-as-a-Judge (Zheng et al. 2023). An LLM takes the output and produces a judgment: e.g. a scalar score, a classification, etc. We use the output as reward signal or selection criterion, Zheng et al. found that GPT-4 agreed with human preferences in over 80% of comparisons on MT-Bench and Chatbot Arena when ties were excluded, but this only measures preference agreement, not correctness on arbitrary tasks.

A simple extension to this approach is sampling multiple judges to get a majority vote over trajectories; GenRM-CoT samples multiple verification rationales from one verifier and averages their “Yes” token probabilities, rather than polling independently trained judges (Zhang et al. 2025). Compellingly, James Evans described an empirical accuracy benefit from using an odd number of judges in work by Google’s Paradigms of Intelligence team (Kim et al. 2026).1

Nevertheless, agreement rates hide systematic biases, of which Zheng et al. identified four:

  1. position bias (the judge prefers whichever response appears first)
  2. verbosity bias (longer responses are rated higher regardless of quality)
  3. self-enhancement bias (a model rates its own outputs higher than a different model’s outputs of equal quality)
  4. limited mathematical reasoning (the judge makes errors when evaluating mathematical correctness that a symbolic checker would catch trivially)

Of note that models of today’s capability likely do not suffer such biases to the same extent as in 2023. Notwithstanding, studies as recently as June 2026 demonstrate that there is still systematic self-preferential bias within today’s models (Yang et al. 2026).

4.4.2 Reward model ensembles

Ensembles are the simplest hybrid stacks, combining multiple judgments homogeneously without layering different verification modalities. Eisenstein et al. studied ensembles of reward models for RLHF and found that they mitigate but do not eliminate reward hacking, a more negative conclusion than Coste et al. reached in a synthetic setup, where conservative ensemble objectives practically eliminated over-optimization for best-of-\(n\) sampling (Eisenstein et al. 2023; Coste et al. 2023). Ensembles that differ in pretraining seeds generalize better than those that differ only in fine-tuning seeds, because the former have more diverse internal representations, and less-overlapping blind spots (Eisenstein et al. 2023).

4.4.3 The calibration problem

Learned surrogate verifiers produce scores, but those scores need not be calibrated against one another. A judge that outputs 0.8 does not mean the solution has an 80% chance of being correct; it means 0.8 is the number the judge’s training objective learned to assign to solutions with that surface profile. Lambert et al. documented this systematically in RewardBench, showing that reward models exhibit large accuracy gaps across domains, and that different training methods (classifier-based, DPO-based, generative) have different calibration profiles (Lambert et al. 2024).

For verifier-stack design, the calibration gap means that raw scores from a learned component cannot be compared directly to outputs from a programmatic component. If a symbolic checker returns “match” and a learned judge returns 0.7, the arbitration logic must account for the fact that 0.7 from the judge does not carry the same epistemic weight as a deterministic pass from the checker. In other words, treating both as commensurable scalars and averaging them is a mistake.

4.5 Hybrid stacks

Hybrid stacks layer verifier components together to robustify reward signal. Unit tests can check functional correctness and specific security properties, but cannot establish general security or judge readability. By the same token, a proof kernel checks validity, but it does not judge whether the theorem was worth proving. Therefore, we combine multiple verifiers together.

One mental model is to think of each verifier as producing a useful signal over a subset of inputs in some high-dimensional vector space. Outside that subset, it may return confident errors rather than remain silent. Stacking verifiers can extend this coverage, and the design problem in a hybrid stack is to determine how to compose rewards commensurately, and how failure modes interact when composed.

OpenAI’s public reinforcement fine-tuning API exposes this pattern as multigrader composition, where string checks, score-model graders, and Python execution can be combined into a single grader (OpenAI 2026). In agent evaluation, Anthropic similarly describes verifiers ranging from exact string comparison to enlisting Claude to judge a response (Anthropic 2025).

Click a tab to see how each verification regime scores the same trajectory.

Step Reasoning Score Source
Figure 4.1: The same trajectory scored by two verification regimes. The PRM assessments are illustrative; how they become training credit depends on the reward construction and optimizer discussed in Chapter 5.

4.6 Formalization

A verifier stack with \(K\) components can be written as:

\[ r_{\text{stack}}(x, y) = \operatorname{Arb}\bigl(v_1(x, y),\, v_2(x, y),\, \ldots,\, v_K(x, y)\bigr) \tag{4.1}\]

where each \(v_i\) is a verifier component that may return a score, a categorical verdict, a vector of step assessments, or a null (indicating abstention), and \(\operatorname{Arb}\) maps these outputs to the final reward, including when components abstain.

Common arbitration patterns include:

  • Priority cascade: check \(v_1\) first; if it returns a verdict, use it; otherwise check \(v_2\), and so on.
  • Weighted aggregation: map outputs to numeric scores \(s_i(x, y)\) on a common reward scale, then compute \(r = \sum_{i \in A} w_i \, s_i(x, y)\) over the non-abstaining components \(A\). Define a fallback if all components abstain. This constructs a reward, not a calibrated probability of correctness.
  • Gated routing: a classifier decides which component to invoke based on input features.
  • Unanimous agreement: require all components to agree before assigning a positive reward.

The choice of arbitration pattern determines the stack’s effective false-positive and false-negative rates. Priority cascade is biased toward the first component’s failure modes. Weighted aggregation can dilute strong signals with weak ones. Gated routing’s errors depend on the routing model. Unanimous agreement can suppress correct outputs; there is no universally correct choice.

4.6.1 Hybrid verifier in code

This code snippet reuses Chapter 2’s answer-extraction and canonicalization helpers; gold is the reference answer in canonicalized form. A parsed mismatch returns zero, while an answer that is missing or cannot be parsed goes to a learned fallback, which receives both the problem and the complete reference answer.

def symbolic_reward(completion: str, gold: tuple[str, ...]) -> float | None:
    answer = extract_answer(completion)
    if answer is None:
        return None
    candidate = canonicalize_answer(answer)
    if not candidate:
        return None
    return float(candidate == gold)

def hybrid_reward(
    problem: str,
    completion: str,
    gold: tuple[str, ...],
    judge,
    *,
    threshold: float,
) -> float:
    if not 0.0 < threshold <= 1.0:
        raise ValueError("threshold must be in (0, 1]")

    exact = symbolic_reward(completion, gold)
    if exact is not None:
        return exact

    judge_score = judge(
        problem=problem,
        completion=completion,
        reference_answer=gold,
        rubric=(
            "Score final-answer correctness from 0 to 1 against the complete "
            "reference answer for this problem. Reject missing or incomplete "
            "answers; do not infer omitted answers from intermediate reasoning."
        ),
    )
    if not 0.0 <= judge_score <= 1.0:
        raise ValueError("judge score must be finite and in [0, 1]")
    return float(judge_score >= threshold)

threshold can be thought of as a value tuned by a task expert or arrived at by balancing false accepts against false rejects.

4.7 Limitations

Adding components to a verifier stack can amplify errors rather than cancel them.

Silent disagreement. Two stack components can return conflicting verdicts on the same input.

Correlated failures. Components can fail on the same hard input, so do not assume that error probabilities multiply as if the components were independent.

Excessive complexity. Adding a component can improve average performance while increasing stack complexity and interpretability costs.

4.8 Open questions

  • When should learned judges be first-class stack components that score every output, rather than fallbacks invoked only on the programmatic residual?
  • What is the ceiling on stacking beyond which debugging costs exceed the gains?
  • Can the marginal value of each stack component be quantified before deployment, or must it be measured empirically on the target task distribution?

4.9 What comes next

The verifier stack defines what gets checked and how, not how those checks become training signal. A stack returning binary outcomes, one returning graded scores, and one returning step-level annotations will produce different learning dynamics even if they agree on output correctness. Transforming verifier outputs into something an optimizer can use is the subject of Chapter 5.


  1. The observation about the number of judges was shared in direct conversation between the book’s author and James Evans, a coauthor of the cited paper.↩︎