CPUNeSy: Controlling Model Writes for Reliable Neuro-Symbolic Reasoning

1 INTRODUCTION

• On tasks requiring several rules or facts from a fixed source, fluent chain-of-thought can skip inferences or introduce unsupported conclusions, while executing unsupported premises can produce the same wrong answer.These risks matter in legal, medical, and formal-mathematics settings where intermediate steps need to be auditable and source-tied.Source: §1 · p. 1
• CPUNeSy checks model-proposed predicate units against source support and an allowed vocabulary, then derives answers deterministically with bounded-depth, replayable derivations.Each accepted premise retains evidence so a served answer can be traced to the source.Source: §1 · p. 2
• Deterministic execution accounts for most accuracy recovery on derivation-heavy tasks, while controlled writes mainly improve selective reliability by withholding unsupported or inconsistent answers at a coverage cost.The paper frames certification as an error–abstention tradeoff on top of execution, not a further accuracy gain.Source: §1 · p. 2
• The experiments disentangle execution from restricted grounding, agreement, and source rechecking, including fixed-trace rechecking and an offline test of the vocabulary barrier.The evaluation spans legal reasoning, formal mathematics, and medical calculation, and reports answered accuracy, coverage, and full-pool accuracy.Source: §1 · p. 2
• The contributions include a checked interface with formal guarantees conditional on source-checker and verifier soundness, plus diagnostics for error, coverage, cost, and optional kernelization.The component analysis separates execution, restricted grounding, agreement, and source rechecking.Source: §1 · p. 2

LLM-to-symbolic solver pipelines

• LLM-to-solver pipelines translate problems into formal representations for execution, then add validation, repair, or symbolic trajectories; CPUNeSy instead checks source support before predicates become premises [1, 3].The cited examples include Logic-LM [1], LINC [3], and SatLM [5], followed by validate-and-repair and symbolic-trajectory refinements.Source: §2 · p. 3

Neuro-symbolic engines, provenance, and structured generation

• Neuro-symbolic learning integrates logic with training, constrained decoding targets formally valid outputs, and provenance tracks which base facts support derived facts [18, 20].The cited approaches span differentiable or probabilistic logic, constrained decoding, and Datalog provenance.Source: §2 · p. 3

Neural theorem proving

• Neural theorem proving develops from predicted proof steps and retrieval toward agentic tactic search; CPUNeSy’s premise pools use a source kernel and dependency closure rather than a raw library [31, 32].The related work notes direct comparison with ReProver and BM25.Source: §2 · p. 3

Selective prediction, verification, and benchmarking

• Selective prediction and post-hoc verification abstain or check after generation, whereas CPUNeSy moves source checking before execution and isolates its contribution with fixed-trace comparisons [39, 40].The passage situates these approaches among benchmarks built to evaluate reasoning errors.Source: §2 · p. 3

3.1 ARCHITECTURE

• DEPLOY checks source units and removes redundant ones; SERVE checks query groundings and derivations before verbalizing only certified results.The kernel preserves the source set’s closure, so derived answers can be reconstructed from certified source units.Source: §3.1 · p. 4, Figure 2 · p. 4, §3.2 · p. 6
• SOURCE mode checks proposed facts and rules against source records, while DERIVED mode checks proof edges over the current kernel and enforces a depth budget.Supported source units enter the certified set; verified derived conclusions may be served or cached with their source dependencies.Source: §3.1 · p. 4
• Implementation coverage varies: historical L1-HARD runs restricted prompt vocabulary, while explicit admission was evaluated separately by offline replay.Complete per-query certificate archival was not instrumented in every adapter.Source: §3.1 · p. 4

3.2 FORMAL GUARANTEES AND OPERATING CONDITIONS

