Reinforcement Learning and Verifier-Gated Reasoning

📍 Where we are: Part V · Neural Depth: Chain-of-Thought and RL — Chapter 14. Chain-of-Thought recovered serial depth by unrolling computation into generated steps, and measured how one corrupted intermediate state derails everything after it; this chapter installs the instrument that stops the corruption at the door, and then learns a better proposer from the door's judgments.

The previous chapter left us with a machine that can reach the right depth but cannot promise the right steps; the classical engines of Volumes 1 and 2 had the opposite profile, every step certified, nothing learned. This chapter composes the two. A policy (a trainable distribution over candidate steps) proposes derivations; an exact verifier (a rule-instantiation check borrowed unchanged from Volume 1) admits or rejects each step. The composite inherits the best clause of each contract: soundness by construction from the gate, learnability from the policy. The companion runs the full argument on the academic world, including its sharpest turn, which is a failure: reward the policy for producing verified facts and it learns to farm valid-but-irrelevant ones. A validity check says a step is correct, not that it is progress, and everything interesting about reinforcement learning for reasoning lives in that gap.

The simple version

Imagine a brilliant but careless apprentice writing proofs on a whiteboard while a pedantic librarian stands beside it with an eraser. The apprentice writes fast and guesses freely; the librarian checks each line against the rulebook and instantly erases anything that does not follow from what is already on the board. Whatever survives on the whiteboard is guaranteed correct, no matter how wild the apprentice is, because the librarian never sleeps. Now train the apprentice by watching which of their surviving lines actually finished proofs, and they get genuinely better. But pay the apprentice per surviving line and something perverse happens: they discover that copying easy, true, useless lines fills the board fastest, and they stop proving anything. The librarian guarantees truth; only the reward defines progress.

What this chapter covers

• The proposer/verifier pattern: the division of labor stated as a design principle, its ancestry in Volume 4's translate-then-prove factorization and in verifier-guided proof search, and what is new here: learning the proposer from the verifier's judgments.
• An exact environment: states as derived-fact sets over the academic knowledge base, actions as rule instantiations from a noisy softmax policy, and the gate as one constant-cost re-derivation check, quoted from the committed code.
• The damage of trusting: ungated chains commit wrong facts at the measured rate of 0.247, and roughly one in nine of those wrong facts is manufactured by an honest step applied to polluted premises.
• Soundness by construction: verifier-constrained decoding keeps every derived set inside the true closure at every budget, proved by a three-line induction and checked across 6,612 accepted steps, with recall the committed budget curve.
• Expert iteration derived and run: sample gated chains toward goals, keep verified successes, refit the proposal logits by a maximum-likelihood gradient we derive in full; success climbs 0.205 → 0.343 → 0.463 → 0.535 with no learned reward model anywhere.
• The reward-hacking exhibit: two rewards, verified-fact count versus goal F1, and the committed collapse: the membership-rewarded policy derives more verified facts than an untrained one while its relevance falls below even the uniform baseline.
• Process supervision positioned: per-step judgment is exactly what an exact verifier gives for free; where the frontier lacks the oracle it trains one, and inherits every audit obligation of Parts I through III.

The division of labor: the policy proposes, the verifier disposes

State the pattern first, because it is a design principle before it is an algorithm. Split the reasoning system into two components with asymmetric contracts. The proposer is statistical: it generates candidate steps, it is allowed to be wrong, and it is the only part that learns. The verifier is exact: it accepts or rejects each candidate by re-deriving it against ground truth, it never learns, and in our fragment it is cheap. The composite satisfies a contract neither component satisfies alone: everything the system asserts passed the verifier, so assertions are sound however bad the proposer is, and everything the system finds was proposed by the policy, so coverage improves as the policy improves. Fallibility is quarantined in the component that can be trained; correctness is anchored in the component that cannot be corrupted.

This series has met the pattern before. Volume 4's translate-then-prove factorization put a fallible parser in front of an exact engine: the translation could be wrong, but conditional on it, the proof was certified. The modern verifier literature grew along the same seam. It opened with learned verifiers reranking sampled math solutions, a proposer/checker split in which both halves are neural [1]; it sharpened when per-step judgments were shown to train more reliable verifiers than outcome-only judgments [2]; it became a learning loop when self-generated rationales, filtered by final-answer correctness, were fed back as training data [3]; and it became a search procedure when a verifier's step scores guided stepwise proof generation, NLProofS being the canonical instance [4]. What is new in this chapter is the feedback edge: the verifier's judgments are not just a filter on outputs but a training signal for the proposer. That closed loop is reinforcement learning, and it arrives with reinforcement learning's characteristic pathology, which the last third of this chapter measures.

