Soft Reasoners: RuleTaker and ProofWriter

📍 Where we are: Part VI · Natural-Language Reasoning — Chapter 19. Foundation Models for CLQA (complex logical query answering) closed Part V with query answerers that transfer across graphs; this chapter opens Part VI by moving the whole enterprise into English, and by building the measuring instrument that can tell answering apart from reasoning.

Every system in this volume so far consumed logic in logical clothing: atoms, rules, queries with quantifiers. Part VI asks what happens when the logic arrives as ordinary English sentences and the machine that consumes them is a statistical text model. The founding experiment of this line is RuleTaker, which posed a deceptively simple question: if you write small logical theories as English and train a transformer to answer true/false questions about them, is the resulting behavior deduction [1]? The headline answer was startling and positive. But the lasting contribution, and the subject of this chapter, is the instrument: a way of generating, labeling, balancing, and stratifying data so that the question even has a measurable meaning. The companion module rebuilds that instrument honestly at desk scale, runs a deliberately weak statistical model through it, and lets the instrument do exactly what it was designed to do: expose the difference between memorizing local patterns and composing rules.

The simple version

Imagine a driving examiner who suspects a student has memorized the test route rather than learned to drive. A naive examiner asks the usual questions and awards the usual pass. A careful examiner designs the exam so that memorization cannot score: she makes half the correct answers "no" so that always saying "yes" earns exactly 50 percent, she sorts every question by how many turns of actual driving it requires, and she trains the student on quiet streets but examines on interchanges the student has never seen. If the student aces the quiet streets and fails every interchange, the exam has revealed something no overall score could: the student learned the streets, not the driving. RuleTaker is that careful examiner for reading-and-reasoning, and this chapter builds her exam from parts you already own.

What this chapter covers

• The question stated with care: not "can a model answer" but "is the answering deduction," made measurable by three instrument choices, each of which kills one specific confound.
• The generator: seeded, stratified theories in controlled English over the academic world, with negation-as-failure under a closed world decoded precisely, and the committed dataset statistics.
• The labeler as the instrument's soul: Volume 1's forward chainer extended to track per-fact minimum derivation depth, with a proof that the round of first appearance is the minimum proof height, and an independent backward-chaining audit of every positive label.
• The stand-in reasoner, declared honestly: a bag-of-local-features logistic model trained only on depths 0 and 1, and the committed per-depth table: 1.000 and 0.966 at trained depths, exactly 0.500 at depths 2 and 3, beside the prover's constant 100 percent.
• The perturbation probe: flip one negation inside a rule, relabel with the prover, and measure whether the model's answers change exactly when the logic changes; the committed numbers show they do not.
• The published results read against this frame: the transformer's genuine depth generalization, where it cracked, and why neither our stand-in's collapse nor the transformer's success settles the mechanism question.
• ProofWriter's two-strategy finding: proofs generated all at once go unfaithful at unseen depths; proofs built by iterated one-step inference stay verifiable by construction, this volume's exactness lesson restated in natural language.

The question, stated with care

"Can a transformer answer questions about rules written in English?" is not, by itself, a scientific question, because a model can answer correctly for reasons that have nothing to do with the rules. It can exploit the class prior (if 70 percent of questions are true, "always true" scores 70 percent), surface correlations (questions containing "not" skewing false), or memorized templates (this sentence shape was true last time). The RuleTaker experiment converts the vague question into a measurable one, "is the answering deduction," through three deliberate instrument choices [1]. Each choice exists to kill one specific confound.

instrument choice	what it is	the confound it kills
depth stratification	every question is labeled with the minimum derivation depth of its answer: how many chained rule applications a shortest proof needs	a model that has merely memorized shallow patterns shows a flat-looking overall score; per-depth accuracy separates "knows the facts" from "chains the rules," catching memorized-length and template heuristics
label balancing	the question bank is balanced 50/50 true/false, proven-true questions paired with same-depth negated conclusions (the companion sharpens this to an exact 50/50 within every depth stratum), and surface markers such as "not" are decorrelated from the label	any constant strategy, and any strategy keyed to the class prior or to a surface token, scores exactly chance
train shallow, test deep	the model trains only on questions provable within some depth budget and is tested beyond it	in-distribution accuracy measures fit; only out-of-depth accuracy measures whether the composition operation itself was learned, isolating generalization from memorization

Notice what the three choices have in common: none of them looks inside the model. The instrument is entirely behavioral, a designed input distribution plus a designed report format. That is both its power (it applies to any black box, a transformer or a logistic regression or a human) and its limit, which the end of this chapter and all of Volume 5 will press on: behavior can narrow the space of plausible mechanisms, but it cannot certify one.

