The Entailment-Benchmark Gap

📍 Where we are: Part VI · Benchmarks and Evaluation — Chapter 17. NeSy Benchmark Suites toured the field's shared testbeds and their aggregate scores; this chapter measures the property those aggregates are structurally blind to: whether a system's answers respect the closures that entailment itself obeys.

Every benchmark in the previous chapter shares one design decision so universal it is invisible: test questions are sampled independently and scored independently, and the report is the fraction answered correctly. That protocol measures a pointwise property, and entailment is not a pointwise property. It is a relation with closure properties: a theory that entails a query also entails every paraphrase of it, denies its negation, is unmoved by a sentence that touches no derivation, and answers a rewritten composite exactly as the rewrite demands. A system that computes entailment inherits those invariances automatically, because all its answers are read off one closure; a system that predicts labels inherits none of them, and plain accuracy cannot tell the two apart. This chapter makes the gap runnable on the academic world: the companion generates matched probe families from the same seeded theories, measures Volume 4's two familiar systems, and posts the number the leaderboard hides.

The simple version

Imagine two students taking a geography quiz. Both score 99 percent. But when you ask the first student "Is Paris north of Madrid?" and, ten questions later, "Is Madrid north of Paris?", she happily answers yes to both. The second student never does that, not because he memorized more facts, but because he answers every question by looking at one mental map, and a single map cannot put Paris both north and south of Madrid. The quiz score cannot separate them, because the quiz asks each question on its own. The fix costs nothing: ask questions in linked pairs whose answers must cohere, and count how often the coherence holds. You need no new answer key, since the second answer of each pair is determined by the first.

What this chapter covers

The gap defined: entailment as an invariance property (closed under transformations) versus accuracy as a pointwise property, with the measurement consequence drawn immediately: test logically linked families, not independent instances.
Four probe families generated by logic: contraposition pairs, irrelevant-expansion (monotonicity) probes, paraphrase probes, and De Morgan rewrites, each with its generation rule quoted from the companion, and none needing a single new human label.
The committed measurement: the statistical reasoner's 98.96 percent plain accuracy against consistency rates of 71.6 and 48.6 percent on two families, and the mechanical reading of which families hurt and why.
The structural contrast: the translate-then-prove pipeline's consistency at exactly 1.0 on every parsed probe in every family, priced honestly by its 24.55 percent abstention on paraphrase probes.
Necessity without sufficiency: consistency can be trained in family by family, and a system can be consistently wrong; the exact logical relationship between invariance and correctness, stated and demonstrated on committed numbers.
The leaderboard proposal: report the triple (accuracy, consistency per family, coverage), with the committed exhibit that the volume's two systems reverse ranking depending on which column you sort by.

Accuracy is pointwise, entailment is closure

Put the two properties side by side on one theory. Let $T$ be a theory of the academic world, a set of facts and rules like Volume 4's generated corpora, and let $q$ be the question "alice is cited." Under the closed-world reading every prior volume has used, $T$ answers $q$ True exactly when the atom is derivable, and answers the partner question $\lnot q$ , "alice is not cited.", with the complement; the pair is one fact asked twice:

	question	entailment's answer	a label predictor's answer
$q$	"alice is cited."	True (the atom is derivable)	whatever its score says
$\lnot q$	"alice is not cited."	False (the complement, by definition)	whatever its score says, independently

The left column is constrained: the two answers are one decision viewed from two sides, and no computation that derives both from a single closure can ever return (True, True). The right column is unconstrained: a model that maps each question to a label through a learned score is free to answer (True, True), and if the test set happens to contain only one member of the pair, that incoherence costs it nothing. Plain accuracy is a pointwise property: it evaluates each (question, gold) pair in isolation, so its value is a sum of independent indicator terms. Decoded, with $n$ the number of test questions, $\hat{y}_i$ the system's answer to question $i$ , and $y_i$ its gold label, and with $\mathbf{1}[\cdot]$ the indicator that is $1$ when its bracketed condition holds and $0$ otherwise:

