NL Reasoning Benchmarks: FOLIO, LogicBench, PrOntoQA

📍 Where we are: Part VI · Natural-Language Reasoning — Chapter 21. Translate-Then-Prove built a pipeline whose every answer arrives with a proof attached; this chapter builds the measurement instruments that can tell such a proof from a lucky label, and runs both of Part VI's systems through them.

The last two chapters produced two systems that answer logical questions posed in English: a soft reasoner that always answers and sometimes guesses, and a translate-then-prove pipeline that abstains rather than guess. Deciding between them requires a measurement, and measurements are made with instruments. This chapter treats reasoning benchmarks as exactly that: instruments, with a design, a resolution, and characteristic failure modes. Three published protocols each repaired one blindness in the naive "accuracy on true/false questions" instrument, and the companion module bench_lite.py rebuilds two of them at desk scale and transplants the third's discipline, so every trap this chapter names is a committed number rather than an anecdote.

The simple version

Imagine grading a math exam by checking only the final boxed answers. A student who answers "(c)" to every multiple-choice question scores 25 percent without reading a single problem, and more if "(c)" is overrepresented in the answer key. A student whose two errors cancel scores the same as one who computed cleanly. Fair grading needs three repairs: an answer key where guessing has a known, low payoff; questions sorted by which skill each exercises, so the report says which skills the student has; and a grader who reads the working line by line, checking that each line follows from the ones before it and that the lines actually reach the answer. The three benchmarks of this chapter are those three repairs, built for machines that claim to reason.

What this chapter covers

• The instrument view: what a benchmark claims to measure versus what its protocol can distinguish; the three illusions (coin-flip inflation, aggregate blur, label-only kindness) the naive protocol permits.
• Three-way entailment under the open world: FOLIO's True/False/Unknown semantics, executed by a dual prover query, with the proof that the three labels partition cleanly.
• The majority-class trap, measured: the best guessing strategy derived, and the committed table where a constant guesser posts 0.500 against the 0.333 random floor.
• Per-rule isolation: LogicBench's one-inference-rule-per-item design and the paired-variation trick against pattern matching.
• PrOntoQA's two design choices: fictional predicates that pretrained knowledge cannot answer, and gold chains-of-thought in one-to-one correspondence with proof steps.
• The step checker: the four-flag verifier (parsed, valid, linear, connects), and why the translate-then-prove pipeline passes it at an asserted 100 percent.
• The greedy exhibit: a baseline whose every step is a sound modus ponens and whose label accuracy beats the pipeline's, yet whose proof accuracy collapses to 0.167, with the right-for-wrong-reason rate of 0.650 derived and measured.
• The metric-trap table: label accuracy, proof accuracy, and abstention side by side, the divergence column Volume 5 will name a reasoning shortcut.

What a benchmark can and cannot see

A benchmark is a claim wrapped around a protocol. The claim says something like "this dataset measures logical reasoning"; the protocol is the machinery of example generation, gold labeling, and scoring. The claim is only as good as what the protocol can distinguish, and the naive protocol, binary questions scored by label accuracy, permits three distinct illusions. Coin-flip inflation: with two labels a coin scores 0.5, and with any label imbalance, always emitting the most frequent label scores more; neither performs one step of inference. Aggregate blur: a single headline accuracy averages over every kind of inference the dataset contains, so a system that has mastered one inference rule and is helpless at another posts the same 0.75 as a system with the opposite profile. Label-only kindness: a label can be right while the reasoning that produced it is wrong, since a broken chain of steps can still land on the correct answer in a small answer space; scoring only the label forgives, and so rewards, exactly this shortcut-taking.

Each protocol this chapter rebuilds closes one hole, and the table below is the chapter's map. FOLIO (named for the First-Order Logic annotations it carries) adds a third label, Unknown, whose semantics forces genuine entailment checking, with gold labels audited by a prover [1]. LogicBench isolates one inference rule per item, so competence is reported per rule rather than en masse [2]. PrOntoQA (Proof and Ontology-generated Question-Answering) makes the reasoning itself part of the data: fictional ontologies deny pretrained knowledge any purchase, gold chains-of-thought correspond one-to-one with proof steps, and a checker verifies each generated step, splitting label accuracy from proof accuracy [3].

illusion	what slips through	protocol that closes it	mechanism
coin-flip inflation	guessers and priors score well	FOLIO-style three-way labels	Unknown carries epistemic weight; per-label slices and baselines reported
aggregate blur	one number hides uneven competence	LogicBench-style rule isolation	one inference rule per item; accuracy reported per rule
label-only kindness	right answers from broken reasoning	PrOntoQA-style checkable chains	gold chain-of-thought equals the proof; a step checker scores the chain, not just the label

