The Honest Verdict: When Integration Pays Off

📍 Where we are: Part VII · The Verdict — Chapter 22. NL Reasoning Benchmarks ended Part VI with a step checker that can tell a right answer from a right proof; this chapter closes the volume by reading every Part's receipts into one ledger.

Volume 4 asked one question seven ways, once per arc of the ledger below (six Parts, seven arcs, because Part II contributes two): what does it cost to make logic differentiable, and when is it worth paying? Part I paid in meaning to buy gradients. Part II refused to pay in meaning, paid in counting instead, and then compiled the count into a circuit so the bill came due only once. Part III industrialized both trades. Part IV asked whether gradients can discover rules, and kept a gradient-free miner on the bench to keep the answer honest. Part V composed one-hop knowledge into fourteen query shapes and found, uncomfortably, that inference sometimes beats training. Part VI moved the whole enterprise into English and watched correctness either factorize or dissolve. This chapter is the settlement. It does not crown a winner, because the volume's evidence does not contain one. It states what each combination buys, what it costs, and which committed check guards the claim, and then it lists, without flinching, the debts the volume leaves unpaid.

The simple version

Imagine the final walkthrough at the end of a long renovation. The contractor does not announce that "the plumbing won." Instead the two of you walk the house with a folder of receipts: this wall cost that much and is load-bearing, this shortcut saved a week and will need attention in five years, this inspection was signed by an independent engineer, not by the crew that poured the slab. Three kinds of lines appear in the folder: things bought, prices paid, and certificates that prove each claim. And on the last page there is a fourth section, the punch list: items everyone agrees are unfinished, which becomes the plan for next year. This chapter is that walkthrough. The receipts are runnable programs, the certificates are assert statements, and the punch list is Volume 5.

What this chapter covers

• The form of the verdict: a ledger of buys, costs, and guards rather than a ranking, every cell a named check in validate.py, with the committed 21/21 summary line quoted as proof.
• The exactness axis, settled: truth-functional fuzzy semantics against the distribution semantics, each restated with the volume's own committed numbers, and the circuit resolution that relocates the exponential cost to compile time with the gradient riding along.
• The supervision inversion: logic as a labeling function, the volume's deepest payoff, stated abstractly with the DeepProbLog and semantic-loss receipts.
• The baseline discipline: three receipts showing a symbolic control on both sides of every comparison, and what that discipline costs.
• The training-free surprise: inference-time composition rivaling trained end-to-end reasoning, read carefully with its limits attached.
• The failure-mode taxonomy: silent-wrong, loud-wrong, and impossible-by-construction, each with its committed exhibit and its deployment reading.
• The oracle discipline: why the suite's hand gradients answer to torch.autograd, and why independent oracles matter more as the machinery gets cleverer.
• The unpaid column: uncalibrated confidences, right-for-wrong-reason, and unbounded approximation dials, handed to Volume 5 as its opening agenda.

The form of the verdict: buys, costs, guards

The surveys that map this field organize it along dimensions, not podiums: which semantics carries the uncertainty, where inference happens, what gets learned [1]. Volume 4's verdict adopts the same shape, because a ranking would answer a question nobody should ask. "Is fuzzy logic better than probabilistic logic?" has no answer; "what does each buy, what does each cost, and what evidence guards the claim?" has twenty-one. The mature reading of the field is a design space in which semantics, inference strategy, and learning target are chosen per problem, with exchange rates between them [2]. The table below is this volume's instantiation, one row per arc, every cell a committed number from its own chapter.