• The soundness theorem guarantees recheckable source support for persistent premises and bounds served or cached consequences relative to the current state, assuming sound checkers.Erasing a source unit also removes cached consequences whose certificates depend on it.Source: §3.2 · pp. 5–6
• Restricted source writes block direct admission of intermediate or target predicates, so accepted derivations of them must include a rule application.This holds for arbitrary model proposals, but does not assume semantic accuracy of allowed leaf predicates.Source: §3.2 · p. 6
• Experimental natural-language source checkers do not have established source soundness, while the mathematical adapters execute recorded dependency graphs rather than evaluating end-to-end proof search.The reported residual risk for natural-language checkers is measured empirically.Source: §3.2 · p. 6
• The voting bound relies on specified shared-bias and independent-slip regimes, and for two traces it may be loose.Two calls alone do not identify the bound’s latent parameters or establish conditional independence.Source: §3.2 · p. 6
• The deletion scan preserves source closure, so the kernel can decide every query the certified source set can decide; storage savings depend on corpus redundancy..Source: §3.2 · p. 6

4.1 RQ1: DOES SYMBOLIC DERIVATION RECOVER ACCURACY WHEN ANSWERS MUST BE DERIVED?

• The certified channel leads every baseline on LD-MH and on ContractNLI with Seed; with same-model fallback, it leads every baseline in every public-benchmark column.Table 2 reports full-pool accuracy, counting abstentions as errors.Source: §4.1 · pp. 6–7, Table 2 · p. 7
• On L1-HARD mid-link-break negatives, neural baselines remain below 80% despite tripled reasoning budgets, while the certified channel serves nearly the whole pool at near-perfect accuracy.Audited baseline failures omitted exactly one intermediate link; on AFP dependency-DAG tasks, CPUNeSy serves most queries at high accuracy while chain-of-thought and retrieval hover around chance.Source: §4.1 · p. 7
• 72.5% to 90.1% for Seed and 63.5% to 90.4% for DeepSeek are the MedCalc full-pool accuracy gains from same-model fallback; on LeanDojo Benchmark 4, kernel and BM25 pools each reach 76% full gold-premise coverage.Fallback routes cases withheld by the certified channel to the same model’s open-book answer; the kernel pool is a competitive premise source relative to learned ReProver retrieval.Source: §4.1 · p. 7

4.2 RQ2: WHICH COMPONENT RECOVERS ACCURACY, AND WHAT DOES CERTIFICATION ADD?

• 98.8% full-pool accuracy for the uncertified one-vote solver versus 97.1% for restricted two-vote serving on L1-HARD shows execution recovers most accuracy, while controls trade coverage for lower accepted-answer risk.The paired difference is not statistically significant (p = 0.34); the interval also does not establish equivalence.Source: §4.2 · p. 8, Table 3 · p. 8
• 25% of DeepSeek’s wrong answers surviving two-vote agreement were withheld by source rechecking, along with 51 correct answers; for Seed, rechecking withheld 6.25% of those wrong answers and 14 correct answers.The fixed-trace ContractNLI comparison isolates a source-rechecking error–abstention tradeoff beyond voting.Source: §4.2 · p. 8

4.3 RQ3: WHICH OBSERVED CONDITIONS EXPLAIN UTILITY?

• Accuracy relative to each model’s better neural control increased for K3 and K2.6, was unchanged for GLM, and decreased for DeepSeek and Qwen, a pattern consistent with shared-error limits on agreement.The diagnostics relate utility to derivation demand, kernel adequacy, and grounding errors shared across calls versus disagreements; vote disagreement and grounding coverage alone do not establish source support.Source: §4.3 · pp. 8–9, Table 4 · p. 8, Figure 5 · p. 9

4.4 RQ4: WHAT IS THE SERVING-TIME COST OF CONTROLLING MODEL WRITES?

• 48.9% of full-pool units retained at the same observed 97.45% answered accuracy reduced tokens by 43% on M-HARD; measured redundancy was 37.1% for AFP and 0.60% for law.These are candidate-restriction measurements, not measured storage-byte savings; physical storage and the scheduler-specific crossover remain unmeasured. Restricted two-call L1-HARD serving is preferred under the stated ledger when 2cW > 6cA + 145,422cT over 240 items.Source: §4.4 · p. 9