Three illusions, three protocol repairs, and the instrument they culminate in: a step checker that splits label accuracy from proof accuracy, exposing the greedy baseline's 0.650 right-for-wrong-reason rate. Original diagram by the authors, created with AI assistance.

Everything below is runnable. The module bench_lite.py generates a PrOntoQA-style corpus and a FOLIO-style corpus from one seeded random stream, runs the translate-then-prove pipeline of the previous chapter and a deliberately greedy baseline over the PrOntoQA-style corpus, runs a dual-query labeler, a closed-world forward chainer, and the majority baseline over the FOLIO-style corpus, and guards every claim with an assert (bench_lite.py lines 586–616). Two runs print byte-identical output, so every number in this chapter is a property of the committed protocol, not of a sampled model.

Three-way entailment under the open world

Start with the label semantics, because the whole FOLIO design follows from it. Write $\Gamma$ (capital gamma) for the premise set, the sentences a single example asserts, and $q$ for the conclusion, the sentence to be judged. The symbol $\models$ reads "entails": $\Gamma \models q$ means every situation that makes all of $\Gamma$ true also makes $q$ true. The symbol $\lnot$ reads "not", so $\lnot q$ is the conclusion's negation. The three labels are defined by two entailment questions rather than one [1]:

$$\text{Label}(\Gamma, q) \;=\; \begin{cases} \textsf{True} & \text{if } \Gamma \models q,\\[2pt] \textsf{False} & \text{if } \Gamma \models \lnot q,\\[2pt] \textsf{Unknown} & \text{otherwise.} \end{cases}$$

This is the open-world assumption from Volume 2, now doing benchmark duty: failure to prove $q$ is not evidence that $q$ is false, only absence of evidence, and the label set contains a class for exactly that state. The Unknown class carries the design's epistemic weight: a system earns credit on Unknown examples only by recognizing that neither entailment holds, a strictly harder act than pattern-matching a conclusion against the premises.

The three cases genuinely partition, provided $\Gamma$ is consistent. Suppose both $\Gamma \models q$ and $\Gamma \models \lnot q$ held. Every model of $\Gamma$ (every situation making all premises true) would have to make $q$ true, by the first entailment, and $\lnot q$ true, by the second; no situation does both, so $\Gamma$ would have no models, contradicting consistency. The corpus generator builds each theory around a satisfiable chain with a stated instance, so its theories have models by construction (bench_lite.py lines 417–464): the three labels are mutually exclusive and exhaustive.

Decode the semantics on one academic-world triple. Premises: every professor is a researcher; every professor is not a student; Alice is a professor. Query "Alice is a researcher": proving $q$ succeeds by one modus ponens step, label True. Query "Alice is a student": proving $q$ fails, but proving $\lnot q$ succeeds through the negative rule, label False. Query "Alice is funded": the premises never touch funding, both proofs fail, label Unknown. Two prover calls per example, and the label is whichever outcome the pair lands in. That is precisely the committed labeler, the body of folio_dual_query (bench_lite.py lines 473–480):

    prog = _compile(ex["context"])
    facts, rules = prog                      # FOLIO-lite text is never corrupted
    a = ex["name"].lower()
    if sld.prove((ex["query_concept"], a), facts, rules) is not None:
        return "True"
    if sld.prove(("not_" + ex["query_concept"], a), facts, rules) is not None:
        return "False"
    return "Unknown"