arc	buys	pays	the committed guard
fuzzy semantics (Part I)	gradients everywhere; compositional truth	meaning: one chain, three defensible confidences (0.80 / 0.72 / 0.70)	t-norm (triangular norm) axioms exact on the grid; t-norm gradients vs finite differences ≤ 1.4e-10 (the max across the four operators)
distribution semantics (Part II)	exactness; probabilities that stay probabilities	counting is #P (sharp-P, the counting analogue of NP, nondeterministic polynomial time); the wall is 2^20 = 1,048,576 assignments at 20 facts	naive proof-sum 1.5750 vs exact 0.8865; weighted model counting (WMC) = enumeration to 0 error
circuits + gradient semiring (Part II)	pay once, evaluate forever, gradient included	compilation cost; circuit size unbounded in the worst case	running-example circuits = brute force to 1.1e-16; 238 ops vs 1,048,576 assignments on the 20-fact wall, exact; semiring vs finite differences 2.7e-13
differentiable frameworks (Part III)	the trade industrialized: loss-level, program-level, axiom-level, hardware-level	approximation dials; satisfaction without guarantees	violations 20 → 6; top-k ladder (keep only the k most probable proofs) 0.7650 → 0.9344 = exact; SatAgg (satisfaction aggregation) 0.5295 → 0.9933; vectorized = loop to 0.0
differentiable rule learning (Part IV)	rules you can read back from weights	gradient machinery a gradient-free miner matches	attention decodes advises∘advises (∘ is relation composition: follow one advises edge, then another) at 0.9990; mined confidence equals the hand count 2/3 exactly
complex query answering (Part V)	fourteen query shapes from one 1-hop predictor	quadratic memory; calibration fragility; trees only for exactness	on the five shared query types, QTO (Query Computation Tree Optimization) and CQD-beam (Continuous Query Decomposition with beam search) post mean reciprocal rank (MRR) 0.5500/0.5500/1.0000/1.0000/1.0000 against 0.6667/0.2381/1.0000/0.4167/1.0000 for the trained GQE (Graph Query Embedding); zero-shot transfer MRR 0.8333
natural-language (NL) reasoning (Part VI)	logic read from and returned to English	either silent failure or reduced coverage	prover 100% beside the soft reasoner's 0.500 at depths 2–3; accuracy on parsed inputs exactly 1.0000

The meta-claim of the whole volume is the last column. Every load-bearing number in this table, and every number re-quoted in the sections below, is produced by the deterministic run of a named competency check in the companion's acceptance harness, whose asserts guard the qualitative claim in each cell. The harness is twenty lines of loop; the ledger is the list of claims it iterates over (validate.py lines 40–103, one yield per chapter), and the exit code is the verdict (validate.py lines 110–125):

    for claim, check in _checks():
        try:
            if verbose:
                check()
            else:
                with contextlib.redirect_stdout(io.StringIO()):
                    check()
            print(f"PASS  {claim}")
            passed += 1
        except AssertionError as exc:
            print(f"FAIL  {claim}  ({exc})")
            failed += 1
    total = passed + failed
    print(f"\nintegration companion: {passed}/{total} competency checks "
          f"passed  ({time.time() - t0:.0f}s)")
    return 0 if failed == 0 else 1

Each check calls one module's run(), which re-executes that chapter's entire experiment deterministically, including its own assert statements; a check passes only if the module's whole evidence chain holds. The committed run ends:

integration companion: 21/21 competency checks passed  (19s)

That line is the sense in which this verdict is honest: it is the output of a program that re-executes every experiment these sentences describe and exits 1 if any module's evidence chain breaks; the exact decimals quoted in the ledger are the committed, seeded output of those runs.

The verdict as a ledger: seven arcs, each with what it buys, what it pays, and the committed check that guards the claim, standing on the 21/21 harness line, with the unpaid column flowing forward into Volume 5. Original diagram by the authors, created with AI assistance.

The exactness axis, settled with the volume's own numbers

The volume's deepest fault line runs between Part I and Part II, and both sides of it are now measured. Truth-functional fuzzy semantics buys compositionality and gradients: the truth of a formula is a fixed function of the truths of its parts, so any formula compiles to a differentiable expression. The price is meaning. The academic world's two-step citation chain, with edge confidences 0.9 and 0.8, comes out as three different numbers depending on an operator choice the logic cannot adjudicate: Gödel's minimum says 0.80, the product t-norm 0.72, Łukasiewicz 0.70 (tnorms.py, the committed chain table). All three satisfy the t-norm axioms exactly; none is "the" confidence of the conclusion. And the same choice reappears inside the gradients as a pathology menu: at 50 conjuncts the Gödel gradient is 0.980 sparse (one input in fifty learns per step) and the product gradient, with every conjunct at truth 0.9, has shrunk to $0.9^{49} \approx 0.00573$, while at just 8 conjuncts Łukasiewicz sits in a dead zone covering 0.99997 of its input volume, where every gradient is exactly zero [3]. The fuzzy side of the ledger, in one sentence: every formula is differentiable, and what the number means is a modeling decision with three defensible answers and three failure modes.

