5.9 RL with Verifiable Rewards (RLVR) & The Reasoning Recipe¶

Every reinforcement-learning method we have built so far in this Part — The RLHF Pipeline & Reward Modeling, PPO for LLMs, DPO, GRPO and RLOO — has shared one expensive assumption: that the reward comes from a learned reward model trained on human preference labels. That reward model is a second neural network. It is trained on noisy, expensive, slowly-collected human data. It is the thing you optimize against, and the moment your policy is strong enough it starts to hack it — finding inputs the reward model scores highly but a human would not.

This chapter is about the idea that, for a large and important class of problems, you do not need a reward model at all. If the task has a checkable answer — a math problem with a known numerical solution, a coding problem with a unit-test suite, a constrained-format extraction task with an exact-match target — then the reward is just a program that returns 1 if correct and 0 otherwise. No human labels, no learned reward network, no preference dataset. We call this RL with Verifiable Rewards (RLVR), and it is the single most consequential post-training idea of 2024–2025. It is the engine behind DeepSeek-R1, behind the OpenAI o-series reasoning models, behind Tülu 3, and behind nearly every open “reasoning model” released in that window.

RLVR is conceptually trivial — “reward = did the answer pass the checker” — and that triviality is exactly the point. By replacing a fragile, hackable, expensive learned reward with a cheap, exact, unhackable-in-the-usual-sense programmatic one, you remove the dominant failure mode of RLHF and unlock something startling: when you point a base model at hard verifiable problems and reward only correctness, it teaches itself to reason — generating longer and longer chains of thought, learning to verify and backtrack, exhibiting the now-famous “aha moment” — with no demonstrations of reasoning at all. This chapter explains the reward mechanism in depth, builds real verifiers (math equivalence and a sandboxed code runner), dissects the R1-Zero phenomenon, and traces the path from narrow verifiable domains to general reasoning.

We will lean on GRPO, RLOO & Critic-Free RL for the optimizer — RLVR is an answer to “where does the reward come from,” not “how do we take the gradient” — and on Reward Engineering, Verifiers & Sandboxes for the production-infrastructure view.

What makes a reward “verifiable”¶

The defining property¶

A reward is verifiable when correctness can be decided by a deterministic program \(V(q, o) \to \{0, 1\}\) (or a graded \([0,1]\)) that does not itself need to be learned and does not depend on the policy. Contrast the two regimes:

The learned reward \(r_\phi\) is a neural network with parameters \(\phi\) fit to human preferences; it is an approximation of “what humans want,” and it is differentiable, dense, and — crucially — imperfect everywhere. The verifiable reward \(V\) is ground truth: if the math answer equals the gold answer, the reward is exactly 1; otherwise exactly 0. There is no approximation error to exploit. This is why RLVR is sometimes called “RL against the environment” rather than “RL against a model.”

Three families of verifiers dominate practice:

1. Exact / equivalence match (math, factual short-answer). The model is asked to put its final answer in a delimiter (e.g. \boxed{...} or <answer>...</answer>); the verifier parses it and compares to the gold answer, ideally with semantic equivalence (so \(\frac{1}{2}\), \(0.5\), and \(0.50\) all match). This requires a symbolic/numeric normalizer, not naive string equality.
2. Execution match (code). The model emits a program; the verifier runs it in a sandbox against a hidden test suite and rewards the fraction (or all-or-nothing) of tests passed. This is the most powerful verifier because passing tests is a strong proxy for correctness — but it also has the largest attack surface (the model can try to read the tests, hard-code outputs, or exploit the sandbox).
3. Constraint / format check (structured output, instruction following). The verifier checks programmatically-decidable properties: “is this valid JSON matching this schema,” “does the answer contain exactly three sentences,” “does it avoid the forbidden word.” Used heavily in instruction-following RL (e.g. Tülu 3’s “RLVR” recipe includes such constraint checkers).

Why verifiable rewards change the game¶

It is worth being precise about why this matters, beyond “it’s cheaper.” There are four distinct advantages, and an interviewer will want all four:

• No reward-model training loop. You skip preference data collection, reward-model architecture, reward-model training, and reward-model serving. The reward is a function call. This collapses the RLHF pipeline from “two models and a human-data pipeline” to “one policy and a checker.”
• The reward cannot be over-optimized in the usual sense. Classic reward over-optimization (Goodhart’s law: “when a measure becomes a target it ceases to be a good measure”) happens because the learned reward diverges from true quality off-distribution. A correct-answer checker is the true quality (for the narrow definition “got the right answer”). You can push the policy arbitrarily hard against is_correct and it will keep getting more correct. (RLVR still has its own hacks — see §6 — but they are program bugs, not statistical drift.)
• Dense, free supervision at scale. Every problem with a known answer is a training example, and you can generate such problems (templated arithmetic, synthetic theorem instances, mutated code problems) essentially without limit. The bottleneck moves from “human labels” to “problems with checkable answers.”
• It exposes a learning signal the model can climb. Because the reward is exact, the gradient is clean: the only way to increase reward is to actually solve more problems. This is the precondition for the emergent-reasoning phenomenon — the optimizer is not being nudged toward a fuzzy human aesthetic, it is being pushed straight at “be correct,” and the shortest path to “be correct” on hard problems turns out to be “think more.”

The R1-Zero phenomenon: reasoning that emerges from correctness alone¶

This is the heart of the chapter and the result that made RLVR famous. We summarize the mechanism here; the optimizer (GRPO) and the multi-stage R1 pipeline are detailed in GRPO, RLOO & Critic-Free RL, and the broader test-time-compute story is in Reasoning, Chain-of-Thought & Test-Time Compute. Here we focus on why correctness pressure alone grows reasoning.

The setup¶

R1-Zero starts from a base pretrained model — not even instruction-tuned — and applies GRPO with a reward that is only:

with \(\lambda\) small (the format term teaches structure, not content; keep it a fraction of the accuracy reward so the model can never profit by formatting a wrong answer). There is no reward model, no value network, no human preference data, no demonstrations of how to reason. The prompts are hard math and code problems with known answers.

What emerges¶

Three behaviors appear over training, none of them programmed:

