core/docs/decisions/ADR-0131.3-bounded-grammar.md

42 lines
2.6 KiB
Markdown

# ADR-0131.3 — Benchmark 3: Bounded-Grammar Word Problems
## Status
Accepted
## Date
2026-05-23
## Context
ADR-0131 re-targeted the `mathematics_logic` expert promotion to three architecture-aligned benchmarks. This decision documents the third and final benchmark of the composite expert gate (ADR-0131.3): bounded-grammar word problems.
Historically, evaluating algebraic cognitive systems against datasets like GSM8K created a paraphrase-chasing trap. GSM8K rewards natural language flexibility over algebraic soundness, leading to statistical coercion or approximate nearest-neighbor fallback, which violates CORE's core invariants.
B3 establishes the alternative, architecture-aligned claim: **within a closed, bounded grammar, the engine must achieve deterministic, 100% end-to-end correctness.**
## Decision
Establish the `math_bounded_grammar` lane under `evals/math_bounded_grammar/v1/`.
### 1. Bounded Grammar as Scope Statement, Not Coverage Claim
The bounded grammar is an explicit, reviewable contract. We declare that the architecture solves problems *only* within this grammar; any input outside it must trigger a typed refusal. Wide coverage of arbitrary natural-language phrasing is out of scope for this benchmark and is deferred to future grammar-expansion ADRs (v1.B / v2).
The templates recognized cover the full typed math pipeline established under:
- Parser & Math Graph: ADR-0115
- Deterministic Solver: ADR-0116
- Trace Verifier: ADR-0117
- Binding Graph: ADR-0132 through ADR-0135
### 2. Dataset Design
We curate a version-pinned set of 50 word problems split across:
- `solved_correct` (35 cases): Grammar-conformant problems with unique correct numeric answers, exercising all 8 operation kinds (`add`, `subtract`, `transfer`, `multiply`, `divide`, `apply_rate`, `compare_additive`, `compare_multiplicative`).
- `solved_wrong` (5 cases): Grammar-conformant problems whose expected answers are deliberately wrong, validating that the verifier/runner catches mismatch errors and that the `wrong == 0` check is load-bearing.
- `refused` (10 cases): Out-of-grammar problems testing clean, typed parser-level or solver-level refusals.
### 3. Exit Criteria
- `wrong == 0` across all three classes.
- `correct_rate >= 0.95`.
- Deterministic byte-equality of the output `report.json` across consecutive runs.
## Consequences
- The B3 benchmark provides a clean, inspectable contract of what CORE can and cannot parse.
- Any future grammar expansions must be explicitly added to the bounded grammar specification (`grammar.md`) and verified by regression tests.
- Refusal remains a first-class, defensive property of the cognitive engine.