core/docs/decisions/ADR-0114a-anti-overfitting-proof-obligations.md

ADR-0114a — Anti-Overfitting Proof Obligations for expert Promotion

Status: Accepted (documentation-only; no code change) Date: 2026-05-22 Author: CORE agents + reviewers Type: Amendment to ADR-0114 Depends on: ADR-0091, ADR-0105, ADR-0106, ADR-0109, ADR-0113, ADR-0114, ADR-0115

---

Context

ADR-0113 reserved the expert namespace for a future ledger tier above audit-passed. ADR-0114 laid out a 7-phase arc toward a first expert promotion (GSM8K-math), with ADR-0120 designated as the eventual "first expert promotion contract."

The intervening discussion surfaced a load-bearing question: how does CORE prove a domain's expert claim is reasoning from concepts rather than pattern-matching from seen examples? This is the distinguishing question for any capability claim beyond the structural asymmetries audit-passed already verifies. An LLM scoring 95% on a benchmark may be memorizing or surface-pattern-matching; the claim "reasons from concepts" requires structural evidence that cannot be faked.

The audit-passed gate does not need this discussion — it verifies claim shapes (signed digest, replay determinism, typed refusal, exact recall) that transformer LLMs structurally cannot produce regardless of accuracy. But the moment a domain reaches for expert on a public benchmark, that's a raw-capability comparison, and the "is it actually reasoning?" question is the only credibility-bearing question.

ADR-0114a writes down, before any expert promotion code is built, the 10-point proof framework that ADR-0120's promotion contract must enforce.

---

Decision

The eventual expert promotion contract (ADR-0120) MUST require all ten obligations below. Each obligation is load-bearing and falsifiable: a domain that cannot satisfy any one of them stays at audit-passed.

These obligations apply to every expert promotion, not just GSM8K-math. Future expert domains (symbolic logic, DSL codegen, etc.) inherit the same framework; per-domain specializations may add further requirements but cannot weaken these.

Obligation 1 — Sealed-holdout discipline

Requirement. The capability benchmark must include a held-out split that is never read by any CORE component during development. Holdout sealing per ADR-0105 (age-encrypted, recipient-keyed).

Falsification. If commit history shows any access to the holdout cases during the window between dev-set authoring and the release event, the promotion is invalid.

Status. Substrate already in place (ADR-0105 sealed holdouts; ADR-0114 §5 GSM8K-test-set-is-holdout commitment). Per-lane enforcement lands in ADR-0119.

Obligation 2 — OOD surface variation must score ≥ 0.95 of dev

Requirement. A capability lane that scores S on its public split must score ≥ 0.95 · S on a programmatically-derived out-of-distribution split that holds the underlying graph constant but varies surface form:

• Entity-name renaming
• Unit relabeling (apples → nebulae, dollars → drachmas)
• Number-magnitude scaling (multiply all by k; for linear-arithmetic domains, answer must scale by k)
• Independent-sentence reordering

If CORE handles graph G correctly, it should handle every surface that lexes to graph G. A drop > 5% from public to OOD signals surface-feature dependence rather than reasoning from concepts.

Falsification. Score the same graphs through three surface renderings; if the lowest-scoring rendering falls below 0.95 · public_score, the promotion is invalid.

Status. OOD generator authoring required. Likely ADR-0118 (stepped realizer extension can do double duty) or a separate ADR-0118a.

Obligation 3 — Every correct answer ships with a replay-equal trace

Requirement. For every problem CORE marks "correct" on the public + holdout splits, an inspectable SolutionTrace artifact exists with:

• Ordered sequence of operations
• Each operation tagged with the pack-lemma identifier it invokes (operation provenance)
• A byte-deterministic trace hash
• Verifier (ADR-0117) re-applies the trace and reproduces the declared answer

Falsification. If any "correct" answer cannot be paired with a trace whose replay reproduces the answer, the promotion is invalid. A trace that reproduces the wrong answer is more useful than no trace at all — the wrong answer is then known to be a real CORE mistake, not a fake reasoning artifact.

Status. Trace produced by ADR-0116 (solver). Verifier in ADR-0117.

Obligation 4 — Refusal is a first-class outcome; misparse rate is zero

Requirement. Every problem produces exactly one of three outcomes:

• correct — answer matches ground truth AND trace replays
• wrong — answer differs from ground truth (trace may still replay)
• refused — typed ParseError / SolveError with a reason naming the unsupported construction

The expert threshold per ADR-0120 must require zero wrong answers. A high refused rate is acceptable and informative; a nonzero wrong rate fails the gate. CORE cannot claim to reason if it sometimes produces silent confabulations.