The generator: a laboratory English

The companion module ruletaker_lite.py rebuilds the instrument on the academic world. Its vocabulary is four predicate layers over the five people of Volume 1's knowledge base: layer 0 holds the four predicates that facts may state (published, funded, cited, diligent), and layers 1 through 3 hold five derived predicates (productive, visible, senior, established, influential) whose rules draw their bodies from the layer directly below (ruletaker_lite.py lines 92–98). Because a layer-$k$ rule needs a layer-$(k-1)$ premise, the layer index of a predicate pins the derivation depth of its atoms, which is what makes stratified sampling possible. Theories are rendered in controlled English: a fixed template per sentence type, so that the text is genuinely natural-language input to whatever model reads it, while remaining machine-invertible for the labeler (all three templates at lines 101–112; the rule template, lines 109–112):

def rule_sentence(head: str, body: list[tuple[bool, str]]) -> str:
    """One rule template: 'If someone is A and not B then they are H.'"""
    conds = " and ".join(f"{'not ' if neg else ''}{p}" for neg, p in body)
    return f"If someone is {conds} then they are {head}."

One theory is roughly nine stated facts (each of the twenty possible person–predicate pairs is stated with probability 0.45) plus one rule per derived predicate, five rules in all, each rule optionally carrying one extra layer-0 condition that is negated with probability one half (lines 125–147). Here is the first evaluation theory of the committed run, verbatim:

    eval theory 40, verbatim:
      alice is funded.
      alice is cited.
      alice is diligent.
      ... (9 more facts)
      If someone is published then they are productive.
      If someone is diligent then they are visible.
      If someone is visible then they are senior.
      If someone is visible and diligent then they are established.
      If someone is senior and not diligent then they are influential.

The last rule contains the ingredient that needs precise decoding: negation-as-failure under a closed-world assumption (CWA). The convention, inherited from Datalog and from Volume 2's open-world chapter, is that an atom which cannot be proved is false, and a rule condition written "not diligent" tests exactly that failure: it holds for a person precisely when "diligent" is absent from the stated facts. Negation over derived predicates can make such semantics treacherous (a rule concluding an atom $p$ from "not $p$" has no stable reading), and the standard cure is stratified negation: negation may only be applied to predicates fully determined at an earlier stratum. The generator gets stratification for free, because negated conditions are allowed only on layer-0 predicates, and layer-0 predicates appear in no rule head, so their truth is fixed by the stated facts alone before any rule fires (lines 87–91). RuleTaker's original release used exactly this closed-world convention; its successor dataset family made the choice explicit by re-releasing the theories in both closed-world and open-world versions [2]. Note also what the templates deliberately withhold: there is no lexical variety, no synonymy, no syntactic paraphrase. This is a laboratory English, and the chapter will return to what that costs.

The labeler: rounds of the consequence operator, read off as depths

An instrument is only as trustworthy as its gold labels, and here the design is uncompromising: every label is computed by a prover, not by a human or a heuristic. The prover is Volume 1's forward chainer, imported rather than retyped (ruletaker_lite.py line 75 imports t_p from forward_chain.py). Recall its one-round operator (forward_chain.py lines 42–49):

def t_p(facts: set, rules: list) -> set:
    """One application of the immediate-consequence operator: the input facts
    plus every head derivable in a single step."""
    out = set(facts)
    for head, body in rules:
        for sub in _match_body(body, facts, {}):
            out.add(apply_sub(head, sub))
    return out

Two preparation steps connect the English theory to this engine. First, each rule quantifies over "someone," so it is grounded once per person. Second, negation-as-failure is compiled away against the closed world of stated facts: a ground condition "not $p_0(x)$", where $p_0$ stands for a layer-0 predicate and $x$ for one of the five people, that holds (the atom is unstated) is simply dropped from the body, and one that fails (the atom is stated) deletes that ground rule entirely (lines 153–179). This compilation is sound precisely because of stratification. Since layer-0 predicates head no rules, a layer-0 atom belongs to the least model if and only if it is stated; the truth value of every negated condition is therefore already settled before chaining begins, and replacing each one by that settled value leaves the least model of the remaining negation-free program unchanged. What survives is an ordinary ground definite program, exactly the object Volume 1's machinery accepts.

