169cec710e
* feat(evals): add deterministic symbolic equivalence generated corpus
* feat(evals): add symbolic equivalence replay helpers
* feat(evals): load generated symbolic equivalence corpus
* feat(evals): emit symbolic equivalence replay manifest
* feat(symbolic): support multivariable integer polynomials
* feat(symbolic): support exact rational polynomial coefficients
* feat(symbolic): align equivalence API with multivariable normalization
* test(ADR-0131.1.B): reconcile v1 expectations to v1.B scope expansion
The v1.B refactor (univariate int → sparse multivariable Fraction) deliberately
admits multivariable polynomials and constant-denominator division. The v1
dataset and tests pinned the old refusal behavior, so the lane runner reported
wrong=4 and 10 unit tests failed.
Reconcile:
- cases.jsonl: flip sym-eq-v1-0029 ('x+y' vs 'x+1') and sym-eq-v1-0030
('x/2' vs 'x') from expected=refused to expected=not_equivalent; rename
categories to multivariable_distinct / constant_denominator_distinct;
extend provenance with adr-0131.1b:scope-expanded.
- generated_cases.py: split _refusal_cases into scope_expanded (admits)
and templates (still refused); the first two adversarial cases move to
the scope-expanded list with expected=not_equivalent.
- test_math_symbolic_normalizer.py: replace test_undefined_variable and
test_unknown_operator_division with positive scope-expansion tests +
symbolic-denominator refusal; rewrite TestPolynomialInvariants for the
new terms/variables constructor (Polynomial(terms={...}, variables=(...)))
with float-rejection and zero-coef-collapse invariants.
- test_math_symbolic_equivalence.py: TestRefused.test_empty_left reason
string matches new normalizer error; flip multivariable + constant-
denominator cases to NOT_EQUIVALENT; add symbolic-denominator-refused
case; relax canonical_a assertion in test_a_normalizes_b_refuses (engine
now zeroes both on either-side refusal).
- report.json + manifest.json: regenerated; lane PASS 185/185 wrong=0.
Lane invariants reaffirmed by the new tests: wrong==0, refusal-first for
truly out-of-scope inputs (symbolic denominator, transcendental, malformed,
negative exponent), determinism via byte-equal report.
97 lines
2.8 KiB
Python
97 lines
2.8 KiB
Python
"""ADR-0131.1.B — Symbolic equivalence check.
|
|
|
|
Given two algebraic expressions A and B, produces an
|
|
:class:`EquivalenceVerdict` of EQUIVALENT, NOT_EQUIVALENT, or REFUSED.
|
|
REFUSED preserves wrong == 0: the engine refuses to guess on
|
|
out-of-scope input rather than emit a wrong verdict.
|
|
"""
|
|
|
|
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
|
|
canonical_b: str | None
|
|
reason: str
|
|
|
|
|
|
REFUSED_VERDICTS: Final[frozenset[Verdict]] = frozenset({Verdict.REFUSED})
|
|
"""Helper set for callers that need to gate on refusal vs decision."""
|
|
|
|
|
|
def _normalize_pair(
|
|
expression_a: str,
|
|
expression_b: str,
|
|
*,
|
|
variable: str | None,
|
|
variables: tuple[str, ...] | None,
|
|
) -> tuple[str, str]:
|
|
if variables is None and variable is None:
|
|
# Infer variables from the union of both expressions so `x + y` and
|
|
# `y + x` normalize in the same variable space.
|
|
poly_a_probe = normalize(expression_a)
|
|
poly_b_probe = normalize(expression_b)
|
|
variables = tuple(sorted(set(poly_a_probe.variables) | set(poly_b_probe.variables)))
|
|
canon_a = normalize(expression_a, variable=variable, variables=variables).to_canonical_string()
|
|
canon_b = normalize(expression_b, variable=variable, variables=variables).to_canonical_string()
|
|
return canon_a, canon_b
|
|
|
|
|
|
def check_equivalence(
|
|
expression_a: str,
|
|
expression_b: str,
|
|
*,
|
|
variable: str | None = None,
|
|
variables: tuple[str, ...] | None = None,
|
|
) -> EquivalenceVerdict:
|
|
"""Return whether two expressions are algebraically equivalent.
|
|
|
|
``variable`` is retained for backward compatibility with the v1
|
|
univariate API. New callers can omit it and allow variable inference, or
|
|
pass an explicit sorted ``variables`` tuple.
|
|
"""
|
|
try:
|
|
canon_a, canon_b = _normalize_pair(
|
|
expression_a,
|
|
expression_b,
|
|
variable=variable,
|
|
variables=variables,
|
|
)
|
|
except SymbolicError as exc:
|
|
return EquivalenceVerdict(
|
|
verdict=Verdict.REFUSED,
|
|
canonical_a=None,
|
|
canonical_b=None,
|
|
reason=f"normalize 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="",
|
|
)
|