docs(ADR-0131): re-target math expert promotion to architecture-aligned benchmarks (proposed)
Docs-only PR. Follow-up to ADR-0127-0128-RESULTS' Path-B trigger.
Replaces ADR-0120's GSM8K-coverage requirement for the
mathematics_logic expert promotion with a composite gate over
three architecture-aligned benchmarks:
Benchmark 1: Symbolic equivalence (~500 algebra cases, public
+ sealed split). Primary discriminator — CGA exact-recall.
Pass: correct_rate >= 0.95, wrong == 0.
Benchmark 2: CORE-native teaching-corpus eval. Internal
consistency lane sourced from ratified packs (en_arithmetic_v1
+ en_units_v1 + en_numerics_v1). Grammar matches by
construction (no paraphrase-variance gap).
Pass: correct_rate >= 0.95, trace_hash byte-equality, wrong == 0.
Benchmark 3: Bounded-grammar word-problem set (~150 cases,
pre-filtered to ADR-0126/0127/0128 parser scope). Demonstrates
end-to-end pipeline determinism on the in-scope distribution.
Includes adversarial out-of-grammar probes.
Pass: correct_rate >= 0.95, wrong == 0.
Three benchmarks (not one) prevent overfitting per ADR-0114a
and force the math expert to demonstrate three distinct
architectural properties (algebraic correctness, internal
consistency, end-to-end pipeline determinism).
GSM8K stays as a stress-test lane the math expert RUNS but is
NOT gated on. Refusal counts reported in expert-claims artifact
as honest disclosure.
Other 12 ADR-0120 expert-promotion checks UNCHANGED.
Status: Proposed. The contract revision (removing GSM8K from
the gate) is a follow-up implementation PR after sub-phases
0131.1-0131.6 land the new benchmark substrate.
This commit is contained in:
Shay
parent
1950ee0b94
commit
29d916ab16
1 changed files with 329 additions and 0 deletions
329
docs/decisions/ADR-0131-math-expert-rebench.md
Normal file
329
docs/decisions/ADR-0131-math-expert-rebench.md
Normal file
|
|
@ -0,0 +1,329 @@
|
|||
# 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.
|
||||
```
|
||||
Loading…
Reference in a new issue