Now the extension that makes the instrument possible: depth tracking. Write $F$ for the set of stated (ground) atoms, $R$ for the ground rules, and $S_k$ for the set of atoms known after $k$ rounds, defined by $S_0 = F$ and $S_{k+1} = T_P(S_k)$, where $T_P$ is the immediate-consequence operator above (the map that adds every atom derivable in a single rule application; the subscript $P$ names the program, the set of ground rules, whose consequences the operator computes). The labeler iterates $T_P$ round by round and records, for each atom, the first round at which it appears (lines 190–200):

    facts, rules = ground_program(theory)
    depth = {atom: 0 for atom in facts}
    frontier, round_no = set(facts), 0
    while True:
        round_no += 1
        new = t_p(frontier, rules)            # one round of consequences
        if new == frontier:
            return depth
        for atom in new - frontier:
            depth[atom] = round_no            # first appearance = min depth
        frontier = new

The claim implicit in that comment deserves a proof. Define a proof tree for an atom $a$: a stated atom is its own proof tree of height 0, and if a rule has head $a$ and body atoms $b_1, \ldots, b_m$ (here $m$ is the number of body atoms) with proof trees of heights $h_1, \ldots, h_m$, then attaching them under $a$ gives a proof tree of height $1 + \max(h_1, \ldots, h_m)$. The minimum derivation depth of $a$ is the smallest height over all its proof trees. We show by induction on $k$ that $S_k$ is exactly the set of atoms having a proof tree of height at most $k$. For $k = 0$: $S_0 = F$ is the set of atoms with height-0 proofs, by definition. For the step, assume the statement for $k$. If $a$ has a proof tree of height at most $k+1$, then either the tree has height 0 (so $a \in F$, where the symbol $\in$ reads "is a member of": $a$ is one of the stated atoms; and $F \subseteq S_{k+1}$, where $\subseteq$ reads "is contained in": every stated atom is still present after $k+1$ rounds, since $T_P$ never removes atoms) or its root rule's body atoms each have proof trees of height at most $k$, hence all lie in $S_k$ by the induction hypothesis; that rule therefore fires in round $k+1$ and puts $a$ into $S_{k+1} = T_P(S_k)$. Conversely, if $a \in S_{k+1}$, then either $a \in S_k$ (and by induction has a proof of height at most $k$, which is at most $k+1$) or some rule with body contained in $S_k$ derived it; by induction each body atom has a proof tree of height at most $k$, and assembling them under the rule gives $a$ a proof tree of height at most $k+1$. This closes the induction. It follows that an atom first appears in round $k$ exactly when its minimum derivation depth is $k$: it is in $S_k$ (some proof has height at most $k$) but not in $S_{k-1}$ (no proof has height at most $k-1$). The loop above therefore computes minimum derivation depth, not an approximation of it.

The labels this produces are gold by construction, the standing theme since Volume 2: for every atom labeled true there exists a concrete proof tree (the chainer built one), and for every atom labeled false the fixpoint was exhausted without deriving it, which under the closed world is the semantics of falsehood. The module then adds a belt to the braces: every positive evaluation question is independently re-decided by Volume 1's backward chainer, sld.provable, on the same compiled ground program, and an assertion demands that forward and backward chaining agree question by question (lines 391–398). Two provers with different search strategies vouching for every label is the desk-scale version of using a verified reasoner as an oracle.

The question bank: balanced to the decimal, by construction

