core/docs/decisions/ADR-0131-math-expert-rebench.md

# ADR-0131 — Re-Target Math Expert Promotion to Architecture-Aligned Benchmarks

**Status:** Proposed
**Date:** 2026-05-23
**Author:** CORE agents + reviewers
**Depends on:** ADR-0114a (10 anti-overfitting obligations), ADR-0119
(+ 8 sub-phases), ADR-0120 (expert promotion contract), ADR-0121
(math expert promotion deferred), ADR-0126 (candidate-graph parser),
ADR-0127 (units pack), ADR-0128 (numerics pack),
ADR-0127-0128-RESULTS (Path-B trigger evidence)
**Supersedes:** the GSM8K-coverage requirement in ADR-0120's
`expert` gate for the `mathematics_logic` domain. The other 12 of
ADR-0120's 13 checks remain unchanged.

---

## Context

ADR-0121 deferred the `mathematics_logic` → `expert` promotion with
named blocker `correct_rate = 0/1319 on sealed GSM8K`. The
project then ran a four-ADR arc to address that blocker:

| ADR | Hypothesis | Sealed-lift result |
|-----|-----------|-------------------|
| ADR-0122 | per-rate-shape grammar expansion | 0 / 1319 |
| ADR-0123 / 0123a / 0123b | comparison-phrasing + upstream shape gaps | 0 / 1319 |
| ADR-0126 (architectural pivot) | candidate-graph topology replaces fail-hard parser | 0 / 50 train sample |
| ADR-0127 + ADR-0128 (substrate) | exhaustive units + numerics packs feed the new architecture | 0 / 50 train sample |

`ADR-0127-0128-RESULTS` documents the architectural verdict: the
full deterministic design (candidate-graph + units + numerics +
pack-aware parser) is correct, complete, replay-deterministic,
and produces zero coverage on the GSM8K train sample. The
refusal-cause breakdown shows 27/50 refusals are OTHER_SHAPE
gaps (cross-statement pronouns, possessives, subordinate clauses,
multi-word entities, multi-step inference) that no pack
substrate can address.

The empirical finding is unambiguous: **GSM8K's distribution is
not parseable by any deterministic rule set at the per-statement
parse rate the substrate enables.** GSM8K rewards paraphrase
flexibility — which is the one thing CORE's algebraic substrate
is structurally weakest at — and undervalues exact recall,
provenance, and replay determinism — which are CORE's structural
strengths.

This ADR re-targets the math expert promotion to benchmarks
that *measure what CORE actually excels at*, rather than
penalizing it for the one axis it doesn't optimize for.

---

## Decision

Define the `mathematics_logic` expert promotion contract in terms
of **three complementary benchmarks**, each measuring a
discriminator the architecture should excel at. All three must
pass at their respective thresholds, AND the other 12 ADR-0120
checks must hold. **The GSM8K-coverage requirement is removed.**

### Benchmark 1 — Symbolic equivalence (primary discriminator)

**What:** Given two algebraic expressions A and B, the engine
must determine whether `A ≡ B` (algebraically equivalent) under
the CGA substrate's exact-recall semantics. Coverage scope:
polynomials in 1–4 variables, rational expressions, equations in
standard form, factored forms, expanded forms.

**Why:** This is *exactly* what CGA exact-recall is built for.
There is no paraphrase-variance ceiling. The discriminator is
algebraic correctness, which is the architecture's strongest
axis.

**Dataset:** Curated, ratified, version-pinned. Initial scope:
~500 (A, B, label) triples drawn from algebra-1 / algebra-2 /
precalc symbolic-equivalence canon. Mirror the
`evals/gsm8k_math/holdouts/v1/cases.jsonl.age` sealing pattern:
public-split + sealed-holdout, never-decrypted-by-CI.

**Pass criterion:** `correct_rate ≥ 0.95 on public split AND on
sealed holdout`. `wrong == 0` invariant preserved. (The high
threshold is appropriate because the architecture has no
structural disadvantage on this task.)

### Benchmark 2 — CORE-native teaching-corpus eval (lane gate)

**What:** Run the math expert against the math teaching corpus's
own evaluation lane. Problems are sourced from ratified
teaching chains in `language_packs/data/en_arithmetic_v1` +
en_units_v1 + en_numerics_v1; the parser's grammar matches the
corpus's surface forms *by construction* (no paraphrase-variance
gap because both sides of the eval consume the same ratified
substrate).

**Why:** This is the lane that proves the math expert is
internally consistent with the ratified knowledge it claims to
encode. If this lane fails, the engine cannot reliably evaluate
its own teaching corpus — a deeper problem than any
external-benchmark coverage gap.

**Pass criterion:** `correct_rate ≥ 0.95 on the corpus eval AND
trace_hash byte-equality across replay AND wrong == 0`. This
mirrors the existing cognition-lane gate pattern.

### Benchmark 3 — Bounded-grammar word-problem set (operator surface)