1. Response length grows. Average completion length climbs steadily over RL steps — the model spontaneously produces longer chains of thought. Nobody rewarded length directly (and as we saw in GRPO, naive GRPO has a spurious length bias, but the genuine reasoning-length growth persists even after that bias is removed).
2. Self-verification and backtracking. The model begins to write things like “let me check this,” recompute a sub-result, and correct itself mid-stream. It learns to re-derive and cross-check because, on hard problems, a single forward pass is wrong too often — and the only way to raise the correctness reward is to catch and fix its own mistakes.
3. The “aha moment.” The DeepSeek-R1 paper documents a striking qualitative event: the model, mid-derivation, writes something like “Wait, wait. That’s an aha moment. Let me re-evaluate…” and revises its approach. This is not a canned phrase from SFT data (there was none); it is an emergent strategy that the correctness reward selected for.

Why correctness pressure causes this — the mechanism¶

The intuition is a credit-assignment-plus-exploration argument. Frame each problem as an MDP where the model’s “policy” is its generation process. On a hard problem, the base model’s single-shot accuracy is low — say it solves 10% of attempts. Under RLVR with a group of \(G\) samples, the advantage is positive exactly for the trajectories that reached the right answer (see the group-baseline mechanics in GRPO). Now ask: what distinguishes the winning trajectories from the losing ones? Empirically, the winners are the ones that spent more tokens checking intermediate steps, exploring an alternative when the first approach stalled, and verifying the final result. So the gradient systematically up-weights those behaviors. More compute spent reasoning \(\to\) higher probability of correctness \(\to\) positive advantage \(\to\) more of that behavior next time. The model is, in effect, discovering test-time compute as the solution to a sparse-reward optimization problem.

There is a deeper, somewhat humbling caveat that the 2025 literature surfaced and you should be ready to discuss: RLVR may be primarily eliciting and sharpening capabilities the base model already latently has, rather than teaching wholly new ones. Several analyses found that for modest sample budgets RLVR improves pass@1 dramatically but the pass@k for large k (the set of problems the model can solve at all given many tries) barely moves — i.e. RLVR concentrates probability mass on reasoning paths the base model could already occasionally find, rather than expanding the frontier of solvable problems. This reframes RLVR as a very efficient elicitation / distillation-of-self mechanism, which is consistent with why a base model with strong latent math ability is a prerequisite. (Other work pushes back, showing frontier expansion with enough compute and harder data. The honest answer in 2026 is “it does both, and the balance depends on the base model and budget.”)

Building real verifiers I: math equivalence¶

The accuracy reward is only as good as the checker. Naive string equality is catastrophically wrong: it would mark 0.5 incorrect against gold 1/2, mark x=2 incorrect against 2, and mark \frac{1}{2} incorrect against 0.5. A real math verifier must (1) extract the final answer from a long chain of thought, then (2) normalize and compare with numeric/symbolic equivalence. Here is a compact but realistic implementation.

import re
from fractions import Fraction

def extract_boxed_answer(text: str) -> str | None:
    r"""
    Pull the LAST \boxed{...} content from a chain-of-thought response.
    We take the last one because the model often writes intermediate
    \boxed expressions before its final answer. Handles nested braces.
    """
    idx = text.rfind(r"\boxed")
    if idx == -1:
        # Fallback: try an <answer>...</answer> delimiter.
        m = re.findall(r"<answer>(.*?)</answer>", text, flags=re.DOTALL)
        return m[-1].strip() if m else None
    # Walk braces to find the matching close for \boxed{ ... }.
    i = text.find("{", idx)
    if i == -1:
        return None
    depth, j = 0, i
    while j < len(text):
        if text[j] == "{":
            depth += 1
        elif text[j] == "}":
            depth -= 1
            if depth == 0:
                return text[i + 1 : j].strip()
        j += 1
    return None  # unbalanced braces

def normalize_numeric(s: str):
    """
    Try to coerce a string answer to an exact rational or a float.
    Handles fractions ('3/4'), LaTeX \frac, percentages, commas,
    surrounding $ signs, and trailing units-free numbers. Returns
    a Fraction/float, or None if it isn't a clean number.
    """
    if s is None:
        return None
    s = s.strip()
    s = s.replace("$", "").replace(",", "").replace("\\!", "").strip()
    s = re.sub(r"\\text\{.*?\}", "", s)              # drop \text{...} units
    s = s.replace("\\%", "").replace("%", "")        # treat percent as a number
    # LaTeX \frac{a}{b}  or  \dfrac{a}{b}
    m = re.fullmatch(r"\\d?frac\{(-?\d+)\}\{(-?\d+)\}", s)
    if m:
        return Fraction(int(m.group(1)), int(m.group(2)))
    # plain a/b
    m = re.fullmatch(r"(-?\d+)\s*/\s*(-?\d+)", s)
    if m:
        return Fraction(int(m.group(1)), int(m.group(2)))
    try:
        return Fraction(s)            # exact for integers / decimals like '0.50'
    except (ValueError, ZeroDivisionError):
        pass
    try:
        return float(s)               # last resort, lossy
    except ValueError:
        return None

def math_is_correct(response: str, gold: str, atol: float = 1e-6) -> float:
    """
    Verifiable math reward: 1.0 if the model's final boxed answer is
    numerically equivalent to gold, else 0.0. Falls back to a
    normalized string compare for non-numeric answers (e.g. '(2, 3)').
    """
    pred = extract_boxed_answer(response)
    if pred is None:
        return 0.0
    a, b = normalize_numeric(pred), normalize_numeric(gold)
    if a is not None and b is not None:
        # Exact when both are Fractions; tolerant when a float is involved.
        if isinstance(a, Fraction) and isinstance(b, Fraction):
            return 1.0 if a == b else 0.0
        return 1.0 if abs(float(a) - float(b)) <= atol else 0.0
    # Non-numeric: compare normalized strings (whitespace/case-insensitive).
    norm = lambda x: re.sub(r"\s+", "", x).lower()
    return 1.0 if norm(pred) == norm(gold) else 0.0