• Execution lifts L1-HARD full-pool accuracy from 87.9% for the strongest neural baseline to 98.8% without a certificate.The conclusion identifies deterministic execution as the main source of accuracy recovery on derivation-heavy tasks.Source: §5 · p. 9
• With grounding traces fixed on ContractNLI, source rechecking removes a quarter of DeepSeek’s wrong answers surviving two-vote agreement, while withholding correct answers too.The conclusion frames certification as selective-serving control rather than an accuracy mechanism.Source: §5 · p. 9
• Certificates establish derivational validity relative to admitted premises, so semantic faithfulness depends on the source checker and prospective validation remains future work.Where grounding errors are shared across calls, agreement repeats them and the gate cannot help.Source: §5 · p. 9

• The legal and medical experiments evaluate benchmark inference and calculation.Source: ETHICS STATEMENT · p. 10
• Clinical or legal use requires further validation of source interpretation because a contract or clinical note may be misread even when subsequent inference passes verification.Source: ETHICS STATEMENT · p. 10
• Applications should expose source evidence, checker identity, and abstention status, and distinguish fallback answers from checked outputs; decisions affecting patients or legal rights require appropriate expert review.Source: ETHICS STATEMENT · p. 10

AI USE STATEMENT

• Language models assisted coding, writing, visualization, and offline analysis; human authors are responsible for verifying records, results, and claims.Source: AI USE STATEMENT · p. 10

A FULL RELATED WORK

• The related-work review covers neural representations of logic, symbolic execution, premise selection, and source checking.Source: A FULL RELATED WORK · p. 15

A.1 FIRST WAVE: CONNECTIONIST–SYMBOLIC INTEGRATION (1990S)

• KBANN encoded propositional Horn rules in feed-forward network topology, while CILP approximated logic-program fixed points with recurrent networks; CPUNeSy adds checks on source premises and storage.Source: §A.1 · p. 15

A.2 STATISTICAL RELATIONAL LEARNING AND PROBABILISTIC LOGICS (2000S)

• Markov logic networks and ProbLog represent uncertainty over logical statements, addressing a different inference concern from CPUNeSy’s source-admission checks.Source: §A.2 · p. 15

A.3 DIFFERENTIABLE DEDUCTIVE ENGINES (2016–2022)

• Differentiable deductive systems made predicate-level processing trainable, but reasoning shortcuts can arise when predictions fit task labels while misrepresenting intended concepts.Source: §A.3 · p. 15

A.4 LOGIC AS LAYERS AND CONSTRAINTS

• Logic-as-layer and constraint methods incorporate logic into computation or training objectives; CPUNeSy instead checks updates to a separate symbolic state before execution.Source: §A.4 · pp. 15–16

A.5 LLM-ERA HYBRIDS

• LLM–solver systems motivate distinguishing inference validation from premise checking; CPUNeSy admits source units through a certificate gate and records dependencies of symbolic conclusions.Source: §A.5 · p. 16

A.6 NEURAL THEOREM PROVING AND PREMISE SELECTION

• Neural theorem proving spans step proving, search-guided training, informal-to-formal pipelines, premise selection, and olympiad geometry; premise selection became a standard interface to large libraries.Examples include GPT-f (Polu & Sutskever, 2020), HTPS (Lample et al., 2022), DSP (Jiang et al., 2023), LeanDojo/ReProver (Yang et al., 2023), and AlphaGeometry.Source: §A.6 · p. 16

A.7 FAILURE MODES: REASONING SHORTCUTS

• NeSy predictors can attain high label accuracy while violating intended semantics, motivating checks of which premises support a prediction.The cited work identifies extra supervision or architectural constraints as mitigation approaches; this paper measures restricted writes, agreement, and source rechecking.Source: §A.7 · p. 16

