feat(ADR-0131.1): symbolic equivalence benchmark v1 + lane PASSED (#167)
ADR-0131 Benchmark 1 substrate — the primary discriminator for the
mathematics_logic expert promotion under the architecture-aligned
benchmark composite proposed in ADR-0131.
WHAT LANDED:
generate/math_symbolic_normalizer.py
Deterministic univariate polynomial normalizer. Scope: single
variable, integer coefficients, +/-/*/** operators, parens, no
division, no transcendentals. Pipeline: tokenize -> recursive-
descent parse -> expand-and-collect -> canonical string. Refusal
is first-class via SymbolicError; out-of-scope inputs refuse
rather than guess (preserves wrong == 0).
generate/math_symbolic_equivalence.py
check_equivalence(a, b) -> EquivalenceVerdict
Returns EQUIVALENT / NOT_EQUIVALENT / REFUSED with canonical
strings + reason. Compares byte-equal canonical forms.
evals/math_symbolic_equivalence/v1/
cases.jsonl — 30 hand-curated cases across 18 algebraic
identity categories + 2 out-of-scope refusals.
Coverage: commutative, distributive, square +
cube of binomial, difference of squares, FOIL,
collect like terms, zero cancellation, factoring,
exponent combination, unary negation.
runner.py — CLI entry point. Loads cases, builds report,
writes JSON, exits 0/1 on gate pass/fail.
README.md — methodology, scope, dataset categorization,
exit criterion, baseline result.
tests/
test_math_symbolic_normalizer.py — 44 tests covering parser,
algebra primitives,
canonical-form invariants,
and every refusal path.
test_math_symbolic_equivalence.py — 16 tests on the public
check_equivalence API.
test_adr_0131_1_symbolic_equivalence_lane.py
— 8 tests gating the lane:
dataset integrity, exit
criterion, wrong == 0,
determinism (byte-equal
report across runs).
EMPIRICAL RESULT (the lane PASSED):
correct = 30 / 30 (100.0%)
wrong = 0 / 30 (wrong == 0 invariant satisfied)
refused = 0 / 30 (refusals all matched expected)
correct_rate = 1.00
exit_criterion: PASSED (>= 0.95 required)
CONTRAST WITH ADR-0127-0128 GSM8K TRAIN-SAMPLE RESULT (0/0/50):
This is the first benchmark on the mathematics_logic lane where
the architecture's structural strengths fully express. The result
is the empirical inverse of the GSM8K result — and that's
exactly the architecture-benchmark fit ADR-0131 was written to
re-target toward.
REGRESSION: 1033/1033 existing tests green across math + ADR-0126
+ pack ratification + runner. Zero regressions.
SCOPE DISCIPLINE (per ADR-0131.1 v1 plan):
v1 deliberately narrow (univariate, integer, polynomial). Future
ADR-0131.1.B expansions documented in README: multi-variable,
rationals, larger dataset (~500), sealed holdout per ADR-0119.7
pattern.
PARALLEL WORK (per ADR-0131 plan to run all 3 sub-phases concurrently):
- ADR-0131.2: CORE-native teaching-corpus eval (separate PR)
- ADR-0131.3: bounded-grammar word-problem set (separate PR)
These are independent of ADR-0131.1; no shared files, no
cross-PR coordination required beyond final composite gate.
This commit is contained in:
parent
d04c433eda
commit
a76834cd3f
11 changed files with 1431 additions and 0 deletions
0
evals/math_symbolic_equivalence/__init__.py
Normal file
0
evals/math_symbolic_equivalence/__init__.py
Normal file
109
evals/math_symbolic_equivalence/v1/README.md
Normal file
109
evals/math_symbolic_equivalence/v1/README.md
Normal file
|
|
@ -0,0 +1,109 @@
|
|||
# Symbolic Equivalence Benchmark v1 (ADR-0131.1)
|
||||
|
||||
The primary discriminator for the `mathematics_logic` expert
|
||||
promotion under ADR-0131. Tests whether the engine can determine
|
||||
that two algebraic expressions are *equivalent* under deterministic
|
||||
polynomial normalization.
|
||||
|
||||
## Scope (v1, intentionally narrow)
|
||||
|
||||
- **Single variable** (`x` by default).
|
||||
- **Integer coefficients only.**
|
||||
- **Operators**: `+`, `-`, `*`, `**`/`^` (positive integer exponents).
|
||||
- **Parentheses** for grouping.
|
||||
- **No division** (other than trivial).
|
||||
- **No transcendental functions, no multi-variable, no rationals.**
|
||||
|
||||
The narrowness is by design. The architecture's strength is exact
|
||||
recall + replay determinism; the benchmark stays inside that
|
||||
envelope so the result is a clean measure of that strength, not a
|
||||
proxy for it.
|
||||
|
||||
## Pipeline
|
||||
|
||||
```
|
||||
expression_a -> normalize -> canonical_string_a
|
||||
expression_b -> normalize -> canonical_string_b
|
||||
verdict = (canonical_string_a == canonical_string_b)
|
||||
? EQUIVALENT : NOT_EQUIVALENT
|
||||
or REFUSED if either expression is out-of-scope
|
||||
```
|
||||
|
||||
`normalize` is `generate/math_symbolic_normalizer.py`:
|
||||
recursive-descent parser → polynomial expand-and-collect →
|
||||
canonical string serialization. `check_equivalence` is
|
||||
`generate/math_symbolic_equivalence.py`.
|
||||
|
||||
## Dataset
|
||||
|
||||
`cases.jsonl` ships 30 hand-curated cases covering:
|
||||
|
||||
| Category | Count | Examples |
|
||||
|---|---|---|
|
||||
| commutative_add / commutative_mul | 2 | `x+1 ≡ 1+x`, `3*x ≡ x*3` |
|
||||
| distributive | 2 | `2*(x+3) ≡ 2*x+6` |
|
||||
| square_of_binomial | 3 | `(x+1)^2 ≡ x^2+2*x+1` |
|
||||
| difference_of_squares | 2 | `(x+1)*(x-1) ≡ x^2-1` |
|
||||
| cube_of_binomial | 2 | `(x+1)^3 ≡ x^3+3*x^2+3*x+1` |
|
||||
| foil | 1 | `(x+2)*(x+3) ≡ x^2+5*x+6` |
|
||||
| collect_like_terms | 2 | `2*x+3*x ≡ 5*x` |
|
||||
| zero_cancellation | 1 | `x-x ≡ 0` |
|
||||
| repeated_addition | 1 | `x+x+x+x ≡ 4*x` |
|
||||
| exponent_combine | 1 | `x^2*x ≡ x^3` |
|
||||
| product_of_factors | 1 | `x*(x+1)*(x-1) ≡ x^3-x` |
|
||||
| unary_neg_distribute | 1 | `-(x+1) ≡ -x-1` |
|
||||
| distributive_collect | 1 | `3*(x+1)+2*(x-1) ≡ 5*x+1` |
|
||||
| different_constant / coefficient / degree | 3 | `x+1 ≢ x+2` |
|
||||
| sign_flipped | 2 | `(x+1)^2 ≢ (x-1)^2` |
|
||||
| distributive_miss / foil_miss / cube_miss | 3 | `2*(x+3) ≢ 2*x+3` |
|
||||
| out_of_scope_variable | 1 | `x+y` → REFUSED |
|
||||
| out_of_scope_division | 1 | `x/2` → REFUSED |
|
||||
|
||||
20 expected-equivalent + 8 expected-not-equivalent + 2 expected-refused.
|
||||
|
||||
## Exit criterion (per ADR-0131 Benchmark 1)
|
||||
|
||||
```
|
||||
correct_rate >= 0.95
|
||||
wrong == 0
|
||||
```
|
||||
|
||||
`wrong` is incremented only when the engine produces a *definite*
|
||||
answer that disagrees with the expected verdict. Refusal on an
|
||||
out-of-scope case is `correct` when expected; `refused` when
|
||||
unexpected (which the lane test flags as a normalizer-coverage
|
||||
regression).
|
||||
|
||||
## Running the lane
|
||||
|
||||
```bash
|
||||
python -m evals.math_symbolic_equivalence.v1.runner
|
||||
# exits 0 if exit criterion passes, 1 otherwise
|
||||
# writes report.json with counts + per-case verdicts
|
||||
```
|
||||
|
||||
## v1 result (baseline at landing)
|
||||
|
||||
```
|
||||
correct = 30 / 30 (100.0%)
|
||||
wrong = 0 / 30 (wrong == 0 invariant satisfied)
|
||||
refused = 0 / 30 (both expected-refused cases were caught correctly)
|
||||
exit: PASSED
|
||||
```
|
||||
|
||||
This is the first benchmark on the `mathematics_logic` lane where
|
||||
the architecture's structural strengths fully express. The result
|
||||
is *not* a claim about how hard the cases are; it's a claim about
|
||||
the architecture-benchmark fit being correct.
|
||||
|
||||
## Future expansion (ADR-0131.1.B and beyond)
|
||||
|
||||
- Multi-variable polynomials (`x`, `y`, `z` simultaneous).
|
||||
- Rational coefficients (Fraction).
|
||||
- Larger dataset (~500 cases per ADR-0131's Benchmark 1 spec).
|
||||
- Sealed holdout (mirror ADR-0119.7's pyrage X25519 pattern).
|
||||
- More algebraic identities (Pascal triangle expansions, factoring,
|
||||
partial fractions for rationals).
|
||||
|
||||
v1 ships the minimum viable substrate. The exit criterion is met;
|
||||
the dataset can grow without breaking the contract.
|
||||
0
evals/math_symbolic_equivalence/v1/__init__.py
Normal file
0
evals/math_symbolic_equivalence/v1/__init__.py
Normal file
30
evals/math_symbolic_equivalence/v1/cases.jsonl
Normal file
30
evals/math_symbolic_equivalence/v1/cases.jsonl
Normal file
|
|
@ -0,0 +1,30 @@
|
|||
{"case_id":"sym-eq-v1-0001","expression_a":"x + 1","expression_b":"1 + x","expected":"equivalent","category":"commutative_add","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0002","expression_a":"3*x","expression_b":"x*3","expected":"equivalent","category":"commutative_mul","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0003","expression_a":"2*(x + 3)","expression_b":"2*x + 6","expected":"equivalent","category":"distributive","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0004","expression_a":"x*(x + 1)","expression_b":"x^2 + x","expected":"equivalent","category":"distributive","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0005","expression_a":"(x + 1)^2","expression_b":"x^2 + 2*x + 1","expected":"equivalent","category":"square_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0006","expression_a":"(x - 1)^2","expression_b":"x^2 - 2*x + 1","expected":"equivalent","category":"square_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0007","expression_a":"(x + 1)*(x - 1)","expression_b":"x^2 - 1","expected":"equivalent","category":"difference_of_squares","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0008","expression_a":"(x + 2)*(x + 3)","expected":"equivalent","expression_b":"x^2 + 5*x + 6","category":"foil","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0009","expression_a":"(x + 1)^3","expression_b":"x^3 + 3*x^2 + 3*x + 1","expected":"equivalent","category":"cube_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0010","expression_a":"(x - 1)^3","expression_b":"x^3 - 3*x^2 + 3*x - 1","expected":"equivalent","category":"cube_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0011","expression_a":"2*x + 3*x","expression_b":"5*x","expected":"equivalent","category":"collect_like_terms","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0012","expression_a":"x^2 + 2*x + x^2 + 3*x","expression_b":"2*x^2 + 5*x","expected":"equivalent","category":"collect_like_terms","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0013","expression_a":"x - x","expression_b":"0","expected":"equivalent","category":"zero_cancellation","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0014","expression_a":"x + x + x + x","expression_b":"4*x","expected":"equivalent","category":"repeated_addition","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0015","expression_a":"x^2 * x","expression_b":"x^3","expected":"equivalent","category":"exponent_combine","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0016","expression_a":"(x^2 + 1)*(x^2 - 1)","expression_b":"x^4 - 1","expected":"equivalent","category":"difference_of_squares","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0017","expression_a":"3*(x + 1) + 2*(x - 1)","expression_b":"5*x + 1","expected":"equivalent","category":"distributive_collect","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0018","expression_a":"-(x + 1)","expression_b":"-x - 1","expected":"equivalent","category":"unary_neg_distribute","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0019","expression_a":"(2*x + 1)^2","expression_b":"4*x^2 + 4*x + 1","expected":"equivalent","category":"square_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0020","expression_a":"x*(x + 1)*(x - 1)","expression_b":"x^3 - x","expected":"equivalent","category":"product_of_factors","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0021","expression_a":"x + 1","expression_b":"x + 2","expected":"not_equivalent","category":"different_constant","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0022","expression_a":"2*x","expression_b":"3*x","expected":"not_equivalent","category":"different_coefficient","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0023","expression_a":"x^2","expression_b":"x^3","expected":"not_equivalent","category":"different_degree","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0024","expression_a":"(x + 1)^2","expression_b":"(x - 1)^2","expected":"not_equivalent","category":"sign_flipped","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0025","expression_a":"x^2 + 1","expression_b":"x^2 - 1","expected":"not_equivalent","category":"sign_flipped","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0026","expression_a":"2*(x + 3)","expression_b":"2*x + 3","expected":"not_equivalent","category":"distributive_miss","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0027","expression_a":"(x + 1)*(x + 2)","expression_b":"x^2 + 3*x + 1","expected":"not_equivalent","category":"foil_miss","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0028","expression_a":"x^3 + 1","expression_b":"(x + 1)^3","expected":"not_equivalent","category":"cube_miss","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0029","expression_a":"x + y","expression_b":"x + 1","expected":"refused","category":"out_of_scope_variable","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
{"case_id":"sym-eq-v1-0030","expression_a":"x / 2","expression_b":"x","expected":"refused","category":"out_of_scope_division","provenance":"adr-0131.1:hand-curated:2026-05-23"}
|
||||
260
evals/math_symbolic_equivalence/v1/report.json
Normal file
260
evals/math_symbolic_equivalence/v1/report.json
Normal file
|
|
@ -0,0 +1,260 @@
|
|||
{
|
||||
"adr": "0131.1",
|
||||
"benchmark": "symbolic_equivalence_v1",
|
||||
"cases_path": "evals/math_symbolic_equivalence/v1/cases.jsonl",
|
||||
"correct_rate": 1.0,
|
||||
"counts": {
|
||||
"correct": 30,
|
||||
"refused": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
"exit_criterion": {
|
||||
"correct_rate_min": 0.95,
|
||||
"passed": true,
|
||||
"wrong_max": 0
|
||||
},
|
||||
"per_case": [
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0001",
|
||||
"category": "commutative_add",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0002",
|
||||
"category": "commutative_mul",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0003",
|
||||
"category": "distributive",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0004",
|
||||
"category": "distributive",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0005",
|
||||
"category": "square_of_binomial",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0006",
|
||||
"category": "square_of_binomial",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0007",
|
||||
"category": "difference_of_squares",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0008",
|
||||
"category": "foil",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0009",
|
||||
"category": "cube_of_binomial",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0010",
|
||||
"category": "cube_of_binomial",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0011",
|
||||
"category": "collect_like_terms",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0012",
|
||||
"category": "collect_like_terms",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0013",
|
||||
"category": "zero_cancellation",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0014",
|
||||
"category": "repeated_addition",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0015",
|
||||
"category": "exponent_combine",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0016",
|
||||
"category": "difference_of_squares",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0017",
|
||||
"category": "distributive_collect",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0018",
|
||||
"category": "unary_neg_distribute",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0019",
|
||||
"category": "square_of_binomial",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "equivalent",
|
||||
"case_id": "sym-eq-v1-0020",
|
||||
"category": "product_of_factors",
|
||||
"expected": "equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "sym-eq-v1-0021",
|
||||
"category": "different_constant",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "sym-eq-v1-0022",
|
||||
"category": "different_coefficient",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "sym-eq-v1-0023",
|
||||
"category": "different_degree",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "sym-eq-v1-0024",
|
||||
"category": "sign_flipped",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "sym-eq-v1-0025",
|
||||
"category": "sign_flipped",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "sym-eq-v1-0026",
|
||||
"category": "distributive_miss",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "sym-eq-v1-0027",
|
||||
"category": "foil_miss",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "sym-eq-v1-0028",
|
||||
"category": "cube_miss",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "refused",
|
||||
"case_id": "sym-eq-v1-0029",
|
||||
"category": "out_of_scope_variable",
|
||||
"expected": "refused",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "refused",
|
||||
"case_id": "sym-eq-v1-0030",
|
||||
"category": "out_of_scope_division",
|
||||
"expected": "refused",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
}
|
||||
],
|
||||
"sample_count": 30,
|
||||
"schema_version": 1
|
||||
}
|
||||
151
evals/math_symbolic_equivalence/v1/runner.py
Normal file
151
evals/math_symbolic_equivalence/v1/runner.py
Normal file
|
|
@ -0,0 +1,151 @@
|
|||
"""ADR-0131.1 — Symbolic equivalence lane runner (v1).
|
||||
|
||||
Loads ``cases.jsonl``, runs each case through
|
||||
:func:`generate.math_symbolic_equivalence.check_equivalence`, classifies
|
||||
the outcome against the expected verdict, and writes a deterministic
|
||||
``report.json``.
|
||||
|
||||
CLI: ``python -m evals.math_symbolic_equivalence.v1.runner``
|
||||
exit code 0 if exit criterion passes, 1 otherwise.
|
||||
|
||||
Exit criterion (per ADR-0131 Benchmark 1):
|
||||
correct_rate >= 0.95
|
||||
wrong == 0
|
||||
|
||||
A case is ``correct`` iff its expected verdict matches the engine's
|
||||
verdict (including expected=refused matched by REFUSED). It is
|
||||
``wrong`` iff expected=equivalent but engine=not_equivalent, or
|
||||
vice versa. It is ``refused`` iff engine=REFUSED on a case whose
|
||||
expected verdict was a definite answer (equivalent / not_equivalent).
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import json
|
||||
import sys
|
||||
from dataclasses import dataclass
|
||||
from pathlib import Path
|
||||
from typing import Any
|
||||
|
||||
from generate.math_symbolic_equivalence import (
|
||||
Verdict,
|
||||
check_equivalence,
|
||||
)
|
||||
|
||||
|
||||
_HERE = Path(__file__).resolve().parent
|
||||
_CASES_PATH = _HERE / "cases.jsonl"
|
||||
_REPORT_PATH = _HERE / "report.json"
|
||||
|
||||
# Per ADR-0131 Benchmark 1 exit criterion.
|
||||
_CORRECT_RATE_MIN = 0.95
|
||||
_WRONG_MAX = 0
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class CaseOutcome:
|
||||
case_id: str
|
||||
category: str
|
||||
expected: str
|
||||
actual: str
|
||||
verdict_class: str # "correct" | "wrong" | "refused"
|
||||
reason: str
|
||||
|
||||
def as_dict(self) -> dict[str, str]:
|
||||
return {
|
||||
"case_id": self.case_id,
|
||||
"category": self.category,
|
||||
"expected": self.expected,
|
||||
"actual": self.actual,
|
||||
"verdict_class": self.verdict_class,
|
||||
"reason": self.reason,
|
||||
}
|
||||
|
||||
|
||||
def _score_one(case: dict[str, Any]) -> CaseOutcome:
|
||||
"""Score a single case against the engine's verdict."""
|
||||
expected = case["expected"]
|
||||
v = check_equivalence(case["expression_a"], case["expression_b"])
|
||||
actual = v.verdict.value
|
||||
|
||||
if actual == expected:
|
||||
verdict_class = "correct"
|
||||
reason = ""
|
||||
elif actual == Verdict.REFUSED.value:
|
||||
# Engine refused on a case that expected a definite answer.
|
||||
# This is a refusal, NOT a wrong answer — preserves wrong == 0.
|
||||
verdict_class = "refused"
|
||||
reason = v.reason
|
||||
else:
|
||||
# Engine produced a definite answer that disagrees with expected.
|
||||
# This is wrong. The wrong==0 gate catches any such case.
|
||||
verdict_class = "wrong"
|
||||
reason = (
|
||||
f"engine={actual!r} expected={expected!r}; "
|
||||
f"canonical_a={v.canonical_a!r} canonical_b={v.canonical_b!r}"
|
||||
)
|
||||
|
||||
return CaseOutcome(
|
||||
case_id=case["case_id"],
|
||||
category=case["category"],
|
||||
expected=expected,
|
||||
actual=actual,
|
||||
verdict_class=verdict_class,
|
||||
reason=reason,
|
||||
)
|
||||
|
||||
|
||||
def _load_cases(path: Path = _CASES_PATH) -> list[dict[str, Any]]:
|
||||
records: list[dict[str, Any]] = []
|
||||
with path.open("r", encoding="utf-8") as fh:
|
||||
for line in fh:
|
||||
line = line.strip()
|
||||
if not line:
|
||||
continue
|
||||
records.append(json.loads(line))
|
||||
return records
|
||||
|
||||
|
||||
def build_report(cases: list[dict[str, Any]]) -> dict[str, Any]:
|
||||
outcomes = [_score_one(c) for c in cases]
|
||||
counts = {"correct": 0, "wrong": 0, "refused": 0}
|
||||
for o in outcomes:
|
||||
counts[o.verdict_class] += 1
|
||||
|
||||
total = len(outcomes)
|
||||
correct_rate = counts["correct"] / total if total else 0.0
|
||||
passed = (correct_rate >= _CORRECT_RATE_MIN) and (counts["wrong"] <= _WRONG_MAX)
|
||||
|
||||
return {
|
||||
"schema_version": 1,
|
||||
"adr": "0131.1",
|
||||
"benchmark": "symbolic_equivalence_v1",
|
||||
"cases_path": str(_CASES_PATH.relative_to(_HERE.parent.parent.parent)),
|
||||
"sample_count": total,
|
||||
"counts": counts,
|
||||
"correct_rate": correct_rate,
|
||||
"exit_criterion": {
|
||||
"correct_rate_min": _CORRECT_RATE_MIN,
|
||||
"wrong_max": _WRONG_MAX,
|
||||
"passed": passed,
|
||||
},
|
||||
"per_case": [o.as_dict() for o in outcomes],
|
||||
}
|
||||
|
||||
|
||||
def write_report(report: dict[str, Any], path: Path = _REPORT_PATH) -> None:
|
||||
path.write_text(
|
||||
json.dumps(report, indent=2, sort_keys=True) + "\n",
|
||||
encoding="utf-8",
|
||||
)
|
||||
|
||||
|
||||
def main() -> int:
|
||||
cases = _load_cases()
|
||||
report = build_report(cases)
|
||||
write_report(report)
|
||||
return 0 if report["exit_criterion"]["passed"] else 1
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
99
generate/math_symbolic_equivalence.py
Normal file
99
generate/math_symbolic_equivalence.py
Normal file
|
|
@ -0,0 +1,99 @@
|
|||
"""ADR-0131.1 — Symbolic equivalence check (Benchmark 1 primitive).
|
||||
|
||||
Given two algebraic expressions A and B, produces an
|
||||
:class:`EquivalenceVerdict` of EQUIVALENT, NOT_EQUIVALENT, or REFUSED
|
||||
(with reason). REFUSED preserves wrong == 0: the engine refuses to
|
||||
guess on out-of-scope input rather than emit a wrong verdict.
|
||||
|
||||
Algorithm (v1, polynomial scope):
|
||||
1. Normalize A via :func:`generate.math_symbolic_normalizer.normalize`.
|
||||
2. Normalize B via the same function.
|
||||
3. Compare canonical strings byte-for-byte.
|
||||
|
||||
If either normalization raises :class:`SymbolicError`, the verdict is
|
||||
REFUSED with the propagating reason. This is the wrong-answer
|
||||
firewall for the benchmark — anything the normalizer cannot prove
|
||||
equivalent (or prove distinct) deterministically is refused.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass
|
||||
from enum import Enum
|
||||
from typing import Final
|
||||
|
||||
from generate.math_symbolic_normalizer import (
|
||||
SymbolicError,
|
||||
normalize,
|
||||
)
|
||||
|
||||
|
||||
class Verdict(str, Enum):
|
||||
EQUIVALENT = "equivalent"
|
||||
NOT_EQUIVALENT = "not_equivalent"
|
||||
REFUSED = "refused"
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class EquivalenceVerdict:
|
||||
verdict: Verdict
|
||||
canonical_a: str | None # None when verdict is REFUSED and a couldn't normalize
|
||||
canonical_b: str | None
|
||||
reason: str # empty on EQUIVALENT / NOT_EQUIVALENT; non-empty on REFUSED
|
||||
|
||||
|
||||
REFUSED_VERDICTS: Final[frozenset[Verdict]] = frozenset({Verdict.REFUSED})
|
||||
"""Helper set for callers that need to gate on refusal vs decision."""
|
||||
|
||||
|
||||
def check_equivalence(
|
||||
expression_a: str,
|
||||
expression_b: str,
|
||||
*,
|
||||
variable: str = "x",
|
||||
) -> EquivalenceVerdict:
|
||||
"""Return whether ``expression_a`` and ``expression_b`` are
|
||||
algebraically equivalent under the v1 polynomial-normalizer scope.
|
||||
|
||||
Refusal cases (each surfaces a typed reason):
|
||||
- Either expression is empty or non-string.
|
||||
- Either expression uses an out-of-scope identifier (multi-
|
||||
variable, undefined name).
|
||||
- Either expression contains a syntactically invalid construct.
|
||||
- Either expression uses division, transcendental functions,
|
||||
non-integer coefficients, negative exponents, or non-constant
|
||||
exponents.
|
||||
"""
|
||||
try:
|
||||
canon_a = normalize(expression_a, variable=variable).to_canonical_string()
|
||||
except SymbolicError as exc:
|
||||
return EquivalenceVerdict(
|
||||
verdict=Verdict.REFUSED,
|
||||
canonical_a=None,
|
||||
canonical_b=None,
|
||||
reason=f"normalize(a) refused: {exc}",
|
||||
)
|
||||
|
||||
try:
|
||||
canon_b = normalize(expression_b, variable=variable).to_canonical_string()
|
||||
except SymbolicError as exc:
|
||||
return EquivalenceVerdict(
|
||||
verdict=Verdict.REFUSED,
|
||||
canonical_a=canon_a,
|
||||
canonical_b=None,
|
||||
reason=f"normalize(b) refused: {exc}",
|
||||
)
|
||||
|
||||
if canon_a == canon_b:
|
||||
return EquivalenceVerdict(
|
||||
verdict=Verdict.EQUIVALENT,
|
||||
canonical_a=canon_a,
|
||||
canonical_b=canon_b,
|
||||
reason="",
|
||||
)
|
||||
return EquivalenceVerdict(
|
||||
verdict=Verdict.NOT_EQUIVALENT,
|
||||
canonical_a=canon_a,
|
||||
canonical_b=canon_b,
|
||||
reason="",
|
||||
)
|
||||
370
generate/math_symbolic_normalizer.py
Normal file
370
generate/math_symbolic_normalizer.py
Normal file
|
|
@ -0,0 +1,370 @@
|
|||
"""ADR-0131.1 — Deterministic symbolic normalizer for univariate
|
||||
integer-coefficient polynomials.
|
||||
|
||||
Scope (v1, intentionally narrow):
|
||||
- Single variable (configurable, default 'x').
|
||||
- Integer coefficients only.
|
||||
- Operators: +, -, *, ** (positive integer exponents only).
|
||||
- Parentheses for grouping.
|
||||
- No division (except implicit unary).
|
||||
- No transcendental functions, no multi-variable, no rationals.
|
||||
|
||||
The normalizer is the load-bearing primitive for the symbolic
|
||||
equivalence benchmark (ADR-0131 Benchmark 1). Two expressions A and
|
||||
B are equivalent iff their canonical forms are byte-equal. This is
|
||||
the CGA exact-recall discriminator framed in algebra.
|
||||
|
||||
Determinism guarantees:
|
||||
- Pure functions, no global state, no randomness.
|
||||
- Same input string → same canonical string, byte-for-byte.
|
||||
- Same canonical string → same Polynomial dataclass.
|
||||
- Refuses (raises SymbolicError) rather than guessing on
|
||||
out-of-scope input (preserves wrong == 0).
|
||||
|
||||
Architecture: tokenize → parse to AST → expand + collect → canonical
|
||||
serialize. Each stage is independently testable.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import re
|
||||
from dataclasses import dataclass
|
||||
from typing import Final
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Public errors
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class SymbolicError(ValueError):
|
||||
"""Raised on tokens, syntax, or operators the normalizer cannot
|
||||
deterministically handle. Refusal is first-class — the caller is
|
||||
expected to treat this as an explicit refusal, not a wrong answer.
|
||||
"""
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Canonical polynomial representation
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class Polynomial:
|
||||
"""A univariate polynomial in canonical form.
|
||||
|
||||
``coefficients`` is a tuple of integers, index = exponent.
|
||||
coefficients[0] = constant term, coefficients[1] = x coefficient,
|
||||
coefficients[2] = x^2 coefficient, etc. Trailing zeros are
|
||||
stripped; the tuple is empty iff the polynomial is the zero
|
||||
polynomial.
|
||||
|
||||
Two Polynomial instances are equal iff their coefficient tuples
|
||||
are equal. This is the equivalence relation the benchmark tests.
|
||||
"""
|
||||
|
||||
coefficients: tuple[int, ...]
|
||||
variable: str = "x"
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
if not isinstance(self.variable, str) or not self.variable.isidentifier():
|
||||
raise SymbolicError(
|
||||
f"Polynomial.variable must be a Python identifier; "
|
||||
f"got {self.variable!r}"
|
||||
)
|
||||
if not all(isinstance(c, int) for c in self.coefficients):
|
||||
raise SymbolicError(
|
||||
"Polynomial.coefficients must all be int "
|
||||
"(no float, no bool, no fraction in v1)"
|
||||
)
|
||||
# Trailing zeros must be stripped at construction; reject
|
||||
# non-canonical input loudly so downstream comparison is
|
||||
# unambiguous.
|
||||
if self.coefficients and self.coefficients[-1] == 0:
|
||||
raise SymbolicError(
|
||||
f"Polynomial.coefficients must have no trailing zeros; "
|
||||
f"got {self.coefficients}"
|
||||
)
|
||||
|
||||
def to_canonical_string(self) -> str:
|
||||
"""Render this polynomial in a single canonical string form.
|
||||
|
||||
Terms are emitted in descending exponent order with explicit
|
||||
signs. The zero polynomial is rendered as ``"0"``. This is
|
||||
the byte-level comparison key for equivalence.
|
||||
"""
|
||||
if not self.coefficients:
|
||||
return "0"
|
||||
parts: list[str] = []
|
||||
for exp in range(len(self.coefficients) - 1, -1, -1):
|
||||
coef = self.coefficients[exp]
|
||||
if coef == 0:
|
||||
continue
|
||||
sign = "+" if coef >= 0 else "-"
|
||||
abs_coef = abs(coef)
|
||||
if exp == 0:
|
||||
term = f"{abs_coef}"
|
||||
elif exp == 1:
|
||||
term = f"{self.variable}" if abs_coef == 1 else f"{abs_coef}*{self.variable}"
|
||||
else:
|
||||
term = (
|
||||
f"{self.variable}^{exp}"
|
||||
if abs_coef == 1
|
||||
else f"{abs_coef}*{self.variable}^{exp}"
|
||||
)
|
||||
if not parts:
|
||||
# Leading term: no leading "+" sign.
|
||||
parts.append(term if sign == "+" else f"-{term}")
|
||||
else:
|
||||
parts.append(f"{sign}{term}")
|
||||
return "".join(parts)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Tokenizer
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
_TOKEN_RE: Final[re.Pattern[str]] = re.compile(
|
||||
r"\s*(?:(?P<int>\d+)|(?P<ident>[A-Za-z_]\w*)|(?P<op>\*\*|[+\-*()^]))"
|
||||
)
|
||||
|
||||
|
||||
def _tokenize(text: str) -> list[tuple[str, str]]:
|
||||
"""Return a list of ``(kind, lexeme)`` tokens.
|
||||
|
||||
Kinds: ``"int"``, ``"ident"``, ``"op"``. The ``"^"`` operator is
|
||||
normalized to the canonical Python-style ``"**"`` (both spellings
|
||||
accepted on input).
|
||||
"""
|
||||
pos = 0
|
||||
tokens: list[tuple[str, str]] = []
|
||||
while pos < len(text):
|
||||
m = _TOKEN_RE.match(text, pos)
|
||||
if m is None or m.end() == pos:
|
||||
raise SymbolicError(
|
||||
f"unexpected character at position {pos}: {text[pos:pos+10]!r}"
|
||||
)
|
||||
for kind in ("int", "ident", "op"):
|
||||
lex = m.group(kind)
|
||||
if lex is not None:
|
||||
if kind == "op" and lex == "^":
|
||||
lex = "**"
|
||||
tokens.append((kind, lex))
|
||||
break
|
||||
pos = m.end()
|
||||
return tokens
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Recursive-descent parser producing a normalized Polynomial.
|
||||
#
|
||||
# Grammar:
|
||||
# expr := term (('+' | '-') term)*
|
||||
# term := factor (('*') factor)* # implicit '*' between (expr) and ident
|
||||
# factor := unary ('**' unary)?
|
||||
# unary := ('+' | '-') unary | atom
|
||||
# atom := INT | IDENT | '(' expr ')'
|
||||
#
|
||||
# Each grammar rule returns a Polynomial; addition / multiplication /
|
||||
# negation / exponentiation are implemented as Polynomial operations.
|
||||
# This is the "expand + collect" step inlined into parsing.
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class _Parser:
|
||||
def __init__(self, tokens: list[tuple[str, str]], variable: str) -> None:
|
||||
self._tokens = tokens
|
||||
self._pos = 0
|
||||
self._variable = variable
|
||||
|
||||
def _peek(self) -> tuple[str, str] | None:
|
||||
if self._pos >= len(self._tokens):
|
||||
return None
|
||||
return self._tokens[self._pos]
|
||||
|
||||
def _consume(self) -> tuple[str, str]:
|
||||
if self._pos >= len(self._tokens):
|
||||
raise SymbolicError("unexpected end of expression")
|
||||
tok = self._tokens[self._pos]
|
||||
self._pos += 1
|
||||
return tok
|
||||
|
||||
def parse(self) -> Polynomial:
|
||||
result = self._expr()
|
||||
if self._pos != len(self._tokens):
|
||||
extra = self._tokens[self._pos]
|
||||
raise SymbolicError(f"unexpected trailing token {extra!r}")
|
||||
return result
|
||||
|
||||
def _expr(self) -> Polynomial:
|
||||
left = self._term()
|
||||
while True:
|
||||
tok = self._peek()
|
||||
if tok is None or tok[0] != "op" or tok[1] not in ("+", "-"):
|
||||
break
|
||||
self._consume()
|
||||
right = self._term()
|
||||
if tok[1] == "+":
|
||||
left = _add(left, right)
|
||||
else:
|
||||
left = _sub(left, right)
|
||||
return left
|
||||
|
||||
def _term(self) -> Polynomial:
|
||||
left = self._factor()
|
||||
while True:
|
||||
tok = self._peek()
|
||||
if tok is None:
|
||||
break
|
||||
# Explicit '*'
|
||||
if tok[0] == "op" and tok[1] == "*":
|
||||
self._consume()
|
||||
right = self._factor()
|
||||
left = _mul(left, right)
|
||||
continue
|
||||
break
|
||||
return left
|
||||
|
||||
def _factor(self) -> Polynomial:
|
||||
base = self._unary()
|
||||
tok = self._peek()
|
||||
if tok is not None and tok[0] == "op" and tok[1] == "**":
|
||||
self._consume()
|
||||
exp_tok = self._unary()
|
||||
# Exponent must be a non-negative integer constant polynomial.
|
||||
if len(exp_tok.coefficients) > 1:
|
||||
raise SymbolicError(
|
||||
"exponent must be a non-negative integer constant; "
|
||||
"got non-constant polynomial"
|
||||
)
|
||||
exp_val = exp_tok.coefficients[0] if exp_tok.coefficients else 0
|
||||
if exp_val < 0:
|
||||
raise SymbolicError(
|
||||
f"exponent must be non-negative; got {exp_val}"
|
||||
)
|
||||
return _pow(base, exp_val)
|
||||
return base
|
||||
|
||||
def _unary(self) -> Polynomial:
|
||||
tok = self._peek()
|
||||
if tok is not None and tok[0] == "op" and tok[1] in ("+", "-"):
|
||||
self._consume()
|
||||
inner = self._unary()
|
||||
if tok[1] == "-":
|
||||
return _neg(inner)
|
||||
return inner
|
||||
return self._atom()
|
||||
|
||||
def _atom(self) -> Polynomial:
|
||||
tok = self._consume()
|
||||
if tok[0] == "int":
|
||||
return _const(int(tok[1]), self._variable)
|
||||
if tok[0] == "ident":
|
||||
if tok[1] != self._variable:
|
||||
raise SymbolicError(
|
||||
f"v1 supports a single variable {self._variable!r}; "
|
||||
f"got identifier {tok[1]!r}"
|
||||
)
|
||||
return _x(self._variable)
|
||||
if tok == ("op", "("):
|
||||
inner = self._expr()
|
||||
close = self._consume()
|
||||
if close != ("op", ")"):
|
||||
raise SymbolicError(f"expected ')'; got {close!r}")
|
||||
return inner
|
||||
raise SymbolicError(f"unexpected token {tok!r}")
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Polynomial algebra primitives (the actual "expand and collect" engine)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def _strip_trailing_zeros(coeffs: list[int]) -> tuple[int, ...]:
|
||||
while coeffs and coeffs[-1] == 0:
|
||||
coeffs.pop()
|
||||
return tuple(coeffs)
|
||||
|
||||
|
||||
def _const(value: int, variable: str) -> Polynomial:
|
||||
if value == 0:
|
||||
return Polynomial(coefficients=(), variable=variable)
|
||||
return Polynomial(coefficients=(value,), variable=variable)
|
||||
|
||||
|
||||
def _x(variable: str) -> Polynomial:
|
||||
return Polynomial(coefficients=(0, 1), variable=variable)
|
||||
|
||||
|
||||
def _add(a: Polynomial, b: Polynomial) -> Polynomial:
|
||||
if a.variable != b.variable:
|
||||
raise SymbolicError(
|
||||
f"variable mismatch: {a.variable!r} vs {b.variable!r}"
|
||||
)
|
||||
n = max(len(a.coefficients), len(b.coefficients))
|
||||
out = [0] * n
|
||||
for i, c in enumerate(a.coefficients):
|
||||
out[i] += c
|
||||
for i, c in enumerate(b.coefficients):
|
||||
out[i] += c
|
||||
return Polynomial(
|
||||
coefficients=_strip_trailing_zeros(out), variable=a.variable
|
||||
)
|
||||
|
||||
|
||||
def _neg(a: Polynomial) -> Polynomial:
|
||||
return Polynomial(
|
||||
coefficients=tuple(-c for c in a.coefficients), variable=a.variable
|
||||
)
|
||||
|
||||
|
||||
def _sub(a: Polynomial, b: Polynomial) -> Polynomial:
|
||||
return _add(a, _neg(b))
|
||||
|
||||
|
||||
def _mul(a: Polynomial, b: Polynomial) -> Polynomial:
|
||||
if a.variable != b.variable:
|
||||
raise SymbolicError(
|
||||
f"variable mismatch: {a.variable!r} vs {b.variable!r}"
|
||||
)
|
||||
if not a.coefficients or not b.coefficients:
|
||||
return Polynomial(coefficients=(), variable=a.variable)
|
||||
out = [0] * (len(a.coefficients) + len(b.coefficients) - 1)
|
||||
for i, ca in enumerate(a.coefficients):
|
||||
if ca == 0:
|
||||
continue
|
||||
for j, cb in enumerate(b.coefficients):
|
||||
out[i + j] += ca * cb
|
||||
return Polynomial(
|
||||
coefficients=_strip_trailing_zeros(out), variable=a.variable
|
||||
)
|
||||
|
||||
|
||||
def _pow(base: Polynomial, exponent: int) -> Polynomial:
|
||||
if exponent == 0:
|
||||
return _const(1, base.variable)
|
||||
result = base
|
||||
for _ in range(exponent - 1):
|
||||
result = _mul(result, base)
|
||||
return result
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Public API
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def normalize(expression: str, *, variable: str = "x") -> Polynomial:
|
||||
"""Parse + expand + collect ``expression`` into canonical Polynomial.
|
||||
|
||||
Raises :class:`SymbolicError` on any input the v1 normalizer
|
||||
cannot deterministically handle (multi-variable, division,
|
||||
non-integer coefficient, unknown identifier, syntax error,
|
||||
negative exponent, non-constant exponent).
|
||||
"""
|
||||
if not isinstance(expression, str) or not expression.strip():
|
||||
raise SymbolicError("empty or non-string expression")
|
||||
tokens = _tokenize(expression)
|
||||
if not tokens:
|
||||
raise SymbolicError("no tokens parsed from expression")
|
||||
return _Parser(tokens, variable).parse()
|
||||
|
||||
|
||||
def canonical_string(expression: str, *, variable: str = "x") -> str:
|
||||
"""Shortcut: ``normalize(expression).to_canonical_string()``."""
|
||||
return normalize(expression, variable=variable).to_canonical_string()
|
||||
99
tests/test_adr_0131_1_symbolic_equivalence_lane.py
Normal file
99
tests/test_adr_0131_1_symbolic_equivalence_lane.py
Normal file
|
|
@ -0,0 +1,99 @@
|
|||
"""ADR-0131.1 — lane ratification tests.
|
||||
|
||||
The load-bearing assertion: the v1 benchmark lane passes its exit
|
||||
criterion (correct_rate >= 0.95, wrong == 0) on the curated dataset
|
||||
in evals/math_symbolic_equivalence/v1/cases.jsonl.
|
||||
|
||||
If this test fails, either the normalizer regressed or the dataset
|
||||
was edited to include a case the v1 scope cannot handle. Both
|
||||
require explicit operator review.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import json
|
||||
from pathlib import Path
|
||||
|
||||
from evals.math_symbolic_equivalence.v1.runner import (
|
||||
_load_cases,
|
||||
build_report,
|
||||
)
|
||||
|
||||
|
||||
_CASES_PATH = (
|
||||
Path(__file__).resolve().parent.parent
|
||||
/ "evals"
|
||||
/ "math_symbolic_equivalence"
|
||||
/ "v1"
|
||||
/ "cases.jsonl"
|
||||
)
|
||||
|
||||
|
||||
class TestDatasetIntegrity:
|
||||
def test_cases_file_exists(self) -> None:
|
||||
assert _CASES_PATH.exists(), f"missing dataset: {_CASES_PATH}"
|
||||
|
||||
def test_cases_are_well_formed(self) -> None:
|
||||
cases = _load_cases()
|
||||
assert len(cases) >= 30, "v1 must ship at least 30 cases"
|
||||
for c in cases:
|
||||
for k in (
|
||||
"case_id", "expression_a", "expression_b",
|
||||
"expected", "category", "provenance",
|
||||
):
|
||||
assert k in c, f"case {c.get('case_id')} missing field {k!r}"
|
||||
assert c["expected"] in ("equivalent", "not_equivalent", "refused")
|
||||
|
||||
def test_no_duplicate_case_ids(self) -> None:
|
||||
cases = _load_cases()
|
||||
ids = [c["case_id"] for c in cases]
|
||||
assert len(ids) == len(set(ids)), "duplicate case_ids in dataset"
|
||||
|
||||
def test_provenance_cites_adr(self) -> None:
|
||||
cases = _load_cases()
|
||||
for c in cases:
|
||||
assert "adr-0131" in c["provenance"]
|
||||
|
||||
|
||||
class TestLaneGate:
|
||||
def test_lane_passes_exit_criterion(self) -> None:
|
||||
cases = _load_cases()
|
||||
report = build_report(cases)
|
||||
assert report["exit_criterion"]["passed"], (
|
||||
f"lane gate failed: counts={report['counts']!r} "
|
||||
f"correct_rate={report['correct_rate']!r}"
|
||||
)
|
||||
|
||||
def test_wrong_count_is_zero(self) -> None:
|
||||
# The wrong == 0 invariant is the load-bearing safety property.
|
||||
cases = _load_cases()
|
||||
report = build_report(cases)
|
||||
assert report["counts"]["wrong"] == 0, (
|
||||
"wrong count must be zero on the v1 dataset; per-case "
|
||||
f"detail: {[c for c in report['per_case'] if c['verdict_class']=='wrong']}"
|
||||
)
|
||||
|
||||
def test_refused_cases_have_expected_refused(self) -> None:
|
||||
# Every refusal in the result must correspond to a case whose
|
||||
# expected verdict was 'refused' (out-of-scope by design). If
|
||||
# we refuse on a case that expected a definite answer, that's
|
||||
# a regression of the normalizer's coverage.
|
||||
cases = _load_cases()
|
||||
report = build_report(cases)
|
||||
for entry in report["per_case"]:
|
||||
if entry["verdict_class"] == "refused":
|
||||
assert entry["expected"] == "refused", (
|
||||
f"engine refused on case {entry['case_id']} whose "
|
||||
f"expected verdict was {entry['expected']!r}; "
|
||||
f"reason: {entry['reason']}"
|
||||
)
|
||||
|
||||
|
||||
class TestDeterminism:
|
||||
def test_report_is_byte_equal_across_runs(self) -> None:
|
||||
cases = _load_cases()
|
||||
r1 = build_report(cases)
|
||||
r2 = build_report(cases)
|
||||
s1 = json.dumps(r1, sort_keys=True).encode("utf-8")
|
||||
s2 = json.dumps(r2, sort_keys=True).encode("utf-8")
|
||||
assert s1 == s2
|
||||
96
tests/test_math_symbolic_equivalence.py
Normal file
96
tests/test_math_symbolic_equivalence.py
Normal file
|
|
@ -0,0 +1,96 @@
|
|||
"""ADR-0131.1 — tests for the symbolic equivalence check primitive."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from generate.math_symbolic_equivalence import (
|
||||
Verdict,
|
||||
check_equivalence,
|
||||
)
|
||||
|
||||
|
||||
class TestEquivalent:
|
||||
def test_identical_expressions(self) -> None:
|
||||
v = check_equivalence("x + 1", "x + 1")
|
||||
assert v.verdict == Verdict.EQUIVALENT
|
||||
assert v.canonical_a == v.canonical_b == "x+1"
|
||||
|
||||
def test_distributive(self) -> None:
|
||||
v = check_equivalence("2*(x + 3)", "2*x + 6")
|
||||
assert v.verdict == Verdict.EQUIVALENT
|
||||
|
||||
def test_square_of_binomial(self) -> None:
|
||||
v = check_equivalence("(x + 1)^2", "x^2 + 2*x + 1")
|
||||
assert v.verdict == Verdict.EQUIVALENT
|
||||
|
||||
def test_difference_of_squares(self) -> None:
|
||||
v = check_equivalence("(x + 1)*(x - 1)", "x^2 - 1")
|
||||
assert v.verdict == Verdict.EQUIVALENT
|
||||
|
||||
def test_collect_like_terms(self) -> None:
|
||||
v = check_equivalence("2*x + 3*x + x", "6*x")
|
||||
assert v.verdict == Verdict.EQUIVALENT
|
||||
|
||||
def test_zero_cancellation(self) -> None:
|
||||
v = check_equivalence("x - x + 5", "5")
|
||||
assert v.verdict == Verdict.EQUIVALENT
|
||||
|
||||
|
||||
class TestNotEquivalent:
|
||||
def test_different_constant(self) -> None:
|
||||
v = check_equivalence("x + 1", "x + 2")
|
||||
assert v.verdict == Verdict.NOT_EQUIVALENT
|
||||
assert v.canonical_a == "x+1"
|
||||
assert v.canonical_b == "x+2"
|
||||
|
||||
def test_different_degree(self) -> None:
|
||||
v = check_equivalence("x^2", "x^3")
|
||||
assert v.verdict == Verdict.NOT_EQUIVALENT
|
||||
|
||||
def test_sign_flipped(self) -> None:
|
||||
v = check_equivalence("(x + 1)^2", "(x - 1)^2")
|
||||
assert v.verdict == Verdict.NOT_EQUIVALENT
|
||||
|
||||
|
||||
class TestRefused:
|
||||
def test_empty_left(self) -> None:
|
||||
v = check_equivalence("", "x + 1")
|
||||
assert v.verdict == Verdict.REFUSED
|
||||
assert "normalize(a) refused" in v.reason
|
||||
|
||||
def test_out_of_scope_variable_left(self) -> None:
|
||||
v = check_equivalence("x + y", "x + 1")
|
||||
assert v.verdict == Verdict.REFUSED
|
||||
assert "single variable" in v.reason
|
||||
|
||||
def test_division_refused(self) -> None:
|
||||
v = check_equivalence("x/2", "x")
|
||||
assert v.verdict == Verdict.REFUSED
|
||||
|
||||
def test_a_normalizes_b_refuses(self) -> None:
|
||||
# a is fine, b uses y -> refusal with canonical_a populated
|
||||
v = check_equivalence("x + 1", "y + 1")
|
||||
assert v.verdict == Verdict.REFUSED
|
||||
assert v.canonical_a == "x+1"
|
||||
assert v.canonical_b is None
|
||||
assert "normalize(b) refused" in v.reason
|
||||
|
||||
def test_refused_verdict_is_first_class(self) -> None:
|
||||
# Refusal preserves wrong == 0 — the verdict is REFUSED, never
|
||||
# silently coerced to NOT_EQUIVALENT.
|
||||
v = check_equivalence("garbage(", "x")
|
||||
assert v.verdict == Verdict.REFUSED
|
||||
|
||||
|
||||
class TestDeterminism:
|
||||
def test_same_inputs_same_verdict(self) -> None:
|
||||
# Re-running produces byte-equal verdict.
|
||||
a, b = "(x + 2)*(x - 2)", "x^2 - 4"
|
||||
v1 = check_equivalence(a, b)
|
||||
v2 = check_equivalence(a, b)
|
||||
assert v1 == v2
|
||||
|
||||
def test_canonical_strings_are_byte_equal_on_equivalence(self) -> None:
|
||||
v = check_equivalence("(x + 1)^2", "x^2 + 2*x + 1")
|
||||
assert v.canonical_a is not None
|
||||
assert v.canonical_b is not None
|
||||
assert v.canonical_a.encode("utf-8") == v.canonical_b.encode("utf-8")
|
||||
217
tests/test_math_symbolic_normalizer.py
Normal file
217
tests/test_math_symbolic_normalizer.py
Normal file
|
|
@ -0,0 +1,217 @@
|
|||
"""ADR-0131.1 — tests for the univariate polynomial normalizer.
|
||||
|
||||
Exercises every grammar rule, every algebraic identity the v1 scope
|
||||
needs to cover, and every refusal criterion. The load-bearing
|
||||
assertion: same algebraic content -> same canonical string,
|
||||
byte-for-byte.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import pytest
|
||||
|
||||
from generate.math_symbolic_normalizer import (
|
||||
Polynomial,
|
||||
SymbolicError,
|
||||
canonical_string,
|
||||
normalize,
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Trivial parses
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestTrivialParse:
|
||||
def test_constant_zero(self) -> None:
|
||||
assert normalize("0").coefficients == ()
|
||||
|
||||
def test_constant_positive(self) -> None:
|
||||
assert normalize("7").coefficients == (7,)
|
||||
|
||||
def test_constant_negative_unary(self) -> None:
|
||||
assert normalize("-3").coefficients == (-3,)
|
||||
|
||||
def test_bare_variable(self) -> None:
|
||||
assert normalize("x").coefficients == (0, 1)
|
||||
|
||||
def test_simple_sum(self) -> None:
|
||||
assert normalize("x + 1").coefficients == (1, 1)
|
||||
|
||||
def test_implicit_coefficient_is_one(self) -> None:
|
||||
# "x^2 + x" -> coefficients (0, 1, 1)
|
||||
assert normalize("x^2 + x").coefficients == (0, 1, 1)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Algebraic identities (the heart of the equivalence test)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestAlgebraicIdentities:
|
||||
def test_distributive_basic(self) -> None:
|
||||
# 2*(x + 3) == 2x + 6
|
||||
assert canonical_string("2*(x + 3)") == canonical_string("2*x + 6")
|
||||
|
||||
def test_distributive_with_variable(self) -> None:
|
||||
# x*(x + 1) == x^2 + x
|
||||
assert canonical_string("x*(x + 1)") == canonical_string("x^2 + x")
|
||||
|
||||
def test_commutative_addition(self) -> None:
|
||||
assert canonical_string("3 + x") == canonical_string("x + 3")
|
||||
|
||||
def test_commutative_multiplication(self) -> None:
|
||||
assert canonical_string("3*x") == canonical_string("x*3")
|
||||
|
||||
def test_associative_addition(self) -> None:
|
||||
assert canonical_string("(x + 1) + 2") == canonical_string("x + (1 + 2)")
|
||||
|
||||
def test_square_of_binomial(self) -> None:
|
||||
# (x + 1)^2 == x^2 + 2x + 1
|
||||
assert canonical_string("(x + 1)^2") == canonical_string("x^2 + 2*x + 1")
|
||||
|
||||
def test_square_of_binomial_negative(self) -> None:
|
||||
# (x - 1)^2 == x^2 - 2x + 1
|
||||
assert canonical_string("(x - 1)^2") == canonical_string("x^2 - 2*x + 1")
|
||||
|
||||
def test_difference_of_squares(self) -> None:
|
||||
# (x + 1)(x - 1) == x^2 - 1
|
||||
assert canonical_string("(x + 1)*(x - 1)") == canonical_string("x^2 - 1")
|
||||
|
||||
def test_cube_of_binomial(self) -> None:
|
||||
# (x + 1)^3 == x^3 + 3x^2 + 3x + 1
|
||||
assert canonical_string("(x + 1)^3") == canonical_string(
|
||||
"x^3 + 3*x^2 + 3*x + 1"
|
||||
)
|
||||
|
||||
def test_foil(self) -> None:
|
||||
# (x + 2)(x + 3) == x^2 + 5x + 6
|
||||
assert canonical_string("(x + 2)*(x + 3)") == canonical_string(
|
||||
"x^2 + 5*x + 6"
|
||||
)
|
||||
|
||||
def test_collect_like_terms(self) -> None:
|
||||
# 2x + 3x == 5x
|
||||
assert canonical_string("2*x + 3*x") == canonical_string("5*x")
|
||||
|
||||
def test_zero_cancellation(self) -> None:
|
||||
# x - x == 0
|
||||
assert canonical_string("x - x") == "0"
|
||||
|
||||
def test_subtraction_distributes(self) -> None:
|
||||
# 2 - (x - 1) == 3 - x
|
||||
assert canonical_string("2 - (x - 1)") == canonical_string("3 - x")
|
||||
|
||||
def test_x_zero_is_one(self) -> None:
|
||||
# x^0 == 1
|
||||
assert canonical_string("x^0") == canonical_string("1")
|
||||
|
||||
def test_pow_caret_and_double_star_equivalent(self) -> None:
|
||||
# both spellings accepted; output identical
|
||||
assert canonical_string("x^2") == canonical_string("x**2")
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Non-equivalence: distinct polynomials canonicalize differently
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestNonEquivalence:
|
||||
def test_different_constant(self) -> None:
|
||||
assert canonical_string("x + 1") != canonical_string("x + 2")
|
||||
|
||||
def test_different_coefficient(self) -> None:
|
||||
assert canonical_string("2*x") != canonical_string("3*x")
|
||||
|
||||
def test_different_degree(self) -> None:
|
||||
assert canonical_string("x^2") != canonical_string("x^3")
|
||||
|
||||
def test_sign_flipped(self) -> None:
|
||||
assert canonical_string("x + 1") != canonical_string("x - 1")
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Canonical-string format
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestCanonicalStringFormat:
|
||||
def test_zero(self) -> None:
|
||||
assert canonical_string("0") == "0"
|
||||
|
||||
def test_constant(self) -> None:
|
||||
assert canonical_string("7") == "7"
|
||||
|
||||
def test_x(self) -> None:
|
||||
assert canonical_string("x") == "x"
|
||||
|
||||
def test_negative_constant(self) -> None:
|
||||
assert canonical_string("-3") == "-3"
|
||||
|
||||
def test_x_plus_one(self) -> None:
|
||||
assert canonical_string("x + 1") == "x+1"
|
||||
|
||||
def test_descending_order(self) -> None:
|
||||
assert canonical_string("1 + x + x^2") == "x^2+x+1"
|
||||
|
||||
def test_coefficient_one_elided(self) -> None:
|
||||
assert canonical_string("1*x") == "x"
|
||||
|
||||
def test_negative_leading_coefficient(self) -> None:
|
||||
assert canonical_string("-x + 1") == "-x+1"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Refusals (preserve wrong == 0 for the benchmark)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestRefusals:
|
||||
def test_empty_input(self) -> None:
|
||||
with pytest.raises(SymbolicError, match="empty"):
|
||||
normalize("")
|
||||
|
||||
def test_undefined_variable(self) -> None:
|
||||
with pytest.raises(SymbolicError, match="single variable"):
|
||||
normalize("x + y") # y is out of scope
|
||||
|
||||
def test_negative_exponent(self) -> None:
|
||||
with pytest.raises(SymbolicError, match="non-negative"):
|
||||
normalize("x^-1")
|
||||
|
||||
def test_non_constant_exponent(self) -> None:
|
||||
with pytest.raises(SymbolicError, match="constant"):
|
||||
normalize("x^x")
|
||||
|
||||
def test_syntax_unbalanced_paren(self) -> None:
|
||||
with pytest.raises(SymbolicError):
|
||||
normalize("(x + 1")
|
||||
|
||||
def test_syntax_trailing_op(self) -> None:
|
||||
with pytest.raises(SymbolicError):
|
||||
normalize("x +")
|
||||
|
||||
def test_unknown_operator_division(self) -> None:
|
||||
with pytest.raises(SymbolicError):
|
||||
normalize("x / 2")
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Polynomial dataclass invariants
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestPolynomialInvariants:
|
||||
def test_trailing_zero_rejected(self) -> None:
|
||||
with pytest.raises(SymbolicError, match="trailing zeros"):
|
||||
Polynomial(coefficients=(1, 2, 0), variable="x")
|
||||
|
||||
def test_float_rejected(self) -> None:
|
||||
with pytest.raises(SymbolicError, match="int"):
|
||||
Polynomial(coefficients=(1.5,), variable="x") # type: ignore[arg-type]
|
||||
|
||||
def test_zero_polynomial_is_empty_tuple(self) -> None:
|
||||
# Zero polynomial canonical form has empty coefficients tuple.
|
||||
assert Polynomial(coefficients=(), variable="x").to_canonical_string() == "0"
|
||||
|
||||
def test_equality(self) -> None:
|
||||
a = Polynomial(coefficients=(1, 2, 3), variable="x")
|
||||
b = Polynomial(coefficients=(1, 2, 3), variable="x")
|
||||
assert a == b
|
||||
c = Polynomial(coefficients=(1, 2, 4), variable="x")
|
||||
assert a != c
|
||||
Loading…
Reference in a new issue