The distribution semantics refuses the operator choice by refusing truth-functionality. Probability attaches to whole worlds, and a query's probability is the total weight of the worlds where it holds. Decoded: $\mathcal{F}$ is the set of probabilistic facts, a world is a subset $F \subseteq \mathcal{F}$ of facts chosen true, each world's probability is a product over independent choices, and

$$P(q) \;=\; \sum_{F \subseteq \mathcal{F},\; F \,\models\, q} \;\prod_{f \in F} p_f \prod_{f \notin F} (1 - p_f),$$

where $F \models q$ reads "world $F$ makes the query $q$ true" and $p_f$ is the probability attached to the individual fact $f$. Nothing here is a design dial; the number is exact and it is a probability by construction. The volume's exhibit for why this matters is the disjoint-sum failure: the existential grandAdvisor query has two ground proofs that share the coin advises(alice, bob), and summing their probabilities as if they were exclusive gives 0.81 + 0.765 = 1.5750, which is not a probability at all, while inclusion-exclusion over the two proofs' shared coin gives the exact 0.8865, confirmed by enumerating all 2,048 worlds (distsem.py, the committed run). The price is printed next to it: exact inference is #P-hard (sharp-P, the counting analogue of NP), and the companion's brute-force wall is concrete, $2^{20} = 1{,}048{,}576$ assignments to enumerate at just twenty facts (wmc.py).

The circuit chapters are the resolution, and their two committed agreements are the receipts. Knowledge compilation pays the exponential cost once, at compile time, producing per query a d-DNNF (deterministic decomposable negation normal form) circuit that answers every later evaluation of that query, under any reweighting of the facts, by one upward pass of sums and products. The committed receipts come in two sizes: on the running example's four queries, circuits of at most 10 operations reproduce the brute-force enumeration to 1.1e-16, and on the twenty-fact wall instance from wmc.py's chain family, 238 circuit operations replace the 1,048,576-assignment enumeration and match the closed form $1 - 0.44^{k}$ exactly, to 0.0e+00, where 0.44 is one chain's failure probability, $1 - 0.8 \cdot 0.7$, and $k = 10$ counts the independent two-coin chains that make up the twenty facts (circuit.py). And once the circuit exists, the gradient is free. Replace the numbers flowing through it by pairs carrying a value and its derivative, with multiplication (the ⊗ below) defined by the product rule and addition (the ⊕ below) acting componentwise,

$$(a, \nabla a) \otimes (b, \nabla b) \;=\; \big(ab,\; a\,\nabla b + b\,\nabla a\big), \qquad (a, \nabla a) \oplus (b, \nabla b) \;=\; (a + b,\; \nabla a + \nabla b),$$

and the same single pass returns $P(q)$ together with $\partial P / \partial p_f$, the sensitivity of the query probability to each individual fact's probability, for every fact at once: the gradient semiring. The committed cross-check agrees with central finite differences to 2.7e-13 (deepproblog_mini.py). So the exactness axis settles into a slogan the rest of the ledger keeps reusing: fuzzy buys gradients and pays in meaning; probabilistic buys meaning and pays in counting; circuits do not remove the counting cost, they relocate it to a place you pay once, and the gradient rides along for free.

The supervision inversion: logic as a labeling function

If the volume has one payoff deeper than the exactness settlement, it is a pattern that appeared twice in consecutive chapters, at the seam between Parts II and III, wearing different clothes. State it abstractly first. A neural network predicts latent variables $z$ (unobserved quantities, here the topic of each document or the class bit of each point); a logical theory $T$ connects those latents to something observable $y$; and the training signal is supervision on $y$ alone, pushed backward through $T$'s exact inference to reach $z$. The logic is acting as a labeling function: it converts cheap supervision on the observable into effective supervision on the latent, and the gradient semiring is what makes the conversion differentiable.