A.8 LOGICAL-REASONING BENCHMARKS AND PRESSURE TESTS

• LogicBench, ProverGen/ProverQA, and RuleArena test contextual rule-following across multiple inference steps, while this paper evaluates execution and premise checks across law, medicine, and formal mathematics.The listed evaluations are L1-HARD, M-HARD, ContractNLI, MedCalc, and LeanDojo.Source: §A.8 · p. 16

A.9 POSITIONING

• Table 5 pairs established components with evaluation questions; the paper’s empirical addition decomposes restricted writes, agreement, and source rechecking using error and refusal counts.The positioning also retains the stated cost assumptions of the depth–information model (Xu, 2026a).Source: §A.9 · pp. 16–17, Table 5 · p. 17

B.1 STATES, FORMULAS, AND DEDUCTIVE CLOSURE

• CPUNeSy models the language model as a carrier proposing statements to a symbolic core, whose finite, decidable proof system induces deductive closure.Function-free Horn/Datalog fragments satisfy the finite-step closure assumption used by the core.Source: §B.1 · p. 17

B.2 DEDUCTIVE SOURCES AND THE IRREDUNDANT KERNEL

• A deterministic deletion scan partitions a deductive source into an irredundant kernel and units derivable from the remainder; under the stated theorem, redundant units are invisible to rate and distortion.The kernel is order-invariant under the stated order-robustness condition.Source: §B.2 · pp. 17–18

B.3 DERIVATION DEPTH AS AN INFORMATION METRIC

• Derivation depth is the shortest proof length along immediate predecessors; under richness and generic incompressibility, it characterizes conditional description length up to logarithmic addressing overhead.The cited characterization is tight and equates derivation depth with conditional Bennett logical depth under efficient proof simulation.Source: §B.3 · p. 18

B.4 PROOF-VALID RELIABILITY UNDER PREMISE ERASURE

• The erasure framework tracks source leaves exposed along a fixed witness DAG, while shared modules can improve reliability and cache selection is NP-complete in general derivation DAGs.The theorem gives leaf-only transparent storage a first-order 1/ε overhead, reduced in the saturated shared regime to ρ/(sε).Source: §B.4 · p. 18

B.5 VERIFICATION OF MODEL-PROPOSED DERIVATIONS

• The bridge model separates proposal unreliability, verification misses, and premise-formalization failures; the grounding interface specifies predicates, entity roles, and which source predicates models may propose.The whitelist does not bypass source checking, and formalization error separates interface-determined bias from independent slips.Source: §B.5 · p. 19
• Certified rounding removes unverifiable edges and conclusions lacking complete verified derivations, admitting only units whose derivation edges all verify.For a finite trace and sound decidable verifier, any nonempty rounded output is a deductive source; a proposal with no surviving unit is rejected.Source: §B.5 · p. 19
• On L1-HARD, broad-interface traces had 9 both-wrong pairs, while restricted-interface traces had none and four correct/wrong pairs; two calls cannot identify bias and slip separately.The restricted vocabulary blocks direct conclusion proposals, but false allowed leaf assertions remain possible.Source: §B.5 · p. 19

B.6 APPLICABILITY CRITERIA

• The proposed compression-and-caching regime requires a decidable fragment, closure-based task fidelity, redundancy above a fixed threshold, and a compatible finite-step depth budget.Checked execution and closure preservation also apply below the redundancy threshold.Source: §B.6 · pp. 19–20

C COVERAGE, KERNEL, AND RESOURCE GUARANTEES

• Under closure fidelity, the irredundant kernel preserves closure and closure-type query answers, while certified coverage and resource guarantees depend on their stated assumptions.The kernel theorem bounds added certified depth by re-derivation depth, and storing redundant units does not improve the achievable rate–distortion function. A cached valid chain improves erasure recovery exactly when it removes an exposed leaf; caching break-even frequency is derived under the stationary depth–information cost model.Source: C COVERAGE, KERNEL, AND RESOURCE… · pp. 20–21