The distinction vs. LLMs is intentional: a frontier LLM scoring 95% on GSM8K typically has ~5% wrong and ~0% refused (it confabulates when uncertain). CORE's expert claim requires the opposite shape: high correct + nonzero refused + zero wrong.

Falsification. Any verified wrong answer on the public or holdout split — where "verified wrong" means the trace replays but yields a value differing from ground truth — invalidates the promotion.

Status. Parser (ADR-0115 Phase 1.3) already enforces typed refusal; solver (ADR-0116) must enforce the same discipline. The zero-wrong-on-public requirement is per-domain calibration; ADR-0120 sets it.

Obligation 5 — Reasoning-isolation perturbation suite

Requirement. A programmatic perturbation generator produces an unbounded test suite by applying invariance-preserving and invariance-breaking transforms to dev/holdout cases:

Transform	Expected behavior
Rename all entities	Answer unchanged
Rename all units	Answer unchanged
Multiply all numbers by k	Answer × k (linear domains); changes predictably (general)
Reorder independent sentences	Answer unchanged
Swap order of non-commuting operations	Answer changes predictably
Replace verb with synonym in registry	Answer unchanged

CORE must pass 100% of invariance-preserving perturbations and produce the predicted change on every invariance-breaking one. A pattern-matcher that learned superficial features fails some perturbations; a system reasoning from concepts passes all.

Falsification. ≥ 1% perturbation failure on any single transform class invalidates the promotion.

Status. Generator authoring required. New ADR (likely ADR-0119 subsidiary or its own).

Obligation 6 — Compositional-depth curve published

Requirement. Score correctness as a function of reasoning depth (number of operations in the ground-truth graph). Publish the depth- vs-accuracy curve from depth 1 through the maximum depth in the benchmark. The curve must be approximately flat — accuracy at depth N should not drop by more than 1 − (1 − ε)^N for some documented ε, where ε represents per-step parser/solver error.

A monotonically-decreasing curve indicates probabilistic accumulation of errors; a flat curve indicates the architecture handles N-step problems by the same mechanism as 1-step problems.

For comparison, LLM GSM8K curves typically decay sharply past depth 4-5. CORE's curve should not.

Falsification. If any depth bucket scores below (1 − ε)^N for the documented ε, the promotion is invalid (or ε must be raised, with justification, in the published curve).

Status. Measurement only; no new code. Computed at promotion time.

Obligation 7 — Frontier-baseline comparison on identical items

Requirement. Run the holdout split through at least one frontier LLM baseline (citation-only, no live API call) and publish:

• Both raw scores
• A per-item disagreement matrix (CORE-correct × LLM-correct, -wrong, -refused/n/a; CORE-refused × LLM-correct, -wrong; etc.)
• Trace replay verification for every CORE-correct answer

The interesting cell — and the honest one to publish — is "LLM correct ∧ CORE refused". Those are problems where rule-based grammar caps out; refusing them is correct behavior but it leaves capability on the table. The size of this cell is a public, durable measurement of CORE's current grammar coverage vs. frontier LLM breadth. ADR-0120's expert threshold sets a maximum acceptable size.

Falsification. If the comparison report cannot demonstrate trace replay on every CORE-correct answer, the promotion is invalid.

Status. Pattern established by ADR-0045 (long-context comparison); GSM8K equivalent landed in ADR-0119.

Obligation 8 — Adversarial generation; misparse rate zero

Requirement. A separate generator produces problems specifically designed to exploit weak grammar / solver coverage:

• Edge-case phrasings within the documented grammar
• Problems combining patterns in untested ways
• Problems with deceptive surface (e.g. red-herring numbers)

Every adversarial problem must produce one of: correct, refused, or — never — silent misparse. A misparse is defined as: parser produces a graph that does NOT correspond to the surface meaning AND the resulting answer is wrong.

Misparse rate must be zero on the adversarial suite. Refused rate may be arbitrarily high; that's the safe failure mode.

Falsification. Any single observed misparse (graph + answer disagreement with the surface) invalidates the promotion.

Status. Generator authoring required; likely under ADR-0119.

Obligation 9 — Determinism across release boundaries

Requirement. Same problem text + same pack revision + same solver revision → byte-equal trace hash across N runs (N ≥ 100) and across at least one re-build of the runtime (proves no floating-point-platform drift, no thread-order drift, no random seed drift).

Falsification. Any non-determinism observation invalidates the promotion until the source is identified and eliminated.

Status. Already an architectural invariant of CORE (versor-closure, replay-determinism). Per-lane test gates run at promotion time.

Obligation 10 — Operation provenance via the pack