The first receipt is DeepProbLog. The committed experiment never labels a single document's topic. It labels only document pairs as relevant or irrelevant, and the program clause "two documents are relevant if they share a topic" connects the pair label to the latent topics. Cross-entropy on $P(\text{relevant})$, differentiated through the compiled circuits by the semiring, trains the topic classifier to hidden-topic accuracy 1.00, measured up to the label permutation that pair supervision provably cannot pin down, with final loss 0.000287 (deepproblog_mini.py, the committed trace). The second receipt is semantic loss, where the logic connects the network's own output bits to each other rather than to a latent: the exactly-one constraint, compiled to the loss $-\log \mathrm{WMC}(\alpha; p)$ (the negative log of the weighted model count, with $\alpha$ the constraint formula and $p$ the network's output probabilities), which three plain axioms (with the source's regularity conditions; syntax independence follows as a derived guarantee) make unique up to a constant, turns 180 unlabeled points into signal. The committed semi-supervised run cuts constraint violations from 20 to 6 while test accuracy rises from 0.8778 to 0.9000 and the satisfaction probability climbs from 0.877 to 0.954 (semantic_loss.py).

Name the inversion, because it inverts the usual economics of supervised learning: ordinarily structure is the expensive thing and labels are the fuel; here the structure replaces labels. The applicability condition is visible in both receipts. There must exist a program or constraint connecting what you can observe to what you want learned, and inference through it must be tractable enough to differentiate (exactly what Part II's circuits bought). Where no such program exists, where the relation between observable and latent is itself the unknown, the pattern has nothing to compile, and you are back to paying for labels. That boundary, not any benchmark number, is the honest statement of when this class of integration pays off.

The baseline discipline: both sides of every comparison

Volume 2's verdict contributed ground truth: a reasoner whose answers are provably correct. Volume 3's verdict contributed protocol: filtered ranking, fixed splits, seeded runs. Volume 4's contribution is to insist on both sides of every comparison: each differentiable system in this volume was scored beside a symbolic control built to the same standard, and three receipts show what that discipline catches.

First, rule learning. Neural-LP and DRUM concentrate attention on the composition advises∘advises at confidence 0.9990, and the Neural Theorem Prover (NTP) decodes the same rule from soft proof scores with a held-out margin of 0.7678. Beside them stands AnyBURL-lite, a gradient-free path sampler that finds the same gold rule with a mined confidence equal to the hand count $2/(2+1) = 2/3$ exactly, and whose ranking of the held-out edges reaches MRR 0.6944 against a random baseline's 0.21 (rule_mining.py); at benchmark scale, the published record that chapter cites reports the same sampler family competitive with the neural state of the art. The differentiable machinery finds real rules; the honest baseline says a counter finds them too, so any claim for the gradients must rest on what the counter cannot do (train perception jointly, share parameters across relations), not on the toy scoreboard. Second, query answering: every model in Part V was scored against the 14-type symbolic executor, De Morgan-consistent on all 36 queries with oracle MRR 1.0000 on the full graph; without it, "hard answers" and "easy answers" would not even be well-defined categories. Third, natural-language reasoning: the soft reasoner's per-depth accuracies 1.000/0.966/0.500/0.500 are printed beside the prover's 100% column, which is what turns "the model does well" into "the model does well exactly where it was trained and collapses to a coin flip one hop beyond."

The principle costs something: someone must build the symbolic control. The executor, the prover, the miner, and the enumerator are a substantial fraction of the companion suite, none of it differentiable, all of it necessary. A field that skips this expense does not save it; it converts measurable claims into unmeasurable ones.

The training-free surprise, read carefully

Part V produced the volume's most uncomfortable number, and it has to be read under the protocol the volume itself installed. The trained query-embedding line, GQE, Query2Box, and BetaE, learns geometry per query structure and posts pooled MRR 0.6085, 0.5794, and 0.4197, but each pool spans only the types its geometry can express (7 for GQE, 9 for Query2Box, 14 for BetaE), and the committed table prints its own caveat beside those numbers: the pools are comparable per row, never across the pooled line (clqa_models.py). The training-free line, CQD-beam and QTO, deletes all query-level training, keeps only Volume 3's calibrated 1-hop predictor, and composes it with fuzzy connectives at inference time, pooling MRR 0.8000 for both on its 5-type bank against a graph-traversal floor of 0.1465 (cqd.py). The protocol-clean comparison is row by row on the five types the two banks share: QTO and CQD-beam post 0.5500/0.5500/1.0000/1.0000/1.0000 on 1p/2p/2i/pi/ip (one projection hop, a two-hop chain, a two-way intersection, projection then intersection, intersection then projection) against GQE's 0.6667/0.2381/1.0000/0.4167/1.0000, so the training-free line wins or ties every shared row except the single-hop 1p, which is precisely the row where composition cannot help. QTO's dynamic program is exact on tree-shaped queries, never misses an easy answer (all 15 training edges pinned to 1), and returns a checkable proof whose three atoms multiply to the answer's score to the last digit. One step further, ULTRA-lite shows the 1-hop predictor itself can be vocabulary-free: a 12-parameter structural scorer transfers zero-shot to the hospital world at MRR 0.8333 against random 0.2198, with scores provably unchanged under relation renaming (invariance 0.0, ultra_lite.py). The training-free and foundation-model chapters' reference lists cite the field-scale evaluations reporting the same ordering on the standard benchmarks; our toy numbers are the auditable miniature of a finding the field has already logged at scale.

Read the finding at the right strength. It does not say training is useless; the 1-hop predictor underneath QTO is trained, and its calibration is fitted. It says the query-level network, the part GQE and its successors spend their parameters on, was buying less than its price on these tasks, because composition is something inference can do exactly. The investment advice that follows: put the budget into the 1-hop predictor and its calibration, and let logic do the composing. Then read the limits, which are also committed. The composition is only as sound as the calibration underneath it (one badly calibrated row is enough to reorder answers); QTO's exactness costs a dense entity-by-entity matrix per relation, quadratic memory that survives at scale only through sparsification; and the exact dynamic program requires tree-shaped queries, so genuinely DAG (directed acyclic graph)-shaped structure falls back to approximation. Training-free is honest only with its qualifier attached: training-free at the query level, on trees, over a substrate someone calibrated.

The failure-mode taxonomy: how each combination breaks

A practitioner choosing among these systems is mostly choosing a failure mode, so the ledger's most useful cut is not by accuracy but by how wrongness presents. Three modes cover the volume, and each has a committed exhibit.

failure mode	committed exhibit	deployment reading
silent-wrong: answers always, errs invisibly	the soft reasoner holds 1.000/0.966 at trained depths and answers 0.500 at depths 2–3 with nothing in the output marking the collapse (ruletaker_lite.py); the greedy step reasoner posts label accuracy 0.817 while only 0.167 of its proofs check (bench_lite.py)	needs an external monitor; accuracy claims are only as good as the distribution they were measured on
loud-wrong: fails by refusing	translate-then-prove abstains on parse failure; repair lifts coverage 0.8080 → 0.9293, accuracy on parsed inputs is exactly 1.0000, and the committed run verifies that abstentions never turn into errors (translate_prove.py)	errors are visible and countable; the cost dial is coverage, and the error dial stays at zero
impossible-by-construction: the bad output has no encoding	QTO pins all 15 training edges to 1, so missing an easy answer is structurally excluded, and the committed check confirms it never does (cqd.py); the constraint layer that renormalizes mass onto satisfying states, so a violating prediction cannot be emitted, is the Semantic Loss chapter's cited construction, not committed code (the committed run trains with the loss and still emits 6 violations)	the guarantee is architectural, holding for every input, but only for the properties the construction encodes

The taxonomy extracts a design rule the volume earned line by line: prefer architectures whose failures are load-bearing walls, not soft carpets. A wall (an abstention, a constraint layer, a pinned edge) fails by stopping you, which is information; a carpet (a fluent wrong answer, a miscalibrated score) fails by letting you keep walking. The division of labor the field is converging toward, perception neural, composition symbolic wherever it can be afforded, is attractive precisely because it moves failure from carpet to wall: the symbolic layer's failures are parse errors and unsatisfiable constraints, which announce themselves [4].

The oracle discipline: hand gradients answer to autograd

One more receipt guards everything the others rest on. Every gradient in the companion suite is written by hand, and nearly every module that takes one checks it against central finite differences; the two exceptions, ntp_mini.py's projected subgradient descent and ruletaker_lite.py's full-batch logistic regression, are guarded by their competency outcomes rather than by a finite-difference certificate. But that check leaves one rival hypothesis standing, and the suite's cross-checker names it in its own docstring: the formula and its checker were written by the same hand, against the same reading of the function (torch_check.py lines 9–12). The remedy is an independent implementation. torch_check.py rebuilds each function from float64 leaf tensors in PyTorch, calls .backward(), and demands agreement to 1e-6 in maximum absolute difference across three derivative pipelines: the gradient semiring, the semantic loss, and softmin (torch_check.py lines 247–252):

    assert sr["max_diff"] < TOL, \
        f"gradient semiring disagrees with autograd: {sr['max_diff']:.3e}"
    assert slc["max_diff"] < TOL, \
        f"semantic-loss gradient disagrees with autograd: {slc['max_diff']:.3e}"
    assert sm["max_diff"] < TOL, \
        f"softmin gradient disagrees with autograd: {sm['max_diff']:.3e}"

The committed run's three verdict lines and its closing summary, under a torch-equipped interpreter (each verdict line closes its own check section; the final two lines are the run's literal tail):

   PASS semiring (max |Δ| = 0.0e+00)
   PASS semantic_loss (max |Δ| = 4.4e-16, loss |Δ| = 0.0e+00)
   PASS softmin (max |Δ| = 1.3e-15)