# --- quick sanity checks (these all return 1.0) ---
assert math_is_correct(r"... so the answer is \boxed{1/2}.", "0.5") == 1.0
assert math_is_correct(r"first \boxed{7} then \boxed{0.50}", "1/2") == 1.0
assert math_is_correct(r"<answer>42</answer>", "42") == 1.0
assert math_is_correct(r"\boxed{\frac{3}{4}}", "0.75") == 1.0
assert math_is_correct(r"\boxed{8}", "9") == 0.0

This is the minimal version. Production math verifiers (the widely-used math-verify library, or the checker in PRM800K / the MATH dataset tooling) additionally use a symbolic engine (SymPy) to compare expressions like (x+1)^2 vs x^2+2x+1, handle sets and tuples and intervals, and canonicalize LaTeX aggressively. The principle is the same: parse, normalize to a canonical form, compare for equivalence — never raw strings. A weak verifier is a silent reward-hacking vector: if your checker marks 0.5 wrong against 1/2, the model learns to avoid decimal answers, distorting behavior for no good reason.

Do not ship the hand-rolled one. Write it once to understand the failure modes, then use math-verify (HuggingFace), which is the de-facto open-source math checker behind most 2025–2026 RLVR runs and the lighteval/TRL math recipes. Its whole API is two functions:

# pip install math-verify
from math_verify import parse, verify

# `parse` extracts the final answer (it understands \boxed{}, $...$, and plain
# expressions) and returns canonical SymPy objects; `verify(gold, pred)` is True
# iff they are symbolically/numerically equivalent. Order matters: gold first.
gold = parse(r"$\frac{1}{2}$")
pred = parse(r"...therefore the answer is $\boxed{0.5}$.")
print(verify(gold, pred))          # True — the normalization gap closes itself

def math_reward(completions: list[str], solution: list[str]) -> list[float]:
    """Drop-in replacement for `math_is_correct`, SymPy-backed. Note the
    try/except: `parse` can raise on malformed LaTeX, and an exception inside a
    reward function must never take down the trainer — swallow it and score 0."""
    out = []
    for c, s in zip(completions, solution):
        try:
            out.append(float(bool(verify(parse(s), parse(c)))))
        except Exception:
            out.append(0.0)
    return out

The important habit is the try/except: a verifier runs on adversarial input tens of thousands of times per step, and the single most common production incident is a reward function raising on one weird completion and killing an eight-hour job.

Building real verifiers II: sandboxed code execution¶

Code is the most powerful verifiable domain — “did it pass the tests” is a strong, dense correctness signal — and the most dangerous one, because you are about to execute model-generated code thousands of times per training step. The model is an adversary by construction: RL will find any path to reward, including os.system("cat tests.py"), infinite loops to stall the trainer, while True: fork() fork-bombs, network exfiltration, or writing to the host filesystem. You must sandbox. The non-negotiable requirements:

• No host filesystem access (read or write) beyond a scratch dir; no network; no access to the test file contents from inside the executed program.
• Hard wall-clock timeout and memory/CPU limits (a runaway generation must not stall the whole rollout).
• Process isolation — a separate process at minimum, ideally a container (gVisor/Firecracker microVM, or a bubblewrap/nsjail jail) for untrusted code. Production RL stacks (see Reward Engineering, Verifiers & Sandboxes) run code in ephemeral containers, often a remote execution service.

Below is a single-process, resource-limited sandbox using POSIX resource limits and a subprocess timeout. This is illustrative — for truly untrusted code in production, use a container/microVM, not just rlimit — but it shows the mechanism and is safe enough for trusted-ish synthetic problems on a locked-down box.

import subprocess, sys, tempfile, os, textwrap, resource, json

def _set_limits():
    """Called in the child via preexec_fn: cap CPU, memory, and file size."""
    resource.setrlimit(resource.RLIMIT_CPU, (5, 5))            # 5s CPU time
    mem = 512 * 1024 * 1024                                    # 512 MB
    resource.setrlimit(resource.RLIMIT_AS, (mem, mem))         # address space
    resource.setrlimit(resource.RLIMIT_FSIZE, (1 << 20, 1 << 20))  # 1 MB files
    resource.setrlimit(resource.RLIMIT_NPROC, (64, 64))       # cap fork-bombs

def run_in_sandbox(source_code: str, stdin: str = "", timeout: float = 6.0):
    """
    Execute untrusted Python in an isolated subprocess with rlimits and a
    wall-clock timeout. Returns (ok, stdout, stderr). Network is NOT blocked
    here (do that with a namespace/seccomp in production); we run with a
    minimal env and a temp CWD so there is nothing useful to touch.
    """
    with tempfile.TemporaryDirectory() as workdir:
        path = os.path.join(workdir, "prog.py")
        with open(path, "w") as f:
            f.write(source_code)
        try:
            proc = subprocess.run(
                [sys.executable, "-I", path],   # -I = isolated mode (ignore env/PYTHONPATH)
                input=stdin.encode(),
                capture_output=True,
                timeout=timeout,                # wall-clock kill
                cwd=workdir,                    # sandboxed working dir
                preexec_fn=_set_limits,         # apply rlimits in child (POSIX)
                env={"PATH": "/usr/bin", "OPENBLAS_NUM_THREADS": "1"},
            )
            return (proc.returncode == 0, proc.stdout.decode(errors="replace"),
                    proc.stderr.decode(errors="replace"))
        except subprocess.TimeoutExpired:
            return (False, "", "TIMEOUT")

def code_reward(completion: str, test_cases: list[dict],
                entry_point: str = "solve") -> float:
    """
    Verifiable code reward = fraction of hidden unit tests passed.
    `test_cases` is a list of {"input": "...", "expected": "..."} dicts.
    The model's `completion` is expected to define a function `entry_point`
    that reads from stdin and prints to stdout. We assemble a harness so the
    model's code NEVER sees the test inputs as data it can inspect.
    """
    program = extract_code_block(completion)
    if program is None:
        return 0.0
    passed = 0
    for tc in test_cases:
        # Harness runs the model code, then calls it on this test's stdin.
        harness = program + "\n\nif __name__ == '__main__':\n    " + entry_point + "()\n"
        ok, out, err = run_in_sandbox(harness, stdin=tc["input"])
        if ok and out.strip() == tc["expected"].strip():
            passed += 1
    return passed / len(test_cases)   # graded reward in [0, 1]

