core/generate/derivation/search.py
Shay 872ed3b52d feat(adr-0175-phase3b): bounded multiplicative search in the sealed practice lane
ADR-0175 Phase 3b — the first live attempt generator. Runs only in the sealed
practice lane, only on cases the engine refused; every proposal is gated by the
Phase 3a self-verification gate.

generate/derivation/:
- extract.py: extract_quantities() — lexeme-level (number + unit word; ADR-0165).
- search.py: search_multiplicative() — one in-clause product candidate per
  sentence with >=2 quantities + a present multiplicative cue; gated by
  select_self_verified. Per-sentence scope + multi-candidate disagreement give
  the uniqueness gate real teeth (two qualifying sentences -> refuse). The cue
  set {each,every,for,per,times} is an explicit PROVISIONAL hypothesis the
  practice loop refines, not a claimed-correct grammar.
evals/gsm8k_math/practice/v1/search_runner.py: search_augmented_scorer +
  build_search_report — base scorer, then a practice-only attempt on refusals.

MEASUREMENT (the deliverable, per the breadth-of-impact test):
  practice with search:  correct=4  wrong=9  refused=37   (baseline 3/0/47)
- Flips +1 (0021, the clean in-clause aggregate) and its renumbered/reworded
  variants (ADR-0114a perturbation guard) -> a real capability, not memorisation.
- 9 wrong attempts -> elimination records (§9), the learning signal. The naive
  full-product cue model over-attempts; the eliminations are exactly the signal
  that refines it.

HONEST FINDING: self-verification (grounding ∧ cue ∧ unit ∧ uniqueness) is
NECESSARY but NOT SUFFICIENT — 9/13 self-verified attempts were wrong vs gold.
The gap is cue PRECISION / which-quantities-compose (the knowledge axis), not
'can we multiply' (skill). This is why the search runs sealed: gold catches the
9, and case 0050 (canary) attempted-and-failed IN PRACTICE without touching
serving -> validates the seal.

Invariants: #1 seal (serving still 3/47/0; 0050 refuses in serving; no
generate/chat import of the lane), #3 determinism. Serving wrong=0 untouched.

Verified: 3a+3b 31/31; ruff clean; serving lane 4/4; smoke 67/67.
2026-05-28 15:29:08 -07:00

75 lines
3.4 KiB
Python

"""ADR-0175 Phase 3b — bounded, deterministic multiplicative derivation search.
The first attempt generator. Conservative by design: it proposes a single
candidate — the **full product of all extracted quantities** — and only when a
multiplicative-relation cue lexeme is present in the text. The proposal is then
passed through the Phase 3a self-verification gate (grounding ∧ unit ∧ unique),
so nothing ungrounded can resolve.
The cue set is an explicit **provisional hypothesis**: it is the search's first
guess at which lexemes license multiplication. It is *not* claimed correct — the
sealed practice lane checks every attempt against gold, and wrong attempts become
elimination records (§9) that refine the hypothesis over time. That refinement is
the compounding loop; this module only stands up the first, gated attempt.
wrong=0 posture: the search runs only in the sealed practice lane (never serving),
every proposal is gated by self-verification, and a non-unique or ungrounded
proposal refuses. Bounded by :data:`MAX_QUANTITIES` (refuse rather than enumerate
an unbounded product).
"""
from __future__ import annotations
import re
from typing import Final
from generate.derivation.extract import extract_quantities
from generate.derivation.model import GroundedDerivation, Step
from generate.derivation.verify import Resolution, select_self_verified
from generate.math_roundtrip import _tokens
# Provisional multiplicative-cue lexemes (the search's first hypothesis; refined
# by practice elimination, not asserted correct). Sorted use for determinism.
MULTIPLICATIVE_CUES: Final[tuple[str, ...]] = ("each", "every", "for", "per", "times")
MAX_QUANTITIES: Final[int] = 6
_SENTENCE_SPLIT: Final[re.Pattern[str]] = re.compile(r"(?<=[.?!])\s+")
def _sentence_candidates(problem_text: str) -> list[GroundedDerivation]:
"""One in-clause product candidate per sentence that has ≥2 quantities and a
present multiplicative cue.
Per-sentence (in-clause) scope is deliberate: it targets the multiplicative
*aggregate* and avoids multiplying quantities that merely co-occur across
sentences. When two sentences each yield a product, they disagree and the
uniqueness gate refuses — so the disagreement rule does real safety work
instead of being trivially satisfied by a single whole-text candidate.
"""
candidates: list[GroundedDerivation] = []
for sentence in _SENTENCE_SPLIT.split(problem_text):
quantities = extract_quantities(sentence)
if not 2 <= len(quantities) <= MAX_QUANTITIES:
continue
present = [c for c in MULTIPLICATIVE_CUES if c in _tokens(sentence)]
if not present:
continue
cue = present[0] # deterministic (MULTIPLICATIVE_CUES is sorted-by-design)
start, *rest = quantities
candidates.append(
GroundedDerivation(
start=start,
steps=tuple(Step(op="multiply", operand=q, cue=cue) for q in rest),
)
)
return candidates
def search_multiplicative(problem_text: str) -> Resolution | None:
"""Attempt a grounded in-clause multiplicative product.
Builds one product candidate per qualifying sentence and runs them through
the Phase 3a gate: a single self-verifying candidate resolves; zero (no
grounded product) or several that disagree refuse. Deterministic and bounded.
"""
return select_self_verified(_sentence_candidates(problem_text), problem_text)