For every derivable atom of depth $d \le 3$ that has a same-layer underivable counterweight, the question bank emits four questions: the atom asserted ("carol is senior.", gold true), the atom negated ("carol is not senior.", gold false), the paired underivable atom asserted (gold false), and that same atom negated (gold true). (An atom with no counterweight is skipped whole, quadruple and all, so the balance below survives; the guard fires for five atoms across the 60 committed theories, lines 237–238.) The pair is drawn, with the seeded generator, from the same predicate layer, so its surface form cannot give it away, and it inherits the pairing depth $d$ as its label depth (lines 209–247); this simplifies RuleTaker's own bookkeeping, which gives a negated proven conclusion the depth of the statement it negates and annotates a wholly unprovable fact with the depth at which its proof attempts fail (the shallowest failing branch, maximized over alternative candidate proofs) [1]. This four-way construction buys the balancing guarantees as theorems rather than as empirical accidents. Within each quadruple the golds are true, false, false, true, so every depth stratum is exactly 50/50; and among the two negated questions the golds are one true and one false, so the token "not" carries zero information about the label. In probability terms, writing $G$ for the gold label, $N$ for the event that the question contains "not", $P(\cdot)$ for the probability of an event, and $P(A \mid B)$ for the probability that $A$ holds given that $B$ does (the vertical bar reads "given": the probability computed only over the questions where $B$ occurs): $P(G = \text{true}) = \tfrac12$ and $P(G = \text{true} \mid N) = \tfrac12$. One line closes the argument. The law of total probability splits the unconditional probability over the two cases, $P(G = \text{true}) = P(G = \text{true} \mid N)\,P(N) + P(G = \text{true} \mid \neg N)\,P(\neg N)$, where $\neg N$ is the complementary event that the question lacks "not"; substituting $\tfrac12$ for the two known probabilities gives $\tfrac12 = \tfrac12\,P(N) + P(G = \text{true} \mid \neg N)\,P(\neg N)$, hence $P(G = \text{true} \mid \neg N)\,P(\neg N) = \tfrac12\,(1 - P(N)) = \tfrac12\,P(\neg N)$, and dividing both sides by $P(\neg N) = \tfrac12$ (half the bank is negated, so this is not zero) yields $P(G = \text{true} \mid \neg N) = \tfrac12$ as well. The label's distribution is the same with and without "not"; writing $p(g,n)$ for the probability that $G$ takes the value $g$ and $N$ the value $n$ (and $p(g)$, $p(n)$ for the two one-variable probabilities), this says $p(g,n) = p(g)\,p(n)$ in all four cells: $G$ and $N$ are independent. Their mutual information (the standard measure of how much knowing one variable reduces uncertainty about the other) is $I(G; N) = \sum p(g,n) \ln \frac{p(g,n)}{p(g)\,p(n)}$, where the summation sign $\sum$ adds the term over all four $(g, n)$ value pairs and $\ln$ is the natural logarithm; independence makes every ratio inside the logarithm equal to 1, so $I(G; N) = \sum p(g,n) \ln 1 = 0$. A classifier keying on polarity alone can only ever earn chance. Both facts are asserted at run time, not merely intended (lines 379–386). The committed corpus: 60 theories, split 40 train and 20 evaluation by theory so no evaluation theory is ever seen in training; 1,892 training questions, all of depth at most 1; 1,500 evaluation questions across all depths.

depth $d$	true	false	total
0	402	402	804
1	176	176	352
2	140	140	280
3	32	32	64

Every count in this table comes from section 3 of the committed output, and the exact 50/50 split at every depth is what the assertion demands. All randomness flows from a single seed (np.random.default_rng(SEED) with SEED = 0, lines 79 and 254), and two runs of the module print byte-identical output.

The stand-in reasoner, declared honestly

The original experiment ran a large pretrained transformer through this instrument. The companion runs something deliberately weaker, and says so in its own docstring (ruletaker_lite.py lines 19–25, first sentence; line 25 continues past the excerpt):

What replaces what, stated plainly: the paper's pretrained transformer is
replaced by a bag-of-local-features logistic model — declared plainly as a
statistical stand-in, because what it EXHIBITS is the point (competence at
trained depths, collapse beyond them), not its architecture; the paper's
100k-question datasets (several thousand theories, fixed name and attribute
pools) become 60 seeded five-person theories over a four-layer predicate
vocabulary in the controlled templates below.

The stand-in reads each (theory, question) pair through ten hand-built features, every one of them a local pattern: with polarity $\mathrm{pol} = +1$ for a positive question and $-1$ for a negated one, the vector is $x = [\,1,\ \mathrm{stated},\ \mathrm{one\_step},\ \mathrm{has\_not},\ \mathrm{head\_pred},\ \mathrm{fact\_frac},\ \mathrm{pol}\cdot\mathrm{stated},\ \mathrm{pol}\cdot\mathrm{one\_step},\ \mathrm{pol},\ \mathrm{pol}\cdot\mathrm{fact\_frac}\,]$, where stated fires when the question's atom appears verbatim as a fact, one_step fires when some rule with this head fires on stated facts alone while checking only its positive conditions (a built-in shortcut the probe will expose), head_pred marks the predicate as derivable at all, and fact_frac is the fraction of layer-0 predicates stated about this person (lines 268–301). The signed copies let a single linear model express "stated and not negated implies true"; the unsigned copies are what a plain bag of tokens and bigrams would also see. Nothing in this vector can represent the composition of two rules, and that is the design.