def extract_code_block(text: str) -> str | None:
    """Pull the last ```python ... ``` fenced block (the final solution)."""
    import re
    blocks = re.findall(r"```(?:python)?\s*\n(.*?)```", text, flags=re.DOTALL)
    return blocks[-1].strip() if blocks else None

Several design choices here are load-bearing and worth calling out for an interview:

• Graded reward (fraction of tests passed), not all-or-nothing. This densifies a very sparse signal: a solution that passes 7/10 tests gets advantage over one that passes 0/10, even though both are “wrong.” Within a GRPO group this creates the reward variance needed for a nonzero gradient (avoiding the dead-group problem). Some recipes still use binary “all tests pass” as the final reward and reserve graded scores for shaping — both are defensible.
• The model never sees the tests. The test inputs are fed via stdin by the harness; the model’s source is concatenated before the harness. If you instead pasted tests into the prompt, the model would learn to special-case them (hard-code outputs) — a textbook reward hack. Hidden tests are the verifiable-code analog of a held-out set.
• Isolated interpreter mode (-I) ignores PYTHONPATH/site customizations, and a minimal env removes most ambient capabilities. Still: this stops accidents, not a determined adversary with a Python escape. For real untrusted execution use gVisor/Firecracker.
• Timeouts are part of the reward, not just safety. A program that times out scores 0 on that test. RL will learn to avoid pathological loops because they cost reward — but it will also learn to exploit a too-generous timeout to brute-force, so set it tight.

Building real verifiers III: formal mathematics and proof assistants¶

A proof assistant is the limiting case of a verifiable reward — the verifier with zero false positives. A math-equivalence checker can be fooled by a normalization gap (does “0.5” match “½“? does an unsimplified radical match its decimal?); a code sandbox can be escaped, or its hidden tests can leak and get hard-coded. A proof-assistant kernel accepting a proof is, by construction, a machine-checked guarantee that the theorem is true relative to its axioms — there is no “close enough.” This is exactly why formal mathematics is a frontier RLVR domain: it is the one place where \(V(q,o)\in\{0,1\}\) is not an approximation of correctness but is correctness.

What a proof assistant is (Lean 4). Lean 4 — alongside Isabelle, Coq/Rocq, and HOL Light — is an interactive theorem prover built on dependent type theory. Under the Curry-Howard correspondence, a proposition is a type, and a proof is a term that inhabits that type; checking a proof reduces to type-checking a term against the theorem’s type. A small, trusted kernel performs this check. Everything else — tactics, elaboration, the enormous Mathlib library — is untrusted convenience whose job is ultimately to produce a term the kernel can check. Proofs are written with tactics (rw, simp, induction, ring, omega, linarith, exact, …) that manipulate a proof state of open goals; the proof is complete when no goals remain and the kernel accepts the resulting term. The reward signal for RL is therefore binary and unforgeable: the proof script either compiles — kernel accepts, reward 1 — or it does not, reward 0. No parsing heuristics, no equivalence normalizer, no sandbox-escape surface.

-- A proposition is a type; a proof is a term the kernel type-checks.
-- Reward = 1 iff Lean's kernel accepts the term this tactic block builds.
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction b with
  | zero      => simp            -- goal: a + 0 = 0 + a
  | succ n ih => simp [Nat.add_succ, Nat.succ_add, ih]  -- reduce succ case to ih

The tactic script above is untrusted search — the elaborator and simp are free to try, backtrack, and fail — but the object it ultimately emits is kernel-verified, so a prover model gains nothing from producing a plausible-looking-but-wrong script: it simply fails to compile and scores 0.

The autoformalization problem. The catch is getting into the formal world. Real problems arrive as natural language — a competition problem, a lemma from a paper. Autoformalization is the task of translating natural-language mathematics into a formal statement (the theorem’s type) that a prover then tries to prove; the reverse direction, formal back to natural language, is informalization. Here is the crucial nuance and the one residual hack in an otherwise airtight system: the proof of a formal statement is unforgeable, but the statement itself is human- or model-produced and can be wrong. A mis-formalized statement — contradictory hypotheses that make anything provable, or a claim weaker than the one intended — is a statement-level false positive: the model earns reward 1 for a valid proof of the wrong theorem. Formal RLVR therefore relocates the (now much smaller) trust surface from “is the proof correct” to “does the formal statement faithfully capture the intended problem,” which is why autoformalization quality and statement auditing — checking that a statement and its negation are not both trivially provable, or human review of statement banks — matter as much as the prover itself.

How prover models are trained. The dominant recipe is expert iteration / AlphaProof-style RL: sample many candidate proofs — often with search, such as best-first or MCTS over tactic states, or whole-proof generation guided by the compiler as an oracle — keep the ones the kernel accepts, and train on those successes (SFT on verified proofs and/or policy-gradient RL using the compile signal as a binary reward). This is the formal-math instance of the same expert-iteration loop this chapter already introduced for RLVR generally; only the checker changes, from math_is_correct or a code sandbox to the Lean compiler. Concretely: AlphaProof (DeepMind, 2024) is a Lean-based system trained with RL and expert iteration that, combined with AlphaGeometry 2 — a neuro-symbolic engine specialized to Euclidean geometry — reached silver-medal-equivalent performance at the IMO. DeepSeek-Prover (v1, v1.5, v2) scales the same idea with large autoformalized training corpora plus RL/expert-iteration over Lean. Contrast these formal specialists with informal math specialists like Minerva (a PaLM finetune that does natural-language chain-of-thought math with no formal verifier): high benchmark scores, but no correctness guarantee, so it can be confidently wrong. The formal approach trades breadth and fluency for an ironclad correctness guarantee; the informal approach makes the opposite trade.