**What:** A small (~150 cases), ratified, hand-curated set of
single-statement-style word problems whose surface forms are
*pre-filtered* to match the ADR-0126/0127/0128 parser scope.
Lane purpose: demonstrate the end-to-end pipeline produces correct
answers on the *in-scope* word-problem distribution.

**Why:** This is the honest version of the GSM8K claim. We are
explicitly *not* claiming to solve arbitrary natural-language
math word problems. We *are* claiming to solve word problems
that fall within a well-defined, externally-inspectable grammar
contract. The bounded-grammar set is the externally-reviewable
proof of that claim.

**Curation policy** (load-bearing):
- Every problem must be solvable by the current parser pipeline
  *without future grammar extensions* — the set proves coverage
  of a fixed grammar, not a moving target.
- Every problem ships with a "shape category" tag
  (`canonical_has_buys`, `there_are_count`, `substance_qualifier`,
  `compare_additive`, etc.) drawn from a closed set documented
  in the lane's README.
- No problem may be added that requires inference beyond a
  single statement's parse. Multi-step problems are excluded
  by design.
- Adversarial probes ensure the parser refuses (`wrong == 0`)
  on out-of-grammar shapes even when those shapes appear
  superficially similar to in-scope shapes.

**Pass criterion:** `correct_rate ≥ 0.95 on public split AND on
sealed holdout`. `wrong == 0` preserved including on adversarial
out-of-grammar shapes.

### Composite expert-promotion gate

For the `mathematics_logic` domain, the `expert` promotion
contract (ADR-0120) is revised:

| ADR-0120 check | Status under ADR-0131 |
|---|---|
| `audit_passed` holds | unchanged |
| ADR-0114a obligations #1–#10 | unchanged |
| Signed `expert_claims` entry with reproducible digest | unchanged |
| **`correct_rate ≥ 0.60` on public AND sealed holdout** | **REVISED:** replaced by composite requirement: Benchmark 1 ≥ 0.95 AND Benchmark 2 ≥ 0.95 AND Benchmark 3 ≥ 0.95, each with `wrong == 0` |
| `wrong == 0` enforcement | strengthened (now three lanes) |