One distinction before the machinery, because the whole chapter turns on it. A verifier answers exactly one question: does this step follow from what is already established? That is a correctness signal. It does not answer: does this step bring the derivation closer to the goal? That is a progress signal, and no soundness check provides it. Deriving researcher(erin) from student(erin) is perfectly valid and perfectly useless if the goal is a citation chain.

The policy proposes, the exact gate disposes: soundness holds by construction at every budget, learning lifts recall and success, and the reward alone decides whether verified steps are progress or farming. Original diagram by the authors, created with AI assistance.

The environment: an exact game over the academic world

The companion verifier_gate.py builds the smallest environment in which every claim above can be tested and none can be faked. The world is Volume 1's, imported and never retyped (verifier_gate.py lines 63–65): the 23 base facts of the academic knowledge base and its 7 Horn rule templates, indexed 0 through 6 (researcher from professor, researcher from student, person from researcher, the grandAdvisor composition, the colleague rule with its inequality guard, and the two citesTransitively rules, base case and recursive case). Ground truth is the least fixpoint $\mathrm{lfp}(T_P)$, where $T_P$ is the immediate-consequence operator of Volume 1: applied to a fact set $F$, $T_P(F)$ is $F$ together with every rule head whose body is satisfied in $F$, and iterating from the base facts until nothing changes yields the closure (forward_chain.py lines 42–63). On this world the closure has 47 atoms: 23 base facts plus 24 derivable atoms, of which 6 are multi-hop goals, the grandAdvisor and citesTransitively atoms that need composition or recursion (verifier_gate.py lines 70–84).

The reinforcement-learning reading of this world is direct. A state is the set $D$ of facts derived so far, starting at the base facts. An action is a candidate step: a rule template $r$ together with a conclusion atom. The policy is deliberately minimal so that every gradient in this chapter can be written by hand: a vector of 7 logits $\mathbf{z} \in \mathbb{R}^{7}$ (one real-valued score per rule template; $\mathbb{R}^{7}$ is the space of lists of seven real numbers) passed through a softmax, $\pi_k = e^{z_k} / \sum_{j} e^{z_j}$, where the sum in the denominator runs over all seven templates and turns the scores into a probability distribution. Each step samples a template $r \sim \pi$, grounds it against $D$ (collecting every fresh conclusion the template licenses right now), and picks one conclusion uniformly. Then the environment's honesty device fires: with probability $\varepsilon = 0.25$ a seeded corruption channel splices a uniformly drawn constant into one argument slot of the conclusion, standing in for an imperfect neural proposer that misreports what it derived (verifier_gate.py lines 141–149). The module is candid about what this miniature omits: the logits do not depend on the state, so the policy is a bandit (a decision problem where the same fixed action distribution is used regardless of state) rather than a sequence model, and the proposer's errors are an explicit noise channel rather than an emergent property (verifier_gate.py lines 41–44). Those simplifications are what make every number below exactly reproducible.

The gate is the chapter's centerpiece instrument, so here it is in full (verifier_gate.py lines 107–120):

def verify_step(r_idx: int, proposed: tuple, derived: set) -> bool:
    """THE GATE — Volume 1's exact step verifier, never a learned score:
    a proposed step is valid iff it instantiates rule ``r_idx`` against
    the facts derived so far, i.e. ∃σ with head·σ = proposed and every
    body atom·σ ∈ ``derived``.  Seeding ``_match_body`` with mgu(head,
    proposed) is equivalent (head variables bound first, the body match
    binds the rest) and RE-DERIVES the step, never trusting the proposer."""
    head, body = RULES[r_idx]
    # σ₀ = mgu(head, proposed); None ⇒ not even an instance of the head.
    sub0 = unify(head, proposed, {})
    if sub0 is None:
        return False
    # Valid iff σ₀ extends to satisfy the WHOLE body inside `derived`.
    return next(_match_body(body, derived, sub0), None) is not None