AGREEMENT CONFIRMED: manual gradients match torch.autograd
SUMMARY torch_check: semiring=0.0e+00 semantic_loss=4.4e-16 softmin=1.3e-15 checks=3/3 tol=1e-06

The observed disagreements are pure floating-point rounding, roughly nine orders of magnitude below the tolerance. Why belabor this in a verdict chapter? Because the need for an independent oracle grows with the cleverness of the machinery. A sign error in a plain cross-entropy gradient makes the loss climb and gets caught in minutes; a sign error inside a semiring accumulator or a dynamic-programming pass produces a gradient that is merely biased, and stochastic optimizers absorb bias: the loss still falls, the accuracy still rises, and the error ships. Training curves cannot certify gradients; only recomputation by an independent route can. This is the same epistemic move as Volume 2's HermiT oracle and Volume 3's autograd check, applied one level up: as inference gets more structured, verification must get more independent.

The unsolved part

The honest column of the ledger is the one with no green check marks, and it has four entries. First, calibration. The volume manufactured four different kinds of confidence, and not one is a probability of being correct: fuzzy degrees (three defensible values for one chain), soft proof scores (the NTP's 0.9032 is the minimum of a proof's unification kernels, the soft symbol-similarity scores its unifier assigns to each matching step, not a likelihood), rule confidences (a closed-world corpus statistic), and query scores (calibrated against the training graph, not against truth). Systems downstream will treat these numbers as trust; nothing in this volume licenses that. Second, right-for-wrong-reason, which appeared three times and now needs a name and a theory: the DeepProbLog chapter's caveat that query-level supervision constrains latent predicates only up to symmetries the program cannot see; the greedy reasoner's measured rate, right answer with a wrong proof 0.650 of the time (bench_lite.py); and the extraction-fidelity gap in rule learning, where the rank-1 decomposition recovers neither gold rule (it spreads attention 0.250 across all four two-hop compositions) and answers 0 of 4 evaluation queries with an exactly correct answer set, while its rank-2 sibling decodes both rules at 0.999 and answers 4 of 4 exactly (neural_lp.py), a reminder that the rule you read back is a hypothesis about the weights, not a property of them. The theory exists: these are reasoning shortcuts, latent concepts that satisfy the training signal while meaning the wrong thing, with formal identifiability conditions and mitigations [5]; Volume 5 opens there. Third, scale. Where this volume went fast, it went fast by an approximation dial whose error is unbounded in general (top-k proofs converged once k covered all six proofs of our world, the committed k = 8 dial keeping all 6 and matching the exact value to 0.0, but no theorem says how large k must be on yours) or by hardware layout, which changes the constant, never the complexity class. Whether exactness-grade trust survives real scale is unresolved. Fourth, containing the other three, trust: every guarantee here is about mechanism (this gradient is exact, this dynamic program is optimal, this abstention is sound), and none is yet about deployment, where inputs drift, calibration decays, and the person reading the score did not read the caveats.

