feat(adr-0175-phase3a): self-verification gate (built before the search)
ADR-0175 Phase 3 splits wrong=0-first: build the gate (3a) and PROVE invariant #2 before the bounded search (3b) that could exploit gaps. generate/derivation/: - model.py: Quantity / Step / GroundedDerivation. A derivation is a left-fold over text-sourced quantities; each Step carries its licensing cue (the lexeme the search claims licenses the op). - verify.py: self_verifies() — grounded operands ∧ grounded operation cues ∧ unit consistency ∧ no divide-by-zero. Grounding REUSES the canonical primitives from math_roundtrip (_tokens/_token_in/_value_grounds) so the gate cannot drift from the round-trip contract. select_self_verified() adds the uniqueness rule: unique self-verifying answer resolves; zero or disagreeing refuse (wrong=0). INVARIANT #2 proven (TestInvariant2_NoSpuriousSelfVerification): the gate refuses to self-verify a derivation that is not grounded+unit-consistent+unique even when its value coincides with gold — the 20/5==4 class: - invented operand not in text -> refused - operation cue not in text -> refused (division not licensed by any present cue) - value coincidence (20/5=4) with ungrounded op -> still refused - add across units (pounds + reps) -> refused - divide-by-zero -> refused Plus uniqueness: disagreeing grounded derivations -> refuse; agreeing -> resolve. Phase 3a is inert (nothing wires generate.derivation into serving). 3b is the bounded search that produces derivations for this gate + measures the flip-curve in the practice lane under perturbation. Verified: 16/16; ruff clean; smoke 67/67; no serving import.
This commit is contained in:
Shay
parent
d90887b80f
commit
0bdb3a441c
4 changed files with 400 additions and 0 deletions
27
generate/derivation/__init__.py
Normal file
27
generate/derivation/__init__.py
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
"""ADR-0175 Phase 3 — grounded derivation search + self-verification gate.
|
||||
|
||||
Phase 3a (this surface): the self-verification gate — grounded operands ∧
|
||||
grounded operation cues ∧ unit consistency ∧ uniqueness. The wrong=0-critical
|
||||
guard that keeps the (Phase 3b) bounded search honest.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from generate.derivation.model import GroundedDerivation, Quantity, Step, VALID_OPS
|
||||
from generate.derivation.verify import (
|
||||
Resolution,
|
||||
SelfVerification,
|
||||
select_self_verified,
|
||||
self_verifies,
|
||||
)
|
||||
|
||||
__all__ = [
|
||||
"GroundedDerivation",
|
||||
"Quantity",
|
||||
"Resolution",
|
||||
"SelfVerification",
|
||||
"Step",
|
||||
"VALID_OPS",
|
||||
"select_self_verified",
|
||||
"self_verifies",
|
||||
]
|
||||
72
generate/derivation/model.py
Normal file
72
generate/derivation/model.py
Normal file
|
|
@ -0,0 +1,72 @@
|
|||
"""ADR-0175 Phase 3a — grounded-derivation value model.
|
||||
|
||||
A derivation is a left-fold over text-sourced quantities: a ``start`` quantity
|
||||
followed by ordered ``Step``s. Each step names the operation, its operand, and
|
||||
the **licensing cue** — the surface lexeme the search claims licenses that
|
||||
operation. The cue is verified against the problem text by the gate
|
||||
(:mod:`generate.derivation.verify`); the model itself only computes the value.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass
|
||||
from typing import Final
|
||||
|
||||
VALID_OPS: Final[frozenset[str]] = frozenset({"multiply", "divide", "add", "subtract"})
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class Quantity:
|
||||
"""A quantity drawn from the problem. ``source_token`` is the surface token
|
||||
as it appears in the text (used by the gate to prove the value is grounded)."""
|
||||
|
||||
value: float
|
||||
unit: str
|
||||
source_token: str
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class Step:
|
||||
"""One operation applied to the running value.
|
||||
|
||||
``cue`` is the surface lexeme the search asserts licenses ``op`` here; the
|
||||
gate refuses to self-verify unless ``cue`` actually appears in the text.
|
||||
"""
|
||||
|
||||
op: str
|
||||
operand: Quantity
|
||||
cue: str
|
||||
|
||||
def __post_init__(self) -> None:
|
||||
if self.op not in VALID_OPS:
|
||||
raise ValueError(f"op must be one of {sorted(VALID_OPS)}, got {self.op!r}")
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class GroundedDerivation:
|
||||
start: Quantity
|
||||
steps: tuple[Step, ...]
|
||||
|
||||
@property
|
||||
def answer(self) -> float:
|
||||
"""Left-fold the steps over ``start``. Raises on divide-by-zero (the gate
|
||||
rejects such derivations before this is relied upon)."""
|
||||
value = self.start.value
|
||||
for step in self.steps:
|
||||
operand = step.operand.value
|
||||
if step.op == "multiply":
|
||||
value = value * operand
|
||||
elif step.op == "divide":
|
||||
value = value / operand # ZeroDivisionError surfaces; gate guards
|
||||
elif step.op == "add":
|
||||
value = value + operand
|
||||
else: # subtract
|
||||
value = value - operand
|
||||
return value
|
||||
|
||||
@property
|
||||
def answer_unit(self) -> str:
|
||||
"""The aggregate keeps the primary (``start``) unit. Multiply/divide
|
||||
compose across units onto the primary; add/subtract require (and the gate
|
||||
enforces) a shared unit, so the primary is correct in every admitted case."""
|
||||
return self.start.unit
|
||||
103
generate/derivation/verify.py
Normal file
103
generate/derivation/verify.py
Normal file
|
|
@ -0,0 +1,103 @@
|
|||
"""ADR-0175 Phase 3a — the self-verification gate.
|
||||
|
||||
The wrong=0-critical gate. A derivation **self-verifies** only when all hold:
|
||||
|
||||
1. **operand grounding** — every operand's value token appears in the problem
|
||||
text (no invented numbers);
|
||||
2. **operation-cue grounding** — every step's licensing cue lexeme appears in the
|
||||
text (the operation is licensed by present evidence, not assumed);
|
||||
3. **unit consistency** — add/subtract require a shared unit; multiply/divide may
|
||||
compose across units onto the primary;
|
||||
4. **no divide-by-zero**.
|
||||
|
||||
Grounding reuses the canonical primitives from :mod:`generate.math_roundtrip`
|
||||
(single source of truth — the same checks the round-trip filter uses), so this
|
||||
gate cannot drift from the round-trip contract.
|
||||
|
||||
``select_self_verified`` adds the cross-derivation **uniqueness** rule: among the
|
||||
self-verifying derivations, a single distinct answer resolves; zero or several
|
||||
refuse (the disagreement rule — preserves wrong=0).
|
||||
|
||||
Invariant #2: a derivation that fails any clause does not self-verify *even if its
|
||||
value coincides with the gold answer* (the ``20/5 == 4`` class).
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass
|
||||
from typing import Final
|
||||
|
||||
# Canonical grounding primitives — reused so this gate stays identical to the
|
||||
# round-trip filter's notion of "appears in the problem text".
|
||||
from generate.math_roundtrip import _token_in, _tokens, _value_grounds
|
||||
from generate.derivation.model import GroundedDerivation
|
||||
|
||||
_SAME_UNIT_REQUIRED: Final[frozenset[str]] = frozenset({"add", "subtract"})
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class SelfVerification:
|
||||
verified: bool
|
||||
reasons: tuple[str, ...] # empty iff verified; named failures otherwise
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class Resolution:
|
||||
answer: float
|
||||
answer_unit: str
|
||||
derivation: GroundedDerivation
|
||||
|
||||
|
||||
def self_verifies(derivation: GroundedDerivation, problem_text: str) -> SelfVerification:
|
||||
"""Decide whether ``derivation`` self-verifies against ``problem_text``."""
|
||||
tokens = _tokens(problem_text)
|
||||
reasons: list[str] = []
|
||||
|
||||
# 1. operand grounding — every value must be sourced from the text.
|
||||
operands = [derivation.start, *(s.operand for s in derivation.steps)]
|
||||
for q in operands:
|
||||
if not _value_grounds(q.source_token, tokens):
|
||||
reasons.append(f"operand {q.source_token!r} not grounded in text")
|
||||
|
||||
# 2. operation-cue grounding — every op licensed by a present lexeme.
|
||||
for step in derivation.steps:
|
||||
if not _token_in(step.cue, tokens):
|
||||
reasons.append(f"operation cue {step.cue!r} not grounded in text")
|
||||
|
||||
# 3. unit consistency.
|
||||
primary_unit = derivation.start.unit
|
||||
for step in derivation.steps:
|
||||
if step.op in _SAME_UNIT_REQUIRED and step.operand.unit != primary_unit:
|
||||
reasons.append(
|
||||
f"unit mismatch: {step.op} of {step.operand.unit!r} into {primary_unit!r}"
|
||||
)
|
||||
|
||||
# 4. divide-by-zero.
|
||||
for step in derivation.steps:
|
||||
if step.op == "divide" and step.operand.value == 0:
|
||||
reasons.append("division by zero")
|
||||
|
||||
return SelfVerification(verified=not reasons, reasons=tuple(reasons))
|
||||
|
||||
|
||||
def select_self_verified(
|
||||
derivations: list[GroundedDerivation],
|
||||
problem_text: str,
|
||||
) -> Resolution | None:
|
||||
"""Among the self-verifying derivations, return the unique answer or refuse.
|
||||
|
||||
Refuse-preferring: ``None`` when zero self-verify (no grounded derivation) or
|
||||
when the self-verifying ones disagree (the multi-branch disagreement rule).
|
||||
"""
|
||||
verified = [d for d in derivations if self_verifies(d, problem_text).verified]
|
||||
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,
|
||||
)
|
||||
198
tests/test_adr_0175_phase3a_selfverify_gate.py
Normal file
198
tests/test_adr_0175_phase3a_selfverify_gate.py
Normal file
|
|
@ -0,0 +1,198 @@
|
|||
"""ADR-0175 Phase 3a — the self-verification gate (built BEFORE the search).
|
||||
|
||||
The wrong=0-critical piece. A bounded derivation search (Phase 3b) will be
|
||||
*allowed* to attempt freely in the sealed practice lane; what keeps it honest is
|
||||
this gate, which decides whether an attempt is **self-verified**:
|
||||
|
||||
grounded operands ∧ grounded operation cues ∧ unit-consistent ∧ unique
|
||||
|
||||
Invariant #2 (CLAUDE.md §Schema-Defined Proof Obligations): the gate MUST refuse
|
||||
to self-verify a derivation that is not grounded+unit-consistent+unique — even
|
||||
when its value coincidentally matches gold (the `20/5 == 4` class). The proof is
|
||||
``TestInvariant2_NoSpuriousSelfVerification`` — each test fails if the gate
|
||||
admits a spurious derivation.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import pytest
|
||||
|
||||
from generate.derivation import (
|
||||
GroundedDerivation,
|
||||
Quantity,
|
||||
Resolution,
|
||||
SelfVerification,
|
||||
Step,
|
||||
select_self_verified,
|
||||
self_verifies,
|
||||
)
|
||||
|
||||
# Case 0021 text — a genuine in-clause multiplicative aggregate.
|
||||
_T0021 = "He bench presses 15 pounds for 10 reps and does 3 sets."
|
||||
|
||||
|
||||
def _q(v: float, unit: str, tok: str) -> Quantity:
|
||||
return Quantity(value=v, unit=unit, source_token=tok)
|
||||
|
||||
|
||||
def _mult_0021() -> GroundedDerivation:
|
||||
# 15 pounds × 10 (cue "reps") × 3 (cue "sets") = 450
|
||||
return GroundedDerivation(
|
||||
start=_q(15, "pounds", "15"),
|
||||
steps=(
|
||||
Step(op="multiply", operand=_q(10, "reps", "10"), cue="reps"),
|
||||
Step(op="multiply", operand=_q(3, "sets", "3"), cue="sets"),
|
||||
),
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Derivation arithmetic
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestDerivationArithmetic:
|
||||
def test_left_fold_multiply(self) -> None:
|
||||
assert _mult_0021().answer == 450.0
|
||||
|
||||
def test_answer_unit_is_primary_for_multiply(self) -> None:
|
||||
assert _mult_0021().answer_unit == "pounds"
|
||||
|
||||
def test_add_same_unit(self) -> None:
|
||||
d = GroundedDerivation(
|
||||
start=_q(5, "apples", "5"),
|
||||
steps=(Step(op="add", operand=_q(3, "apples", "3"), cue="and"),),
|
||||
)
|
||||
assert d.answer == 8.0
|
||||
assert d.answer_unit == "apples"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# self_verifies — the per-derivation gate
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestSelfVerifies:
|
||||
def test_grounded_multiplicative_self_verifies(self) -> None:
|
||||
sv = self_verifies(_mult_0021(), _T0021)
|
||||
assert isinstance(sv, SelfVerification)
|
||||
assert sv.verified is True
|
||||
|
||||
def test_grounded_additive_self_verifies(self) -> None:
|
||||
text = "She has 5 apples and 3 apples."
|
||||
d = GroundedDerivation(
|
||||
start=_q(5, "apples", "5"),
|
||||
steps=(Step(op="add", operand=_q(3, "apples", "3"), cue="and"),),
|
||||
)
|
||||
assert self_verifies(d, text).verified is True
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# INVARIANT #2 — the gate refuses to self-verify spurious derivations
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestInvariant2_NoSpuriousSelfVerification:
|
||||
def test_invented_operand_not_in_text_refused(self) -> None:
|
||||
# 15 × 8 = 120, but "8" is not in the problem -> operand ungrounded
|
||||
d = GroundedDerivation(
|
||||
start=_q(15, "pounds", "15"),
|
||||
steps=(Step(op="multiply", operand=_q(8, "things", "8"), cue="reps"),),
|
||||
)
|
||||
sv = self_verifies(d, _T0021)
|
||||
assert sv.verified is False
|
||||
assert any("operand" in r for r in sv.reasons)
|
||||
|
||||
def test_operation_cue_not_in_text_refused(self) -> None:
|
||||
# 20 / 5 = 4 with operands present, but cue "divided" is NOT in the text.
|
||||
# Even though 4 might match gold, an ungrounded op cannot self-verify.
|
||||
text = "Martha has 20 apples and 5 friends."
|
||||
d = GroundedDerivation(
|
||||
start=_q(20, "apples", "20"),
|
||||
steps=(Step(op="divide", operand=_q(5, "friends", "5"), cue="divided"),),
|
||||
)
|
||||
sv = self_verifies(d, text)
|
||||
assert sv.verified is False
|
||||
assert any("cue" in r for r in sv.reasons)
|
||||
|
||||
def test_value_coincidence_does_not_rescue_ungrounded_op(self) -> None:
|
||||
# The `20/5 == 4` coincidence: gold is 4, the derivation computes 4, the
|
||||
# operands are in text — but division is not licensed by any present cue.
|
||||
text = "Martha has 20 apples and 5 friends." # no division cue
|
||||
d = GroundedDerivation(
|
||||
start=_q(20, "apples", "20"),
|
||||
steps=(Step(op="divide", operand=_q(5, "friends", "5"), cue="per"),),
|
||||
) # cue "per" is also absent from the text
|
||||
assert d.answer == 4.0 # coincides with a plausible gold
|
||||
assert self_verifies(d, text).verified is False # but does NOT self-verify
|
||||
|
||||
def test_add_across_units_refused(self) -> None:
|
||||
# 5 pounds + 10 reps is unit-incoherent even if both tokens are present.
|
||||
d = GroundedDerivation(
|
||||
start=_q(5, "pounds", "15"),
|
||||
steps=(Step(op="add", operand=_q(10, "reps", "10"), cue="and"),),
|
||||
)
|
||||
sv = self_verifies(d, _T0021)
|
||||
assert sv.verified is False
|
||||
assert any("unit" in r for r in sv.reasons)
|
||||
|
||||
def test_division_by_zero_refused(self) -> None:
|
||||
text = "There are 6 boxes and 0 shelves."
|
||||
d = GroundedDerivation(
|
||||
start=_q(6, "boxes", "6"),
|
||||
steps=(Step(op="divide", operand=_q(0, "shelves", "0"), cue="per"),),
|
||||
)
|
||||
assert self_verifies(d, text).verified is False
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# select_self_verified — uniqueness / refuse-on-disagreement
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestSelectUnique:
|
||||
def test_unique_self_verified_resolves(self) -> None:
|
||||
res = select_self_verified([_mult_0021()], _T0021)
|
||||
assert isinstance(res, Resolution)
|
||||
assert res.answer == 450.0
|
||||
assert res.answer_unit == "pounds"
|
||||
|
||||
def test_zero_self_verified_refuses(self) -> None:
|
||||
# only a spurious derivation present -> nothing self-verifies -> refuse
|
||||
spurious = GroundedDerivation(
|
||||
start=_q(20, "apples", "20"),
|
||||
steps=(Step(op="divide", operand=_q(5, "friends", "5"), cue="divided"),),
|
||||
)
|
||||
assert select_self_verified([spurious], "Martha has 20 apples and 5 friends.") is None
|
||||
|
||||
def test_disagreeing_self_verified_refuses(self) -> None:
|
||||
# two grounded derivations that disagree on the answer -> refuse (wrong=0)
|
||||
text = "He bench presses 15 pounds for 10 reps and does 3 sets."
|
||||
d1 = _mult_0021() # 450
|
||||
d2 = GroundedDerivation( # 15 x 10 = 150 (grounded but different answer)
|
||||
start=_q(15, "pounds", "15"),
|
||||
steps=(Step(op="multiply", operand=_q(10, "reps", "10"), cue="reps"),),
|
||||
)
|
||||
assert d1.answer != d2.answer
|
||||
assert select_self_verified([d1, d2], text) is None
|
||||
|
||||
def test_agreeing_self_verified_resolves(self) -> None:
|
||||
# two self-verifying derivations that AGREE -> resolve (convergent evidence)
|
||||
text = "He bench presses 15 pounds for 10 reps and does 3 sets."
|
||||
d1 = _mult_0021()
|
||||
d2 = _mult_0021()
|
||||
res = select_self_verified([d1, d2], text)
|
||||
assert res is not None and res.answer == 450.0
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# Determinism (invariant #3)
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
class TestDeterminism:
|
||||
def test_self_verifies_is_deterministic(self) -> None:
|
||||
a = self_verifies(_mult_0021(), _T0021)
|
||||
b = self_verifies(_mult_0021(), _T0021)
|
||||
assert a == b
|
||||
|
||||
def test_frozen_types(self) -> None:
|
||||
import dataclasses
|
||||
q = _q(1, "x", "1")
|
||||
with pytest.raises(dataclasses.FrozenInstanceError):
|
||||
q.value = 9.0 # type: ignore[misc]
|
||||
Loading…
Reference in a new issue