Requirement. Every operation in every published SolutionTrace dispatches through a math-pack (or relevant-domain-pack) lemma identifier, not a hardcoded string in solver code. The trace includes the resolved lemma id for every operation, and changing the pack changes the resolved set deterministically.

This obligation makes "reasons from concepts" architecturally true rather than rhetorical. Without it, the parser-to-pack binding is informal and the claim "the math pack provides the operation vocabulary" is decorative.

Falsification. If any operation in a published trace cannot resolve to a pack-lemma id, the promotion is invalid.

Status. Currently informal (parser hardcodes verb→operation-kind mapping in ADR-0115 Phase 1.3). Closing this gap is in-scope for ADR-0116 (solver). ADR-0114a documents the requirement; ADR-0116 implements the binding.

---

Acceptance & enforcement

ADR-0114a is a documentation-only contract. No code lands with this ADR.

It binds future ADRs:

• ADR-0116 (solver) — must add operation-provenance binding (#10) and trace shape that supports #3.
• ADR-0117 (verifier) — must produce replay-verdicts that support #3 and #9.
• ADR-0118 / ADR-0118a (realizer + OOD surface generator) — must produce OOD-rendering capability for #2.
• ADR-0119 (GSM8K eval lane) — must wire #1, #6, #7, #8 into the lane runner.
• ADR-0120 (first expert promotion contract) — must require all 10 obligations as hard gates, including the explicit numeric thresholds (zero wrong; ≥ 0.95·S on OOD; flat depth curve within documented ε).

Each downstream ADR cites which obligation it discharges. ADR-0120 finally invokes all ten.

---

Invariants

adr_0114a_obligations_enumerated

The 10 obligations above are the complete, ordered list. Adding an obligation, removing one, or weakening one requires a numbered amendment ADR. The list itself is sticky.

adr_0114a_no_silent_overfit

Any future expert promotion ADR that omits one of the ten obligations from its acceptance criteria is invalid. Reviewers checking promotion ADRs MUST verify the obligations checklist is populated. Skipping the checklist is grounds for refusal at review.

adr_0114a_audit_passed_unaffected

ADR-0114a does NOT amend ADR-0106 / ADR-0109 / ADR-0113. The audit-passed gate continues to verify CORE claim-shape compliance (signed digest + replay determinism + typed refusal + exact recall) without any of these ten obligations. The two tiers measure orthogonal properties.

---

Out of scope

• Specific numeric thresholds. Those belong to ADR-0120 (e.g. "depth curve ε ≤ 0.02"; "OOD score ≥ 0.95 · public_score"). ADR-0114a documents the shape of each obligation, not the numbers.
• Implementation of the perturbation generator. Future ADR.
• Implementation of the adversarial generator. Future ADR.
• LLM-vendor selection for #7 (frontier comparison). ADR-0045 set the convention (citation, not live API); ADR-0119 picks the specific baseline.
• Domains beyond mathematics_logic. The framework is domain-agnostic; each future expert domain (symbolic logic, DSL codegen, ...) inherits it. Per-domain specializations may add obligations but cannot remove any of these ten.
• Writing / open-prose capability. Even with all ten obligations satisfied, prose-domain expert claims need additional discussion (what "correct" means for prose is fuzzily defined); deferred per ADR-0114 §Phase F.

---

Consequences

• The repo carries a public, dated commitment to a falsifiable proof framework for any future expert claim. The "are you sure you're reasoning, not pattern-matching?" question has a written answer: the 10 obligations, every one checkable.
• ADR-0116 / ADR-0117 / ADR-0118 / ADR-0119 / ADR-0120 each gain a subset of these obligations as scope items. Each downstream ADR cites which obligations it discharges.
• The audit-passed tier and the expert tier remain cleanly distinguished. Audit-passed verifies claim shapes (transformer-unreachable invariants); expert verifies capability with anti-overfitting proof. A domain can be one without the other, though in practice audit-passed is a prerequisite for expert.
• External readers (reviewers, investors, skeptics) now have an enumerated checklist to evaluate any future expert claim against. Promotions that omit obligations are easily distinguished from promotions that satisfy them.

---

Open candidate directions (no ADR yet)

• Cross-domain transfer probes. Once two domains land at expert, can CORE solve a problem that requires combining operations from both packs (e.g. physics-units-aware arithmetic)? Not part of these 10 obligations but a natural next-tier question.
• Adversarial generation budget. How many adversarial problems is "enough" for #8? Likely answer: keep generating until refused rate stabilizes. ADR-0119 picks the convention.
• Frontier baseline freshness. ADR-0045's citation freezes vendor numbers at a point in time. Frontier scores drift up; CORE's comparison should be re-cited periodically. The cadence is a governance choice deferred to a future ADR.