\text{acc} \;=\; \frac{1}{n}\sum_{i=1}^{n} \mathbf{1}[\hat{y}_i = y_i].

Entailment is an invariance property: a family of statements of the form "for every theory $T$ , query $q$ , and transformation $\tau$ in some class, the answer to $\tau(q)$ over $\tau(T)$ is determined by the answer to $q$ over $T$ ." The transformation may rewrite the question (negation, paraphrase, De Morgan) or extend the theory (adding an irrelevant sentence); what makes it a closure is the determination. A consistency rate measures how often a system honors one closure: for a family $F$ of $n_F$ probes, each probe a matched set of questions whose answers logic mutually constrains,

\text{cons}_F \;=\; \frac{1}{n_F}\sum_{i=1}^{n_F} \mathbf{1}[\text{the answers to probe } i \text{ respect } F\text{'s closure}],

and the chapter's central quantity is the gap, $\text{gap}_F = \text{acc} - \text{cons}_F$ , the distance between how often the system is right and how often it is even coherent. Note what the definition does not need: no gold label appears in $\text{cons}_F$ at all. Consistency compares the system's answers to each other, under a constraint logic supplies; that is why the probes are cheap, and also the seed of the honest coda below, since a system can satisfy every constraint while being wrong everywhere.

The measurement consequence follows immediately. A test set that samples questions independently almost never contains both members of a linked pair, and even when it does, the scoring never joins them: accuracy sums indicators one question at a time, so an incoherent (True, True) on a contraposition pair scores at least as well as a coherent pair with one error. To see the closure at all, the benchmark must sample families, matched sets generated together and scored together. That is the design the companion implements and mainstream leaderboards omit; the omission is the gap this chapter is named for.

The same two systems under two protocols: independent questions call them a tie at a point apart; logically linked families separate them by 51 points. Original diagram by the authors, created with AI assistance.

Four probe families, generated by logic

The companion entailment_gap.py builds its probe base from Volume 4's committed corpus without retyping a sentence: it re-runs ruletaker_lite.run (re-executing Volume 4's own asserts, so the corpus arrives pre-audited) and keeps the evaluation-split questions of depth ≤ 1, the soft reasoner's trained regime (entailment_gap.py lines 110–117). The restriction is load-bearing: Volume 4 already showed the bag-of-features model failing beyond its trained depth, and this chapter must not be that result rerun. The probes stay where the model is good, 1156 questions at 98.96 percent plain accuracy, so whatever gap appears is a property of the protocol, not of extrapolation. The two systems are Volume 4's pair, wrapped once each: the soft reasoner answers True exactly when its trained weight vector $\mathbf{w}$ gives $\mathbf{w}^\top \mathbf{x} \gt 0$ , the dot product of the weights with the ten local features $\mathbf{x}$ of the (theory, question) pair, and the translate-then-prove pipeline parses each sentence with its strict grammar, repairs a failed question once through its partial lexicon, and answers by membership in the parsed theory's least fixpoint under the closed-world assumption, abstaining with None whenever the grammar defeats it (entailment_gap.py lines 177–189; in the excerpt's comments, CWA abbreviates the closed-world assumption, lfp the least fixpoint, "iff" the phrase "if and only if", and XOR is the exclusive or, true exactly when its two bits differ):

    def answer(self, sentences: list[str], question: str) -> bool | None:
        """Parse (repairing once if the strict grammar objects), then decide
        by closed-world membership; None = abstention on a parse failure."""
        try:
            person, pred, neg = tp.parse_statement(question)
        except tp.ParseError:
            try:
                person, pred, neg = tp.parse_statement(tp.repair(question))
            except tp.ParseError:
                return None
        # CWA: True iff the atom is derivable, complemented for "not":
        #   answer = [ is(person, pred) in lfp ] XOR neg
        return (("is", person, pred) in self.closure(sentences)) ^ neg

