feat(derivation): math-serving reach seam — select_self_verified is policy-aware (ADR-0206 §5)
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.
This commit is contained in:
Shay
parent
546045eb4d
commit
c5f0c90738
5 changed files with 275 additions and 11 deletions
|
|
@ -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.
|
||||
54
docs/analysis/math-serving-seam-design-2026-06-06.md
Normal file
54
docs/analysis/math-serving-seam-design-2026-06-06.md
Normal file
|
|
@ -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).
|
||||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
90
tests/test_adr_0206_math_serving_seam.py
Normal file
90
tests/test_adr_0206_math_serving_seam.py
Normal file
|
|
@ -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
|
||||
Loading…
Reference in a new issue