D PROOFS AND AUXILIARY RESULTS

• The appendix states auxiliary results before proving the guarantees and identifies the background results used in those arguments.Its proofs cover certified coverage, depth overhead, voting, kernel storage, and scheduling.Source: D PROOFS AND AUXILIARY RESULTS · p. 21

D.1 STANDING ASSUMPTIONS

• The standing assumptions include a sound and complete verifier for a decidable fragment, a fixed canonical order, and independent channel errors, with grounding bias treated separately from slips.The framework also specifies stationary amortized costs and a canonical-witness erasure regime.Source: §D.1 · p. 21

D.2 CERTIFIED-STATE SOUNDNESS

• Certified-state soundness preserves source support and verified witnesses through admission, derived queries, caching, erasure, and eviction.Rejected proposals and uncertified fallback answers remain outside the certified serving channel.Source: §D.2 · pp. 21–22

D.3 CERTIFIED ROUNDING AS A DEDUCTIVE SOURCE

• Certified rounding yields a finite, effectively listable deductive source because retained conclusions come from verified derivation DAGs and the verifier is sound.The source is formed from the conclusions of extracted DAGs whose edges all verify.Source: §D.3 · p. 22

D.4 CERTIFIED COVERAGE

• On the bias-free query mass, the intended derivation survives rounding when its steps are proposed and verified and its exposed premises are formalized.Independence in the slip channel supports multiplying the lower bounds for those events.Source: §D.4 · p. 22

D.5 CERTIFIED-DEPTH OVERHEAD

• Certification overhead is bounded by the additional depth needed to reconstruct subgoals removed by rounding.The proof restores each removed subgoal using its shortest certified reconstruction from the premise base.Source: §D.5 · p. 22

D.6 VOTING UNDER SHARED BIAS AND INDEPENDENT SLIPS

• Voting bounds distinguish shared-error queries, where a common wrong answer can persist, from queries where independent traces favor the unique correct answer.A missing strict majority, including a tie, yields abstention; the lower concentration bound requires conditional independence in the shared-error regime.Source: §D.6 · p. 22

D.7 KERNEL SUFFICIENCY AND STORAGE

• The fixed-order deletion scan preserves closure and closure-type answers, while the final per-message rate claim assumes a uniform law on the nonconfusable core alphabet.The kernel’s unit-count consequence and its per-message claim concern different resources; equality with the order-robust essential set is separate from closure preservation.Source: §D.7 · p. 23

D.9 RELIABILITY UNDER PREMISE ERASURE

• Cache recovery after premise erasure succeeds exactly when every exposed leaf survives, and adding a cache segment strictly improves recovery only if it shrinks the exposed-leaf set.The model assumes storage loss while the cache survives and source support remains valid; source withdrawal requires a separate model.Source: §D.9 · p. 24

E.3 DOMAIN INSTANCE 1: FORMAL MATHEMATICS

• On the 14-entry AFP subset, redundancy was about 20% under uniform reading and 46.7% under dependency-weighted reading, with the latter crossing τ; measured depth quantiles were 0/2/3/4, maximum 10.The protocol had hypothesized redundancy of at least 0.6 under both readings.Source: §E.3 · p. 26

E.4 DOMAIN INSTANCE 2: REGULATORY / LEGAL COMPLIANCE KNOWLEDGE BASE

• The legal mixed-corpus audit found only 2.2% overall redundancy, below the predicted 10-point reduction; case-specific facts were essential, so savings depended on rule-layer redundancy and rule share.The rule-layer measurement was 13.8%; a certified remeasurement gave 12.87% [9.1, 16.6].Source: §D.7 · pp. 23–24, §E.4 · p. 27

E.5 SETTING THE THRESHOLD τ