Why it matters

The verdict's content is a division of labor with exchange rates. The division: perception and ranking stay with the neural pillar, composition and guarantees with the symbolic one, and this volume's machinery, semirings, circuits, relaxations, executors, is the customs house between them where every crossing pays a stated price. The exchange rates: gradients for meaning, exactness for counting, coverage for error, memory for optimality, each measured on the same small world so the prices are comparable. This is the operational answer to the question Volume 1 opened with, whether the two pillars can be one system: yes, at these prices, with these guards. And the unpaid column is not a footnote; it is the research frontier by definition, since everything with a check mark is, in this volume's precise sense, already solved. Calibration, faithfulness, reasoning shortcuts, and trust at scale are where the checks run out: exactly the questions a system must answer before anyone is entitled to rely on it.

Key terms

• The ledger: this volume's verdict form: for each neural-symbolic combination, what it buys, what it pays, and the committed check that guards the claim; the acceptance harness's 21/21 line is its certificate.
• Exactness axis: the fault line between truth-functional fuzzy semantics (compositional, differentiable, meaning-ambiguous) and the distribution semantics (exact, calibrated by construction, #P to compute).
• Knowledge compilation: paying inference's exponential cost once, at compile time, to obtain per query a circuit that answers every later evaluation of that query, under any reweighting of the facts, in one linear pass; on the twenty-fact wall instance, 238 operations standing in for 1,048,576 assignments.
• Gradient semiring: the value-and-derivative pairs $(a, \nabla a)$ whose product rule turns one circuit evaluation into the query probability and its full gradient simultaneously.
• Supervision inversion (logic as a labeling function): training latents from observables through a theory that connects them; DeepProbLog's pair labels and semantic loss's unlabeled points are the volume's two receipts.
• Baseline discipline: a symbolic control on both sides of every comparison: the executor for queries, the prover for entailment, the miner for rules, the enumerator for probabilities.
• Silent-wrong / loud-wrong / impossible-by-construction: the failure-mode taxonomy: fluent errors, visible abstentions, and outputs the architecture cannot emit.
• Oracle discipline: verifying hand-derived machinery by an independent implementation (finite differences, then torch.autograd), because training curves absorb the very errors that matter.
• Reasoning shortcut: a latent concept that satisfies the training signal while meaning the wrong thing; the named theory behind the volume's three right-for-wrong-reason sightings, and Volume 5's opening topic.

Where this leads

The unpaid column is a table of contents. Volume 5 — The Reasoning Frontier takes each debt in order: calibration (when is a confidence a probability of being right), faithfulness (when is a produced proof the reason for the answer), reasoning shortcuts (when does distant supervision identify the concepts it was supposed to), and trust at scale (what survives when the approximation dials are set by budget rather than by theorem). The instruments this volume built, the executors, the provers, the checkers, the harness, travel forward with it: the frontier is not a new method but a new standard of evidence, and the ledger you have just read is its first exhibit.

---

Companion code: examples/integration/validate.py is the acceptance harness this chapter quotes: one named competency check per chapter (lines 40–103), the pass/fail loop and the summary line (lines 106–125), exit code 0 only if every check passes. examples/integration/torch_check.py is the optional autograd oracle (three pipelines, tolerance 1e-6, lines 230–258). Run python3 examples/integration/validate.py to re-execute every experiment in the volume; the committed run ends integration companion: 21/21 competency checks passed (19s).