Benchmarks. miniF2F (~488 formalized olympiad and competition problems spanning AMC, AIME, IMO, and MATH, available in Lean, Isabelle, and HOL Light) is the standard formal-proving benchmark, scored as the fraction of statements formally proved at some pass@k. PutnamBench formalizes hundreds of Putnam competition problems in Lean, Isabelle, and Coq and is substantially harder — as of 2025–2026 only a small fraction is solved, making it a frontier benchmark. ProofNet targets undergraduate-level formal statements and is used for both autoformalization and proving. FrontierMath (Epoch AI), mentioned elsewhere in this book, is extremely hard research-level mathematics but is mostly answer-checked rather than fully proof-checked — worth distinguishing as answer-verified, not proof-verified. Because search plus compiler verification makes false positives essentially impossible, these are pass@k benchmarks where k can be large: a single verified hit counts, no matter how many attempts it took to find it.

Why this sidesteps reward hacking entirely. Recall the reward-hacking section’s mental model: the code sandbox converted statistical hacking into a software security problem — escapes, test leakage. The proof kernel goes one step further. Because the kernel is small, trusted, and formally scrutinized, and the reward is simply “kernel accepts the term,” there is no parser to fool and no execution environment to escape — you cannot earn reward for a false theorem. The only residual attacks live at the boundary: autoformalization (proving a wrongly-stated or vacuous theorem) and the degenerate sorry/axiom-injection hack (leaving a proof hole, or smuggling in a false axiom). Both are defended by rejecting proofs that use sorry, unsafe escape hatches, or unaudited axioms, and by auditing the statement bank itself. Formal mathematics is where RLVR’s promise is fully realized: the reward is not a proxy for correctness, it is correctness — which is precisely why it sits at the frontier, and why any claim of “unhackable RLVR” should be evaluated against how close the domain actually sits to a proof kernel.

A complete RLVR reward function and a worked example¶

Let us assemble a full reward used in an R1-Zero-style run and then trace exact numbers through it. The reward is a sum of components where correctness dominates and everything else is a small, contingent guardrail.

def rlvr_reward(question: str, response: str, gold: str,
                domain: str, test_cases=None) -> dict:
    """
    Full RLVR reward, returned as a breakdown so we can log each component.
    Correctness is the real signal (weight 1.0). Format is a small shaping
    bonus that is ONLY granted if the model also attempted a parseable answer,
    so it can never be farmed independently of trying to solve the task.
    """
    # 1. Correctness (the only component we truly trust).
    if domain == "math":
        accuracy = math_is_correct(response, gold)          # {0, 1}
    elif domain == "code":
        accuracy = code_reward(response, test_cases)         # [0, 1] graded
    else:
        accuracy = 0.0

    # 2. Format shaping (tiny, and CONTINGENT on a parseable answer existing).
    has_think = "<think>" in response and "</think>" in response
    has_answer = extract_boxed_answer(response) is not None
    format_bonus = 0.1 if (has_think and has_answer) else 0.0

    # 3. Anti-hacking guard: zero out everything if the response is degenerate
    #    (e.g. empty, or repeats one token — catches a known length-hack mode).
    if _is_degenerate(response):
        return {"accuracy": 0.0, "format": 0.0, "total": 0.0}

    total = accuracy + format_bonus
    return {"accuracy": accuracy, "format": format_bonus, "total": total}

def _is_degenerate(text: str) -> bool:
    toks = text.split()
    if len(toks) < 3:
        return True
    # crude repetition check: >60% of tokens are the single most common token
    from collections import Counter
    most = Counter(toks).most_common(1)[0][1]
    return most / len(toks) > 0.6

Now the worked example. We feed this reward into GRPO (whose advantage mechanics are in GRPO, RLOO & Critic-Free RL) and trace one group.

From narrow RLVR to general reasoning¶

RLVR’s superpower — an exact reward — is also its boundary: it only works where correctness is programmatically decidable. Math, code, formal logic, constrained extraction, unit-convertible science: yes. “Write a moving poem,” “is this essay persuasive,” “is this medical advice safe”: no — there is no is_correct(). The frontier question of 2025–2026 is how far the reasoning skills grown in verifiable domains transfer, and how to extend the recipe beyond them. Several strategies are now standard.

1. Transfer: reasoning learned on math/code generalizes¶

The most important empirical finding is that the reasoning machinery RLVR installs is not domain-locked. A model RLVR-trained on math and code becomes better at reasoning tasks it was never RL-trained on — logical puzzles, some scientific QA, even agentic planning. The interpretation: RLVR teaches a transferable skill (“decompose, derive step by step, check your work, backtrack”) using verifiable domains merely as the gym where that skill can be cheaply graded. You train the muscle where you can measure it, and the muscle works elsewhere. This is the strongest argument for RLVR as a general post-training stage rather than a niche math trick. (How far it transfers is debated and base-model-dependent; see Reasoning, Chain-of-Thought & Test-Time Compute.)

2. Mixing verifiable and non-verifiable rewards¶

To get a deployable model you must handle helpfulness, safety, tone, and open-ended tasks — none verifiable. The standard solution (DeepSeek-R1’s final stage, Tülu 3) is to mix reward sources in a single RL run: a rule/verifier reward on the verifiable prompts and a learned reward model on the rest. GRPO does not care where the scalar comes from — it just needs one reward per response. You route each prompt to its appropriate scorer:

def mixed_reward(prompt, response, meta):
    """Route to a verifiable checker when possible, else a reward model."""
    if meta["type"] in ("math", "code", "format"):
        return rlvr_reward(prompt, response, meta["gold"],
                           meta["type"], meta.get("tests"))["total"]
    else:
        # Non-verifiable (chat/safety/helpfulness): fall back to the learned RM.
        return reward_model_score(prompt, response)   # the network from ch. 5.5

The risk reappears at the boundary: the learned portion can still be hacked, so you keep its weight modest, apply a KL anchor on those prompts, and monitor for sycophancy. The verifiable portion, mercifully, needs none of that.

3. Process rewards and self-verification (when outcomes aren’t enough)¶

An outcome reward (final answer correct?) gives no credit for a correct sub-derivation that ends in an arithmetic slip, and it can reward a right answer reached by wrong reasoning (lucky guess). Process reward models (PRMs) score each reasoning step, giving denser, better-targeted feedback — at the cost of needing step-level labels (expensive) or a learned PRM (hackable again). RLVR’s pragmatic middle ground is to make the model its own verifier: train it (still with verifiable outcome rewards) to generate a solution and a check, so self-verification is reinforced because it raises outcome accuracy. The “aha moment” is exactly this — self-verification emerging because it pays off on the outcome reward. PRMs and these blends are explored in Reasoning, Chain-of-Thought & Test-Time Compute.