• The measurement protocol sets τ=0.5 so an eligible core at least halves unit count; domains with redundancy in [τ/2, τ) are hybrid-eligible.Eligibility is intended to require savings materially exceeding the fixed cost of the deductive engine and bridge.Source: §E.5 · p. 27

E.7 BOUNDED-STEP REDERIVATION AND PARENT-DESIGNATION SENSITIVITY

• Bounded rederivation added no legal-corpus redundancy through k=4; AFP redundancy nearly doubled at k=2 but saturated 12.9 points below τ.The legal result is consistent with maximum depth 2; both domains remained below τ=0.5 through k=4.Source: §E.7 · pp. 27–28, Table 6 · p. 28
• Randomly changing the designated parent left the 95th-percentile depth unchanged across 2,000 resamples: 1 for legal and 2 for AFP.The max-parent rule remained a conservative upper envelope, with AFP depth 3 versus 2.Source: §E.7 · p. 28

F.1 LD-MH: REPLICATION ON THE REAL MATHLIB4 DAG

• On the mathlib4 dependency DAG extracted by the LeanDojo tracer, M-HARD used depth strata 2–6, near-miss negatives, and twin-extended closure; neural baselines remained near chance, while the certified channel answered nearly all queries with high accuracy.Source: §F.1 · p. 28

F.2 EXTERNAL VALIDITY ON LEANDOJO BENCHMARK 4

• Applicability criteria C1, C2, and C4 held on the real corpus, while C3 remained unresolved because each traced theorem records only one derivation.Observed premise usage was 36.5%; establishing redundancy requires testing whether omitted premises can be derived from retained ones.Source: §F.2 · p. 29
• On 300 theorem tasks, the reference grounder reached 11.2% exact-set accuracy at 83% coverage; DeepSeek and Qwen improved answered exact-set accuracy over RAG, with 39.3% and 57.0% coverage.The reference run had 9.3% full-pool exact-set accuracy versus BM25’s 11.3%; exact-set matching is limited because gold premises come from one traced proof among potentially many valid proofs.Source: §F.2 · p. 29, Table 8 · p. 29
• 89.3% recall@15: the kernel-restricted pool matched BM25, and both had 76.0% full coverage, exceeding ReProver in this candidate-pool evaluation.BM25 was the stronger retrieval control here because the pools had equal coverage; a matched index-size comparison was not available.Source: Table 8 · p. 29, §F.2 · p. 30
• The appendix reports 0.46–0.51 selected premises on average against a gold mean of 2.76, indicating frequent omission of needed premises.The gold set is based on a single traced proof, which limits exact-set interpretation.Source: §F.2 · p. 29
• On the real mathlib4 DAG closure task, Seed two-vote certification reached 92.5% full-pool accuracy versus 51.0% for RAG, a 41.5-point advantage over the better neural control.The certified channel was 93.9% accurate on its 98.5% served subset; the evaluation measures derivability over recorded graphs, not end-to-end Lean proof search.Source: §F.2 · p. 29, Table 9 · p. 30

F.4 FAIRNESS AND ROBUSTNESS CONTROLS (FULL)

• Across regenerated suites, a weaker grounder retained an approximately 36-point compositional-stratum advantage; reported gaps also persisted under paraphrases and alternative distractor pools.Three-seed regeneration preserved the reported performance gaps.Source: §F.4 · p. 30

F.5 OBSERVED ERROR COUNTS AND CHANNEL-MODEL SCOPE

• Observed error fractions use different denominators and describe distinct events; they do not directly estimate Proposition 2’s channel parameters.Empirical instantiation would require step-level annotations, probability bounds, and assessment of the independence assumptions.Source: §F.5 · pp. 30–31

G.1 SOURCE CHECKING AND FIXED-TRACE GATE EFFECT

• With grounding traces fixed, source rechecking withheld answers while leaving other outputs unchanged; estimating premise-level false acceptance and rejection requires independent source-support annotations.The retrospective records lack those annotations.Source: §G.1 · p. 31