Decode the check. A substitution $\sigma$ is an assignment of constants to the rule's variables; the claim "step is valid" means there exists a $\sigma$ under which the rule's head becomes exactly the proposed atom and every body atom becomes a fact already in $D$. The code finds $\sigma$ in two stages: unify(head, proposed, {}) computes the most general unifier of the head with the proposal (binding the head's variables), and _match_body, imported from Volume 1's forward chainer (forward_chain.py lines 19–39), extends that binding through the body atoms left to right against $D$. Nothing the proposer says is trusted; the step is re-derived from scratch. Note the cost: one head unification (constant work for fixed arity) plus a body match against the derived set, polynomial in $\lvert D \rvert$, the number of facts derived so far (the bars $\lvert\cdot\rvert$ denote the size of a set), with degree the body length, and effectively constant on this 47-atom world. This cheapness is a privilege of the fragment. Horn rules, Datalog, and Volume 2's EL family all admit polynomial step checks; the frontier does not always have one. When the steps are informal mathematics or open-domain text, there is no verify_step to import, and the field's response, training a checker instead [1][2], returns at the end of this chapter with its own costs.

One episode of the game is then a budgeted loop (verifier_gate.py lines 152–193): sample a template by inverse-CDF (cumulative distribution function) sampling, in which cumulative probabilities are computed and a uniform draw picks the first template whose cumulative mass exceeds it, then ground it, maybe corrupt the conclusion, and either accept it blind (ungated mode) or admit it only if verify_step re-derives it (gated mode). Accepted atoms enter $D$ immediately and feed later groundings; a template with no fresh conclusion is a dud and spends its budget step producing nothing.

Ungated: what trusting the proposer costs

Experiment (a) accepts every proposal. Two hundred episodes of 24 steps each, uniform policy, and an audit of every accepted atom against the true closure (verifier_gate.py lines 198–216). The committed output:

[1] ungated chains — accept every proposed conclusion (200 episodes x 24 steps)
    accepted 3416 facts; wrong (outside the closure): 844 — committed wrong-fact rate 0.247
      injected by the corruption channel         : 752
      DOWNSTREAM: valid steps, polluted premises : 92  (rate 0.027)
    one wrong atom breeds more: unsound derivations pollute the closure

The headline rate is no surprise: the corruption channel fires a quarter of the time, and 752 of 3,416 accepted facts (a fraction of 0.220) are its direct injections. The number that matters is the second one. Ninety-two wrong facts, 2.7 percent of everything accepted and roughly one in nine of the wrong facts, were committed by steps that were perfectly valid rule applications: the audit classifies a wrong atom as downstream when its own step was not corrupted, which means the rule fired honestly over premises that were already polluted (verifier_gate.py lines 206–213). A spliced advises fact breeds fake grandAdvisor conclusions by a textbook application of the composition rule; a spliced cites breeds a fake transitive chain. This is the previous chapter's propagation exhibit in a harder currency: there, one corrupted intermediate state derailed the rest of one computation; here, one corrupted fact enters a shared store and corrupts every future derivation that touches it. Pollution compounds, and no amount of downstream honesty repairs it. That is the negative result that motivates the gate: checking the final answer of a chain is too late, because by then the wrongness has been laundered through valid inferences.

Verifier-constrained decoding: soundness by construction

Experiment (b) changes exactly one thing: every step must pass verify_step before it enters the derived set (verifier_gate.py lines 184–186). Same policy, same noise, same budgets. The guarantee this buys is worth deriving in full, because its hypotheses are all visible in the code.

Claim. Let $F^{\star} = \mathrm{lfp}(T_P)$ be the true closure, and let $D_t$ be the gated derived set after $t$ accepted steps. Then $D_t \subseteq F^{\star}$ ($\subseteq$ reads "is a subset of": every fact in the gated derived set also lies in the true closure) for every $t$, at every budget, under every policy.

Derivation. The proof is induction on $t$, and it uses one property of the closure: $F^{\star}$ is a fixpoint, $T_P(F^{\star}) = F^{\star}$, meaning that firing any rule on premises inside $F^{\star}$ produces a conclusion already inside $F^{\star}$ (that is what "closed under the rules" says, and it is how least_fixpoint decides to stop iterating, forward_chain.py lines 52–63). Base case: $D_0$ is the 23 base facts, and the closure is built starting from them, so $D_0 \subseteq F^{\star}$. Inductive step: suppose $D_t \subseteq F^{\star}$ and the gate admits an atom $a$ under rule $r$. Admission means verify_step found a substitution $\sigma$ with $\mathrm{head}_r\sigma = a$ and every body atom $\mathrm{body}_r\sigma \in D_t$. Since $D_t \subseteq F^{\star}$, those premises all lie in $F^{\star}$, so the rule fires inside $F^{\star}$ and its conclusion satisfies $a \in T_P(F^{\star})$. By the fixpoint property $T_P(F^{\star}) = F^{\star}$, so $a \in F^{\star}$, and $D_{t+1} = D_t \cup \lbrace a \rbrace$, the old set plus the one new atom $a$ ($\cup$ is set union, $\lbrace a \rbrace$ the one-element set containing $a$), satisfies $D_{t+1} \subseteq F^{\star}$. ∎

Notice what the induction never mentioned: the policy, the logits, the corruption rate. Soundness is a property of the gate alone, which is why the chapter keeps saying "by construction": the proposer can be arbitrarily malicious and the guarantee stands, because the verifier re-derives rather than trusts. The companion still checks the theorem empirically, sound &= new <= DERIVED_TRUE on every episode against the independently computed closure, then asserts it (verifier_gate.py lines 234–235 and 384); the assert audits the implementation (a bug in verify_step would void the proof's hypotheses), not the mathematics. The committed result: across all budgets, 0 wrong facts in 6,612 accepted steps.

What the guarantee does not give is completeness, and the committed budget sweep prices that honestly (verifier_gate.py lines 221–244):

[2] verifier-constrained decoding — same policy, same noise, exact gate (100 episodes per budget)
    budget T   recall of 24   accepted   rejected   duds
           6         0.147       3.53       0.96    1.51
          12         0.294       7.06       2.04    2.90
          24         0.538      12.92       3.64    7.44
          48         0.797      19.12       6.07   22.81
          96         0.979      23.49       7.62   64.89
    wrong facts committed: 0 of 6612 accepted — every derived set ⊆ lfp(T_P):
    soundness is BY CONSTRUCTION; the budget buys only recall

Read the columns together. Recall is the mean fraction of the 24 derivable atoms an episode actually derives; it is nondecreasing in the budget (asserted with tolerance at verifier_gate.py lines 385–387) and climbs from 0.147 at 6 steps to 0.979 at 96. This is the truncation law of the previous chapter reappearing in policy form: serial budget buys reach, and only reach. The duds column shows the price curve bending: at budget 96 an average of 64.89 of the 96 steps ground nothing new, because the derived set is nearly the whole closure. A uniform policy pays most of a large budget rediscovering that little is left to discover; that inefficiency is the slack that learning, next section, takes up. The rejected column is the gate earning its keep, 7.62 corrupted proposals per 96-step episode bounced at the door instead of entering the record.

The sweep also fixes this chapter's place in the volume's taxonomy of error postures:

posture	contract	where this series lives it	failure it accepts
sound but truncated	everything asserted is true; some truths unreached at a finite budget	this chapter's gate; any exact fixpoint stopped before convergence	missing answers
complete-ish but unsound	everything gets an answer or a score; no per-answer certificate	Volumes 3–4's embedding scorers over the same knowledge base	wrong facts enter silently
sound when accepted, else abstain	accepted answers certified; the rest declined, coverage measured	the gate composed with Part III's abstention	reduced coverage

The third row is the deployment composite: run gated decoding, answer when the goal is derived, abstain otherwise, and report the risk-coverage point; it is this section's guarantee wearing Part III's interface.

Expert iteration: reinforcement learning without a reward model

So far the policy is dead weight, a uniform distribution paying budget to duds. Experiment (c) makes it learn, using the oldest trick in the verifier line: expert iteration, the loop that samples attempts, keeps the verified successes, and refits the proposer on them, known in its modern form as STaR (Self-Taught Reasoner) [3]. One honesty note on the ancestry: STaR keeps rationales checked only by final-answer correctness, while our loop additionally step-gates every kept trajectory, a strictly stronger filter. The companion targets the 6 multi-hop goals under a deliberately tight budget of 5 steps, where a uniform policy usually wastes its few draws on taxonomy rules (verifier_gate.py lines 263–284): each round samples 400 gated episodes, each toward a uniformly drawn goal atom; an episode succeeds if its goal is derived within budget; the verified steps of successful trajectories are kept, and the logits are refit to them by maximum likelihood.

The refit deserves its derivation, because it is four lines of algebra that the code applies verbatim. Collect the kept steps' template indices $r_1, \ldots, r_M$ (here $M$ counts every accepted step across all successful trajectories in the round) and maximize their mean log-likelihood under the softmax policy,

$$L(\mathbf{z}) \;=\; \frac{1}{M} \sum_{t=1}^{M} \log \pi_{r_t} \;=\; \frac{1}{M} \sum_{t=1}^{M} \Big( z_{r_t} - \log \sum_{j} e^{z_j} \Big),$$

where the second equality just expands $\log$ of the softmax: the numerator contributes its logit, the denominator its log-sum. Differentiate with respect to one logit $z_k$. The first term contributes $1$ exactly when $r_t = k$, so averaging over $t$ gives the empirical frequency $\bar{c}_k$, the fraction of kept steps that used template $k$. The second term is the same for every $t$, and its derivative is

$$\frac{\partial}{\partial z_k} \log \sum_{j} e^{z_j} \;=\; \frac{e^{z_k}}{\sum_{j} e^{z_j}} \;=\; \pi_k ,$$

by the chain rule (derivative of $\log u$ is $u'/u$, and only the $j = k$ term of the inner sum depends on $z_k$). Subtracting,

$$\frac{\partial L}{\partial z_k} \;=\; \bar{c}_k - \pi_k ,$$

the softmax/cross-entropy cancellation this series first derived for one neuron in Volume 1, reappearing as a policy update. Gradient ascent $\mathbf{z} \leftarrow \mathbf{z} + \eta\,(\bar{\mathbf{c}} - \boldsymbol{\pi})$, where $\eta$ is the learning rate, the step size of each ascent update (the lr argument below, LR_STAR in verifier_gate.py), is stationary exactly when $\boldsymbol{\pi} = \bar{\mathbf{c}}$: the refit moves the policy toward the empirical distribution of templates that verified successes actually used, the maximum-likelihood estimate. The code is the equation (verifier_gate.py lines 249–260):

def refit(logits: np.ndarray, counts: np.ndarray, lr: float = LR_STAR,
          steps: int = STAR_STEPS) -> np.ndarray:
    """Fit the policy to the kept verified steps by gradient ascent on the
    mean log-likelihood  L(z) = (1/M) Σ_t log softmax(z)_{r_t}.  With
    empirical frequencies c̄_k = counts_k / Σ counts, the gradient is
    ∂L/∂z_k = c̄_k − p_k (the softmax/cross-entropy cancellation), so the
    ascent  z ← z + η (c̄ − p)  converges toward p = c̄, the MLE."""
    z, c = logits.copy(), counts / counts.sum()
    for _ in range(steps):
        # ∂L/∂z = c̄ − softmax(z)
        z = z + lr * (c - softmax(z))
    return z

Why call this reinforcement learning at all, when there is no value network, no reward model, and the update is supervised maximum likelihood? Because the data is chosen by a reward. Keeping only successful trajectories is policy improvement against the environment's binary return (goal derived within budget: 1, else 0), in a scheme where the environment itself, closure membership checked by an exact gate, plays the perfect judge. Reinforcement learning needs a reward model only when the environment cannot score its own episodes. Ours can, which is the deep economy of the polynomial fragment. The committed run:

[3] expert iteration (STaR-lite) — keep verified successful trajectories, refit (400 goal episodes/round, budget 5)
    iter   success rate   policy mass on goal rules (3,5,6)
       0          0.205             0.429
       1          0.343             0.689
       2          0.463             0.807
       3          0.535             0.884
    gradient ascent on kept steps: dL/dz = c_bar - softmax(z)

Read the second column as the mechanism: rules 3, 5, 6 are the templates whose heads can produce goal atoms (grandAdvisor and the two citesTransitively rules, verifier_gate.py lines 82–84), and the uniform policy gives them $3/7 \approx 0.429$ of its mass. Each round of keep-and-refit moves mass onto them, 0.429 → 0.689 → 0.807 → 0.884, and success follows, 0.205 → 0.343 → 0.463 → 0.535, a lift of 0.330 that the harness asserts is monotone within sampling tolerance and at least 0.20 in total (verifier_gate.py lines 391–398). The honest caveats are the module's own: this is a bandit policy on a 23-fact world, with no exploration pressure (nothing forces the policy to keep visiting rare templates once mass concentrates), no risk of catastrophic forgetting (there is nothing else to forget), and none of the scale phenomena of the real bootstrapping literature, including the tendency to saturate when the model can no longer solve new problems to learn from, documented in the STaR line [3], and the scale-dependence of whether pure reinforcement-learning bootstrapping pays off at all [5].

The reward-hacking exhibit: validity is not progress

Now the chapter's centerpiece, experiment (d), which puts a sharper optimizer in the loop and lets the reward definition make or break it. The optimizer is REINFORCE, the score-function policy gradient, and since this chapter owns the derivation, here it is from the definition. The objective is the expected return, $J(\mathbf{z}) = \mathbb{E}_{\tau \sim P_{\mathbf{z}}}[R(\tau)]$, where $\tau$ is a whole episode (a trajectory), $P_{\mathbf{z}}(\tau)$ is the probability the current policy generates it, $R(\tau)$ is its scalar return, and $\mathbb{E}$ is the expectation, the return averaged over trajectories weighted by their probabilities. Write the expectation as a sum over trajectories and differentiate:

$$\nabla_{\mathbf{z}} J \;=\; \nabla_{\mathbf{z}} \sum_{\tau} P_{\mathbf{z}}(\tau)\, R(\tau) \;=\; \sum_{\tau} R(\tau)\, \nabla_{\mathbf{z}} P_{\mathbf{z}}(\tau),$$

since $R(\tau)$ does not depend on $\mathbf{z}$. Now the likelihood-ratio trick: because the derivative of $\log u$ is $u'/u$, every positive function satisfies $\nabla P = P \, \nabla \log P$, so

$$\nabla_{\mathbf{z}} J \;=\; \sum_{\tau} P_{\mathbf{z}}(\tau)\, R(\tau)\, \nabla_{\mathbf{z}} \log P_{\mathbf{z}}(\tau) \;=\; \mathbb{E}_{\tau}\big[ R(\tau)\, \nabla_{\mathbf{z}} \log P_{\mathbf{z}}(\tau) \big],$$

an expectation we can estimate by sampling episodes from the very policy being improved. The trajectory's log-probability factors over everything random in an episode: the template draws, the uniform grounding choices, the corruption coin, the gate's verdicts. Only the template draws depend on $\mathbf{z}$, so every other factor differentiates to zero and $\nabla_{\mathbf{z}} \log P_{\mathbf{z}}(\tau) = \sum_{t} \nabla_{\mathbf{z}} \log \pi_{r_t}$, summed over every draw $r_t$ in the episode, including duds and verifier-rejected steps, because each carried policy probability. The per-draw gradient is the same computation as the refit's, done for a single sample: $\log \pi_{r} = z_r - \log \sum_j e^{z_j}$, so $\partial \log \pi_r / \partial z_k = \delta_{rk} - \pi_k$, where $\delta_{rk}$ is the Kronecker delta ($1$ when $k = r$, else $0$); in vector form $\nabla_{\mathbf{z}} \log \pi_r = \mathbf{e}_r - \boldsymbol{\pi}$, the one-hot vector of the drawn template minus the policy. Finally, subtracting any constant baseline $b$ from the return leaves the estimator unbiased, because

$$\mathbb{E}_{\tau}\big[ b\, \nabla_{\mathbf{z}} \log P_{\mathbf{z}}(\tau) \big] \;=\; b \sum_{\tau} P_{\mathbf{z}}(\tau)\, \nabla_{\mathbf{z}} \log P_{\mathbf{z}}(\tau) \;=\; b\, \nabla_{\mathbf{z}} \sum_{\tau} P_{\mathbf{z}}(\tau) \;=\; b\, \nabla_{\mathbf{z}} 1 \;=\; \mathbf{0},$$

the probabilities summing to one for every $\mathbf{z}$. The companion uses the batch mean as $b$ and additionally divides by the batch standard deviation; that division is a variance-control step-size heuristic (it rescales the gradient rather than shifting it), standard practice and flagged as such. The whole derivation is applied by hand, with no autodiff anywhere (verifier_gate.py lines 301–337), the score function appearing as np.bincount(out["drawn"], minlength=N_RULES) - len(out["drawn"]) * p.

Two policies are trained with this identical machinery, identical gate, identical budget of 12, differing in one line, the definition of $R$ (verifier_gate.py lines 320–326):

• Membership reward: $R =$ the number of verifier-approved facts the episode derived. This is the seductive one: it rewards exactly what the gate certifies, so it looks like "reward for verified reasoning".
• Goal-F1 reward: $R = F_1(D',\, G)$ against the 6-atom goal set $G$, where $D' = D \setminus \mathrm{base}$ is the episode's derived-only atoms, the derived set with the 23 base facts removed ($\setminus$ reads "minus, as sets"): with $\mathrm{hit} = \lvert D' \cap G \rvert$, precision is $P = \mathrm{hit}/\lvert D' \rvert$ (the fraction of what was derived that was wanted), recall is $R_c = \mathrm{hit}/\lvert G \rvert$ (the fraction of what was wanted that was derived), and $F_1 = 2 P R_c / (P + R_c)$, their harmonic mean (verifier_gate.py lines 289–298).

After 15 REINFORCE updates each, both policies and the untrained uniform baseline are frozen and evaluated on 300 fresh gated episodes (verifier_gate.py lines 340–356). The committed comparison:

[4] reward hacking — same gate, same budget (12), two rewards (15 REINFORCE updates)
    policy               verified facts   relevance   F1 vs goals
    uniform (untrained)           7.26       0.382       0.412
    reward = #verified            8.80       0.154       0.183
    reward = set-level F1         5.04       0.976       0.882
    the membership policy piles 0.643 of its mass on rule 4,
    colleague(X,Y) <- shared affiliation: 8 valid, goal-irrelevant
    atoms to harvest.  More verified facts, LESS progress —
    validity is a correctness signal, not a progress signal

Sit with the middle row, because it is the chapter's thesis in three numbers. The membership-rewarded policy succeeded at its objective: 8.80 verified facts per episode against the uniform baseline's 7.26 (the harness asserts the margin, verifier_gate.py lines 406–407). It is also perfectly sound: the gate never moved, so every one of those facts is in the true closure. And it is worse than an untrained policy at the actual task: its relevance fraction, the share of its derived atoms that are goal atoms, collapsed from the uniform policy's 0.382 to 0.154 (asserted, verifier_gate.py lines 408–409), and its goal F1 fell from 0.412 to 0.183. The mechanism is printed with the exhibit: the policy discovered rule 4, the colleague rule, whose shared-affiliation body is satisfied by base facts alone and which licenses 8 distinct valid atoms (the ordered colleague pairs at MIT and CMU), the largest harvest of easy verified facts any one template offers. It piled 0.643 of its probability mass there and farmed. Every colleague fact passes the gate; none advances a citation chain. Meanwhile the F1-rewarded policy derives the fewest facts of the three, 5.04 per episode, and dominates everything that matters: relevance 0.976, F1 0.882. Progress is not volume either; a policy optimizing the right objective derives less and achieves more.

This is reward hacking at desk scale, and the shape matches the documented frontier phenomenon: an optimizer given a proxy reward maximizes the proxy, and the gap between proxy and intent is where the behavior goes. The frontier's verifiable-reward systems lean on exactly the gate-like rewards this chapter builds, rule-based checks chosen over learned reward models precisely because learned ones invite hacking at scale [5]; and the process-supervision result, per-step judgment outperforming outcome-only judgment on hard math, is the same gap measured from the other side [2]. The naming this chapter insists on: the gate emits a correctness signal (is this step valid?), the reward must encode a progress signal (is this step advancing the goal?), and no soundness guarantee converts one into the other. Our exhibit makes the distinction unusually clean because the correctness signal is perfect, an exact oracle, and the hacking happens anyway. Whatever went wrong, it was not verification.

Process supervision, positioned

The frontier's name for per-step judgment is process supervision: score or filter each step of a reasoning trace, rather than only its final answer, and train on that denser signal [2]. This chapter has been doing process supervision throughout without ceremony, because in the polynomial fragment the per-step judge is free: verify_step is an exact oracle, costs microseconds, and cannot be flattered. That is the neuro-symbolic edge stated plainly. No reward budget is spent teaching the policy not to lie about steps; the gate makes lying unprofitable by construction, and the entire learning signal is left to address the genuinely hard question of which valid step to take, which is where the previous section showed it must be spent carefully.

Where the frontier lacks such an oracle, on informal mathematics, code without tests, open-domain argument, it trains one: first outcome-supervised verifiers that judge whole solutions [1], and, more effectively, a process-reward model, a neural scorer of step quality fit to human or automated step labels [2]. The move is forced and productive, but notice what it surrenders: the learned verifier is itself a model, and every audit this volume has built now applies to it. Is its step score calibrated, or confidently wrong (Part III)? Did it learn the concept "valid step" or a reasoning shortcut that co-occurs with validity in its training pool? Is the explanation it implicitly offers, this step scored low, faithful to its actual computation? A learned gate can be farmed exactly the way a learned reward can, and at frontier scale the documented failure reports read like our exhibit with the oracle removed [5]. The volume's threads braid here: Parts I through III were not detours from the reasoning frontier; they are the due diligence that becomes mandatory the moment the verifier stops being exact.

The unsolved part

Three open edges, in increasing order of how much they should worry a researcher. First, reward design for open-ended derivation. Our F1 reward fixed the hacking exhibit, but it cheats in a way the fix should make you notice: it presupposes a known goal set to score against. Genuinely exploratory reasoning, deriving toward theorems nobody has stated, needs a progress signal without goal leakage, and no principled construction exists; novelty rewards, learned progress estimators, and curriculum schedules are all live proposals with the same vulnerability our membership reward exhibited, a proxy an optimizer can farm. Second, verifier coverage. The soundness induction was airtight, but everything in it is relative to the rule set defining $T_P$. The gate is only as sound as the rules are right, and only as complete as the rules are complete; an incomplete verifier does not fail loudly, it silently truncates the reachable space, rejecting valid reasoning it cannot re-derive, and the policy then learns never to propose it. On our 7-rule world coverage is total by fiat. On SNOMED CT-scale ontologies, with modeling gaps and versioned rule sets, "the gate rejected it" and "it is wrong" quietly diverge, and no committed assert can detect a truth the verifier cannot express. Third, the scale question this desk cannot touch: whether verified self-improvement compounds or saturates. Our expert iteration climbs for four rounds on six goals; the frontier question is whether a policy that trains on its own verified successes keeps generating problems hard enough to learn from, or exhausts its curriculum and plateaus. The bootstrapping literature shows both behaviors in different regimes [3][5], and which regime obtains at a given scale is, as of this volume, an empirical question with no theory worth the name.

Why it matters

This chapter closes Part V's arc with the volume's most exportable design pattern. The depth-ceiling chapter said a fixed-depth network cannot, by itself, do unbounded derivation; Chain-of-Thought recovered depth by unrolling, at the price of trusting every generated step; this chapter removed the trust without removing the learning. The composite, statistical proposer behind an exact gate, is the deployable shape of everything this series has built: Volume 1's fixpoint became the gate's ground truth, Volume 4's differentiable proposers became the thing worth training, and Parts I through III of this volume became the audit kit for the day the gate itself is learned. For your own research the exhibit to keep is the cheapest one: before adding a reward to any reasoning loop, ask whether it measures correctness or progress. The two are orthogonal by construction here, on a 23-fact world with a perfect verifier, which means no amount of verifier quality at scale will merge them for you. And the numbers to keep are the contract: wrong-fact rate 0.247 ungated, 0 in 6,612 gated, recall bought at a measured price. Soundness by construction is real, purchasable, and cheap in the polynomial fragment; what it does not buy, direction, is precisely what remains to be learned.

Key terms

• Proposer/verifier pattern: the division of a reasoning system into a statistical component that generates candidate steps and an exact component that admits only steps it can re-derive; assertions inherit the verifier's soundness, coverage inherits the proposer's quality.
• Verifier-constrained decoding: applying the verifier per step during generation, so invalid steps never enter the derived record; contrast with reranking, where a verifier scores only completed outputs.
• Soundness by construction: the guarantee, proved by induction on accepted steps, that the gated derived set stays inside $\mathrm{lfp}(T_P)$ at every budget under every policy; a property of the gate alone.
• Expert iteration: the loop sample attempts → keep verified successes → refit the proposer on their steps; policy improvement against an environment reward with no learned value or reward model.
• REINFORCE / score-function gradient: the policy-gradient estimator $\nabla_{\mathbf{z}} J = \mathbb{E}[R\, \nabla_{\mathbf{z}} \log P_{\mathbf{z}}(\tau)]$, with $\nabla_{\mathbf{z}} \log \pi_r = \mathbf{e}_r - \boldsymbol{\pi}$ for a softmax policy; baselines subtract without bias because $\mathbb{E}[\nabla \log P] = \mathbf{0}$.
• Reward hacking: an optimizer maximizing a proxy reward at the expense of the intent it proxies; here, a membership reward maximized by farming valid-but-irrelevant facts.
• Correctness signal vs progress signal: what a verifier certifies (this step is valid) versus what a reward must encode (this step advances the goal); no soundness check supplies the latter.
• Process supervision: training on per-step judgments of a reasoning trace rather than outcome-only judgment; free and exact in the polynomial fragment, approximated by trained process-reward models where no oracle exists.
• Relevance fraction: the share of an episode's derived atoms that lie in the goal set; the quantity that collapses under membership reward (0.382 → 0.154) while verified-fact count rises.

Where this leads

Part V ends with a system that is sound by construction, improvable by reinforcement, and honest about the one thing it cannot measure from inside: whether its benchmark numbers mean what they appear to mean. That question needs instruments of its own. The Seven Difficulty Axes opens Part VI by refusing to treat "accuracy on a reasoning benchmark" as a single number, decomposing task difficulty into orthogonal axes (depth, width, recursion, distraction, and beyond) and showing, on the same academic world, how two systems with identical aggregate scores can occupy entirely different difficulty surfaces.

---

Companion code: examples/frontier/verifier_gate.py implements the noisy proposal policy, the exact step gate imported from Volume 1's examples/logic/forward_chain.py, and all four experiments: ungated pollution, the gated budget sweep, expert iteration, and the two-reward hacking comparison. Run python3 examples/frontier/verifier_gate.py to reproduce every number in this chapter; the run is deterministic and every claim is guarded by an assert.