The classifier on top is logistic regression with the gradient written by hand (lines 304–316). The model scores $s = \mathbf{w} \cdot \mathbf{x}$ (the dot product of the weight vector $\mathbf{w}$ with the feature vector $\mathbf{x}$), predicts $p = \sigma(s) = 1/(1 + e^{-s})$, where $\sigma$ is the sigmoid, the S-shaped function that squashes any real score into a probability strictly between 0 and 1 ($e \approx 2.718$ is the base of the natural exponential), and trains on the binary cross-entropy loss $\ell = -[\,y \ln p + (1-y)\ln(1-p)\,]$ with label $y \in \lbrace 0, 1 \rbrace$. The chain rule runs through three links, each a partial derivative (written with the symbol $\partial$: the rate of change of one quantity as a single input varies, everything else held fixed): $\partial \ell / \partial p = -y/p + (1-y)/(1-p) = (p - y)/\big(p(1-p)\big)$ from differentiating the two logarithms and combining over the common denominator $p(1-p)$, $\partial p / \partial s = \sigma'(s) = e^{-s}/(1+e^{-s})^2 = \sigma(s)\big(1 - \sigma(s)\big) = p(1-p)$ from the quotient rule on the sigmoid, and $\partial s / \partial \mathbf{w} = \mathbf{x}$; multiplying the first two links cancels the $p(1-p)$ factors exactly, leaving $\partial \ell / \partial s = p - y$ and hence $\nabla_{\mathbf{w}} \ell = (p - y)\,\mathbf{x}$, where the gradient $\nabla_{\mathbf{w}} \ell$ collects the partial derivatives of the loss with respect to each of the ten weights into one vector. Volume 1's gradient-descent chapter derived every step of this cancellation; the companion's training loop is that boxed formula in two lines of NumPy, full-batch with learning rate $0.5$ for $300$ epochs:

    for _ in range(EPOCHS):
        p = 1.0 / (1.0 + np.exp(-(X @ w)))
        w -= LR * (X.T @ (p - y)) / len(y)

The crucial protocol line sits elsewhere: the training questions are filtered to depth <= TRAIN_DEPTH with TRAIN_DEPTH = 1 (lines 82 and 260). The stand-in never sees a question whose shortest proof chains two rules. Whatever it does at depths 2 and 3 is generalization or it is nothing.

Reading the per-depth table

Here is the committed table, the instrument's centerpiece, exactly as the run prints it:

[4] the per-depth table: local features vs the prover
      depth   stand-in accuracy   prover
      0       1.0000              1.00  <- trained depths
      1       0.9659              1.00  <- trained depths
      2       0.5000              1.00  <- collapse (never composed a rule)
      3       0.5000              1.00  <- collapse (never composed a rule)
    learned weights: pol*stated +5.81, pol*one_step +4.45, pol -2.40 (the local
    shortcut in numbers: answer 'stated or one rule from stated', else lean on polarity)

Read it row by row. At depth 0 the stand-in is perfect, 1.0000: a depth-0 question asks whether an atom is stated, the stated feature answers it directly, and the learned weight $+5.81$ on $\mathrm{pol}\cdot\mathrm{stated}$ is that answer in numbers. At depth 1 it scores 0.9659: one rule application, and the $\mathrm{pol}\cdot\mathrm{one\_step}$ feature (weight $+4.45$) covers most cases, missing only the ones its positive-conditions-only shortcut mislabels. Then the floor gives way. At depths 2 and 3 the accuracy is 0.5000, exactly the coin-flip rate that the 50/50 balancing guarantees to any strategy blind to the logic, while the prover's column reads 1.00 at every depth, tautologically, because its answers are the labels, independently audited by the backward chainer. The run asserts all of it: trained-depth accuracy at least 0.80, depth-3 accuracy at most 0.65, a gap of at least 25 points (lines 412–416).

The collapse is not bad luck; it is arithmetic. For any question about a layer-2 or layer-3 predicate, stated is 0 (facts state only layer-0 predicates), and one_step is 0 as well, because the rule for a layer-2 head has a layer-1 positive premise that is never a stated fact. Every informative feature is dead, and what remains ($\mathrm{head\_pred}$, polarity, $\mathrm{fact\_frac}$) is, by the pairing construction, distributed almost identically across the true item and its false counterweight from the same layer. When the features cannot distinguish the members of a balanced pair, expected accuracy on the pair is exactly one half no matter what the classifier does, and 0.5000 is what the table shows. This is what the collapse identifies: the features can memorize local patterns of rules-and-facts, but they cannot compose them, and depth is precisely the number of compositions a question requires. The distinction matters beyond our toy: work that asks models to emit the proof alongside the answer found answers systematically more accurate than complete proofs, right answers arriving without a recoverable derivation [3], which is the same gap seen from the other side.

The instrument end to end: a seeded generator, a proof-derived labeler with depth read off the chaining rounds, balanced strata, and the two verdicts it produces: the stand-in's collapse beyond its trained depths and its failure to track a one-word logic edit that the prover tracks by construction. Original diagram by the authors, created with AI assistance.

The perturbation probe: change exactly when the logic changes