G.5 SUPPLEMENTARY GATE EFFECT AND COST ANALYSIS

• ContractNLI source rechecking improves loss above cW/cA thresholds of 1.81 for DeepSeek and 2.75 for Seed; restricted L1-HARD serving is preferred when 2cW > 6cA + 145,422cT.The paired accuracy-difference interval is [−4.17, 0.83] percentage points and does not establish equivalence; logged call durations assume sequential calls.Source: §G.5 · p. 32

G.6 SELECTIVE OPERATING POINTS AND PAIRED TESTS

• Table 10 reports discrete policies with risk as wrong answers divided by served answers and coverage as served answers divided by the common pool; risk–coverage curves require a threshold sweep.Table 11 gives paired full-pool accuracy tests, counts abstentions as incorrect, and applies Holm correction to six exploratory comparisons.Source: §G.6 · p. 33, Table 10 · p. 33, Table 11 · p. 33

G.7 REPRODUCIBLE ARTIFACT AND RECORDED MODEL IDENTITIES

• The audit package preserves frozen inputs, source hashes, scripts, generated counts, and policy outcomes, but caches lack consistent sampling dates and immutable model revisions.On valid traces, two-vote majority with abstention on ties equals the binary agreement rule, so the fixed-trace ablation isolates source rechecking.Source: §G.7 · p. 33

G.8 PROCESS-FIGURE PROVENANCE

• Process figures use different model and split provenance: LD-MH geometry uses K3’s 181/19 split, while the public accuracy table uses Seed’s 185/15 split.The plotted features summarize grounding, admission, closure, and output logs; the fixed-trace comparison measures source rechecking.Source: §G.8 · pp. 33–34

G.9 HISTORICAL TASK-ADAPTER RESULTS

• Historical task-adapter scores are descriptive, excluded from primary rankings, and cannot identify the causes of near-zero results.Per-row split identifiers, model profiles, sample counts, and failure breakdowns are unspecified.Source: §G.9 · p. 34, Table 13 · p. 34

H SUPPLEMENTARY VISUALIZATIONS

• Figures 8, 11, and 13 show schematic theoretical curves, while other supplementary panels report stress tests or Monte Carlo premise-erasure trials.Figure 12’s erasure simulation assumes storage loss with a surviving cache and unchanged source support.Source: H SUPPLEMENTARY VISUALIZATIONS · p. 34, Figure 12 · p. 36
• On M-HARD, CPUNeSy separates from pure and retrieval baselines, removes positive-versus-near-miss-negative polarity asymmetry, and stays stable as proof depth increases.On L1-HARD, its accuracy gain is concentrated on mid-link-break negatives, where factual access alone is insufficient.Source: Figure 9 · p. 35, Figure 10 · p. 35

I.1 CROSS-MODEL ERROR REGIMES ON L1-HARD

• GLM produced 2 pairs agreeing on a wrong answer, while the agreement rule filtered all 15/15 disagreements; full-pool accuracy counts abstentions as errors.Table 14 uses 240 L1-HARD queries with identical prompts, solver, and parsers across models.Source: §I.1 · p. 37, Table 14 · p. 37
• 99.6% [97.6, 99.9] served accuracy for the weaker same-family grounder and 99.1% [96.8, 99.8] for GLM exceed their pure and RAG baselines, while DeepSeek and Qwen are on par with neural baselines.Reference served accuracy is 100% at 97.1% coverage; weaker same-family coverage is 94.6%, and GLM coverage is 93.8%.Source: §I.1 · p. 37, Table 14 · p. 37
• DeepSeek served accuracy is 83.6% [78.2, 87.9] at 91.7% coverage, and Qwen served accuracy is 88.0% [83.0, 91.6] at 93.3% coverage.DeepSeek and Qwen have more shared errors, consistent with the shared-error boundary of Lemma 1.Source: §I.1 · p. 37