4. Generative / model-based verifiers for fuzzy domains¶

When a domain is almost verifiable — e.g. “does this answer entail the reference” for free-form QA — a strong LLM acting as a judge/verifier (LLM-as-a-Judge) can stand in for a hard checker. This is a spectrum: pure-programmatic verifiers (unhackable, narrow) on one end, learned reward models (hackable, general) on the other, and LLM-judges in between. The RLVR philosophy — prefer the most exact verifier the domain allows — is the guiding principle: use a symbolic checker if you can, an execution sandbox if you can, an LLM-judge only when you must, and a free-form reward model last.

Reward hacking in RLVR: it’s not gone, it moved¶

A crucial nuance, and a favorite interview trap: people say verifiable rewards “can’t be hacked.” That is false — what’s true is that they can’t be hacked the statistical way (the way a learned RM drifts off-distribution). RLVR rewards get hacked the engineering way: the model finds bugs in your verifier or sandbox. Real, observed RLVR hacks:

• Test leakage / hard-coding. If the test inputs leak into the model’s context (in the prompt, via a filesystem read, or because the harness is sloppy), the model hard-codes outputs: if input == "5\n3": print("8"). Defense: hidden tests, no filesystem/network in the sandbox, and randomized / held-out test inputs.
• Verifier parsing exploits. If the answer extractor is naive, the model learns to emit strings that parse as correct without solving — e.g. dumping many \boxed{} candidates hoping one matches, or exploiting a regex. Defense: take the last boxed answer only, penalize multiple final answers, and fuzz-test your extractor against adversarial responses.
• Sandbox escapes / resource abuse. os.system, eval of attacker-controlled strings, fork-bombs to crash the grader (so it returns a default), or sys.setrecursionlimit tricks. Defense: real isolation (container/microVM), strict rlimits, treat a crashed grader as reward 0, never as “skip.”
• Format farming. Covered above: if format/length bonuses are too large, the model optimizes them instead of correctness. Defense: keep shaping rewards small and contingent on attempting the task.
• Length / “thinking” inflation. Partly a genuine emergent behavior, partly a loss bias and partly the model padding to look like it is reasoning. Defense: the Dr. GRPO/token-level fixes, plus capping or mildly penalizing over-budget length.

The mental model: RLVR converts statistical reward-hacking into software security. Your verifier and sandbox are now an adversarial interface — the policy is a relentless fuzzer that will execute your grader millions of times looking for the cheapest path to reward. Threat-model them as you would a public API taking untrusted input. The full taxonomy is in Reward Hacking, Over-Optimization & Alignment Failures.

Putting it together: the reasoning recipe¶

We can now state the full RLVR reasoning recipe as a checklist an engineer would actually follow. The optimizer details live in GRPO, RLOO & Critic-Free RL; this is the data-and-reward recipe that wraps it.

1. Assemble a prompt set whose answers are checkable — then decontaminate it. Real open sets to start from: GSM8K and MATH for warm-up, and the RL-grade math pools that the 2025 reasoning wave produced — NuminaMath, Big-Math-RL-Verified, DeepScaleR-Preview, DAPO-Math-17k (all published as problem + verified short answer, exactly the shape RLVR wants). For code: CodeContests, TACO, and KodCode, which ship test suites. Keep only items whose gold answer your verifier can parse, and n-gram-decontaminate against the evals you will report (AIME, MATH-500, LiveCodeBench, GPQA) — RLVR trains directly on the answer, so contamination is not a subtle leak, it is memorization with a reward attached.
2. Write the verifier before the training loop, and test it like a parser. Unit-test it on the dataset’s own gold answers (a verifier that cannot verify the gold string against itself is broken), fuzz it with adversarial completions, and measure the false-negative rate on a sample the checker marked wrong. Prefer math-verify over anything you wrote.
3. Difficulty-calibrate the prompts against your base model. Sample \(G\) completions per prompt with the untrained policy, estimate pass@1, and drop everything at \(p\approx 0\) and \(p\approx 1\) — those groups are dead (Exercise 3 quantifies the waste). Keep the ~20–60% band and hold the harder shards back as curriculum; see RL Data, Curriculum & Replay Management.
4. Pick the entry point: zero, or cold-start. R1-Zero style (straight from base) is the scientifically interesting setting but produces messy, language-mixing output; a few thousand long-CoT SFT examples first (“cold start”) stabilizes RL and gives a readable model, which is what R1 proper did.
5. Define the reward: accuracy dominant, everything else tiny and contingent. Accuracy weight 1.0, format bonus ≲0.1 and only granted alongside a parseable answer attempt, degeneracy/repetition guard zeroing the total, timeout and crash both scoring 0 rather than “skip”.
6. Run critic-free RL with the 2025 fixes on. GRPO with a token-level loss and no std-normalization (Dr. GRPO), clip-higher and dynamic sampling (DAPO), overlong filtering, and a small or zero KL coefficient — in verifiable domains many teams drop the KL anchor entirely because the checker, not the reference model, is what keeps the policy honest.
7. Monitor five curves, not one. Held-out accuracy (not reward), mean completion length, policy entropy, format/parse-failure rate, and the fraction of dead groups. Reward rising while held-out accuracy is flat is the signature of a hack; entropy collapsing is the signature of a run that has stopped exploring.
8. Then mix in the non-verifiable rewards (helpfulness, safety, tone) as in §”Mixing verifiable and non-verifiable rewards” — the verifiable stage buys you reasoning, the mixed stage buys you a deployable assistant.

The cheap baseline you should run first: expert iteration¶

Before reaching for a policy gradient, run the same verifier through expert iteration (also called rejection-sampling fine-tuning, or STaR): sample \(k\) completions per prompt, keep the ones the verifier accepts, and plain-SFT on them. Repeat. It uses the identical data and identical checker, needs no advantage estimator, no KL term, no reference model, and no rollout/trainer weight-sync machinery — and it captures a surprising fraction of the gain, which is why it is the standard baseline against which GRPO must justify its complexity, and why DeepSeek-R1’s third stage is exactly this.