Per-depth accuracy still measures the model only on the distribution the generator defines. A sharper instrument asks a counterfactual question: if the logic of the theory changes minimally, does the model's answer change with it? This is invariance/sensitivity testing, and a diagnostic benchmark named RobustLR, built on RuleTaker-style theories, showed how much it exposes: models that look competent on standard test sets fail systematically when a theory is edited by a logical operation that flips or preserves the gold answer [4]. The logic of the design is symmetric and unforgiving. A reasoner must be sensitive to edits that change the entailment and invariant to edits that do not; failing the first means it ignores the logic, failing the second means it reads something other than the logic.

The companion miniaturizes the sensitivity half. The edit is one flipped negation: in the first rule whose body carries a positive layer-0 extra condition, that condition is negated (in eval theory 40, "and diligent" becomes "and not diligent"), everything else identical (lines 327–340). The perturbed theory is relabeled from scratch by the prover, and the probe keeps exactly the questions whose gold answer flips under the edit; on those items it asks whether each reasoner's answer tracks the flip (lines 343–366). For the prover the answer is yes on every item, by construction, because its answers are recomputed from the edited theory. For the stand-in, the committed run reports:

[5] the RobustLR-style probe: flip one rule negation, relabel, remeasure
    gold-flipped questions: 66   stand-in accuracy on them BEFORE the edit: 0.485
    tracked after the edit: 54/66 = 0.818   (prover: 1.000 by construction)
    the pre-edit accuracy is an aggregate (perfect at depth 1, zero at depths 2-3);
    every miss is one_step ignoring the newly negated condition (asserted < 1.0)

Two numbers carry the verdict, and both must be read as the aggregates they are. First, 0.485: before any edit, the stand-in sits near chance on these 66 questions, but not because each item is a coin flip. Split by depth, the 66 items are bimodal: 32 live at depth 1 and 34 at depths 2 and 3. On the 32 depth-1 items the pre-edit accuracy is 1.000, because before the edit the hinge condition is positive (perturb_theory negates the first positive layer-0 extra it finds, lines 327–340, so pre-edit that condition is positive), and checking positive conditions is exactly what one_step does. On the 34 depth-2/3 items the pre-edit accuracy is 0.000: these are the same composition failures the table's collapse rows document, nothing to do with negation. The aggregate $32/66 = 0.485$ lands near chance for a less flattering reason than chance: two certainties pointing in opposite directions.

Second, $54/66 = 0.818$: after the edit, the stand-in misses 12 of the gold flips, and here too the decomposition is the honest reading. All 12 misses are depth-1 items, and they are precisely the persons for whom the newly negated condition is a stated fact: for such a person the edited rule dies and the gold flips, but one_step ignores negated conditions, so the feature vector, and with it the prediction, does not move. This is where the built-in shortcut is actually exposed: on 12 of the 32 depth-1 items. The remaining 34 deep items are counted as tracked, but with the ten features (and so the prediction) identical before and after the edit: the stand-in was wrong on all of them beforehand, and the gold flipped underneath its unchanged answer to meet it. Only the depth-1 half of the probe measures genuine sensitivity, and there the stand-in tracks 20 of 32. A sound reasoner misses no flip at any depth, and the module asserts both committed facts, an aggregate pre-edit accuracy below 0.65 and a track rate strictly below 1.0 (lines 420–425). The general principle deserves its one-sentence form: a reasoner must change exactly when the logic changes, and any mismatch in either direction is evidence that something other than the logic is producing the answers.

What the real instrument found

Now read the published experiment against this frame, because the frame is what makes its result meaningful. The original study fine-tuned a large pretrained transformer on theories generated much like ours (100,000 questions per depth-graded dataset, posed against several thousand theories whose names and attributes are sampled from fixed pools, depths stratified and labels balanced) and reported two findings [1]. In distribution, the model trained on questions of depth at most 3 answered its own test set at 99.3 percent accuracy, which after the balancing and stratification cannot be a prior or a surface artifact. Out of depth, the finding our stand-in exists to calibrate: that same model scored 98.8 percent on held-out questions of depth 4 and 97.6 percent at depth 5, chains strictly deeper than anything seen in training. Whatever a bag of local patterns can do, we have just measured it: exactly 0.5000 one depth past its training budget. A transformer holding 97.6 percent two depths past its budget is therefore doing something no shallow-feature account predicts, and the instrument is what licenses that sentence. The same study also reported where the behavior cracked: zero-shot transfer to hand-authored theory families was uneven (five of six rulebases cleared 90 percent, the sixth did not), and on rule sets paraphrased into open English by crowdworkers that same depth-3-trained model managed only 66.1 percent zero-shot, recovering to 98.8 percent once paraphrased data joined the training mix [1]. Robust to depth, brittle to wording: exactly the opposite profile of the prover, which is indifferent to wording (the templates are parsed away) and indifferent to depth (the fixpoint runs as long as it must).

