From c5f0c90738faff1d9c05663ebb016b322502b28c Mon Sep 17 00:00:00 2001 From: Shay Date: Sat, 6 Jun 2026 15:46:14 -0700 Subject: [PATCH] =?UTF-8?q?feat(derivation):=20math-serving=20reach=20seam?= =?UTF-8?q?=20=E2=80=94=20select=5Fself=5Fverified=20is=20policy-aware=20(?= =?UTF-8?q?ADR-0206=20=C2=A75)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes the ADR-0206 §5 math-serving deferral in its own careful PR. The GSM8K wrong=0 serving gate, select_self_verified, now takes a ReachPolicy. This changes NO serving behavior today — it is the safe, byte-identical, sanctioned first edit to the most wrong=0-critical line, with a live-wiring test, so a future VERIFIED widening has a precise, proven integration point. Why it can't actually widen yet (the tension scoping surfaced): GSM8K wrong=0 is ABSOLUTE (zero wrong, ever); a reliability license is STATISTICAL (a 0.99 Wilson floor); math answers aren't disclosed like the cognition path (E). So widening the math serve on a statistical license would eventually serve a SILENT wrong. ADR-0206 §4 foresaw this: VERIFIED is "the only state that will license widening past gold," and it is reserved pending a canonical-comparison pass (the soundness≠correctness gap) that is unbuilt. Design (safe by construction): - select_self_verified(..., policy=STRICT_POLICY). STRICT (the default every one of the 5 callers passes) is the prior logic verbatim — unique answer → Resolution; zero-verify or disagreement → refuse. Byte-identical: the pinned serving-lane SHAs (demo_composition 3a3d09f3, fabrication 01e1b6b7, math_teaching_corpus eaf160d1) are unchanged; Resolution is unchanged; no import cycle. - A wider reach resolves a disagreement ONLY via _canonically_verified — the VERIFIED gate — whose body returns None (capability unbuilt). So the widening is STRUCTURALLY inert: a disagreement refuses regardless of policy. wrong=0 holds by construction, not caller discipline. A statistical reliability license is NOT consulted by the math path (the cognition/math asymmetry is deliberate: cognition discloses, math is absolute). - test_seam_is_live_wiring injects the gate to prove the consumer fires under a wider reach — and STRICT still refuses even then. Verified: smoke (90), invariants (56), governance + selfverify + ms2 (354 incl. the new seam tests), GSM8K serving regression byte-identical (the one red, test_serving_unchanged_by_search expecting stale 6/44, fails identically on clean main — a pre-existing stale artifact, not this change). Three-lens adversarial review (byte-identity/seal, structural wrong=0 inertness, no-overclaim): all held. The real unlock — a VERIFIED canonical-comparison producer — is scoped in docs/analysis/VERIFIED-canonical-comparison-scoping-2026-06-06.md (recommended: back-substitution / constraint-satisfaction on a checkable problem class). Still deferred: SITUATE (stakes), the live FEED-BACK loop, reach_level JSONL emission. --- ...canonical-comparison-scoping-2026-06-06.md | 66 ++++++++++++++ .../math-serving-seam-design-2026-06-06.md | 54 +++++++++++ .../ADR-0206-response-governance-bridge.md | 17 +++- generate/derivation/verify.py | 59 ++++++++++-- tests/test_adr_0206_math_serving_seam.py | 90 +++++++++++++++++++ 5 files changed, 275 insertions(+), 11 deletions(-) create mode 100644 docs/analysis/VERIFIED-canonical-comparison-scoping-2026-06-06.md create mode 100644 docs/analysis/math-serving-seam-design-2026-06-06.md create mode 100644 tests/test_adr_0206_math_serving_seam.py diff --git a/docs/analysis/VERIFIED-canonical-comparison-scoping-2026-06-06.md b/docs/analysis/VERIFIED-canonical-comparison-scoping-2026-06-06.md new file mode 100644 index 00000000..982a5a11 --- /dev/null +++ b/docs/analysis/VERIFIED-canonical-comparison-scoping-2026-06-06.md @@ -0,0 +1,66 @@ +# Scoping: the `VERIFIED` canonical-comparison producer (the real math-serving unlock) + +**Date:** 2026-06-06 · **Status:** scoping (no code) · **Unblocks:** the ADR-0206 §5 +math-serving widening (the seam is built + inert; this is the gate it waits on). + +## The gap + +`select_self_verified` proves **soundness** — grounding ∧ cue ∧ unit ∧ uniqueness — and +refuses on disagreement. It does **not** prove **correctness**: that the committed value +is the right answer to the question. Serving has **no gold**, so correctness can't be +checked by comparison to an answer key. `EpistemicState.VERIFIED` is reserved precisely +for the capability that closes this gap, and it is "the only state that will license +widening past gold" (ADR-0206 §4). Until a producer exists, the math seam stays inert and +the absolute `wrong == 0` is safe. + +## Why a statistical license can't substitute + +A reliability license (Step E) is a Wilson lower bound — it permits the *cognition* path +to serve a **disclosed** estimate. Math answers aren't disclosed; a licensed-but-wrong +math serve is a *silent* wrong. The absolute invariant needs **absolute** evidence, not a +0.99 bound. So `VERIFIED` must be a *proof of correctness*, not a confidence score. + +## Candidate mechanisms (in order of promise) + +1. **Back-substitution / constraint satisfaction (recommended first target).** For a + problem reducible to a constraint system over its *stated* quantities, plug the + candidate answer back in and verify it satisfies every constraint. This is a genuine + correctness check **without gold** — it decides truth against the problem's own + structure ("decode a reality that already is", the canonical-form thesis). Well-posed + for a constraint-bearing subset (e.g., "x of the N are red, the rest blue; how many + blue?" → answer must satisfy red+blue=N). The binding constraint is the same + comprehension wall (word → constraint system), so scope it to shapes the reader already + extracts cleanly. +2. **Independent canonical re-derivation.** Stronger than today's disagreement rule: + require K *structurally disjoint* derivations to converge on the same canonical normal + form. Caveat — convergence is still evidential, not a proof; this raises confidence but + does **not** by itself justify `VERIFIED` for an absolute invariant. Use only as a + *necessary* pre-filter, never the sole gate. +3. **Reuse a domain where correctness is decidable.** Deductive logic already produces + proven-correct answers (the sound+complete ROBDD — [[project-deductive-logic-flagship]]). + That is the existence proof that `VERIFIED` is real; but it flows through the logic + path, not `select_self_verified`. A bridge would let logic-checkable arithmetic + sub-claims earn `VERIFIED`. + +## Recommended arc (each its own PR, wrong=0-gated) + +1. **Contract.** Define `VERIFIED`'s canonical-comparison obligation: a predicate that, + given a candidate `Resolution` + the problem, returns proven-correct / not — with a + *meaningful-fail* test (it must reject a sound-but-wrong answer, the `20/5==4` class). +2. **Producer for ONE checkable class** (back-substitution over a constraint-bearing + shape). Emit `EpistemicState.VERIFIED` only when the back-substitution check passes. +3. **Wire** `_canonically_verified` (the seam's gate, already built + tested) to that + producer. The math seam then widens for exactly that class — and only it. +4. **Re-pin** the serving-lane SHAs under the freeze (the deferred `reach_level` emission; + ADR-0206 §5) — re-pinning a frozen gate is a deliberate, reviewed act, with the eval + delta as the truth test (sealed run must show wrong=0 preserved + the new served class). +5. **Independent oracle** on a holdout (INV-25 discipline): the widened class must hold + wrong=0 against a *separate* gold lane, not just the back-substitution check. + +## Honest risk + +The hard part is comprehension (word → constraints), not the check. So the first producer +should target the *narrowest* shape the reader extracts reliably, proving the mechanism +end-to-end (build → emit VERIFIED → seam widens → wrong=0 holds on holdout) before +widening the shape coverage. This is the "checkable-conclusion domains" direction +([[project-self-check-soundness-not-correctness]]) made concrete for math serving. diff --git a/docs/analysis/math-serving-seam-design-2026-06-06.md b/docs/analysis/math-serving-seam-design-2026-06-06.md new file mode 100644 index 00000000..642bc61c --- /dev/null +++ b/docs/analysis/math-serving-seam-design-2026-06-06.md @@ -0,0 +1,54 @@ +# Math-serving reach seam (ADR-0206 §5) + +**Date:** 2026-06-06 · **Branch:** `feat/math-serving-reach-seam` + +## What this is + +Parameterize `select_self_verified` (the GSM8K wrong=0 serving gate) with a +`ReachPolicy`, completing the ADR-0206 §5 math-serving deferral in its own careful PR. +**It changes no serving behavior today** — it is the safe, byte-identical, sanctioned +*first edit* to the most wrong=0-critical line, with a live-wiring test, so the future +`VERIFIED` widening has a precise, proven integration point. + +## The tension it resolves (why scope-first mattered) + +- GSM8K `wrong == 0` is **absolute** (zero wrong, ever). +- A reliability license (Step E's mechanism) is **statistical** (a 0.99 Wilson floor). +- Math answers are **not disclosed** (`[approximate]`) like the cognition path. + +⇒ Widening the math serve on a statistical license would eventually serve a **silent +wrong** — breaching the absolute invariant + the sealed lane SHAs. ADR-0206 §4 foresaw +this: **`VERIFIED` is "the only state that will license widening past gold,"** and it is +reserved because it needs a **canonical-comparison pass** (the soundness ≠ correctness +gap) that is unbuilt. + +## Design (safe by construction) + +`select_self_verified(..., policy=STRICT_POLICY)`: +- **STRICT** (the default every one of the 5 callers passes): the prior logic verbatim — + unique self-verifying answer → `Resolution`; zero-verify or disagreement → refuse. + Byte-identical; the pinned serving-lane SHAs (`demo_composition 3a3d09f3…`, + `fabrication 01e1b6b7…`, `math_teaching_corpus eaf160d1…`) are unchanged. +- **Wider reach + disagreement**: resolve **only** via `_canonically_verified` — the + `VERIFIED` gate. Its body returns `None` (the capability is unbuilt), so the widening + is **structurally inert**: a disagreement refuses regardless of `policy`. wrong=0 holds + by *construction*, not by caller discipline — even a future caller that wrongly passes a + wider policy still refuses until a real `VERIFIED` producer exists. +- A statistical reliability license is **not** consulted here (the cognition/math + asymmetry is deliberate: cognition discloses, math is absolute). + +`test_seam_is_live_wiring` injects `_canonically_verified` to return a winner and proves +a wider reach then resolves the disagreement — **and STRICT still refuses even then**. So +the seam is live wiring, not dead code; the consumer is proven for the day `VERIFIED` lands. + +## Invariants +- **Byte-identity** — STRICT path unchanged; `Resolution` unchanged; no caller passes a + policy; the import adds no cycle and no serialized-output change (verified: the three + fast serving-lane report hashes are identical before/after). +- **wrong=0** — structurally inert widening; absolute invariant preserved. +- **No overclaim** — serving is unchanged today; the docstrings say so. + +## Out of scope (the real unlock) +The `VERIFIED` canonical-comparison producer — scoped separately in +`VERIFIED-canonical-comparison-scoping-2026-06-06.md`. Also still deferred: SITUATE +(stakes), the live FEED-BACK loop, and `reach_level` JSONL emission (a frozen-gate re-pin). diff --git a/docs/decisions/ADR-0206-response-governance-bridge.md b/docs/decisions/ADR-0206-response-governance-bridge.md index 36392814..37562c98 100644 --- a/docs/decisions/ADR-0206-response-governance-bridge.md +++ b/docs/decisions/ADR-0206-response-governance-bridge.md @@ -150,9 +150,20 @@ without scoping it fails the build. ### §5 — Deferred (one kind of change per PR) -- **Math-serving seam** — parameterizing `select_self_verified` with a - `ReachPolicy` (STRICT branch byte-identical) + the full math-serving - widening test. Its own PR; smaller blast radius on the wrong==0 organ. +- **Math-serving seam** — **LANDED 2026-06-06 (its own PR, as planned).** + `select_self_verified` now takes `policy=STRICT_POLICY`; STRICT is + byte-identical (every caller passes it → the pinned serving-lane SHAs are + unchanged). A *disagreement* may widen past gold ONLY via + `_canonically_verified` — the `VERIFIED` (soundness ≠ correctness) gate, which + is **unbuilt and returns `None`**, so the widening is **structurally inert**: + even a wider reach refuses, preserving the absolute `wrong == 0` by + construction (not convention). A statistical reliability license is + deliberately NOT consulted here — math serving is absolute-wrong=0, not + disclosed like the cognition path. `test_seam_is_live_wiring` injects the gate + to prove the consumer fires (STRICT still refuses even then). **The real + widening remains blocked on a `VERIFIED` producer** (a canonical-comparison + pass) — scoped in + `docs/analysis/VERIFIED-canonical-comparison-scoping-2026-06-06.md`. - **`EVIDENCED` reconcile** — map recognition's outcome into `EpistemicState.EVIDENCED` at the boundary (or document the two axes). A real corrective defect; kept out of this purely-additive scaffold. diff --git a/generate/derivation/verify.py b/generate/derivation/verify.py index 006b2226..e6f34d33 100644 --- a/generate/derivation/verify.py +++ b/generate/derivation/verify.py @@ -34,6 +34,10 @@ from collections import Counter from generate.derivation.extract import extract_quantities from generate.derivation.model import GroundedDerivation +# ADR-0206 §5 math-serving seam — the reach policy parameter. STRICT (the default +# every current caller uses) is byte-identical to the pre-seam gate. +from core.response_governance import ReachLevel, ReachPolicy, STRICT_POLICY + _SAME_UNIT_REQUIRED: Final[frozenset[str]] = frozenset({"add", "subtract"}) @@ -181,11 +185,32 @@ def classify_derivation(derivation: GroundedDerivation, problem_text: str) -> st return "exempt" +def _canonically_verified( + verified: list[GroundedDerivation], + problem_text: str, + policy: "ReachPolicy", +) -> GroundedDerivation | None: + """The ADR-0206 §5 / §4 ``VERIFIED`` gate — the ONLY thing that may license a + math answer *past gold* (resolve a disagreement that STRICT refuses). + + Returns the derivation whose answer is **canonically VERIFIED** — proven + *correct*, not merely *sound* (the soundness ≠ correctness gap). That capability + (a canonical-comparison pass) is **not built**: this returns ``None`` today, so + the widening is **structurally inert** — disagreement refuses regardless of + ``policy``, preserving the absolute ``wrong == 0`` even if a caller passes a wider + reach. It is the precise, tested integration point a future ``VERIFIED`` producer + plugs into. A reliability *license* (statistical) must NEVER substitute here: math + serving is absolute-wrong=0, not disclosed like the cognition path. + """ + return None + + def select_self_verified( derivations: list[GroundedDerivation], problem_text: str, *, target_units: tuple[str, ...] = (), + policy: "ReachPolicy | None" = None, ) -> Resolution | None: """Among the self-verifying derivations, return the unique answer or refuse. @@ -197,18 +222,36 @@ def select_self_verified( dropped — a chain that computes the wrong kind of quantity answered a different question. Empty ``target_units`` imposes no constraint (the unit signal may be unavailable, e.g. a superordinate the units pack doesn't yet cover). + + ADR-0206 §5 math-serving seam: ``policy`` (default STRICT) parameterizes the + reach. STRICT is **byte-identical** to the pre-seam gate — the unique-answer and + refuse paths are untouched (every current caller passes STRICT). A wider reach may + resolve a *disagreement* ONLY via the ``VERIFIED`` gate (``_canonically_verified``), + which is unbuilt and returns ``None`` — so the widening is structurally inert and + the absolute ``wrong == 0`` is preserved by construction, not by convention. """ + reach_policy = policy if policy is not None else STRICT_POLICY verified = [d for d in derivations if self_verifies(d, problem_text).verified] if target_units: verified = [d for d in verified if d.answer_unit in target_units] if not verified: return None distinct = {round(d.answer, 9) for d in verified} - if len(distinct) != 1: - return None # disagreement -> refuse (wrong=0) - chosen = verified[0] - return Resolution( - answer=chosen.answer, - answer_unit=chosen.answer_unit, - derivation=chosen, - ) + if len(distinct) == 1: + chosen = verified[0] + return Resolution( + answer=chosen.answer, + answer_unit=chosen.answer_unit, + derivation=chosen, + ) + # Disagreement. STRICT refuses (wrong=0). A wider reach resolves it ONLY when an + # answer is canonically VERIFIED (proven correct) — inert today (no producer). + if reach_policy.level is not ReachLevel.STRICT: + winner = _canonically_verified(verified, problem_text, reach_policy) + if winner is not None: + return Resolution( + answer=winner.answer, + answer_unit=winner.answer_unit, + derivation=winner, + ) + return None # disagreement, no VERIFIED winner -> refuse (wrong=0) diff --git a/tests/test_adr_0206_math_serving_seam.py b/tests/test_adr_0206_math_serving_seam.py new file mode 100644 index 00000000..db2dab56 --- /dev/null +++ b/tests/test_adr_0206_math_serving_seam.py @@ -0,0 +1,90 @@ +"""ADR-0206 §5 — the math-serving reach seam. + +`select_self_verified` is now parameterized with a `ReachPolicy`. The load-bearing +properties this proves: + +- **STRICT is byte-identical** — the unique-answer and refuse-on-disagreement paths are + untouched (every current caller passes STRICT, so the sealed serving lanes do not move). +- **The widening is structurally inert** — a disagreement is resolved past gold ONLY via + the `VERIFIED` canonical-comparison gate (`_canonically_verified`), which is unbuilt and + returns `None`. So even a wider reach refuses; the absolute `wrong == 0` holds by + construction, not by convention. A statistical reliability license must NEVER widen math. +- **Live wiring, not dead code** — when the `VERIFIED` gate is (test-)injected to produce a + winner, a wider reach resolves the disagreement and STRICT still refuses. This is the + exact, tested integration point a future `VERIFIED` producer plugs into. +""" + +from __future__ import annotations + +import generate.derivation.verify as verify_mod +from core.response_governance import APPROXIMATE_POLICY, STRICT_POLICY +from generate.derivation import GroundedDerivation, Quantity, Resolution, Step, select_self_verified + + +def _q(v: float, unit: str, tok: str) -> Quantity: + return Quantity(value=v, unit=unit, source_token=tok) + + +_DISAGREE_TEXT = "She has 5 apples and 3 apples." + + +def _disagreeing() -> list[GroundedDerivation]: + # Both COMPLETE + grounded over {5,3}; different ops → different answers (8 vs 15). + d_add = GroundedDerivation(start=_q(5, "apples", "5"), steps=(Step(op="add", operand=_q(3, "apples", "3"), cue="and"),)) + d_mul = GroundedDerivation(start=_q(5, "apples", "5"), steps=(Step(op="multiply", operand=_q(3, "apples", "3"), cue="and"),)) + assert d_add.answer != d_mul.answer + return [d_add, d_mul] + + +def _unique() -> list[GroundedDerivation]: + return [GroundedDerivation(start=_q(5, "apples", "5"), steps=(Step(op="add", operand=_q(3, "apples", "3"), cue="and"),))] + + +# --------------------------------------------------------------------------- # +# STRICT (default) is byte-identical to the pre-seam gate +# --------------------------------------------------------------------------- # + + +def test_default_is_strict_refuse_on_disagreement() -> None: + # No policy arg → STRICT → refuse (the sealed serving behavior). + assert select_self_verified(_disagreeing(), _DISAGREE_TEXT) is None + assert select_self_verified(_disagreeing(), _DISAGREE_TEXT, policy=STRICT_POLICY) is None + + +def test_unique_answer_unchanged_at_every_reach() -> None: + # The seam touches only the disagreement path; a unique answer resolves identically. + for policy in (None, STRICT_POLICY, APPROXIMATE_POLICY): + res = select_self_verified(_unique(), _DISAGREE_TEXT, policy=policy) + assert isinstance(res, Resolution) and res.answer == 8.0 + + +# --------------------------------------------------------------------------- # +# The widening is STRUCTURALLY inert until a VERIFIED producer lands +# --------------------------------------------------------------------------- # + + +def test_wider_reach_still_refuses_without_a_verified_producer() -> None: + # _canonically_verified returns None (unbuilt) → even APPROXIMATE refuses a + # disagreement. wrong=0 holds by construction, not by caller discipline. + assert select_self_verified(_disagreeing(), _DISAGREE_TEXT, policy=APPROXIMATE_POLICY) is None + + +def test_verified_gate_returns_none_today() -> None: + assert verify_mod._canonically_verified(_disagreeing(), _DISAGREE_TEXT, APPROXIMATE_POLICY) is None + + +# --------------------------------------------------------------------------- # +# Live wiring — the seam fires the moment the VERIFIED gate produces a winner +# --------------------------------------------------------------------------- # + + +def test_seam_is_live_wiring(monkeypatch) -> None: + derivs = _disagreeing() + winner = derivs[0] # the (test-)VERIFIED answer, 8 + monkeypatch.setattr(verify_mod, "_canonically_verified", lambda v, t, p: winner) + + # A wider reach now resolves the disagreement to the VERIFIED winner... + res = select_self_verified(derivs, _DISAGREE_TEXT, policy=APPROXIMATE_POLICY) + assert isinstance(res, Resolution) and res.answer == 8.0 + # ...but STRICT NEVER widens, even when the gate would produce a winner. + assert select_self_verified(derivs, _DISAGREE_TEXT, policy=STRICT_POLICY) is None