diff --git a/generate/derivation/__init__.py b/generate/derivation/__init__.py new file mode 100644 index 00000000..881a5dd3 --- /dev/null +++ b/generate/derivation/__init__.py @@ -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", +] diff --git a/generate/derivation/model.py b/generate/derivation/model.py new file mode 100644 index 00000000..121de862 --- /dev/null +++ b/generate/derivation/model.py @@ -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 diff --git a/generate/derivation/verify.py b/generate/derivation/verify.py new file mode 100644 index 00000000..420d25b6 --- /dev/null +++ b/generate/derivation/verify.py @@ -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, + ) diff --git a/tests/test_adr_0175_phase3a_selfverify_gate.py b/tests/test_adr_0175_phase3a_selfverify_gate.py new file mode 100644 index 00000000..440c2345 --- /dev/null +++ b/tests/test_adr_0175_phase3a_selfverify_gate.py @@ -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]