diff --git a/docs/decisions/ADR-0114a-anti-overfitting-proof-obligations.md b/docs/decisions/ADR-0114a-anti-overfitting-proof-obligations.md new file mode 100644 index 00000000..c0ee6fbb --- /dev/null +++ b/docs/decisions/ADR-0114a-anti-overfitting-proof-obligations.md @@ -0,0 +1,378 @@ +# 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. diff --git a/docs/decisions/README.md b/docs/decisions/README.md index fbf6c834..7fcf8d59 100644 --- a/docs/decisions/README.md +++ b/docs/decisions/README.md @@ -35,7 +35,8 @@ ADRs record significant architectural decisions: what was decided, why, what alt | [ADR-0112](ADR-0112-runnable-expert-demo-showcase.md) | Runnable Audit-Passed Showcase (originally "Expert-Demo") | Accepted (2026-05-22) | | [ADR-0113](ADR-0113-rename-expert-demo-to-audit-passed.md) | Rename `expert-demo` → `audit-passed`; Reserve `expert` for Future Capability Tier | Accepted (2026-05-22) | | [ADR-0114](ADR-0114-expert-capability-roadmap-gsm8k-first.md) | Expert-Capability Roadmap: GSM8K-Math First | Proposed (2026-05-22) | -| [ADR-0115](ADR-0115-math-problem-parser-and-graph.md) | Math Problem Parser and Typed Proposition Graph | Phase 1.1 Accepted (2026-05-22) | +| [ADR-0114a](ADR-0114a-anti-overfitting-proof-obligations.md) | Anti-Overfitting Proof Obligations for `expert` Promotion | Accepted (2026-05-22) | +| [ADR-0115](ADR-0115-math-problem-parser-and-graph.md) | Math Problem Parser and Typed Proposition Graph | Phase 1.1+1.2+1.3 Accepted (2026-05-22) | --- @@ -67,7 +68,8 @@ The ADR-0091..0114 slate is fully accepted (0091..0113) plus one proposed-roadma - Runnable Audit-Passed Showcase (originally "Expert-Demo"; renamed) — ADR-0112 + ADR-0113 - Rename `expert-demo` → `audit-passed`; reserve `expert` namespace — ADR-0113 - Expert-Capability Roadmap (GSM8K-Math first); proposed — ADR-0114 -- Math Problem Parser & Typed Graph (Phase 1.1 schema + 5 seed cases); Phase 1.2 (45 more cases) delegated — ADR-0115 +- Math Problem Parser & Typed Graph (Phase 1.1 schema + 5 seeds + Phase 1.2 45 more cases + Phase 1.3 parser engine; 50/50 byte-equal) — ADR-0115 +- Anti-Overfitting Proof Obligations for any future `expert` promotion (10-point falsifiable framework) — ADR-0114a ADR-0080 has also landed: Contemplation Loop Phase 1 adds a read-only frontier-compare miner that emits `SPECULATIVE` findings only.