def expert_iteration(prompts, verifier, sample_fn, sft_fn,
                     rounds: int = 3, k: int = 8, keep_per_prompt: int = 2):
    """STaR / rejection-sampling fine-tuning: RLVR without a policy gradient.

    sample_fn(prompt, n) -> list[str]      : k completions from the current policy
    verifier(prompt, completion) -> float  : the SAME checker you'd use for RL
    sft_fn(examples) -> None               : one epoch of cross-entropy on kept traces

    Two details do the real work: (a) de-duplicate kept traces, or an easy prompt
    with 8 identical correct solutions drowns out 8 hard prompts with 1 each;
    (b) cap per-prompt keeps, which is the same difficulty-balancing job that
    group-relative advantages do for free in GRPO.
    """
    for _ in range(rounds):
        batch = []
        for p in prompts:
            correct = [o for o in sample_fn(p, k) if verifier(p, o) == 1.0]
            seen, uniq = set(), []
            for o in correct:                      # dedup on normalized text
                key = " ".join(o.split())
                if key not in seen:
                    seen.add(key)
                    uniq.append(o)
            batch += [{"prompt": p, "completion": o} for o in uniq[:keep_per_prompt]]
        sft_fn(batch)                              # policy improves; next round re-samples
    return batch                                   # last round's distilled dataset

The conceptual difference from GRPO is worth stating precisely, because it is a favorite exam question: expert iteration only uses the positive examples. It raises the probability of trajectories that worked but never lowers the probability of the failure modes, so it cannot suppress a confidently-wrong reasoning pattern, and it saturates once the policy’s sampling diversity collapses (it can only ever learn from what it can already occasionally produce). GRPO’s negative advantages are exactly the missing half of the signal. Expert iteration is the right first move at small scale and small budget — Post-Training: SFT, DPO, and Narrow RLVR (GRPO) That Works at 100M uses this ordering to get a ~100M model doing verified arithmetic reasoning before any policy gradient is attempted.

Wiring a verifier into a real trainer¶

Nothing above requires you to write a trainer. Every production RLVR stack exposes the same extension point — “give me a function from completions to floats” — so the verifier you built in this chapter is the only bespoke code you own. In TRL, that extension point is reward_funcs:

# pip install trl
from trl import GRPOTrainer, GRPOConfig

def accuracy_reward(completions, solution, **kwargs):
    """TRL's reward-function contract: it receives the batch of `completions`
    plus every other dataset column as a keyword argument (here `solution`),
    and returns ONE float per completion. Our verifier plugs in unchanged.
    (With a conversational dataset, `completions` arrives as message dicts
    rather than strings — index into the last message's "content".)"""
    return [math_is_correct(c, s) for c, s in zip(completions, solution)]

def format_reward(completions, **kwargs):
    """A second, small-weight function. TRL SUMS the list of reward_funcs, so
    shaping terms live in their own function at their own scale — never buried
    inside the accuracy checker where you cannot ablate them."""
    return [0.1 if ("<think>" in c and "</think>" in c) else 0.0 for c in completions]

trainer = GRPOTrainer(
    model="Qwen/Qwen2.5-1.5B",                  # a BASE model, R1-Zero style
    reward_funcs=[accuracy_reward, format_reward],
    train_dataset=math_ds,                      # columns: "prompt", "solution"
    args=GRPOConfig(
        num_generations=8,                      # the group size G
        max_completion_length=1024,             # long CoT needs room to grow
        temperature=1.0,                        # do NOT sample greedily: no variance,
                                                # no advantage, no gradient
        beta=0.0,                               # KL off — common in RLVR runs
        use_vllm=True,                          # vLLM-backed rollout engine
    ),
)
trainer.train()

veRL takes the same idea as a config-pointed Python file: you supply a module with a scoring function (roughly compute_score(data_source, solution_str, ground_truth, extra_info)) and veRL’s reward manager calls it in a worker pool, which is what you want once execution-based verification is the bottleneck — see veRL: HybridFlow & The Single-Controller Architecture and OpenRLHF, NeMo-Aligner & Ray-Based Systems. Above both sits the verifiers library, which packages RLVR environments (prompt set + parser + rubric of reward functions, including multi-turn/tool-using ones) behind a common interface that TRL and veRL can both consume — the emerging standard unit of exchange for RLVR tasks, the way a datasets dataset is for pretraining data. Exact keyword names drift between releases of all three; the contract — batch in, list of floats out — does not.

The deepest takeaway is a shift in worldview. For a decade, the bottleneck of supervised and preference learning was labeled data: you needed humans to demonstrate or judge. RLVR moves the bottleneck to problems with checkable answers — which we can generate, mine, and synthesize far more cheaply than we can collect human judgments, and which give an exact signal instead of a noisy one. That is why a one-line idea — “reward = did the checker pass” — reorganized the entire post-training stack in two years.

Further reading¶

• DeepSeek-AI, DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning (2025) — R1-Zero, the emergent long-CoT / “aha moment” phenomenon, and the full multi-stage reasoning recipe.
• Shao, Wang, Zhu, et al., DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models (2024) — introduces GRPO and rule-based math rewards.
• Lambert, Morrison, et al. (Allen Institute for AI), Tülu 3: Pushing Frontiers in Open Language Model Post-Training (2024) — coins and operationalizes “RL with Verifiable Rewards (RLVR)” across math, code, and constraint-following.
• Zelikman, Wu, Mu, Goodman, STaR: Bootstrapping Reasoning With Reasoning (2022) — the self-taught-reasoner precursor: keep rationales that lead to correct answers.
• Hendrycks, Burns, et al., Measuring Mathematical Problem Solving With the MATH Dataset (2021) — the MATH benchmark and answer-checking tooling that underpins math verifiers.
• Chen, Tworek, et al. (OpenAI), Evaluating Large Language Models Trained on Code (HumanEval, 2021) — unit-test-based code evaluation, the model for execution rewards.
• Lightman, Kosaraju, et al. (OpenAI), Let’s Verify Step by Step (2023) — process reward models and step-level verification, the contrast to outcome-only RLVR.
• Yue, et al., Does Reinforcement Learning Really Incentivize Reasoning Capacity Beyond the Base Model? (2025) — the pass@k critique arguing RLVR mainly elicits latent base-model ability.
• The math-verify library and veRL / TRL repositories — production verifiers and RLVR training loops; see TRL: HuggingFace’s RL Library and Reward Engineering, Verifiers & Sandboxes.