The negation is handled by reification: the rule "every $b$ is not an $h$" ($b$ names the rule's body concept, the one being generalized over; $h$ names its head concept, the one being denied) compiles to a rule whose head is the fresh predicate not_h, so proving not_h(alice) is proving the negation (bench_lite.py lines 349–372). On the theories this generator emits, Volume 1's prover, built on SLD (Selective Linear Definite clause) resolution, is sound and complete, so the dual query is not an approximation of the label semantics; it is the label semantics, executed. One honest qualifier: the reification deliberately forgoes contrapositive reasoning. Classically, "every $b$ is not an $h$" together with the fact "Alice is an $h$" entails that Alice is not a $b$, but not_b(alice) has no SLD derivation under the encoding. The exactness is a property of the generated corpus rather than of the signed fragment at large: the generator never states a negative-rule head as a fact and never places one in a rule body (bench_lite.py lines 417–464), so no query it poses ever needs a contrapositive, and the committed assert certifies exactness at that corpus level: dual_acc == 1.0, exactly (bench_lite.py line 612).

That construction mirrors a discipline in the source protocol worth naming. FOLIO pairs expert-written natural language with hand-authored first-order logic annotations, and the protocol did not trust the hand: the FOL annotations were run through an inference engine, whose verdicts audited the gold, and examples whose annotated label failed the machine check were repaired [1]. Gold verified by a prover is the difference between measuring entailment and measuring agreement with annotators. Our miniature inherits the property by construction: the labels are prover outputs in the first place.

The majority-class trap, measured

Three-way labels close the coin-flip hole only if the label distribution is watched, and FOLIO's own mix shows why: the paper puts its majority baseline at 38.5 percent, its test split carrying 87 True, 78 False, and 61 Unknown examples [1]; tallied from the released train split, the counts are 388, 286, and 330. The miniature pushes the imbalance a little harder so the trap is unmissable, targeting a 45/22/33 mix (bench_lite.py line 107).

Derive the guesser's payoff before quoting it. Write $p_\ell$ for the fraction of examples carrying label $\ell$, and consider a system that ignores the input and emits label $\ell$ with probability $g_\ell$ (any fixed guessing strategy, the $g_\ell$ summing to one). Write $\mathbb{E}$ for the expectation, the probability-weighted average, and read the symbol $\sum_{\ell}$ as "sum over the three labels". The guesser's expected accuracy is the probability that its guess matches the gold label, obtained by adding up, over every label $\ell$, the chance $p_\ell$ that the gold label is $\ell$ times the chance $g_\ell$ that the guess is $\ell$:

$$\mathbb{E}[\text{acc}] \;=\; \sum_{\ell} p_\ell\, g_\ell \;\le\; \Big(\max_{\ell} p_\ell\Big) \sum_{\ell} g_\ell \;=\; \max_{\ell}\, p_\ell,$$

where the inequality replaces each $p_\ell$ by the largest one, and the bound is achieved by putting all guessing mass on the most frequent label ($g_{\ell^\ast} = 1$ for $\ell^\ast$ the majority class). The best input-blind strategy is therefore the majority baseline, its accuracy is the majority frequency $\max_\ell p_\ell$, and the uniform coin's $1/3$ is merely one point of the guessing family, the only mix-independent one: the family's full range runs from $\min_\ell p_\ell$ (all guessing mass on the rarest label) up to $\max_\ell p_\ell$ (on the committed mix stated below, $11/60 \approx 0.183$ up to $30/60 = 0.500$), so neither $1/3$ nor any other single number is the guessing ceiling. Headline numbers must be read against $\max_\ell p_\ell$, not against $1/3$.

The committed run realizes the target mix as 30 True, 11 False, 19 Unknown out of 60, so $\max_\ell p_\ell = 30/60 = 0.500$, and the per-label table shows all three systems' profiles at once:

[4] FOLIO-lite (3-way open-world, dual query), n=60, mix True/False/Unknown = 30/11/19
    system             True   False  Unknown  overall
    dual-query prover   1.00   1.00   1.00    1.000
    greedy CWA          1.00   1.00   0.00    0.683
    majority (True)     1.00   0.00   0.00    0.500
    majority beats the 33.3% random floor at 50.0% (the imbalance trap);
    never saying Unknown caps a system at 68.3% — greedy CWA sits exactly there.

Two lessons sit in this table. The first is the trap itself: the majority row performs zero inference and posts 0.500, a full 16.7 points above the random floor; "our system reaches 55 percent on three-way entailment" reports almost nothing until the majority baseline is printed beside it. The second belongs to the Unknown column. The row greedy CWA, short for the closed-world assumption (whatever is not derivable is false), is a forward chainer that answers True if the query atom is derivable and False otherwise (bench_lite.py lines 483–499). It can never say Unknown, so it is wrong on every Unknown example, bounding its accuracy by $1 - p_{\textsf{Unknown}} = 1 - 19/60 = 41/60 \approx 0.683$; the committed run shows it sitting exactly on that ceiling, since it is perfect on the two labels it can utter. A system's label vocabulary bounds its accuracy before any question of reasoning arises, and the per-label slice reveals the bound. This is Volume 3's ranking-protocol discipline transplanted into natural language: never publish a headline number without the baseline and slices that show where it comes from.

One rule per item: the LogicBench discipline

The second illusion, aggregate blur, survives balanced labels. Two systems can share an aggregate accuracy while commanding disjoint sets of inference rules, and no reweighting of a mixed dataset separates them. The repair is structural: build the dataset so each item exercises exactly one inference-rule pattern, then report accuracy per rule. That is LogicBench's design: 25 reasoning patterns spanning propositional, first-order, and non-monotonic logic, each item instantiating a single named rule such as modus ponens, modus tollens, or a disjunctive syllogism, so the evaluation reads out a competence profile rather than a scalar [2]. One more anti-shortcut device rides along: each context is paired with multiple yes/no question variations, systematically negating and permuting the conclusion, so a system keying on surface overlap rather than on the rule is caught contradicting itself across the variations of a single context [2].

The published finding reads uncomfortably against the aggregate-blur illusion: evaluated per rule, frontier language models fell short of the human baseline, with the profile uneven in a consistent direction, rules involving negations among the hardest, and models sometimes overlooking contextual information the inference needs [2]. A single aggregate would have blended those weak rules into a respectable-looking mean; the per-rule table localizes the failure.

Our miniature applies the discipline in the form the desk-scale corpus allows. The PrOntoQA-lite generator deliberately uses one rule family, modus ponens over positive unary rules (the shared grammar also carries a signed form, used only by the FOLIO-lite generator), so "per rule" collapses; what remains to slice by is depth (how many rule applications the gold proof needs) and label, and the committed output reports both: the per-depth table below, the per-label FOLIO table above. The axis differs; the discipline is identical: report competence per isolated skill, never only en masse. The module also encodes LogicBench's other lesson, that natural language varies while strict patterns do not, as a corruption operator (bench_lite.py lines 189–195), applied with per-example probability 0.25 (CORRUPT_FRAC, bench_lite.py line 102; the per-example coin, lines 235–237) and realized as 20 of the 60 committed examples:

def corrupt_sentence(sign: int, body: str, head: str) -> str:
    """The out-of-grammar paraphrase (the LogicBench lesson: natural language
    varies; a strict grammar does not).  Pluralizing "Every b is a h." into
    "All bs are hs." preserves the meaning exactly — a human or an LLM reads
    straight through it — but the strict parser returns None."""
    neg = "" if sign > 0 else "not "
    return f"All {body}es are {neg}{head}es."

A meaning-preserving paraphrase that defeats a strict parser is the desk-scale stand-in for linguistic variation, and it is what generates the abstention column of the final table.

Fictional worlds and checkable chains: PrOntoQA's two design choices

The third protocol is the chapter's centerpiece, and its two design choices each answer a specific threat to measurement validity.

Choice one: fictional predicates. A model pretrained on the web already knows that cats are mammals; ask it to "deduce" that from stated premises and the measurement is confounded, since a correct answer may come from the premises or from parametric memory. PrOntoQA generates ontologies over invented concept nouns, wumpuses and yumpuses and zumpuses, about which no pretrained model can know anything, so any correct answer must have come through the stated context [3]. The published comparison confirms the confound is real: models score best when the ontology agrees with common-sense knowledge, worse on fictional ontologies, and slightly worse still when the ontology contradicts pretraining; the source finds the fictional and contradicting settings comparable, with the large gap lying between the agreeing ontology and both, and that gap measures exactly the leakage the fictional vocabulary shuts off [3]. The miniature adopts the vocabulary wholesale (bench_lite.py lines 111–114) and generates, per example, a linear subtype chain $c_0 \sqsubseteq c_1 \sqsubseteq \cdots \sqsubseteq c_h$ over $h$ hops (rule applications), where $\sqsubseteq$ is Volume 2's subsumption symbol and reads "is a subtype of": every $c_0$ is a $c_1$, every $c_1$ is a $c_2$, and so on up the chain. Alongside the chain sits one distractor rule per hop, a fork $c_k \sqsubseteq d_k$ at each hop $k$ (the hop index, counting from $0$) into a dead-end concept $d_k$, the anti-shortcut device that will matter enormously below (bench_lite.py lines 200–255).

Choice two: gold chains-of-thought in one-to-one correspondence with proof steps. This is a requirement on the data, not the model. If the gold explanation is a free paragraph, nothing mechanical can compare a system's reasoning against it. PrOntoQA generates each example from a formal proof and verbalizes it one sentence per modus ponens step, so the gold chain-of-thought is the proof, in a controlled grammar that can be inverted [3]. Invertibility is the load-bearing property: generator and checker share one grammar, so every generated sentence parses back to exactly the atom or rule it came from, and a predicted chain-of-thought in the same grammar can be semantically parsed and checked step by step. Checkable reasoning cannot be bolted on afterward; it must be engineered into the generator. The miniature builds its gold chain in the same breath as the example, one verbalized instance fact per chain concept in derivation order (bench_lite.py line 253), and a seeded coin asks the chain's end positively ("Sam is a jompus", gold True) or negatively ("Sam is not a jompus", gold False); both polarities share the same gold proof, so polarity guessing and proof production are decoupled (bench_lite.py lines 233–251).

The step checker: the chapter's instrument

Now the instrument itself. Given an example and a predicted chain-of-thought, a list of generated sentences, the checker check_trace parses each line back to logic and asks four questions, the first three of increasing strength plus an end-to-end connectivity check (bench_lite.py lines 284–304):

    established = {ex["chain"][0]}          # the instance axiom c_0(a)
    prev = ex["chain"][0]                   # conclusion of the previous step
    parsed = valid = linear = True
    for line in cot:
        p = parse_sentence(line)
        if p is None or p[0] != "fact" or p[1] != entity:
            parsed = valid = False
            break
        c = p[2]
        # valid: ∃ rule (b → c) with b(a) established before this step.
        if not any(b in established and h == c for b, h in pos_rules):
            valid = False
        # linear: the premise used must be the previous step's conclusion.
        if not any(b == prev and h == c for b, h in pos_rules):
            linear = False
        established.add(c)
        prev = c
    connects = parsed and len(cot) > 0 and prev == ex["query_concept"]
    return {"parsed": parsed, "valid": valid, "linear": linear,
            "connects": connects,
            "strict": parsed and valid and linear and connects}

Decode the four flags. Parsed: every line inverts through the shared grammar to an atom about the right entity; an unparseable step is marked incorrect, as the source protocol scores it [3]. Valid: each step is a correct rule instantiation, some context rule $\forall x\,(b(x) \rightarrow c(x))$ (read: for every individual $x$, if $b$ holds of $x$ then $c$ holds of $x$) whose premise $b(a)$ was already established by the instance axiom or an earlier step; this is local soundness. Linear: the premise each step consumes must be the conclusion of the immediately preceding step. The source protocol distinguishes strictly valid steps, derivable by the gold proofs' own deduction rule (modus ponens), from broadly valid ones, derivable only under a stronger proof calculus, such as chaining two rules into one step [3]; the linkage requirement is a further tightening from the out-of-distribution extension, which requires that a proof step immediately follow one of its premises [4]. Connects: the final conclusion is the queried atom, so the accepted steps form a premises-to-goal path. The strict verdict is the conjunction of all four, the miniature of the published proof-accuracy metric under its strict step standard [4].

The strict/lenient distinction is not pedantry. The published analysis found model-produced steps overwhelmingly locally sound: at five hops, 93.2 percent were strictly valid [3]. If local validity were the standard, chain-of-thought would look nearly solved. The strict standard exists because a pile of individually sound steps is not a proof; the steps must connect, and connectivity is where systems fail.

One structural fact makes the pipeline's relationship to this checker exact. The translate-then-prove pipeline parses question and context strictly, abstaining on any failure, then runs Volume 1's goal-directed SLD prover (bench_lite.py lines 388–412), the architecture of the previous chapter's translate_prove.py (translate_prove.py lines 211–228) rebuilt over the fictional grammar. Backward chaining starts at the goal and works toward the premises, so any proof it emits is, by construction, a connecting linear chain; flattened into sentences (bench_lite.py lines 375–385), such a trace cannot fail the strict checker. The committed assert states it as a theorem checked by execution: every trace the pipeline emits passes, a trace pass rate of exactly 1.0 (bench_lite.py line 589). The 100 percent is not a benchmark score; it is a structural property of goal-directed proof search, verified on every example.

The greedy reasoner, read three ways

The instrument earns its keep against a system built to fool the naive protocol. The published finding it miniaturizes: language models prompted for chain-of-thought produce individually valid steps but fail as planners; when several rules apply they greedily pursue whichever is salient rather than the one on the goal path, so the characteristic failure is a misleading step, not an invalid one [3]. The module runs the finding as an algorithm, the body of greedy_reason (bench_lite.py lines 324–344):

    goal = ex["query_concept"]
    established = {ex["chain"][0]}
    lines: list[str] = []
    for _ in range(cap):
        fired = None
        for s, b, h in ex["rules"]:            # fixed listed order
            if s > 0 and b in established and h not in established:
                fired = (b, h)
                break                          # FIRST applicable rule
        if fired is None:
            break
        established.add(fired[1])
        lines.append(verbalize_fact(ex["name"], fired[1]))
        if fired[1] == goal:
            break
    reached = goal in established
    if reached:
        label = "True" if ex["polarity"] == 0 else "False"
    else:                                       # not derived within the cap
        label = "False" if ex["polarity"] == 0 else "True"
    return label, lines

Forward-chain from the instance axiom, fire the first applicable rule in the listed order, stop at the goal or at a cap of 9 steps. Every fired step is a genuinely valid modus ponens; no step is ever wrong. It also reads the gold symbolic rules directly, the stand-in for a model that wording never stops, so it never abstains. Here is the committed worked example, a 3-hop context, with both systems' traces and verdicts:

[1] worked example #20 (hops=3) — the greedy trap
      Every wumpus is a rompus.
      Every wumpus is a yumpus.
      Every rompus is a brimpus.
      Every rompus is a zumpus.
      Every zumpus is a jompus.
      Every zumpus is an impus.
      Sam is a wumpus.
      True or false: Sam is not a jompus.   (gold label: False)
    translate-then-prove answers False; its SLD proof chain:
      rompus -> zumpus -> jompus
      checker: parsed=yes valid=yes linear=yes connects=yes  -> strict PASS
    greedy reasoner answers False; its first-applicable trace:
      rompus -> yumpus -> brimpus -> zumpus -> jompus
      checker: parsed=yes valid=yes linear=NO connects=yes  -> strict FAIL

Both systems answer False, and False is right. The pipeline's chain is the three-step proof. The greedy trace contains that proof interleaved with two excursions into the distractor forks (yumpus, brimpus): all five steps parse and validly instantiate context rules, but already at the second line the rule fired (every wumpus is a yumpus) consumes wumpus, not the previous line's conclusion rompus, and the same stitching failure repeats at the third and fourth lines (brimpus after yumpus, zumpus after brimpus), so linear fails and the trace is no proof. The naive protocol scores these two systems identically here. The strict checker does not.

Now the committed per-depth table (twenty examples per hop count), read three ways:

[3] per-depth accuracy (label vs strict proof), 20 examples each
    hops   pipeline label/proof     greedy label/proof
       1        0.55 / 0.55              1.00 / 0.50
       3        0.70 / 0.70              1.00 / 0.00
       5        0.75 / 0.75              0.45 / 0.00
    greedy right-for-wrong-reason rate: 0.65 (label correct, proof invalid or non-connecting)

Stratifying accuracy by proof depth is itself an inherited discipline: the line of work behind ProofWriter established per-depth evaluation and the scoring of generated proofs, not just labels, as the way to tell composition from memorization [5]. Read the greedy column against the mechanism. Label accuracy is flattering. At 1 and 3 hops it is perfect: the goal atom is always derivable, a hop-$h$ context lists $2h$ rules, each firing adds one new atom, so at most $2h$ firings exhaust the context, and for $h \le 3$ that is at most 6 firings, inside the cap of 9. At 5 hops the arithmetic flips. The first-applicable scan fires each hop's two rules consecutively, in their coin-listed order, because a hop's not-yet-fired rule sits earlier in the list than every later hop's rule; hop $k$'s pair therefore occupies firings $2k+1$ and $2k+2$ (counting hops from $k=0$), and the goal $c_h$ lands at firing $2h-1$ when the final hop's coin listed gold before its distractor, at firing $2h$ otherwise. Whether the run is truncated is decided by the final hop's order coin alone: gold first means the goal arrives at firing $2 \times 5 - 1 = 9$, exactly the cap; distractor first pushes it to $2 \times 5 = 10$, one past it (the budget arithmetic spelled out at bench_lite.py lines 96–101). The prediction is a success probability of one half; the committed corpus realizes 9 of 20, the 0.45 in the per-depth table above, and the depth-collapse assert guards exactly that drop (bench_lite.py lines 606–608): a planning-budget failure, invisible at shallow depths, catastrophic at deep ones. Step validity is high by construction: every fired step is sound, exactly the published profile of locally valid steps [3]. Proof accuracy is brutal. At 1 hop the trace is strict only when the seeded coin listed the gold rule before the distractor, probability one half, measured 0.50. At 3 and 5 hops it is exactly 0.00: even when every pair lists gold first, the first-applicable scan returns to an earlier distractor before advancing the chain, so the trace always interleaves and linear always fails.

The gap between the first and third readings has a name and a formula. Define, over the 60 examples, the events $L$ (the label is correct) and $S$ (the trace passes the strict checker), and the right-for-wrong-reason rate $r = P(L \wedge \lnot S)$, where $\wedge$ reads "and": the probability of a correct label carried by a non-proof. Splitting $L$ over the two cases of $S$, and reading the double arrow $\Longrightarrow$ below as "therefore":

$$P(L) \;=\; P(L \wedge S) + P(L \wedge \lnot S) \quad\Longrightarrow\quad r \;=\; P(L) - P(L \wedge S).$$

For the greedy reasoner, a strict pass implies a correct label: a connecting chain ends at the queried atom, so the goal was reached and the polarity mapping returns the gold label. Hence $S \subseteq L$, where $\subseteq$ reads "is contained in": every strict-pass example is also a correct-label example. So $P(L \wedge S) = P(S)$, and the rate collapses to a difference of the two headline columns:

$$r \;=\; P(L) - P(S) \;=\; 0.817 - 0.167 \;=\; 0.650,$$

which is exactly the committed rfwr=0.650: on 39 of 60 examples the greedy reasoner is right for the wrong reason, and the assert guards the phenomenon's existence rather than trusting the prose (bench_lite.py line 597). The divergence between label accuracy and proof accuracy is not a discrepancy between two metrics; it is the measured rate of unearned correctness.

The metric trap: one number is not enough

The chapter's legacy table puts the three measurements side by side, with abstentions counted as wrong so neither system can hide behind silence:

[5] metric-trap summary (PrOntoQA-lite, abstentions count wrong)
    system                label acc   proof acc   abstention
    translate-then-prove     0.667       0.667        0.333
    greedy heuristic         0.817       0.167        0.000
    the trap: greedy WINS the label column (0.817 vs 0.667) while its proofs
    collapse (0.167 vs 0.667); on answered examples the pipeline is at 100%/100%.

Read column by column. Under label accuracy alone, the greedy heuristic wins, 0.817 to 0.667, and the assert pins that ordering deliberately (bench_lite.py lines 600–601): the trap is committed, not hypothetical. The pipeline's 0.667 is pure coverage arithmetic, the previous chapter's factorization $P(\text{correct}) = P(\text{parse}) \times 1$ made visible again: the seeded corruption pushed one sentence out of grammar in 20 of the 60 examples, the pipeline abstained on exactly those 20 (asserted, bench_lite.py lines 593–595), and on the 40 it answered it is at 100 percent labels and 100 percent proofs. Its per-depth label and proof numbers are equal for the same reason: every answered example carries a strict proof, so both columns reduce to per-depth coverage, 0.55, 0.70, 0.75. Under the proof-accuracy column the ordering inverts, 0.667 against 0.167, by a margin the assert requires to be at least 25 points (bench_lite.py lines 602–603).

The table is the volume's measurement legacy because each column answers a different question. Label accuracy: how often is the output right. Proof accuracy: how often is it right for the stated reason. Abstention: how often does the system know it cannot answer. No column subsumes the others, and an evaluation reporting only the first systematically prefers confident shortcut-takers over sound abstainers. The divergence column, label accuracy minus proof accuracy, is precisely the quantity Volume 5 will study under the name reasoning shortcut: a mechanism that reaches correct outputs without computing the sanctioned function, harmless on the training distribution, primed to fail off it, exactly as the greedy reasoner's flattering shallow-depth numbers concealed its 5-hop collapse.

A common misconception

"If the steps are correct, the reasoning is correct." The committed exhibit shows the dominant failure mode is the opposite: the greedy reasoner's steps are all individually correct, and its chains are still not proofs. Step-level and chain-level validity are different measurements; the published analysis this exhibit miniaturizes found model steps 93.2 percent strictly valid at five hops even as the chains failed as plans [3]. Grade the chain, not the steps.

The unsolved part

The step checker is the strongest instrument in this chapter, and its reach is bounded by a requirement it cannot relax: the steps must be parseable. The miniature's checker inverts a grammar the generator itself wrote, so parsing is exact by construction; the published protocol likewise leans on a controlled grammar it can semantically parse [3]. Free-form chain-of-thought defeats this. The moment a system phrases a step as "so Sam must be one of those jompus-like things," no grammar inversion recovers an atom, and the checker's only honest verdicts are "unparseable" (punishing phrasing rather than reasoning) or a lenient semantic match that reintroduces judgment exactly where the instrument was supposed to remove it. The tension between naturalness and checkability is real: the more natural the language a benchmark accepts, the less mechanical its verification can be, and no current protocol holds both ends of that rope.

Two further caveats keep the chapter honest. Fictional worlds test deduction in isolation, which is their purpose, but real reasoning interleaves deduction with knowledge the premises never state, and nothing in this protocol measures that integration. And every synthetic generator leaks its grammar into what it measures: our corpus has one sentence template per axiom shape, one distractor per hop, and modus ponens only, so a system could in principle master the generator rather than the logic. The protocol's out-of-distribution extension exists precisely because of this worry, testing generalization to deeper, wider, and rule-wise unfamiliar proofs than the demonstrations [4], and the docstring of bench_lite.py states its own simplifications out loud (bench_lite.py lines 53–60). Benchmarks are instruments, and instruments have error bars of their own; the verdict chapter inherits both the measurements and these caveats.

Why it matters

This chapter closes Part VI by delivering what the two preceding chapters could not measure for themselves. The soft reasoner and the translate-then-prove pipeline each claimed a virtue, robustness for one, soundness for the other; the three protocols here turn those claims into columns of a table. The methodological payoff generalizes far beyond desk scale: report per-label slices and the majority baseline with every headline number, isolate skills so the report says which ones a system commands, and wherever the output is supposed to be reasoning, score the reasoning with a checker rather than trusting the label.

The forward payoff is Volume 5's agenda, stated in this chapter's own numbers. The divergence between a 0.817 label column and a 0.167 proof column is the reasoning-shortcut phenomenon in miniature; the abstention column is the seed of calibration and selective prediction; the step checker is the ancestor of the verifier-gated reasoning Volume 5 builds; and the fictional-ontology device returns there as the standard control separating parametric knowledge from in-context inference. Trust at scale begins with instruments that cannot be flattered, and this chapter built three.

Key terms

• Benchmark protocol: the machinery of a benchmark, example generation, gold labeling, required outputs, scoring; what it can distinguish, as opposed to what it claims to measure.
• Three-way entailment label: True if the premises entail the conclusion, False if they entail its negation, Unknown if neither; decided by a dual prover query under the open world.
• Majority baseline: the input-blind strategy that always emits the most frequent label, with accuracy $\max_\ell p_\ell$; 0.500 on the committed FOLIO-lite mix.
• Per-rule isolation: building each item around exactly one inference-rule pattern so accuracy can be reported per rule; LogicBench's design.
• Fictional ontology: a theory over invented predicates that pretrained knowledge cannot answer, isolating in-context deduction from parametric memory; PrOntoQA's design.
• Step checker: the verifier that parses each chain-of-thought line and tests rule instantiation (valid), immediate premise linkage (linear), and premises-to-goal connectivity (connects); the conjunction is strict proof accuracy.
• Strict vs broad step validity: the source protocol's per-step axis: strictly valid means derivable by the deduction rule the gold proofs use (modus ponens), broadly valid means derivable only under a stronger calculus, such as two rules chained into one step; the separate linkage requirement (the linear flag) comes from the out-of-distribution extension and is what separates piles of sound steps from proofs.
• Right-for-wrong-reason rate: $P(L \wedge \lnot S)$, a correct label carried by a non-proof; equals label accuracy minus proof accuracy when strict proofs imply correct labels; 0.650 for the committed greedy baseline.
• Metric trap: the committed inversion where one system wins label accuracy (0.817 vs 0.667) while losing proof accuracy (0.167 vs 0.667); no single column suffices.

Where this leads

Part VI is complete: a monolithic reader that fails quietly, a factorized pipeline that fails loudly, and now the instruments that tell those failure modes apart and price them. What remains is the settlement. The Honest Verdict closes the volume by reading every Part's committed receipts into one ledger: what each way of making logic differentiable bought, what it cost, which assert guards each claim, and which debts (calibration, faithfulness, reasoning shortcuts, trust at scale) are carried forward as Volume 5's table of contents.

---

Companion code: examples/integration/bench_lite.py generates both corpora, runs both systems, applies the step checker and the dual-query labeler, and asserts every committed claim: the 100 percent trace pass rate, the abstention/corruption coincidence, the nonzero right-for-wrong-reason rate, the metric-trap inversion, the greedy depth collapse, and the majority and never-Unknown bounds. Run python3 examples/integration/bench_lite.py to reproduce every number in this chapter; examples/integration/translate_prove.py holds the pipeline architecture the benchmark systems inherit.