GSM8K is **retained as a stress-test lane** that the math expert
*runs* but is *not gated on*. GSM8K refusal counts are reported
in the expert-claims artifact as honest disclosure ("here's what
we can't do") without blocking promotion.

---

## Why three benchmarks instead of one

A single benchmark is brittle: if the gate is set against any
one of them, that benchmark becomes the optimization target and
the architecture risks the same overfitting pathology ADR-0114a
was written to prevent. Three orthogonal benchmarks force the
math expert to demonstrate three distinct architectural
properties:

| Property | Benchmark that tests it |
|----------|------------------------|
| Algebraic correctness under exact recall | Benchmark 1 |
| Internal consistency with ratified teaching substrate | Benchmark 2 |
| End-to-end pipeline determinism on in-scope NL inputs | Benchmark 3 |

A pass on all three is a meaningful claim. A pass on any one in
isolation is not.

---

## Alternatives considered

### A. Keep GSM8K as the gate; lower the threshold (e.g., 0.20).
**Rejected.** ADR-0114a Obligation #4 ("wrong rate strictly
zero") AND the 4-ADR-zero-lift evidence both point against
optimizing for a benchmark the architecture cannot meaningfully
move. Lowering the threshold to fit our actual result is exactly
the goalpost-shifting that ADR-0114a was written to forbid.

### B. Switch to a single new benchmark (MATH symbolic subset).
**Considered.** MATH (Hendrycks et al.) has many of the same
paraphrase-variance issues GSM8K has. Symbolic-equivalence
problems are a *subset* of MATH and are the right discriminator,
but the rest of MATH would reproduce the GSM8K trap.

### C. Switch to MMLU-Math.
**Rejected.** Multiple-choice format is the wrong shape for the
architecture — it rewards calibrated guessing, which violates
`wrong == 0`. Refusing-on-uncertainty would surface as
"selected the wrong option" rather than "abstained," collapsing
the architecture's primary defensive property.

### D. Use a theorem-proving subset (miniF2F-style).
**Rejected for now.** Theorem proving is further from the
current substrate's capabilities than algebraic equivalence.
Worth revisiting as a future expansion of the math expert's
scope after ADR-0131 lands.

### E. Define the expert promotion in terms of CORE-native eval only (Benchmark 2 alone).
**Rejected.** External reviewability matters. Benchmark 2 alone
would be self-graded and lack the discipline of an external
discriminator. Benchmarks 1 and 3 provide that discipline.

### F. Skip the expert promotion entirely; keep math at audit-passed indefinitely.
**Considered.** The math substrate is already useful at
audit-passed tier. But the expert tier exists for a reason
(stronger claims, broader operator trust, downstream
dependencies). Indefinite deferral is a worse outcome than
re-targeted promotion.

---

## Exit criterion for ADR-0131 itself

ADR-0131 becomes Accepted when:

1. The composite benchmark definitions (Benchmarks 1, 2, 3) are
   ratified — initial dataset curation + sealed-holdout
   encryption + lane runner code + ratification tests all land.
2. The `mathematics_logic` domain re-runs the revised promotion
   contract and either passes (promotion lands) or fails on a
   specific named benchmark (which becomes the next blocker).
3. ADR-0121's `gap:mathematics_logic_expert_first_attempt_deferred`
   entry in `docs/gaps.md` is updated to reflect the new gate
   structure.

Until that work lands, ADR-0131 remains **Proposed** — the
GSM8K-coverage requirement is *not yet removed from ADR-0120*.
This ADR documents the proposed direction; the actual contract
revision is a follow-up implementation PR.

---

## Implementation plan (proposed sub-phases)

| Phase | Module / Lane | Description |
|-------|---------------|-------------|
| 0131.1 | `evals/math_symbolic_equivalence/` | Benchmark 1 substrate: dataset, public/sealed split, lane runner, ratification tests |
| 0131.2 | `evals/math_teaching_corpus_lane/` | Benchmark 2 substrate: pull from ratified packs, lane runner, byte-equality replay gate |
| 0131.3 | `evals/math_bounded_grammar_v1/` | Benchmark 3 substrate: hand-curated cases with shape-category tags, public/sealed split, adversarial probes |
| 0131.4 | `formation/ratify.py` + `formation/promote.py` | Update expert-promotion gate to consult the composite benchmark result |
| 0131.5 | `docs/decisions/ADR-0120-amendment.md` | Companion amendment to ADR-0120 documenting the composite gate; cross-reference ADR-0131 |
| 0131.6 | Re-run promotion attempt | Run revised gate; emit expert-claims artifact; either land promotion or open new named-blocker ADR |

Regression gates (must remain green at every phase):
- `core test --suite smoke -q`
- `core test --suite math -q` (existing 700+)
- `core test --suite packs -q` (en_units_v1 + en_numerics_v1 ratification)
- ADR-0126 candidate-graph test suite

---

## What this does NOT do

- Does NOT discard the GSM8K work. The substrate (ADR-0126 / 0127 /
  0128) stays in main as load-bearing infrastructure. GSM8K stays
  as a stress-test lane with honest-disclosure refusal counts.
- Does NOT weaken ADR-0114a obligations. All 10 remain unchanged;
  `wrong == 0` is *strengthened* (now three lanes instead of one).
- Does NOT introduce stochastic, learned, or LLM-assisted
  components anywhere in the math expert pipeline.
- Does NOT promote math to expert by fiat. Promotion still
  requires the composite gate to pass on real datasets that have
  to be built (sub-phases 0131.1–0131.3).
- Does NOT pre-judge whether the math expert will pass the new
  gate. The architecture's actual coverage on symbolic
  equivalence + corpus eval + bounded grammar is an empirical
  question that 0131.6 answers. The bet is that the architecture
  excels on these benchmarks because they align with its
  structural strengths; the bet may or may not pay off.

---

## Composition with other in-flight work

- **ADR-0129 + ADR-0130 (deferred teaching-loop ADRs):** these
  become more interesting once a stable correction-store
  population exists. Benchmark 2 (teaching-corpus eval) is the
  natural surface where reviewed corrections accumulate; if
  ADR-0131 promotes math to expert, the corrections from
  Benchmark 2's failures become the population that triggers
  ADR-0129/0130's un-deferral exit criteria.
- **Future language packs (`es_units_v1`, etc.):** Benchmarks 1
  and 3 are inherently language-bound. Cross-language expansion
  would require parallel benchmark sets per language.
- **Future domain expansions** (physics, etc.): the three-
  benchmark composite pattern this ADR introduces is a template
  that other domain expert promotions can adopt with their own
  domain-specific Benchmark 1 / 2 / 3 definitions.

---

## PR checklist (when proposing for acceptance + sub-phase implementations)

```
What capability did this add/protect?
  → Re-targeted math expert promotion gate to architecture-
    aligned benchmarks; preserves wrong == 0 across three lanes
    instead of one; honest disclosure of GSM8K refusal counts
    without GSM8K-coverage gating.
What invariant proves the field remains valid?
  → wrong == 0 enforced across all three new benchmark lanes
    (strengthened from previous single-lane enforcement).
    Replay determinism, pack-binding, trace_hash byte-equality
    all preserved.
Which CLI suite/eval proves the lane?
  → New: `core test --suite math-symbolic-equivalence`,
    `core test --suite math-teaching-corpus`,
    `core test --suite math-bounded-grammar`. Plus existing
    smoke + math + packs.
Did this avoid hidden normalization, stochastic fallback,
approximate recall, unreviewed mutation?
  → Yes. All three benchmarks are deterministic, ratified,
    version-pinned. No LLM-assisted scoring. No probabilistic
    thresholds for refusal.
If it touches user input, what trust boundary was enforced?
  → No new user-input surfaces. Sealed-holdout encryption
    pattern mirrors ADR-0119.7. Public split is unsealed by
    design. Adversarial probes in Benchmark 3 are bounded by
    the lane's curation policy.
```