What separates the transformer from our stand-in is worth naming precisely, because it is not magic: scale (hundreds of millions of parameters against our ten), pretraining (a language model arrives with distributed representations of English already built), and above all an architecture whose core operation, attention, composes representations across positions in stacked layers, giving it at least the capacity to implement multi-step propagation that no fixed bag of local features possesses. But capacity is not identity. The instrument shows the transformer's behavior is consistent with deduction up to depth 5 on this distribution; it does not show that a soundness-preserving procedure is what the weights implement, and the paraphrase brittleness is a warning that the consistency is conditional. Our stand-in makes the caution vivid in miniature: at depths 0 and 1 it, too, looked like a reasoner, at 1.0000 and 0.9659, and it is nothing of the kind. Whether the mechanism behind good behavior can ever be certified from behavior is the identifiability question, and it belongs to Volume 5.

ProofWriter: all at once, or one step at a time

The follow-up experiment completes the chapter's lesson by moving from answers to proofs. ProofWriter, a generative successor trained on the re-released theories, produces not just the truth value but the derivation, and it was built in two deliberately contrasted versions [2]. The all-at-once version reads the theory and emits the answer together with the entire proof in a single generation pass. The iterative version does something structurally different: it generates only one-step implications, each new fact derived directly from sentences present in its input, then adds the generated fact to the theory and repeats, assembling deep proofs as chains of shallow ones. In distribution, both versions answered and proved with high accuracy. The reported divergence came exactly where this chapter has taught you to look: at proof depths beyond those seen in training. For models trained on closed-world theories of depth at most 3, answer accuracy stayed high one depth out (95.4 percent for the all-at-once model, 99.7 for the iterative, at unseen depth 4), and at unseen depth 5 the iterative model still answered 98.9 percent while the all-at-once model's answers slipped to 72.9 percent. The proofs told a starker story. Matched against the gold proofs, the all-at-once model's proof correctness fell to 69.9 percent at unseen depth 4 and 27.4 percent at depth 5, while the iterative model's proofs, assembled step by step from generated one-step implications, held at 88.9 and 87.8 percent at those same depths [2]. A separate measurement makes the failure concrete. Re-asking the model, step by step, whether each line of its own emitted proofs follows (a check that is only partial for closed-world theories, where steps resting on negation-as-failure resist one-step confirmation) validated just 66.7 percent of the all-at-once proofs at depth 4 and 13.8 percent at depth 5; the iterative model needs no such audit, because its proofs are verifiable by construction [2]. Right answers, unfaithful derivations: plausible-looking proofs not licensed by the theory, the failure mode the field calls hallucination, surfacing only once the required derivation outgrew the training distribution.

The reason is an argument, not an observation, and it is this volume's recurring design principle wearing natural-language clothes. Each step of the iterative strategy is a bounded, checkable object: one new sentence, claimed to follow from stated sentences in one rule application, exactly the granularity at which the model was trained and exactly the granularity at which a verifier (or Volume 1's t_p) can confirm it. A proof assembled from verified one-step inferences is faithful by construction, for the same reason forward chaining is trustworthy: the composition is performed by iteration in the world, outside the model, rather than imagined by the model in one pass. The all-at-once strategy asks the network to hallucinate the entire fixpoint computation internally, with nothing pinning intermediate steps to the theory, and at unseen depths the hallucination comes apart. The companion's own structure mirrors the winning side: its labeler never asks any component to leap to the fixpoint; it reaches depth 3 by calling the one-round operator three times, and each round is auditable. Exact inference by small certified steps has beaten one-shot approximation everywhere this volume has staged the contest: in circuits versus direct enumeration, in proof aggregation, and now in English.

The unsolved part

