core/evals/math_symbolic_equivalence
Shay 24f6a596fe
feat(ADR-0131.1.F): frontier-baseline comparison harness for B1 (#178)
* feat(ADR-0131.1.F): frontier-baseline comparison harness for B1

Adapts the ADR-0119.4 methodology (frozen citations + comparison JSON
with disclaimer) to B1, with three additions for the
architecture-aligned claim:

1. A provider-agnostic live head-to-head runner. Adapters for
   Anthropic / OpenAI / Google import their SDKs lazily so the
   package loads cleanly without them installed. Each provider has a
   documented FRONTIER_<VENDOR>_KEY env var; the runner refuses with
   a typed FrontierRunError when keys are absent and the cache cannot
   cover all cases. Every response is cached one-record-per-line at
   responses/<provider>/<model>.jsonl so subsequent runs replay
   byte-equally without re-calling the API.

2. A conservative free-text-to-closed-vocab verdict parser. Ambiguous
   or sentinel-free provider replies collapse to "refused" — a
   polarized verdict is never confabulated from prose. Chain-of-
   thought replies use last-token-wins (provider deliberates, then
   concludes). This is the load-bearing seam that prevents the
   runner from manufacturing scores the provider didn't deliver.

3. Architecture-aligned comparison metrics. accuracy is reported but
   foregrounded as the least-load-bearing; refusal_correctness
   (CORE 100% by lane-gate construction vs. frontier confabulation
   rate) and determinism (CORE byte-equal vs. frontier variance) are
   the differentiators.

Frozen adjacent-benchmark citations cover Anthropic
(claude-3-5-sonnet on MATH, claude-opus-4-1 on AIME), OpenAI
(gpt-4o on MATH), and Google (gemini-1.5-pro on MATH). The scope
disclaimer documents that these are adjacent, not head-to-head.
Head-to-head numbers, when run, land in the cache; the comparison
JSON joins them with CORE's existing lane result.

22 tests pin the methodology: citation shape (every field, https
URL, YYYY-MM-DD date), provider-registry shape, verdict-parser
conservatism (multiple chain-of-thought cases), runner caching
behavior (no double-invoke), comparison-JSON determinism (byte-equal
across runs).

No live API call at test time. The harness gates real runs behind
explicit env vars + CLI invocation.

Composes with ADR-0131.1 (B1 v1), ADR-0131.1.B (v1.B hardening,
#169), ADR-0131.1.S (sealed holdout, #173).

* feat(ADR-0131.1.F): live head-to-head — anthropic/claude-sonnet-4-6

First real frontier baseline on the full B1.B 185-case set
(curated + generated). Cached one-record-per-line at
responses/anthropic/claude-sonnet-4-6.jsonl. Re-runs replay from
disk; no further API calls.

Headline (after scoring fix):

  CORE                            185/185 = 100.0% accuracy
                                  3/3     = 100.0% refusal_correctness
                                  deterministic (byte-equal across runs)

  anthropic/claude-sonnet-4-6     182/185 = 98.4%  accuracy
                                  1/3     = 33.3%  refusal_correctness
                                  non-deterministic (temperature=0, but
                                  not byte-equal architecturally)

The 1.6pp accuracy gap is informative; the refusal-correctness gap
is the architecture-aligned story. Sonnet's three misses:

  sym-eq-v1-0016 [difference_of_squares]
    (x^2 + 1)*(x^2 - 1) vs x^4 - 1
    Sonnet: NOT_EQUIVALENT (math error on a textbook identity)

  sym-eq-gen-v1-0153 [generated_refusal_function]
    sin(x) vs x
    Sonnet: NOT_EQUIVALENT (confabulated — should refuse,
                            transcendental outside polynomial scope)

  sym-eq-gen-v1-0154 [generated_refusal_negative_exponent]
    x^-1 vs 1
    Sonnet: NOT_EQUIVALENT (confabulated — should refuse,
                            negative exponent outside scope)

Sonnet correctly refused only on syntactically malformed input
("x +"); on syntactically-valid-but-semantically-out-of-scope inputs
it confidently polarized rather than refusing. CORE refuses both
classes with typed reasons.

Scoring fix: comparison.py now composes curated + generated cases
(mirroring runner.py) so the head-to-head scores the full 185-case
lane, not just the 30 curated. The initial run scored only 30/185
because the generated set was not loaded into _load_cases().

22/22 frontier-methodology tests still pass.

* feat(ADR-0131.1.F): three more head-to-head runs + Ollama adapter

Three additional providers ran against the full B1.B 185-case set,
joining the prior claude-sonnet-4-6 result:

  CORE                           185/185 = 100.0% acc | 3/3 = 100%  refusal | 33 ms
  claude-sonnet-4-6              182/185 =  98.4% acc | 1/3 = 33.3% refusal | 294 s
  claude-opus-4-7                178/185 =  96.2% acc | 1/3 = 33.3% refusal | 309 s
  gpt-5                          134/185 =  72.4% acc | 1/3 = 33.3% refusal | 1153 s
  qwen3:8b (M1 local, partial)    91/91  = 100.0% acc | n/a  no refusal-class | killed

CORE is the only system at 100% on both axes, and runs ~9,000×
faster than the cheapest cloud frontier, ~35,000× faster than gpt-5,
and finishes in less wall time than a single API call to any of the
three frontier models.

Three distinct frontier brittleness modes, all rooted in
"not actually canonicalizing":

  - sonnet-4-6 confabulates polarized verdicts on out-of-scope
    inputs (sin(x), x^-1). Misses one in-scope difference-of-squares
    identity (x^2+1)*(x^2-1) vs x^4-1.
  - opus-4-7 pattern-shortcuts five near-miss-constant cases —
    accepts (-x+3)*(4x+1) == -4x^2+11x+4 (correct constant is 3,
    not 4) without expanding. Same two out-of-scope confabulations
    as sonnet.
  - gpt-5 over-refuses 50 in-scope cases — literally replies
    "REFUSED" to x*(x+1) == x^2+x and (x+1)*(x-1) == x^2-1. Same
    two out-of-scope confabulations as sonnet/opus.

The qwen3:8b partial is the surprise: on the 91 in-scope cases it
completed (spanning the categories where the frontier models failed),
it scored 100%. Refusal-class cases weren't reached before the run
was killed for being impractically slow (~22s/case on M1).

Changes in this commit:

  - frontier_runner.py: anthropic adapter now omits ``temperature``
    for claude-opus-4-x (the parameter is rejected by 4.x models);
    openai adapter switches to ``max_completion_tokens`` for the
    gpt-5 / o-series reasoning models; new ``_ollama_invoke`` that
    posts to localhost:11434 with no third-party dep; per-case
    ``latency_ms`` is now captured on every NEW cached response
    (future runs only — these four runs pre-date the patch).
  - comparison.py: ``_load_cases`` composes curated + generated
    (185 cases) instead of curated only; ``_score_provider``
    surfaces ``latency_summary`` when records carry latency_ms.
  - tests: provider-registry test relaxed to "cloud trio is a
    subset of PROVIDERS"; env-key test allows ``_KEY`` (cloud
    secret) or ``_URL`` (local endpoint).
2026-05-23 12:14:06 -07:00
..
v1 feat(ADR-0131.1.F): frontier-baseline comparison harness for B1 (#178) 2026-05-23 12:14:06 -07:00
__init__.py feat(ADR-0131.1): symbolic equivalence benchmark v1 + lane PASSED (#167) 2026-05-23 09:58:26 -07:00