Each probe family instantiates one closure, and each is a miniature of a published diagnostic. Contraposition pairs recover both polarities of the same atom from the same theory (Volume 4's bank emits both, so the pairs are grouped, not resampled): the closure under the closed world is that $T$ answers $q$ True exactly when it answers $\lnot q$ False, so the two answers must disagree (entailment_gap.py lines 209–219). This is a question-level transposition of RobustLR's theory-side negation contrasts [1], and the move is this chapter's own adaptation: RobustLR always edits the rulebase and holds the statement under test fixed, and its rule-level contrapositive edits need the classical negation our closed-world corpus does not carry, so the probe here lives at the question level, a stated narrowing.

Irrelevant-expansion probes test monotonicity of the answer under additions that provably change nothing. Here the volume's oldest discipline earns its keep, because the corpus logic is not monotone: negation as failure means an inserted fact can kill a rule whose body says "not c", the antimonotonicity that Difficulty Axes exhibited as its semantics gadget (difficulty_axes.py lines 285–305). So "irrelevant" is never assumed; it is verified against Volume 4's own labeler, in both directions, before a probe is built (entailment_gap.py lines 243–265):

    for person in rt.PEOPLE:
        for c in rt.L0:
            if (person, c) in stated:
                continue
            aug = {"facts": theory["facts"] + [(person, c)],
                   "rules": theory["rules"]}
            # lfp(T + f) = lfp(T) u {f}   (gain exactly the inserted atom)
            if set(rt.label_with_depth(aug)) == ref | {("is", person, c)}:
                found["facts"].append((person, c))

Decode the check: an inserted fact $f$ is certified irrelevant only when the least fixpoint (the code comment's lfp, with u standing for set union) of the extended theory equals the old fixpoint plus exactly the inserted atom, nothing lost (no rule killed) and nothing extra gained (no rule newly fired). A second insertion kind, the distractor rule "if c and not e then h", is certified by the stricter equality $\mathrm{lfp}(T + r) = \mathrm{lfp}(T)$ : the rule never fires at all, though its positive condition may be satisfied for some person, exactly the bait a distractor rule dangles before any reasoner that pattern-matches on rule bodies instead of tracking derivations. The probe then demands invariance over the whole verified neighborhood: the answer to $q$ must survive every certified insertion, the honest reading of a universally quantified closure. Both this family and the next are invariance tests in exactly the sense CheckList made methodological, perturbations under which the output must not move [2].

Paraphrase probes reuse the lexical-variation knob Volume 4 committed: the five street-name synonyms of translate_prove.SYNONYM_CORRUPTION ("productive" to "prolific", "cited" to "referenced", and three more; the pipeline's repair lexicon knows only three of the five). Each base question whose predicate has a variant is paired with its rewritten self, the same atom under a street name, so the gold transfers unchanged and a consistent reasoner answers both alike or abstains honestly (entailment_gap.py lines 280–294). De Morgan probes are seeded two-literal composites: the conjunction $C = A \wedge B$ , where $A$ and $B$ name the two literals ("x is p" and "y is q") and $\wedge$ is the symbol for "and", rendered "x is p and y is q.", is paired with the literal rewrite of its negation by De Morgan's law, $\lnot(A \wedge B) = (\lnot A) \vee (\lnot B)$ with $\vee$ the symbol for "or", rendered "x is not p or y is not q."; the two answers must disagree (entailment_gap.py lines 297–328). Composites force an honest modeling decision, because the soft reasoner has no representation of a connective at all: the companion answers a composite the only way a bag of local features can, by averaging the two literals' feature vectors, $\mathbf{x}_C = (\mathbf{x}_{l_1} + \mathbf{x}_{l_2})/2$ , and thresholding as usual, a declared reading rather than a strawman (entailment_gap.py lines 130–142). The pipeline answers compositionally: prove each literal, combine with the connective's truth function.

Two flags on the generation scheme. First, no probe required a new annotation: the gold for every member of every family comes from the same fixpoint labeler that generated the corpus. Logic is the labeler, the discipline this series has run on since Volume 1 and the one FOLIO institutionalized at field scale by verifying every gold label with a first-order prover [3]. Second, the closed world buys simplicity at a price: DELTA runs this same program under open-world three-way labels, True, False, and Unknown, where consistency has more room to fail [4]; our closed world collapses Unknown, so consistency here is two-way, a stated simplification.

The committed measurement

The experiment measures both systems on every family and guards every claim with an assert (entailment_gap.py lines 335–468). First, the view a leaderboard would publish:

[1] the leaderboard view: plain label accuracy on the probe base
    base: 1156 eval questions of depth <= 1 (the soft reasoner's trained regime)
      system                 plain accuracy
      soft reasoner          0.9896
      translate-then-prove   1.0000
    delta: 1.04 points — a label-only leaderboard calls this a tie

Then the view the probes see, the chapter's spine:

[3] the committed table: consistency per probe family
      family           n     soft cons.   pipeline cons.   pipeline coverage
      contraposition   470     1.0000       1.0000           1.0000
      expansion       1156     0.7163       1.0000           1.0000
      paraphrase       782     0.4859       1.0000           0.7545
      de morgan        289     1.0000       1.0000           1.0000
    expansion sub-rates: facts only 0.9931, distractor rules 0.7197

Read the gaps against the 0.9896 plain accuracy. The module computes $\text{gap}_F$ from the unrounded rates and prints contraposition and De Morgan at $-1.04$ points (consistency above accuracy), expansion at $+27.34$ points, and paraphrase at $+50.37$ points: two families far past the committed 10-point threshold that _check asserts (entailment_gap.py lines 487–488). The same model, on the same theories, at the same depth it was trained on, is coherent on barely half its paraphrase neighborhoods. Nothing about that number is visible in 0.9896.

Which families hurt, and why, is mechanical rather than mysterious; the committed exemplars name the springs (entailment_gap.py demo, section [2]):

    expansion        add 'If someone is published and not cited then they are diligent.'
                     (verified never-firing; its positive half baits one_step, which
                     ignores 'not' — the soft answer to 'dave is diligent.' flips False -> True)
    paraphrase       'alice is cited.' -> 'alice is referenced.'  (soft flips True -> False)

The expansion failure is Volume 4's distractor mechanism made quantitative. The soft reasoner's one_step feature fires when some rule with the queried head has all its positive body atoms stated, ignoring the negated ones (ruletaker_lite.py lines 286–302). The certified never-firing rule "if published and not cited then diligent" leaves the fixpoint untouched, because dave is cited and negation as failure blocks the rule; but dave is published, the positive half matches, one_step flips from 0 to 1, and the score crosses the threshold. The sub-rates isolate the spring: 99.3 percent invariant under fact insertions, 72.0 percent under distractor rules. The paraphrase failure is starker: every evidence feature keyed on the predicate token reads zero, because a street-name predicate like "referenced" appears in no stated fact and heads no rule, so stated, one_step, and head_pred all vanish; what survives the rewrite is the person-keyed fact_frac prior plus the bias and polarity features, and in the committed run the trained weights dominate that residual's swing, so the variant answer is constant per polarity, every positive variant answered False and every negated variant True, whatever the gold; 48.6 percent consistency is what remains. Both failures live on axes Difficulty Axes charted as orthogonal to depth: the probes pinned depth at the model's trained regime, and the incoherence arrived anyway, through distractor sensitivity and vocabulary shift, never through a longer derivation.

The structural contrast: a theorem versus an achievement

The pipeline's column reads 1.0000 four times, and the reading matters as much as the number: it is an asserted property of the run, _check fails if any parsed probe in any family breaks its closure (entailment_gap.py lines 506–509), but it is not an empirical surprise. Every answer the pipeline gives is read off one object, the least fixpoint of the parsed theory, and the closures are theorems about that object. Contraposition holds because answer returns the membership bit XOR the question's negation flag, so $q$ and $\lnot q$ literally read one bit twice with opposite signs. Expansion holds because a certified-irrelevant insertion leaves the fixpoint (minus the inserted atom itself) identical, and identical fixpoints give identical bits. Paraphrase holds on whatever the grammar can place, because repair maps the variant token back to the canonical predicate before the fixpoint is consulted. De Morgan holds because each literal is proved and the connective's truth table applied, and $\lnot(A \wedge B)$ and $(\lnot A) \vee (\lnot B)$ have the same truth table. Even this is not taken on faith: the companion spot-audits the cached closure answers against Volume 1's SLD (Selective Linear Definite-clause resolution) prover on 200 seeded samples, asserting agreement with sld.provable on the compiled ground program every time (entailment_gap.py lines 364–374).

The price is the third column. On paraphrase probes the pipeline's coverage is 0.7545: it abstains on 24.55 percent of the variant questions, exactly those whose street-name predicate falls outside its repair lexicon ("referenced" and "veteran" stay out-of-grammar; the lexicon recovers the other three synonyms). The abstention is honest, None rather than a guess, and Part III's abstention machinery already priced that honesty; but it means the pipeline's perfect consistency is a statement about a smaller world. A system that abstains on half the probes is trivially consistent on the half it answers; coverage is the column that keeps the consistency column honest. The two-systems picture is now complete: statistical consistency is an empirical achievement, present where training put it and absent one distractor away, while symbolic consistency is a theorem, purchased with coverage. Hybrid designs, the business of Part VII starting next door, are attempts to have the theorem without paying the full coverage bill.

Necessary, not sufficient: consistency can be trained in, and can lie

The two families where the soft reasoner posts 1.0000 are not noise, and they are the most instructive rows in the table. Consistency there was trained in, and the mechanism can be derived from the feature set in four lines. Write the ten features of a question about a fixed atom (ruletaker_lite.py lines 286–302) in two groups: the polarity-even evidence, and the polarity-signed copies. Decode the evidence features first: $\text{stated}$ indicates the queried atom is a stated fact, $\text{one\_step}$ is the rule-bait indicator defined above, $\text{head\_pred}$ indicates some rule can derive the queried predicate, and $\text{fact\_frac}$ is the fraction of base predicates stated for the queried person. With $\text{pol} = +1$ for a positive question and $-1$ for a negated one, and $\text{has\_not}$ the 0/1 flag for the word "not", the ten features, in the order the code commits them, are: a constant bias feature fixed at $1$ (its weight is $w_0$ ), the five raw quantities $\text{stated}$ , $\text{one\_step}$ , $\text{has\_not}$ , $\text{head\_pred}$ , $\text{fact\_frac}$ (weights $w_1$ through $w_5$ ), and the four polarity-signed copies $\text{pol}\cdot\text{stated}$ , $\text{pol}\cdot\text{one\_step}$ , the bare flag $\text{pol}$ itself, and $\text{pol}\cdot\text{fact\_frac}$ (weights $w_6$ through $w_9$ ). Because the first feature is the constant $1$ and the ninth is $\text{pol}$ alone, $w_0$ and $w_8$ appear below with no feature symbol beside them. The score $s = \mathbf{w}^\top \mathbf{x}$ decomposes as

s \;=\; \underbrace{w_0 + w_1\,\text{stated} + w_2\,\text{one\_step} + w_4\,\text{head\_pred} + w_5\,\text{fact\_frac}}_{u,\ \text{polarity-even}} \;+\; w_3\,\text{has\_not} \;+\; \text{pol}\cdot \underbrace{\left(w_6\,\text{stated} + w_7\,\text{one\_step} + w_8 + w_9\,\text{fact\_frac}\right)}_{v,\ \text{polarity-odd}}.

For the positive question, $\text{has\_not} = 0$ and $\text{pol} = +1$ , so $s^{+} = u + v$ . For its contrapositive partner, $\text{has\_not} = 1$ and $\text{pol} = -1$ , so $s^{-} = u + w_3 - v$ . Now substitute $a = u + w_3/2$ and $b = v - w_3/2$ and check both directions: $a + b = u + w_3/2 + v - w_3/2 = u + v = s^{+}$ , and $a - b = u + w_3/2 - v + w_3/2 = u + w_3 - v = s^{-}$ . So every contraposition pair's two scores have the exact form

s^{+} = a + b, \qquad s^{-} = a - b,

with $a$ the pair's polarity-even score and $b$ its polarity-odd score. The model answers True when the score is positive, so the pair is consistent (answers disagree) exactly when one of $a+b$ , $a-b$ is positive and the other is not. If $\lvert b\rvert \gt \lvert a\rvert$ , then $b$ dominates and the two expressions take opposite signs: for $b \gt 0$ we get $a + b \geq b - \lvert a\rvert \gt 0$ and $a - b \leq \lvert a\rvert - b \lt 0$ , and symmetrically for $b \lt 0$ . If $\lvert b\rvert \lt \lvert a\rvert$ , both expressions share the sign of $a$ and the pair is answered incoherently. The pair is therefore consistent precisely when its polarity-odd score outweighs its polarity-even score. Volume 4's training bank asked every atom in both polarities with complementary golds, and a polarity-balanced bank punishes exactly the even part: only the signed features can fit complementary labels, so gradient descent loads $w_6$ through $w_9$ until $\lvert b\rvert \gt \lvert a\rvert$ on the training distribution. The committed 1.0000 over 470 pairs says it succeeded on every evaluation pair too.

The De Morgan row now comes free, and it is the chapter's sharpest exhibit. The composite score is linear in the averaged features, so it is the average of the literal scores: $s_C = \mathbf{w}^\top (\mathbf{x}_1^{+} + \mathbf{x}_2^{+})/2 = (s_1^{+} + s_2^{+})/2 = \bar{a} + \bar{b}$ , where $\bar{a}$ and $\bar{b}$ average the two literals' even and odd scores. The rewritten negation is the same two literals with polarity flipped, $s_{C'} = (s_1^{-} + s_2^{-})/2 = \bar{a} - \bar{b}$ . The same condition $\lvert\bar{b}\rvert \gt \lvert\bar{a}\rvert$ delivers the mirror, so the model respects De Morgan's law perfectly, at 1.0000 over 289 pairs, despite having no representation of a connective at all: the rewrite only flips polarity, and polarity antisymmetry was trained in. But watch the accuracy column of the same family: the mean of two literal scores implements neither conjunction nor disjunction. A conjunction with one confidently true literal and one false literal averages positive and answers True while the gold is False. The committed run makes the divergence exact: the soft model's De Morgan pairs mirror at 1.0000 while only 0.6055 of its composite answers are correct; the pipeline scores 1.0000 on both, asserted (entailment_gap.py lines 494–509).

This is the precise logical relationship the chapter owes. Passing an invariance probe is a necessary condition for computing entailment, because every function that reads its answers off a single closure satisfies the closure properties as theorems; a failed probe is therefore a proof, not evidence, that the system is not computing entailment. It is not a sufficient condition: the closures constrain the shape of the answer function, never its ground truth, and the set of closure-respecting functions contains the correct one alongside every consistent impostor. The soft model's De Morgan row is one impostor caught in the act, coherently wrong on 39.45 percent of composites; Reasoning Shortcuts supplied the deeper species, a mis-grounded model that runs genuine deduction over systematically wrong symbols, perfectly consistent by construction and wrong about the world. Two corollaries follow. Because $\text{cons}_F$ references no gold label, it can be optimized directly: a consistency loss over unlabeled probe families enforces the closure without annotation, and the polarity-balanced bank is the committed demonstration that the enforcement works family by family, matching the diagnostic literature's finding that a closure appears only where the training distribution carried data aligned with it, and even then not reliably [1]. And for the same reason, a consistency loss can descend into a consistently wrong basin, so it belongs beside a correctness signal, never in place of one.

The field, read through the gap

Each of the chapter's sources is a partial instance of the same principle, benchmark the invariance and not just the instance, and each covers a different face of it. RobustLR applies logical edits, contrapositives, negations, conjunction rewrites, to deductive rulebases and scores whether models' answers move coherently: the rule-side (theory-edit) closures, instantiated for transformer reasoners, with logic generating the edited gold; what it does not price is abstention, since every system answers everything [1]. CheckList is the methodology in general form: minimum-functionality, invariance, and directional-expectation tests as first-class benchmark citizens beyond accuracy; its breadth is bought by hand-authored expectations, so its catalogs do not compose the way a calculus does, and nothing certifies a template's gold [2]. FOLIO fixes exactly that certification: every gold label in its three-way entailment protocol is checked by a first-order prover against its human-written first-order annotation, soundness by construction up to the human natural-language-to-logic alignment; the scoring, though, remains pointwise, instances rather than linked families [3]. DELTA generates description-logic entailment tasks with open-world three-way labels and controlled compositional splits, the right substrate for family generation, again scored instance by instance [4]. And the ontology world solved its version of this problem two decades ago: LUBM (the Lehigh University Benchmark) grades a knowledge-base system per query on completeness (did it return every entailed answer?) and soundness (was everything it returned entailed?), metrics on the entailment relation itself rather than on sampled labels; what it never needed, because its systems were reasoners by assumption, is a protocol for catching a statistical predictor pretending [5]. The gap this chapter is named for is the composition of those parts that no mainstream leaderboard currently assembles: logic-generated linked families, prover-certified gold, per-family consistency, and coverage, reported together.

The leaderboard proposal

Part VI closes on a concrete export: report the triple (accuracy, consistency per family, coverage). The committed run is the argument that all three columns carry non-redundant information, because the volume's two systems reverse ranking depending on which column you sort by:

sort by	soft reasoner	translate-then-prove	leader
plain accuracy	0.9896	1.0000	a statistical tie, 1.04 points
worst-family consistency	0.4859	1.0000	the pipeline, by 51.41 points
probe coverage (paraphrase)	1.0000	0.7545	the soft reasoner, by 24.55 points

[5] the exhibit: what the leaderboard sees vs what the probes see
      plain-accuracy delta            1.04 points   (indistinguishable)
      worst-family consistency delta 51.41 points   (structural vs statistical)

Both deltas are asserted, plain accuracies within 5 points and worst-family consistencies at least 25 points apart (entailment_gap.py lines 519–522), so the exhibit survives any rerun of the seeded generation. The single-number leaderboard projects this three-column picture onto its least informative axis: sorted by accuracy the two systems are interchangeable, sorted by consistency the pipeline's structural guarantee dominates, sorted by coverage the soft model's answer-everything posture dominates. A practitioner choosing a system for a medical-coding assistant and one choosing for a brainstorming tool should sort by different columns; a leaderboard that pre-sorts by accuracy has silently made that choice for both, and made it wrong for at least one. The extra columns cost no annotation and run in seconds on the volume's corpus; the barrier to adoption is convention, not cost.

The unsolved part

The probe catalog in this chapter belongs to one logic, and the catalog question is open in three directions. First, richer logics need their own catalogs, and they are not translations of this one: contraposition is not even valid for defeasible conditionals ("birds typically fly" does not license "non-fliers are typically non-birds"), so exporting today's contraposition probe to a defeasible reasoner would punish correct behavior. Which closures a probabilistic, defeasible, or paraconsistent reasoner should obey is a semantics question that must be settled before the benchmark question can be posed. Second, consistency under uncertainty is nearly unmeasured. This chapter compared hard labels, but a calibrated system, in the sense of Part III's calibration chapter, owes more: its confidence should be paraphrase-invariant, its probabilities on $q$ and $\lnot q$ should sum to one under the closed world, and an irrelevant insertion should leave its whole posterior untouched. A model can pass every label-level probe while its confidence swings twenty points under a synonym, and no standard protocol catches it. Third, the human question Part VI keeps gesturing at remains an unwritten study: whether users detect inconsistency in deployed systems, how quickly incoherent answers erode trust relative to plainly wrong ones, and whether consistency commands any price in practice. The leaderboard proposal assumes coherence matters to someone; the missing human-computer-interaction experiment would establish how much, and for whom.

Why it matters

This chapter is Part VI's closing principle in executable form: benchmark the invariance, not just the instance. The volume began with trust instruments aimed at single answers, justifications, faithfulness, calibration; the benchmark chapters then showed how aggregate scores blur even those. The entailment gap is the sharpest version of the blur, because it hides a structural difference between systems, computing a relation versus imitating its outputs, behind a 1.04-point accuracy delta. For the reader's own research the export is unusually cheap: any evaluation that already generates data from a formal substrate (after four volumes of logic-as-labeler, yours does) can emit linked families instead of independent instances at no annotation cost, and every such family is a lens plain accuracy cannot replicate. For the series arc, the two-systems picture completed here, consistency as achievement versus consistency as theorem, is the exact tension Part VII now tries to dissolve.

Key terms

Closure property (of entailment): a statement that the answer to a transformed query over a transformed theory is determined by the original answer; contraposition, irrelevant expansion, paraphrase invariance, and De Morgan duality are the four instantiated here.
Pointwise property: a benchmark quantity, like plain accuracy, that is a mean of per-instance indicators and therefore cannot see relations between answers.
Probe family: a matched set of questions generated from one theory whose answers are mutually constrained by logic; the unit of consistency scoring.
Consistency rate: the fraction of a family's probes on which a system's answers respect the family's closure; computable without gold labels.
Gap (of a family): plain accuracy minus the family's consistency rate; the committed run posts gaps of 27.3 and 50.4 points on expansion and paraphrase.
Irrelevant expansion: insertion of a fact or a never-firing distractor rule verified to leave the theory's least fixpoint unchanged (up to the inserted atom itself); the verification is mandatory because negation as failure makes the logic nonmonotonic.
Coverage: the fraction of probes a system answers rather than abstains on; the column that keeps a perfect consistency score honest.
Necessary, not sufficient: failing an invariance probe proves a system does not compute entailment; passing all of them does not prove it does, since consistent impostors, including mis-grounded reasoners, exist.

Where this leads

The two-systems picture ends Part VI with a tension it cannot resolve: the soft model covers everything and guarantees nothing; the pipeline guarantees everything it answers and abstains on the rest. Part VII opens with the architectural bet that the tension is not fundamental. Symbolic Attention builds the SATORI-lite kernel, an attention mechanism whose weights are computed by a symbolic reasoner, so that the closure properties this chapter measured from the outside move inside the model, holding over whatever the neural component learns to cover.

Companion code: examples/frontier/entailment_gap.py generates all four probe families from Volume 4's committed corpus, measures both systems, audits the pipeline's cached closure against the SLD prover, and asserts every number quoted in this chapter; examples/frontier/difficulty_axes.py supplies the antimonotonicity gadget that motivates the irrelevance verification. Run python3 examples/frontier/entailment_gap.py; the run is deterministic and completes in well under a minute.

What this chapter covers​

Accuracy is pointwise, entailment is closure​

Four probe families, generated by logic​

The committed measurement​

The structural contrast: a theorem versus an achievement​

Necessary, not sufficient: consistency can be trained in, and can lie​

The field, read through the gap​

The leaderboard proposal​

The unsolved part​

Why it matters​

Key terms​

Where this leads​