The instrument measures behavior; the claim we care about is mechanism, and the gap between them is this chapter's honest residue. Even a perfect per-depth curve cannot certify that deduction is what produces it. Our own table proves the point in miniature: restrict attention to depths 0 and 1 and the stand-in's curve reads 1.0000 and 0.9659, indistinguishable from a reasoner, while the depth-2 collapse and the probe reveal that its competence was a bundle of local shortcuts all along. Right answers from wrong features is not a hypothetical failure mode; it is what every row of that table above depth 1 documents, and nothing but a wider instrument (more depths, more perturbations) exposed it. For a transformer, the wider instrument helps but never closes the question: some still-unprobed family of shortcuts could always underlie the observed generalization. Volume 5 will formalize exactly this as the reasoning-shortcut problem, with machinery for counting the distinct mechanisms consistent with a training signal. And a second honesty is owed: everything measured here lives in a closed world of synthetic, templated English, where every sentence parses, every predicate is known, and unprovability means falsehood. That laboratory is what made gold labels possible, and it is not the language. Whether these findings survive open vocabulary, ambiguity, and an open world is the benchmark-design question taken up two chapters from now.

Why it matters

This chapter is Part VI's methodological foundation, and its lesson travels in both directions along the book. Backward: the instrument only exists because the symbolic pillar supplies incorruptible labels, and the chapter's quiet hero is Volume 1's forward chainer, promoted from example to measuring device, with its rounds reinterpreted as a difficulty dial. That is a general pattern worth owning: wherever exact inference is feasible, it can grade approximate inference, and the grading is only as good as the balancing and stratification around it. Forward: every trust question in Volume 5 (faithfulness of explanations, calibration, reasoning shortcuts, verifier-gated generation) is this chapter's question at scale, and the two findings to carry there are precise. First, depth-stratified, balanced, perturbation-tested evaluation can separate hypotheses that overall accuracy cannot. Second, when generation must be trusted, generate small checkable steps and compose them outside the model; faithfulness by construction beats faithfulness by hope. Systems that act on model outputs, and the SATORI-style architectures this series builds toward, inherit both.

Key terms

• RuleTaker: the experiment that trains transformers to answer true/false questions about small English theories, with depth-stratified, label-balanced data generated under a closed world; its instrument, not its headline, is this chapter's subject [1].
• Minimum derivation depth: the smallest height of any proof tree for an atom; equal, as proved here, to the first round of the immediate-consequence operator $T_P$ at which the atom appears.
• Negation-as-failure / closed-world assumption: the convention that an unprovable atom is false, and that a rule condition "not $p$" succeeds exactly when $p$ cannot be proved; safe here because negation is stratified, applied only to predicates no rule can derive.
• Label balancing: constructing the question bank so every depth stratum is exactly 50/50 true/false and surface markers are independent of the label ($I(G;N) = 0$), so any logic-blind strategy scores chance.
• Train shallow, test deep: the protocol of training only on questions of depth at most 1 (companion) or 3 (published) and measuring per-depth accuracy beyond, isolating compositional generalization from memorization.
• Stand-in reasoner: the companion's bag-of-local-features logistic model: perfect at depth 0, 0.9659 at depth 1, exactly 0.5000 at depths 2 and 3, the concrete face of "high accuracy without deduction."
• Invariance/sensitivity probe: editing a theory by a minimal logical operation and requiring the reasoner's answers to change exactly when the entailment changes [4]; the companion's negation-flip probe caught the stand-in missing 12 of 66 gold flips, every miss a depth-1 item whose newly negated condition the one_step shortcut ignores, against the prover's 1.000.
• All-at-once vs iterative proof generation: ProofWriter's two strategies: emitting a whole proof in one pass (proof correctness falling to 27.4 percent at unseen depth 5) versus generating one checkable implication at a time and composing by iteration (verifiable by construction, proof correctness 87.8 percent at unseen depth 5) [2].

Where this leads

The soft reasoner read English and answered directly, and the instrument showed exactly how far that can be trusted. The obvious alternative refuses the direct route altogether: parse the English into formal logic, hand the logic to a prover that is sound by theorem rather than by training, and return the prover's answer. The next chapter, Translate-Then-Prove, builds that pipeline on the same 20 evaluation theories and the same 1,500 questions this chapter committed (the companion exports them for exactly this purpose), so the two architectures meet on identical ground, and the failure modes trade places: the soft reasoner's composition errors vanish, and translation errors take their seat.

---

Companion code: examples/integration/ruletaker_lite.py implements the entire instrument: the controlled-English generator (lines 87–147), the ground compilation of negation-as-failure and the depth-tracking labeler built on Volume 1's t_p (lines 153–201), the balanced question bank (lines 209–263), the stand-in and its hand-written gradient (lines 268–320), the negation-flip probe (lines 327–366), and the assertions guarding every number quoted here (lines 372–425). Run python3 examples/integration/ruletaker_lite.py to reproduce this chapter's output byte for byte; the run ends with SUMMARY ruletaker_lite: eval_n=1500 acc_by_depth=1.000/0.966/0.500/0.500 probe_flipped=66 probe_track=0.818.