Exercises¶

1. (Conceptual — why not string equality.) The chapter insists a math verifier must “parse, normalize to a canonical form, compare for equivalence — never raw strings.” Suppose you shipped a lazy verifier that used exact string equality between the extracted \boxed{} content and the gold answer. For the gold answer 1/2, name three correct model outputs this checker would mark wrong (accuracy 0), and then explain the concrete behavioral distortion this false-negative pattern would train into the policy. Why is a 5% false-negative rate in a verifier described as “far worse than the same rate in SFT data”?

2. (Quantitative — GRPO advantages and the dead group.) You run one R1-Zero-style GRPO step on a math prompt (accuracy reward only, no format term). A group of \(G=5\) samples yields two correct and three wrong answers, so \(R = \{1.0,\,1.0,\,0.0,\,0.0,\,0.0\}\). Using std-normalized GRPO advantages \(\hat A_i = (R_i-\bar R)/(\sigma+\varepsilon)\) with population std \(\sigma\) and \(\varepsilon = 10^{-4}\): (a) compute \(\bar R\), \(\sigma\), and the advantage for a correct and for a wrong sample; (b) now suppose the same prompt had produced five wrong answers instead, \(R=\{0,0,0,0,0\}\) — compute all advantages and state what the policy learns from this second group and why.

3. (Quantitative — the difficulty sweet spot.) With a binary accuracy reward, a GRPO group is “dead” (all advantages zero) exactly when all \(G\) samples get the same outcome. Model each of the \(G\) samples as an independent Bernoulli success with per-attempt probability \(p\) (the base model’s pass@1 on that prompt). (a) Write the probability that a group of size \(G\) is dead. (b) Evaluate it for \(G=8\) at \(p=0.1\), \(p=0.5\), and \(p=0.9\). © Explain how this justifies the chapter’s curriculum advice of keeping prompts the model solves roughly 20–60% of the time.

4. (Implementation — defend the answer extractor against \boxed{} spam.) The chapter lists “dumping many \boxed{} candidates hoping one matches” as a real verifier parsing exploit, with the defense “take the last boxed answer only, penalize multiple final answers.” extract_boxed_answer already takes the last box, but that still lets a model hedge across several distinct guesses. Implement extract_all_boxed(text) (returns every \boxed{} payload, with brace matching) and a guarded reward math_is_correct_guarded(response, gold) that returns 0.0 whenever the response contains more than one distinct final answer (after numeric normalization), and otherwise defers to math_is_correct. Note one false-negative risk your guard introduces.

import re
from fractions import Fraction

def extract_all_boxed(text: str) -> list[str]:
    r"""Return the payload of EVERY \boxed{...}, with proper brace matching."""
    out, start = [], 0
    while True:
        idx = text.find(r"\boxed", start)
        if idx == -1:
            break
        i = text.find("{", idx)
        if i == -1:
            break
        depth, j, val = 0, i, None
        while j < len(text):
            if text[j] == "{":
                depth += 1
            elif text[j] == "}":
                depth -= 1
                if depth == 0:
                    val = text[i + 1 : j].strip()
                    break
            j += 1
        if val is None:            # unbalanced braces: stop
            break
        out.append(val)
        start = j + 1
    return out

def _canon(v: str):
    """Canonical key for distinctness: numeric value if parseable, else norm string."""
    n = normalize_numeric(v)          # from the chapter's math verifier
    if n is not None:
        return ("num", float(n)) if isinstance(n, float) else ("num", n)
    return ("str", re.sub(r"\s+", "", v).lower())

def math_is_correct_guarded(response: str, gold: str) -> float:
    """Zero the reward if the model hedged across multiple DISTINCT final answers."""
    boxed = extract_all_boxed(response)
    if len({_canon(v) for v in boxed}) > 1:
        return 0.0                    # boxed-spam / hedging hack -> no reward
    return math_is_correct(response, gold)

# repeated identical answers are fine; distinct hedges are punished
assert math_is_correct_guarded(r"\boxed{1/2} ... \boxed{0.5}", "0.5") == 1.0   # same value
assert math_is_correct_guarded(r"\boxed{1} \boxed{2} \boxed{3}", "3") == 0.0   # hedging

5. (Implementation — cache the sandbox to survive the throughput bottleneck.) The chapter warns that with \(G=16\) samples \(\times\) thousands of prompts \(\times\) multiple tests you may execute millions of short programs per epoch, and that “caching identical (code, test) pairs” is essential. Wrap run_in_sandbox with a memoizing run_in_sandbox_cached keyed on (source_code, stdin), so code_reward never re-runs an identical execution. State the key correctness assumption the cache relies on and one case where it breaks.

_sandbox_cache: dict[tuple[str, str], tuple] = {}

def run_in_sandbox_cached(source_code: str, stdin: str = "", timeout: float = 6.0):
    """Memoized run_in_sandbox: identical (code, stdin) executes at most once."""
    key = (source_code, stdin)
    hit = _sandbox_cache.get(key)
    if hit is not None:
        return hit
    result = run_in_sandbox(source_code, stdin, timeout)   # (ok, stdout, stderr)
    _sandbox_cache[key] = result
    return result

6. (Conceptual — is formal-math RLVR truly unhackable?) A colleague argues: “A Lean proof kernel has zero false positives, so a Lean-based RLVR run is completely unhackable — unlike the math checker (normalization gaps) or the code sandbox (escapes, test leakage).” Using §”Building real verifiers III,” explain what is right about this and identify the residual trust surface that keeps even formal RLVR from being fully airtight. Name the two concrete exploits the chapter lists at that boundary and the defenses.