The Seven Difficulty Axes Beyond Completeness
📍 Where we are: Part VI · Benchmarks and Evaluation — Chapter 15. Reinforcement Learning and Verifier-Gated Reasoning closed Part V by putting a checker between a sampled chain and its reward; Part VI opens by turning the same scrutiny on ourselves and asking what the scores we report actually measure.
Every leaderboard in the reasoning literature reports, at bottom, one number: the fraction of questions a system answered correctly. This chapter argues that the number is not wrong but underdetermined. Accuracy over a question bank is a weighted average over that bank's hidden difficulty composition, and two systems with opposite failure modes can tie, or swap ranks, purely because of how the bank was mixed. The repair is the oldest idea in experimental science, imported into benchmarking: identify the independent knobs that make an instance hard, build a generator where each knob turns on its own, and measure systems one factor at a time, so that when performance falls you can say which knob pulled it down. The companion module difficulty_axes.py names seven such knobs beyond the one everybody already measures (completeness, recall along a derivation), and demonstrates each with a gadget in which the completeness axis is deliberately pinned while the gadget's own failure still occurs and is counted.
Imagine rating two hikers by their average time over "a hike." Hikes differ in length, steepness, altitude, and how well the trail is marked. One hiker is strong but hopeless when the markings vanish; the other navigates flawlessly but tires on long climbs. If your sample of hikes happens to be short and well marked, the first hiker looks better; make the hikes long and wild and the ranking flips. The single average told you about your sample of hikes, not about the hikers. The fix is what any coach would do: time them separately on a steep hill, a long flat, an unmarked forest, changing one thing at a time. This chapter does exactly that for reasoning systems, with derivation depth playing the hill, and six further kinds of terrain the field rarely times at all.
What this chapter covers
- The confound, made exact: aggregate accuracy is a weighted average of per-stratum accuracies, weighted by the bank's hidden difficulty mix; with the companion's real numbers we derive the mixture that makes two opposite systems tie exactly, so "who is better" becomes a property of the bank, not the systems.
- The controlled generator: how
ruletaker_lite.pypins derivation depth by construction (a layered vocabulary), balances labels per depth, and seeds every random choice, so that one knob turns while everything else holds still. - Two systems, two failure geometries: the committed per-depth table in which a statistical reasoner degrades along depth while a translate-then-prove pipeline stays depth-flat on what it parses and pays instead in coverage when the surface vocabulary drifts.
- Seven axes beyond completeness: soundness, termination, proof width, query joins, semantics change, grounding trust, and engineering scale, each decoded mechanically, each with its lineage in the field's controlled benchmark designs, each demonstrated by a committed gadget with the completeness axis pinned.
- Interactions and the factorial price: what one-factor-at-a-time misses, the interaction the committed instruments already exhibit, and the arithmetic of why nobody runs the full seven-way grid.
- The axes as diagnosis: mapping each axis to its mitigation elsewhere in this series, so a degradation profile becomes a repair menu rather than a scoreboard.
A score is one sample from an unknown mixture
Fix an evaluation bank of questions, where is the bank size, and suppose each question carries a hidden difficulty coordinate; for now let it be the derivation depth , the number of rule applications a proof of the answer needs. Write for the number of questions at depth , for the number of those a given system answers correctly, and define the per-depth accuracy . Aggregate accuracy is the total correct over the total asked, and splitting the sums by depth turns it into a weighted average:
where (the Greek letter pi with a subscript, not the circle constant) is the mixture weight: the fraction of the bank that sits at depth . The algebra is trivial; its consequence is not. The vector is a property of the system. The vector is a property of whoever built the bank. The reported score entangles the two, and no reader of alone can untangle them. A model can buy competence at depth 2 by learning to ignore irrelevant facts, and look identical in to a model that does the reverse; the aggregate is one sample from a distribution over possible banks that nobody wrote down.
The companion makes this concrete with committed numbers. Volume 4's two instruments, run unchanged, score two very different systems on the same 1,500 evaluation questions, and their per-depth accuracies are, with the soft reasoner's profile called and the pipeline's called (both quoted from the committed tables we requote below):
for depths through . The committed bank mixes depths as , so , and the two aggregates come out and : the pipeline wins by five points. Now ask when a bank would make them tie. Restrict the mixture to depths 0 and 1, so , and set the aggregates equal:
Collect the terms on one side:
Substituting the exact committed fractions, and , gives
A bank drawn 31.7% at depth 0 and 68.3% at depth 1 scores both systems at exactly . A bank of pure depth-0 questions ranks the soft reasoner first ( against ); a depth-2-heavy bank ranks the pipeline first by 33 points ( against ). The sign of the comparison is a free parameter of the bank's composition. This is the sense in which a benchmark score without a difficulty model is a single sample from an unknown distribution: it is an inner product (the superscript is the transpose, laying the weight column on its side so that the row-times-column product is again the sum ) in which the evaluator silently chose .
The repair frame comes from experimental design. An aggregate over an uncontrolled bank is an observational score: many difficulty factors vary at once, so degradation cannot be attributed to any one of them. A one-factor-at-a-time design holds every factor at a baseline and turns a single knob, so a drop in accuracy names its cause. The landmark controlled repair in this style, the line this chapter generalizes, is the depth-stratified rulebase design: generate synthetic theories, label every question with the minimum depth of its proof, balance the labels inside each stratum so no class prior leaks, and report accuracy per depth rather than in aggregate [1]. Everything in this chapter generalizes that move.
The instrument: a generator where depth is pinned by construction
To turn one knob you need a generator in which the knob exists mechanically, not statistically. Volume 4's Soft Reasoners chapter built one, and Part VI now reads it as a piece of experimental apparatus. The module examples/integration/ruletaker_lite.py samples theories in controlled English over a layered predicate vocabulary (lines 92–98): four stated layer-0 predicates, then heads at layers 1, 2, 3. The rule sampler is the depth knob itself (ruletaker_lite.py, lines 125–136):
def _sample_rule(head: str, rng: np.random.Generator) -> tuple:
"""One rule for ``head``: a positive literal from the layer directly
below (this pins derivation depth to the layer index) plus, with
probability 1/2, one extra layer-0 literal, negated with probability
1/2 — the negation-as-failure ingredient."""
below = [p for p in PREDICATES if LAYER[p] == LAYER[head] - 1]
body = [(False, below[int(rng.integers(len(below)))])]
if rng.random() < 0.5:
extra = L0[int(rng.integers(len(L0)))]
if extra != body[0][1]:
body.append((bool(rng.random() < 0.5), extra))
return (head, body)
Because every rule head at layer draws its positive body literal from layer , an atom's minimum derivation depth is its layer index: the depth label is assigned by construction and then independently confirmed, since the labeler iterates Volume 1's one-round consequence operator and reads depth off the round of first appearance (label_with_depth, lines 182–200), with every positive label re-decided by the backward chainer (lines 391–398). Two balance disciplines complete the instrument. First, every derivable atom is paired with a seeded underivable atom from the same layer, and both are asked positively and negated (lines 225–247), which forces every depth stratum to exactly 50/50 True/False and makes the word "not" carry zero information about the label (asserted at lines 379–386). Second, all randomness flows from a single seed, so two runs print byte-identical output. The committed balance check:
[3] eval-question balance (per depth: True/False, asserted exactly 50/50)
depth 0: 402 True / 402 False
depth 1: 176 True / 176 False
depth 2: 140 True / 140 False
depth 3: 32 True / 32 False
This is the lineage of the balanced, depth-stratified question bank [1], and the natural next step is factorial: turn a second knob against the first and fill a grid. The description-logic line did exactly that, generating reasoning problems over a two-factor grid of derivation depth against linguistic complexity, with held-out grid levels to test generalization beyond the training cells [2]. The companion's second knob is of that second kind: a surface knob, turned by translate_prove.py.
Two systems, two failure geometries
The second instrument, Volume 4's Translate-Then-Prove pipeline (examples/integration/translate_prove.py), consumes the same committed evaluation split and adds the lexical variation knob: every eval question whose predicate has an entry in a five-word synonym table is rewritten through it with seeded probability , and the pipeline's strict grammar knows none of the rewrites (lines 112–118):
SYNONYM_CORRUPTION: dict[str, str] = {
"productive": "prolific",
"funded": "sponsored",
"published": "printed",
"cited": "referenced", # not in REPAIR_LEXICON: stays out-of-grammar
"senior": "veteran", # not in REPAIR_LEXICON: stays out-of-grammar
}
288 of the 1,500 questions get rewritten; a one-round repair lexicon knows three of the five synonyms, deliberately leaving two unrecoverable. The committed per-depth table then puts both systems side by side on identical questions:
[3] the per-depth factorization table, beside the soft reasoner (same questions)
depth n coverage acc-on-parsed overall soft reasoner
0 804 0.9266 1.0000 0.9266 1.0000
1 352 1.0000 1.0000 1.0000 0.9659
2 280 0.8321 1.0000 0.8321 0.5000
3 64 1.0000 1.0000 1.0000 0.5000
Read the two geometries off the columns. The soft reasoner (a bag-of-local-features stand-in, trained on depths 0–1) degrades along the depth column: , a collapse to exactly chance at the depths where answering requires composing two rules, and the collapse is asserted, not eyeballed: the module requires depth-3 accuracy at or below and a gap of at least 25 points from depth 0 (ruletaker_lite.py, lines 412–416). The pipeline is depth-flat on what it parses: the acc-on-parsed column is exactly at every depth, again asserted question by question (translate_prove.py, lines 298–309). Its failures live in a different column entirely: coverage, which falls exactly where the lexical knob bites, under the strict grammar and after the repair round (asserted strictly higher and strictly below 1, lines 311–316). Its correctness factorizes as , where denotes the probability of the named event over the question bank: the chance of a correct answer equals the chance of a successful parse times a conditional accuracy of exactly 1. Every end-to-end error is a visible abstention, never a silent wrong answer, so the pipeline's difficulty response is an abstention rate where the soft reasoner's is an error rate.
The third knob the instruments turn is negation. The flip probe, styled after RobustLR's logic-changing rule edits [3], edits one rule body by negating one condition, relabels with the prover, and keeps only the questions whose gold answer flips (ruletaker_lite.py, lines 327–366):
[5] the RobustLR-style probe: flip one rule negation, relabel, remeasure
gold-flipped questions: 66 stand-in accuracy on them BEFORE the edit: 0.485
tracked after the edit: 54/66 = 0.818 (prover: 1.000 by construction)
The soft reasoner tracks only 54 of the 66 logic flips; every miss is its one_step feature ignoring the newly negated condition. The pipeline, whose answers are recomputed from the edited theory, tracks all of them by construction.
So: two systems, two failure geometries. One falls along depth and stumbles on negation while shrugging off surface noise (the statistical reader never parses, so synonyms cost it nothing); the other is provably flat along depth and exact under negation, but bleeds coverage the moment the vocabulary drifts. The aggregates, against , sit five points apart and say none of this; the section above showed a bank composition that makes them exactly equal. Published controlled generators expose still more knobs in the same spirit: number of hops, ordering of the facts, and distractor branches, irrelevant rule chains a greedy reader wanders into, which turn out to dominate errors even when depth is held fixed [4]. Each knob is an axis; per-axis reporting is what makes degradation attributable.
Seven axes beyond completeness, one pinned gadget each
Every knob so far still measures one family of things: recall along a monotone derivation. Did the system recover the entailed answer, at depth , through surface noise? Call that the completeness axis. The frontier companion examples/frontier/difficulty_axes.py makes the chapter's structural claim runnable: at least seven further axes, each orthogonal to completeness, make a reasoner hard, and orthogonality is an empirical claim, so each axis gets a finite gadget engineered to a strict discipline. In every gadget the completeness axis is pinned: the reasoner inside is run to its full fixpoint, or its recall is measured at exactly 1, or its derivation depth is held constant between the compared conditions, and then the gadget's own failure still occurs and is counted (run(), lines 412–435, executes all seven gadgets, each of which carries its own pinning assert, and re-asserts the soundness pin plus the headline failures). A depth-complete reasoner fails all seven ways at once; no depth budget fixes any of them.
Seven orthogonal difficulty axes radiating from a pinned completeness hub, each spoke carrying its gadget's committed measurement; the inset strip shows the two instruments' opposite failure geometries.
Original diagram by the authors, created with AI assistance.
The table reads the module in one screen; the subsections then take each axis at speed, giving (a) what it stresses mechanically, (b) which system class it should hurt a priori, and (c) the committed measurement.
| # | axis | the gadget turns | the pinned control | committed reading |
|---|---|---|---|---|
| 1 | soundness | an over-general subsumption predictor on the real TBox | recall exactly | precision , 22 invented pairs |
| 2 | termination | one existential advisor-regress rule under the chase | a terminating control saturates at 10 atoms and stays put | sizes , never saturated |
| 3 | proof width | a Horn ladder against its disjunctive twin | per-branch depth 20 in both | 1 leaf against 1,024 leaves |
| 4 | query joins | the variable count of a cycle query | same 6-edge graph, same answer "yes" | probes 42 → 2,274 |
| 5 | semantics | one negation-as-failure rule | Horn core verified monotone under all 20 candidate additions | one added fact retracts a conclusion |
| 6 | trust | a label-swapped concept extractor | task accuracy for both extractors | concept accuracy against |
| 7 | scale | chain length, naive against semi-naive evaluation | identical closures, identical wave depth | probe ratio |
Axis 1: soundness, the error completeness cannot see
Completeness counts the entailments you found; soundness counts the ones you invented. The gadget runs an over-generalizing subsumption predictor against Volume 2's completed classification of the academic TBox (terminological box, the ontology's concept-level axioms): predict (read: every is a , the concept is subsumed by ) whenever the truth says so or the two concepts share any subsumer besides (the top concept, the universal class that subsumes everything, TOP in the code) (axis_soundness, lines 87–118):
truth = {(a, b) for a in names for b in names
if a != b and b in S[a]}
pred = {(a, b) for a in names for b in names if a != b
and (b in S[a] or (S[a] & S[b]) - {TOP, a, b})}
The prediction set is a superset of the truth by construction, so with the true positives and the vertical bars counting the number of pairs in a set, exactly: completeness is pinned. But : the predictor invents 22 subsumptions, flagship among them Professor ⊑ Student, minted from the shared subsumer Researcher. A priori this axis hurts geometric predictors most: Volume 3's box and order embeddings default to exactly this complete-but-unsound posture, where overlapping regions assert relations the ontology never licensed. A benchmark that grades only recall certifies nothing about this axis, because the two error directions are independent.
Axis 2: termination, when "complete at last" never arrives
The gadget feeds Volume 2's restricted chase one existential rule, the advisor regress (every researcher was advised by some researcher), which mints a fresh anonymous individual at every firing. At step budgets 10, 20, and 40 the instance has grown to 21, 41, and 81 atoms and is still unsaturated at every cap, strictly larger at each; the terminating control rules reach their 10-atom fixpoint after 3 firings and do not move when the budget quadruples (axis_termination, lines 126–152). The mechanical stress is that there is no fixpoint to be complete about: recall is undefined at every finite budget, so the completeness axis is not failed but prior. The gadget can exhibit a run that keeps growing; it cannot certify that no budget would ever suffice, and Volume 2's chase chapter carries the classical negative results on deciding that question in general. This axis hurts any system whose evaluation assumes a bounded closure: materialization engines, fixed-depth unrolled networks, and every benchmark harvested from "the" closure of a rulebase.
Axis 3: proof width, the same depth with bills
Depth counts rule applications along one proof branch; width counts the branches. The gadget builds two propositional ladders of rungs (ladder, lines 160–174):
cl: list[tuple[frozenset, tuple]] = []
for i in range(k):
if disjunctive:
cl.append((frozenset({f"a{i}"}), (f"b{i}", f"c{i}")))
cl.append((frozenset({f"c{i}"}), (f"a{i + 1}",)))
else:
cl.append((frozenset({f"a{i}"}), (f"b{i}",)))
cl.append((frozenset({f"b{i}"}), (f"a{i + 1}",)))
return cl
The Horn twin steps ; the disjunctive twin replaces the first step by ( is logical or). A classical case-splitting prover must establish the goal in every disjunct's branch, so each rung forks the proof tree in two. Write for the number of open branches after rung ; the recurrence is with , and unrolling it one rung at a time gives . Along any single branch, each rung costs one split plus one definite firing, so every branch closes at depth exactly , in both ladders. The committed run confirms both counts: per-branch depth 20 in both, leaves 1 (Horn) against (disjunctive), with the depth equality asserted (axis_width, lines 210–227). Width is a second, independent bill that no depth budget pays. It is the cliff Volume 2 crossed between EL, whose Horn-like saturation is polynomial, and expressive logics whose tableau must reason by cases; a priori it hurts search-based provers and any chain-of-thought whose trace is one branch of a tree it never finishes.
Axis 4: query joins, hardness that lives in the question
Freeze the data completely and hardness can still grow, inside the query. The gadget evaluates Boolean cycle queries over one unchanged 6-edge graph with no rules at all: the query asks whether there exist (, the existential quantifier) nodes to fill the variables such that every listed edge holds simultaneously (, logical and), closing a cycle. Written out, , where is the number of variables (axis_query, lines 239–260):
[4] query joins — cycle queries over one 6-edge graph, no rules
k vars probes witnesses answer
2 42 6 yes
3 114 6 yes
4 258 18 yes
5 546 30 yes
6 1122 66 yes
7 2274 126 yes
data and entailment depth frozen; the bill is the query's alone
Both non-cost columns are derivable by hand, which is worth doing because it proves the instance never changed. The graph is the complete loopless digraph on three nodes, with adjacency matrix , where is the all-ones matrix and the identity (we write rather than the customary because already names this chapter's aggregate score). A witness for is an assignment of nodes to with every consecutive edge present, which is precisely a closed walk of length , and the number of closed -walks is , the trace (sum of diagonal entries) of the -th matrix power. That trace has a closed form, reachable with nothing beyond matrix multiplication. Two ingredients. First, : each entry of is a row of ones times a column of ones, three terms of , so every entry is . Second, multiplying any combination by and expanding term by term gives : still a combination of and . So every power of has this form, and induction on pins the coefficients:
For the claim reads : true. Assume it at and multiply once more by , using the expansion above with and . The new coefficient is , and the new coefficient is : exactly the claim at . The diagonal entries of and of are all , so each matrix contributes times its coefficient to the trace:
Evaluate: gives ; gives ; gives ; then , , . The committed witness column matches term for term. Meanwhile the certain Boolean answer is the same single bit at every , yet the counted join probes grow , with successive ratios falling toward , the out-degree that multiplies the join frontier per added variable. This is database theory's distinction between data complexity and combined complexity, exhibited rather than proved: the bill can be a function of the question's structure alone. It hurts any evaluator that treats queries as free and data as the only size parameter, which is most knowledge-graph benchmarks.
Axis 5: semantics change, when adding a fact retracts a conclusion
Completeness talk presupposes monotone growth: more input, never less output. The gadget first verifies that presupposition for the Horn core: writing for the Horn program's facts, for one candidate added fact, and for the least fixpoint of Volume 1's chainer, it checks , meaning every conclusion of the smaller program is contained in (, is a subset of) the conclusions of the larger one, for every one of 20 candidate fact additions. Then it adds one negation-as-failure rule, "independent(X) if person(X) and not advised(X)," evaluated the stratified way (_naf_independent and axis_semantics, lines 268–305). In the base academic world, alice is the one unadvised person, so independent(alice) holds; add the single fact advises(bob, alice) and the conclusion is retracted: the committed run prints before: ['alice'] after adding advises(bob, alice): {}. The consequence operator has become antimonotone; the algebra of the fixpoint changed, not its depth. This is the same phenomenon the flip probe caught behaviorally in the soft reasoner, now located structurally, and it hurts precisely the systems whose training distribution taught them that conclusions only accumulate.
Axis 6: trust, right answers about the wrong things
The gadget builds two concept extractors over the five people of the academic world: the faithful one reads the true professor/student concepts; the shuffled one swaps them. The downstream task, "researcher(x) = professor(x) or student(x)," is symmetric in the two concepts, so both extractors give the identical verdict on every person: task accuracy against , indistinguishable, while concept accuracy is against (axis_trust, lines 310–340). This is the case of the ( factorial, the number of ways to permute concept labels, with here counting the concepts) mis-grounding optima that Reasoning Shortcuts counted, pinned here only as a coordinate in the taxonomy: a system can be sound, complete, and wrong about meaning, and no behavioral benchmark score, on any mixture, can see it. It hurts neuro-symbolic stacks specifically, because they are the systems that claim their intermediate symbols mean something.
Axis 7: scale, the same logic with a growing bill
The last axis is pure engineering. The gadget closes the same two transitive-closure rules over citation chains of edges, once with naive evaluation (re-join every rule against the full store every wave) and once semi-naive (seed each round at the previous round's delta, so no rule instance is re-derived), asserting at every size that both closures equal Volume 1's oracle and both pay the same wave depth (axis_scale and seminaive_lfp, lines 349–407):
[7] scale — naive vs semi-naive on growing citation chains
m closure waves naive semi ratio
8 44 8 1,776 340 5.2x
16 152 16 24,480 2,344 10.4x
32 560 32 368,192 17,488 21.1x
The closure sizes are exactly , where reads " choose 2": the number of ways to pick 2 of the chain's nodes, equal to , counting all ordered pairs along the chain, plus the base edges: , , . The chain forces waves, and the store grows to order atoms, so naive evaluation's bill scales like waves times store, order , against semi-naive's order : the ratio should grow linearly in , and the committed ratios double as doubles, on identical logic and identical depth. This is the axis on which materialization engines like RDFox earn their living, and GPU Reasoning already showed its batched cousin; a benchmark that fixes its data size never turns this knob at all.
Interactions, honestly bounded
One-factor-at-a-time is cheap because it is incomplete. With levels per axis (say : off, moderate, hard) and seven axes, the one-factor design measures a baseline cell plus each axis alone at its non-baseline levels:
What it cannot see is interaction: the case where the accuracy surface is not additive, , so that two knobs turned together cost more (or less) than the sum of their solo costs. Depth and distractors compounding is the canonical worry: a distractor that costs 2 points at depth 1 can cost 20 at depth 3, because each extra hop multiplies the chances of wandering down the irrelevant branch.
The committed instruments already exhibit one interaction, and it is worth reading closely because it arrived uninvited. The pipeline's coverage column is not constant across depth: . The lexical knob was turned uniformly, so why does depth 2 pay most? Because the synonym table attaches to predicates, and the predicates are layer-tied: the unrepairable "senior → veteran" hits a depth-2 head, so depth 2 bleeds coverage; the unrepairable "cited → referenced" hits a stated layer-0 predicate, so depth 0 bleeds; the depth-1 and depth-3 predicates are either repairable or absent from the table, so their coverage returns to exactly after the repair round. The lexical axis's effect is a function of depth, not a number. One-factor reporting would have averaged this into a single coverage figure and lost the geography.
The honest fix would be the full factorial, and the arithmetic explains why the field does not run it. Seven axes at three levels is cells. To resolve a cell's accuracy to a 95% confidence half-width of , the binomial worst case requires, from the half-width formula solved for the per-cell sample size :
so the grid needs labeled questions per system, per seed, every label proof-verified. The frontier module accordingly commits no factorial grid; its seven gadgets are one-factor designs by declared policy, with completeness pinned in each, and the two-knob interaction above is an observation the instruments happened to afford, not a designed cell. Any benchmark paper claiming to control "difficulty" should be read against this arithmetic: full control of even seven axes is a six-figure question bank.
The axes as diagnosis: a repair menu
The point of attributable degradation is that each axis, once named, has a literature aimed at it. Read the committed tables as a diagnosis and this series as the pharmacy:
- Depth falls when a constant-depth architecture must simulate a serial derivation; the mitigation is serial compute at decode time, the subject of Chain-of-Thought and its ceiling in The Transformer Depth Ceiling.
- Lexical variation starves strict parsers of coverage; the mitigations are exactly the pipeline's own repair loop (normalization before parsing) and richer translators, with the coverage-versus-soundness trade priced in Abstention.
- Negation and semantics change break systems trained on monotone data; Volume 4's lesson from the flip probe is to evaluate under logic-changing edits, and to compile non-monotone constructs down to stratified form before the learner ever sees them, as the labeler here does.
- Distractors are an attention and retrieval problem: the greedy reader follows the wrong branch [4], and the fix is to score selection separately from derivation.
- Soundness failures at pinned recall call for calibrated confidence and selective answering: Calibration and the risk-coverage machinery built earlier in this volume.
- Termination demands budgets with certificates: report saturated against cut off, never a bare score, the discipline Materialization versus Rewriting formalized.
- Width wants search policy, not more depth: case budgets, clause ordering, and the verifier-gated sampling of the previous chapter.
- Trust requires concept-level audits, since no task score can see the orbit; Reasoning Shortcuts and Identifiability are that audit.
- Scale is an engineering axis with an engineering answer: semi-naive deltas and batched fixpoints, as in GPU Reasoning.
A leaderboard that reports one aggregate can rank; a per-axis table can prescribe. That difference is the chapter's export to the rest of Part VI.
What the field's benchmarks control
Placed on the seven-axis grid, the field's controlled generators each pin a few axes well and leave the rest loose. The table compresses the survey; every row is a generator family whose design intent was exactly the discipline of this chapter.
| generator line | axes it turns deliberately | held-out discipline | left loose |
|---|---|---|---|
| depth-stratified rulebases (RuleTaker) [1] | derivation depth (strata), closed-world negation, label balance per stratum | test depths beyond the trained strata | proof width (Horn only), vocabulary scale |
| depth-by-linguistic-complexity grids (the ALCQ line) [2] | depth and linguistic complexity as a two-factor grid | held-out grid levels | distractors, width, scale |
| fictional-ontology chains (PrOntoQA) [4] | hops, fact ordering, distractor branches; fictional vocabulary neutralizes memorization; every step checkable | ontology regime crossed with hop count | width, data scale |
| abstract urban simulation (LogiCity) [5] | abstraction complexity of the rule set, horizon, compositional splits | unseen rule-agent compositions | soundness attribution, vocabulary |
| kinship composition chains (CLUTRR) [6] | chain length as the generalization axis, three graded noise-fact regimes, crowd-sourced paraphrase (lexical) | train on short chains, test on strictly longer | negation, width |
Two columns of the seven are under-studied across the entire row set, and it is worth saying so plainly. No generator in the table turns the proof-width knob: every rulebase is Horn-shaped or policy-shaped, so case-splitting cost, the axis that separates saturation from search, is simply absent from the field's controlled evidence. And vocabulary size as a graded memorization-pressure knob is controlled only by the fictionalization trick, which sets it to zero rather than sweeping it [4]; nobody's public grid measures accuracy as a function of how many distinct predicates and entities a system must keep apart. Both knobs are cheap to add to a generator of the ruletaker_lite kind, which is part of why this volume ships one.
The unsolved part
Three gaps stand between this chapter's discipline and a settled science of reasoning difficulty. First, axes for soft knowledge. Every gadget above lives in a crisp world: premises are true or absent, and difficulty is structural. When premises carry uncertainty, as they do everywhere this series has attached weights and probabilities, difficulty acquires a component no standard axis measures: calibration pressure, the degree to which an instance punishes a system for the shape of its confidence rather than the identity of its answer. A bank where the right output is a probability has no agreed stratification, and mixing "hard because deep" with "hard because the posterior is genuinely 0.6" confounds exactly the way depth and distractors did.
Second, difficulty for generative proofs. When the required output is a derivation rather than a bit, step count is the axis everyone reports and a weak proxy for hardness: two proofs of identical length can sit atop search trees whose widths differ by the of the ladder gadget, and a proof that reuses a lemma is easier to find but no shorter to write. A difficulty model for proof generation would need to score the search landscape, not the artifact.
Third, and most consequential, the transfer question. The entire construction assumes that per-axis degradation profiles measured on synthetic generators predict behavior on natural corpora, where the axes vary uncontrolled and correlated. That is a testable claim: estimate a natural benchmark's difficulty mixture, predict each system's aggregate from its measured profile via the mixture identity of this chapter's first section, and check the prediction. To our knowledge no published study has run that regression at scale. Until one does, the axes are an instrument validated on the instrument's own terrain.
Why it matters
This chapter is Part VI's methodological hinge. The volume has spent fourteen chapters building trust machinery (justifications, calibration, abstention) and scale machinery (materialization, batched fixpoints, depth budgets); the question "did it work?" now lands on benchmarks, and benchmarks are experiments whether their authors admit it or not. The difficulty axes are to benchmarks what controlled variables are to experiments: without them a score is an observation, with them it is a measurement. For the reader's own research the export is concrete. Report per-axis tables, not aggregates; pin the axis you are not studying, the way every committed gadget pinned completeness; state which knobs your generator cannot turn. And when reading a leaderboard, ask the one question this chapter has made precise: if this system's score fell, could anyone say which axis pulled it down? A leaderboard that cannot answer is measuring something. It is just not measuring reasoning.
Key terms
- Completeness axis: the difficulty dimension benchmarks usually grade: recall of entailed answers along a monotone derivation, stratified by depth.
- Difficulty axis: an independent mechanical property of an instance that makes reasoning hard; this chapter's seven, beyond completeness: soundness, termination, proof width, query joins, semantics change, grounding trust, and scale.
- Mixture confound: the identity : an aggregate score entangles the system's per-stratum accuracy with the bank's composition , so rankings can flip with the mix.
- One-factor-at-a-time design: hold every difficulty factor at baseline, turn one knob, attribute the drop; cheap ( cells) but blind to interactions.
- Label balance: the generator discipline forcing every difficulty stratum to 50/50 True/False so no class prior leaks into the score.
- Pinning: running the gadget so the axis not under study is held at its ideal (recall exactly 1, fixpoint reached, depth constant), making the measured failure attributable.
- Proof width: the number of branches a case-splitting proof needs; grows as on the disjunctive ladder while per-branch depth stays .
- Combined complexity: cost that grows with the query's structure at frozen data, exhibited by the cycle-query gadget's probes rising over one 6-edge graph.
- Antimonotonicity: the semantics-change failure: adding a fact retracts a conclusion, breaking the more-input-never-less-output premise of completeness talk.
- Degradation profile: a system's vector of per-axis deltas from baseline; two systems with equal aggregates can have opposite profiles, as the committed tables show.
Where this leads
This chapter built the rulers; the next assembles them into an instrument panel. NeSy Benchmark Suites and Simulators takes the five instruments this volume has committed, the per-depth banks, the probes, the calibration and consistency meters, and welds them into a suite harness whose committed digits double as the volume's regression test, then reads the field's benchmark suites (rsbench, KANDY, LTLZinc, NeSy4VRD and their kin) through the same lens: which axes each suite pins, and what its headline numbers can therefore attribute.
Companion code: examples/frontier/difficulty_axes.py implements the seven pinned gadgets, guards every claim quoted here with an assert, and reproduces every quoted digit deterministically; examples/integration/ruletaker_lite.py and examples/integration/translate_prove.py are the two instruments whose committed tables this chapter re-reads. Run each with python3 <module>.py to reproduce every figure in this chapter byte for byte; the volume's acceptance harness examples/frontier/validate.py re-runs them as part of its 19-check ledger.