Merge pull request #685 from AssetOverflow/feat/adr-0184-s3-candidate-source-boundary
feat(derivation): define semantic-ledger candidate source boundary
This commit is contained in:
Shay
GitHub
commit
a6e846ebdb
8 changed files with 581 additions and 116 deletions
|
|
@ -0,0 +1,216 @@
|
|||
# ADR-0184 S3–S5 — the semantic-ledger candidate-source boundary
|
||||
|
||||
**Date:** 2026-06-10
|
||||
**Scope:** design for the boundary stack between the S2 semantic-state ledger and the
|
||||
existing derivation candidate/verification system, plus the first load-bearing slice
|
||||
(implemented in the accompanying PR).
|
||||
**Authority unchanged:** `generate/derivation/verify.py` and `generate/derivation/pool.py`
|
||||
remain the sole commit authority. Nothing in this stack may commit an answer.
|
||||
|
||||
## 0. Numbering reconciliation
|
||||
|
||||
The mission brief numbers the boundary stack S3–S5. ADR-0184 §7 already assigns
|
||||
S3 = semantic target wrapper, S4 = semantic candidate source to pool, S5 = transfer
|
||||
events. To avoid corrupting the repo's durable numbering, **code and tests use the
|
||||
ADR's numbering**; this note carries the mapping:
|
||||
|
||||
| Brief | Content | ADR-0184 §7 |
|
||||
|---|---|---|
|
||||
| S3 | candidate-source adapter boundary (this PR) | **S4** (pool source swap) |
|
||||
| S4 | replay/provenance equivalence boundary | new — proposed as **S4b** amendment |
|
||||
| S5 | first narrow semantic-primary path | **S3** (semantic target) then **S5** (transfer) |
|
||||
|
||||
The ADR's S3 (semantic target wrapper) is *not* skipped — it is re-sequenced as a
|
||||
prerequisite of the first semantic-primary path, because question/target binding is
|
||||
what makes a semantic-only world safe to expose. The pool source swap (ADR S4) has no
|
||||
dependency on the target wrapper: it is a byte-equivalent re-plumbing, and ADR-0184
|
||||
§11.3 requires it for the ADR to move to Accepted.
|
||||
|
||||
## 1. The current legacy candidate path
|
||||
|
||||
The derivation lane (sealed; no serving import) resolves a problem like this:
|
||||
|
||||
```text
|
||||
composers (each emits ungated GroundedDerivation candidates)
|
||||
accumulate.accumulation_candidates — 3 readings: strict, distractor-skip, anchor-skip
|
||||
search.multiplicative_candidates — in-clause products
|
||||
multistep.candidate_chains — target-guided bounded search
|
||||
goal_residual.build_goal_residual — ADR-0207 R4
|
||||
|
|
||||
v
|
||||
pool.pooled_candidates — dedup by (answer, start token, step tokens), fixed order
|
||||
|
|
||||
v
|
||||
pool.resolve_pooled — classify_derivation (complete/exempt/None) per candidate;
|
||||
refuse on prior-state question, on zero verifying readings,
|
||||
on disagreement, on exempt-only; commit sole complete answer
|
||||
```
|
||||
|
||||
`compose_accumulation` separately gates the strict reading through
|
||||
`select_self_verified` for the practice lane. The committed serving metric is owned by
|
||||
the candidate-graph reader, a disjoint organ; nothing here touches serving.
|
||||
|
||||
**The parser-patch accumulation problem.** Historically each new problem shape landed
|
||||
as a local composer/matcher patch (the pattern ADR-0175 warns against). ADR-0184's bet
|
||||
is that capability should instead land as new *transition kinds* over the semantic
|
||||
ledger plus replay rules — one reading layer, not N parser patches. For that to ever
|
||||
be true, ledger output needs a single, governed entry point into the candidate pool.
|
||||
That entry point is what this stack defines.
|
||||
|
||||
## 2. What S2 added (PR #684)
|
||||
|
||||
- `state/model.py` — frozen `SemanticQuantity` / `StateKey` / `StateTransition` /
|
||||
`SemanticLedger`, closed op set `{set, gain, loss}`, structural validation
|
||||
(`SemanticStateError`), unit typed `str` (`""` = unitless) to match the extractor
|
||||
and prevent a `None`-vs-`""` key-identity split.
|
||||
- `state/ledger.py` — `build_accumulation_ledger`: the proven single-referent
|
||||
gain/loss reading expressed as SET + GAIN/LOSS transitions over one entity/unit key.
|
||||
- `state/replay.py` — `replay_accumulation_ledger`: the ONLY bridge from ledger to
|
||||
`GroundedDerivation` (set→start, gain→add, loss→subtract, change operands inherit
|
||||
the anchor unit). Refuses non-SET start, cross-key mutation, non-gain/loss ops.
|
||||
- `accumulate.py` rerouted both reading builders through build+replay.
|
||||
- Proven behavior-equivalent: byte-for-byte differential over 937 GSM8K problems,
|
||||
0 differences.
|
||||
|
||||
After S2, the ledger exists and is exercised, but the *candidate enumeration* (which
|
||||
worlds exist for a problem) still lives privately in `accumulate.py`, and `pool.py`
|
||||
still imports `accumulation_candidates` — a composer-named surface, not a
|
||||
semantic-state surface. There is no single place where ledger worlds become pool
|
||||
candidates.
|
||||
|
||||
## 3. What the semantic ledger can already express / cannot yet express safely
|
||||
|
||||
**Can express (S2):** linear single-key histories — one entity/unit `StateKey`, a SET
|
||||
anchor, ordered GAIN/LOSS deltas with licensed cues; build-time distractor-skip
|
||||
(in-clause foreign-unit drop) and anchor-skip (leading non-anchorable block) readings.
|
||||
|
||||
**Cannot yet express safely:**
|
||||
|
||||
- multi-key worlds (transfer: `Sam gives Tom 3` needs two keys + a conservation law);
|
||||
- question/target binding (no TARGET transition; the pool's prior-state guard is the
|
||||
only temporal scope check, and it lives outside the ledger);
|
||||
- comparison/difference relations; rate/container products (op set excludes
|
||||
multiply/divide by design);
|
||||
- temporal scoping (prior-state replay);
|
||||
- competing worlds as first-class objects (the pool sees only flattened candidates);
|
||||
- candidate provenance (a `GroundedDerivation` in the pool does not carry which
|
||||
ledger produced it).
|
||||
|
||||
Every one of these stays out of the candidate path until its own phase lands with
|
||||
refusal-first tests.
|
||||
|
||||
## 4. The correct adapter boundary (brief-S3 / ADR-S4 — this PR)
|
||||
|
||||
One new module, `generate/derivation/state/source.py`, owns world enumeration and the
|
||||
ledger→candidate conversion:
|
||||
|
||||
```text
|
||||
accumulation_world(text, drop_isolated_foreign) -> SemanticLedger | None
|
||||
anchor_skip_world(text) -> SemanticLedger | None
|
||||
accumulation_ledger_worlds(text) -> tuple[SemanticLedger, ...]
|
||||
semantic_state_candidates(text) -> tuple[GroundedDerivation, ...]
|
||||
```
|
||||
|
||||
`pool.py` swaps its accumulation source from `accumulate.accumulation_candidates` to
|
||||
`state.source.semantic_state_candidates` (the ADR §7-S4 swap, verbatim).
|
||||
`accumulate.py` keeps its public surfaces (`compose_accumulation`,
|
||||
`accumulation_candidates`) as thin compatibility wrappers per ADR §10, so every
|
||||
existing consumer (practice runners, tests) is untouched.
|
||||
|
||||
Boundary properties (each pinned by a test):
|
||||
|
||||
1. **Output type is inert.** The boundary emits only `GroundedDerivation` — a value
|
||||
model with no commit semantics. Acceptance/refusal happens only in verify/pool.
|
||||
2. **No authority import.** Nothing under `generate/derivation/state/` imports
|
||||
`verify`, `pool`, or names `Resolution` / `select_self_verified` /
|
||||
`classify_derivation` / `self_verifies` / `resolve_pooled`. A structural AST scan
|
||||
(with a predicate self-test so it cannot be vacuous) enforces this.
|
||||
3. **Fail-closed.** A world that cannot be built (`None`) or a ledger replay that
|
||||
refuses contributes *nothing* — never a placeholder or synthesized candidate.
|
||||
4. **Deterministic order** — strict, distractor-skip, anchor-skip — byte-identical to
|
||||
the legacy enumeration including duplicates (pool dedup is unchanged).
|
||||
|
||||
Why the pool swap is in the same PR as the adapter: an adapter with no consumer is a
|
||||
dead organ (the router-organ-hygiene precedent, PR #646) and a "schema-defined proof
|
||||
obligation" with no executing test. The swap is what makes the boundary load-bearing,
|
||||
and ADR-0184 §11.3 makes it an explicit acceptance criterion.
|
||||
|
||||
## 5. What verifier/pool need to see (and must keep seeing)
|
||||
|
||||
Unchanged tuples of `GroundedDerivation` whose operand `source_token`s, cues, and
|
||||
units come from the problem text. Three properties of the current pool behavior are
|
||||
load-bearing and must not drift:
|
||||
|
||||
- the **exempt rival readings** (distractor-skip, anchor-skip) must still be emitted —
|
||||
ADR-0182's disagreement refusals depend on them; dropping one can unmask a unique
|
||||
*wrong* commit;
|
||||
- **candidate multiplicity and order** presented to pool dedup must be identical
|
||||
(order determines which derivation object a commit reports);
|
||||
- **unit inheritance** (change operands take the anchor unit) must be preserved, since
|
||||
classification (complete/exempt) keys off used/unused units.
|
||||
|
||||
## 6. Failure modes that would create wrong=0 violations
|
||||
|
||||
| # | Failure mode | Defense |
|
||||
|---|---|---|
|
||||
| 1 | Lost exempt rival reading → disagreement disappears → unique wrong commit | byte-equivalence differential (937 problems); anchor-skip/distractor-skip presence tests |
|
||||
| 2 | Reorder/dedup drift → different committed derivation object | identical enumeration order pinned by test; pool dedup untouched |
|
||||
| 3 | Fabricated semantics — a candidate with no deriving ledger, or replay unfaithful to transitions | S2 replay is the only bridge; brief-S4 adds the faithfulness checker before any semantic-only world |
|
||||
| 4 | Exception swallowing — structural invalidity (`SemanticStateError`) silently became "no candidate" | the boundary catches nothing; structural errors propagate loudly |
|
||||
| 5 | Direct commit path from `state/` | structural no-authority-import scan (non-vacuous) |
|
||||
| 6 | Unit-inheritance drift → classification flips | replay untouched; inheritance test exists in S2 suite |
|
||||
| 7 | Future semantic world emits verifying-but-wrong candidates (soundness ≠ correctness) | out of scope for S3/S4 by construction (no new worlds); brief-S5 requires refusal-first acceptance + sealed gold tether before any new world enters the boundary |
|
||||
|
||||
## 7. Tests proving semantic candidates cannot bypass verifier/pool
|
||||
|
||||
- structural: no module under `state/` imports verify/pool or names any commit
|
||||
surface (AST scan + predicate self-test on a known-violating snippet);
|
||||
- behavioral: a boundary candidate that fails verification (ungrounded against the
|
||||
actual problem text) never commits; rejection (no world) yields `()` and the pool
|
||||
refuses or falls through to other composers exactly as before;
|
||||
- the pool's own wrong=0 obligations (disagreement refusal, exempt-only never
|
||||
commits, prior-state guard) re-run green against the swapped source;
|
||||
- delegation equality: `accumulation_candidates(text) == semantic_state_candidates(text)`
|
||||
across the canonical case battery;
|
||||
- 937-problem byte-for-byte differential vs `main` (local harness, reported in PR).
|
||||
|
||||
## 8. The S3–S5 sequence (brief numbering)
|
||||
|
||||
**S3 (this PR, = ADR S4).** Adapter boundary + pool source swap, byte-equivalent.
|
||||
No new capability; no serving, CLAIMS, metric, or lane-pin movement.
|
||||
|
||||
**S4 (next, = proposed ADR S4b amendment).** Replay/provenance equivalence boundary —
|
||||
the precondition for any semantic-only world:
|
||||
|
||||
- an internal provenance record binding each emitted candidate to the ledger that
|
||||
produced it (`(ledger, derivation)`), so a candidate cannot exist at the boundary
|
||||
without a deriving ledger;
|
||||
- a structural `replay_is_faithful(ledger, derivation)` checker — steps correspond 1:1
|
||||
to transitions (set→start, gain→add, loss→subtract), values/source tokens/cues
|
||||
equal, unit-inheritance rule respected — wired into tests so an unfaithful replay
|
||||
fails loudly;
|
||||
- a committed equivalence harness (legacy-twin vs boundary) so the legacy enumeration
|
||||
in `accumulate.py` can later be deleted without losing the equivalence proof.
|
||||
|
||||
**S5 (after S4, = ADR S3 then ADR S5).** First narrow semantic-primary path — the
|
||||
first reading that exists *only* as a ledger:
|
||||
|
||||
1. land ADR S3 (semantic target wrapper: entity/unit/time-scope/relation binding,
|
||||
conservative, preserving the prior-state refusals) — question binding is what makes
|
||||
a multi-key world answerable;
|
||||
2. then ADR S5 transfer events as the first semantic-primary world: two-key ledgers,
|
||||
replay restricted to the question-bound key, refusing ambiguous source/target, no
|
||||
initial state, or unbound questions;
|
||||
3. entry only through `semantic_state_candidates`; commit only through the unchanged
|
||||
verify/pool; refusal-first acceptance tests plus sealed-lane gold tether before any
|
||||
committed metric may move (and then only via ratified PR).
|
||||
|
||||
If at any point a semantic world needs the verifier to change to be admissible, that
|
||||
is a stop signal, not an integration task.
|
||||
|
||||
## 9. What is deliberately NOT in this PR
|
||||
|
||||
No serving/runtime edits; no CLAIMS/metric/lane-pin movement; no new readings or
|
||||
capability; no parser changes; no deletion of legacy surfaces (compat wrappers stay
|
||||
per ADR §10 until brief-S4's committed equivalence harness exists); no provenance
|
||||
record yet (S4); no transfer/target/temporal work (S5+).
|
||||
|
|
@ -29,6 +29,7 @@ from generate.derivation.search import (
|
|||
multiplicative_candidates,
|
||||
search_multiplicative,
|
||||
)
|
||||
from generate.derivation.state.source import semantic_state_candidates
|
||||
from generate.derivation.target import Target, asks_prior_state, extract_target
|
||||
from generate.derivation.verify import (
|
||||
Resolution,
|
||||
|
|
@ -70,4 +71,5 @@ __all__ = [
|
|||
"segment_clauses",
|
||||
"select_self_verified",
|
||||
"self_verifies",
|
||||
"semantic_state_candidates",
|
||||
]
|
||||
|
|
|
|||
|
|
@ -8,116 +8,34 @@ across clauses **only** when (a) the later clause stays on the **same referent**
|
|||
and (b) it carries a **licensed change cue** whose polarity is unambiguous.
|
||||
Otherwise we refuse — the guard is generalised, never weakened.
|
||||
|
||||
Reading:
|
||||
|
||||
1. **Anchor** — clause 1 must establish exactly one quantity ``(actor, N, unit)``.
|
||||
2. **Change steps** — each later quantity-bearing clause applies ``+ M`` (gain) or
|
||||
``- M`` (loss) to the running total, where ``M`` is the clause's single grounded
|
||||
quantity, taken **in the anchor's unit** (``9 more`` = 9 more *apples*; the unit
|
||||
is inherited from the running total, which is what accumulation means).
|
||||
3. **Gate** — the constructed chain runs through the unchanged self-verification
|
||||
gate (grounding ∧ unit ∧ completeness ∧ uniqueness). The gate keeps
|
||||
wrong=0; this only proposes a structurally-licensed candidate.
|
||||
|
||||
ADR-0184 S1 extracted the reusable referent and change-cue helpers into
|
||||
``generate.derivation.state``. S2 routes both accumulation readings through a
|
||||
minimal semantic ledger (SET/GAIN/LOSS over one entity/unit key) and replays it to
|
||||
``GroundedDerivation`` — the transition construction now lives in ``state.ledger``
|
||||
and ``state.replay``, not as inline arithmetic here. This module remains the public
|
||||
accumulation composer surface; behavior is intentionally unchanged, and the replayed
|
||||
``GroundedDerivation`` still faces the unchanged verifier/pool.
|
||||
``generate.derivation.state``; S2 routed both accumulation readings through the
|
||||
semantic ledger (SET/GAIN/LOSS over one entity/unit key) with replay back to
|
||||
``GroundedDerivation``; §7 S4 moved world enumeration into the candidate-source
|
||||
boundary, :mod:`generate.derivation.state.source`. This module remains the public
|
||||
accumulation composer surface — :func:`compose_accumulation` (the gated strict
|
||||
reading) and :func:`accumulation_candidates` (a thin compatibility wrapper over
|
||||
:func:`generate.derivation.state.source.semantic_state_candidates`, per ADR-0184
|
||||
§10). Behavior is intentionally unchanged, and every candidate still faces the
|
||||
unchanged verifier/pool.
|
||||
|
||||
Sealed (no ``chat/`` import); deterministic; refuse-preferring.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import re
|
||||
from typing import Final
|
||||
|
||||
from generate.derivation.clauses import segment_clauses
|
||||
from generate.derivation.extract import extract_quantities
|
||||
from generate.derivation.model import GroundedDerivation
|
||||
from generate.derivation.state.ledger import build_accumulation_ledger
|
||||
from generate.derivation.state.replay import replay_accumulation_ledger
|
||||
from generate.derivation.state.source import accumulation_world, semantic_state_candidates
|
||||
from generate.derivation.verify import Resolution, select_self_verified
|
||||
|
||||
|
||||
def _quantity_clauses(problem_text: str) -> list[str]:
|
||||
"""Sentence-level clauses that carry extracted quantities (the ledger anchor +
|
||||
change-clause sequence)."""
|
||||
return [c for c in segment_clauses(problem_text) if extract_quantities(c)]
|
||||
|
||||
|
||||
def _build_accumulation(
|
||||
problem_text: str, *, drop_isolated_foreign: bool
|
||||
) -> GroundedDerivation | None:
|
||||
"""Construct the single-referent accumulation chain (ungated).
|
||||
|
||||
``drop_isolated_foreign`` (ADR-0182): when a change clause carries more than
|
||||
one quantity, drop those with a **non-empty unit foreign to the anchor's unit**
|
||||
(a candidate distractor — ``studies for 3 hours`` among ``pencils``) and proceed
|
||||
if exactly one same-unit/unitless change remains. With the flag off this is the
|
||||
strict GB-3b.1 reading (a multi-quantity change clause refuses), so
|
||||
:func:`compose_accumulation` is byte-identical to its pre-ADR-0182 behavior.
|
||||
The distractor-skip reading is **never committed alone** — it only ever enters
|
||||
the pool to force a disagreement refusal (see :mod:`generate.derivation.pool`).
|
||||
|
||||
ADR-0184 S2: the SET/GAIN/LOSS reading is built as a semantic ledger and replayed
|
||||
to ``GroundedDerivation``; the construction is unchanged in behavior.
|
||||
"""
|
||||
ledger = build_accumulation_ledger(
|
||||
_quantity_clauses(problem_text), drop_isolated_foreign=drop_isolated_foreign
|
||||
)
|
||||
if ledger is None:
|
||||
return None
|
||||
return replay_accumulation_ledger(ledger)
|
||||
|
||||
|
||||
# ADR-0182 anchor-skip: sub-clause split on conjunctions. A single sentence can pack
|
||||
# a state and its change ("Tom has 8 tickets and buys 4 more tickets") — the
|
||||
# sentence-level segmenter (used everywhere; not changed) keeps them together. This
|
||||
# finer split is *local* to the ungated candidate generator, so it cannot move
|
||||
# GB-1/GB-2/serving/practice (which never call it). Lexeme-level (ADR-0165): it names
|
||||
# coordinating conjunctions, it does not parse grammar.
|
||||
_CONJUNCTION_SPLIT: Final[re.Pattern[str]] = re.compile(r",?\s+(?:and then|and|then)\s+")
|
||||
|
||||
|
||||
def _sub_clauses(problem_text: str) -> list[str]:
|
||||
"""Sentence clauses, each further split on coordinating conjunctions."""
|
||||
parts: list[str] = []
|
||||
for clause in segment_clauses(problem_text):
|
||||
parts.extend(p.strip() for p in _CONJUNCTION_SPLIT.split(clause) if p.strip())
|
||||
return parts
|
||||
|
||||
|
||||
def _build_accumulation_anchor_skip(problem_text: str) -> GroundedDerivation | None:
|
||||
"""ADR-0182 — accumulation over sub-clauses, skipping a leading all-foreign block.
|
||||
|
||||
Reads ``A train travels 60 mph for 2 hours. Tom has 8 tickets and buys 4 more
|
||||
tickets.`` by skipping the (anchor-position) train block — its quantities cannot
|
||||
seed an anchor (≠1 quantity) — and anchoring on the first single-quantity
|
||||
sub-clause (``Tom has 8 tickets``), then chaining its conjunction-mate change
|
||||
(``buys 4 more`` → +4). The skipped block's quantities go unused; the pool's
|
||||
isolated-foreign exemption then classifies the reading ``exempt`` (commit-
|
||||
ineligible), so it can only force a disagreement refusal, never commit. Ungated.
|
||||
"""
|
||||
sub_clauses = [(s, extract_quantities(s)) for s in _sub_clauses(problem_text)]
|
||||
quantity_subs = [(s, qs) for s, qs in sub_clauses if qs]
|
||||
if len(quantity_subs) < 2:
|
||||
return None
|
||||
|
||||
# Anchor = first single-quantity sub-clause; leading non-anchorable (≠1
|
||||
# quantity) sub-clauses are skipped (candidate distractor blocks). The anchor and
|
||||
# its trailing change sub-clauses are then read by the same semantic ledger as the
|
||||
# sentence-level path (ADR-0184 S2): same referent guard, same one-change-per-clause
|
||||
# rule, same polarity gate. drop_isolated_foreign stays off here — the anchor-skip
|
||||
# reading drops a whole leading block, not an in-clause foreign quantity.
|
||||
anchor_idx = next((i for i, (_, qs) in enumerate(quantity_subs) if len(qs) == 1), None)
|
||||
if anchor_idx is None:
|
||||
return None
|
||||
selected = [sub for sub, _ in quantity_subs[anchor_idx:]]
|
||||
ledger = build_accumulation_ledger(selected, drop_isolated_foreign=False)
|
||||
"""Construct the single-referent accumulation chain (ungated) — build the
|
||||
semantic world at the S4 boundary, replay through the S2 bridge."""
|
||||
ledger = accumulation_world(problem_text, drop_isolated_foreign=drop_isolated_foreign)
|
||||
if ledger is None:
|
||||
return None
|
||||
return replay_accumulation_ledger(ledger)
|
||||
|
|
@ -138,19 +56,9 @@ def compose_accumulation(problem_text: str) -> Resolution | None:
|
|||
def accumulation_candidates(problem_text: str) -> tuple[GroundedDerivation, ...]:
|
||||
"""ADR-0182 — the ungated accumulation readings for cross-composer pooling.
|
||||
|
||||
Three readings: the strict GB-3b.1 reading, the distractor-skip reading (drops an
|
||||
isolated-foreign quantity in a multi-quantity change clause — 0014), and the
|
||||
anchor-skip reading (skips a leading all-foreign block + reads a conjunction-mate
|
||||
intra-sentence change — 0016). Ungated: the pool classifies each (``complete``
|
||||
commits, ``exempt`` refuses-only) and the disagreement rule does the wrong=0 work.
|
||||
Deterministic; de-dup is the pool's job.
|
||||
Compatibility wrapper (ADR-0184 §10): the enumeration lives at the semantic
|
||||
candidate-source boundary and is byte-identical to the pre-S4 behavior — three
|
||||
readings (strict, distractor-skip, anchor-skip), ungated, deterministic order,
|
||||
de-dup left to the pool.
|
||||
"""
|
||||
candidates: list[GroundedDerivation] = []
|
||||
for drop in (False, True):
|
||||
derivation = _build_accumulation(problem_text, drop_isolated_foreign=drop)
|
||||
if derivation is not None:
|
||||
candidates.append(derivation)
|
||||
anchor_skip = _build_accumulation_anchor_skip(problem_text)
|
||||
if anchor_skip is not None:
|
||||
candidates.append(anchor_skip)
|
||||
return tuple(candidates)
|
||||
return semantic_state_candidates(problem_text)
|
||||
|
|
|
|||
|
|
@ -29,23 +29,24 @@ never invoked here).
|
|||
|
||||
from __future__ import annotations
|
||||
|
||||
from generate.derivation.accumulate import accumulation_candidates
|
||||
from generate.derivation.goal_residual import build_goal_residual
|
||||
from generate.derivation.model import GroundedDerivation
|
||||
from generate.derivation.multistep import candidate_chains
|
||||
from generate.derivation.search import multiplicative_candidates
|
||||
from generate.derivation.state.source import semantic_state_candidates
|
||||
from generate.derivation.target import asks_prior_state
|
||||
from generate.derivation.verify import Resolution, classify_derivation
|
||||
|
||||
|
||||
def pooled_candidates(problem_text: str) -> list[GroundedDerivation]:
|
||||
"""Every composer's ungated candidate readings, de-duplicated. Deterministic
|
||||
order (accumulation, then multiplicative, then chain)."""
|
||||
order (semantic-state accumulation worlds via the ADR-0184 §7-S4 candidate-source
|
||||
boundary, then multiplicative, then chain)."""
|
||||
seen: set[tuple[object, ...]] = set()
|
||||
pooled: list[GroundedDerivation] = []
|
||||
_goal_residual = build_goal_residual(problem_text)
|
||||
for derivation in (
|
||||
*accumulation_candidates(problem_text),
|
||||
*semantic_state_candidates(problem_text),
|
||||
*multiplicative_candidates(problem_text),
|
||||
*candidate_chains(problem_text),
|
||||
*((_goal_residual,) if _goal_residual is not None else ()),
|
||||
|
|
|
|||
|
|
@ -126,7 +126,7 @@ _GREATER_THAN_RE: Final[re.Pattern[str]] = re.compile(
|
|||
re.IGNORECASE,
|
||||
)
|
||||
_DOUBLE_WHAT_RE: Final[re.Pattern[str]] = re.compile(
|
||||
rf"(?P<prefix>.+?)\b(?P<factor>twice|double)\s+what\s+(?P<ref>[^,.?]+)",
|
||||
r"(?P<prefix>.+?)\b(?P<factor>twice|double)\s+what\s+(?P<ref>[^,.?]+)",
|
||||
re.IGNORECASE,
|
||||
)
|
||||
_THAT_MANY_RE: Final[re.Pattern[str]] = re.compile(
|
||||
|
|
|
|||
|
|
@ -4,10 +4,13 @@ This package is the sealed derivation-lane home for reusable semantic reading
|
|||
helpers. S1 exposes behavior-equivalent referent/change-cue helpers extracted from
|
||||
:mod:`generate.derivation.accumulate`. S2 adds a minimal semantic-state model
|
||||
(SET/GAIN/LOSS over one entity/unit key), an accumulation ledger builder, and a
|
||||
replay bridge back to ``GroundedDerivation``. No serving path imports this package,
|
||||
replay bridge back to ``GroundedDerivation``. §7 S4 adds the candidate-source
|
||||
boundary (:mod:`generate.derivation.state.source`): the single surface through which
|
||||
semantic worlds become pool candidates. No serving path imports this package,
|
||||
and no new candidate behavior is introduced here: the ledger only re-expresses the
|
||||
proven accumulation reading, and arithmetic commitment still happens only after
|
||||
replay through the existing verifier/pool.
|
||||
replay through the existing verifier/pool — nothing in this package imports the
|
||||
verifier or the pool, and nothing here can commit an answer.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
|
@ -33,6 +36,10 @@ from generate.derivation.state.model import (
|
|||
StateTransition,
|
||||
)
|
||||
from generate.derivation.state.replay import replay_accumulation_ledger
|
||||
from generate.derivation.state.source import (
|
||||
accumulation_ledger_worlds,
|
||||
semantic_state_candidates,
|
||||
)
|
||||
|
||||
__all__ = [
|
||||
"GAIN_VERBS",
|
||||
|
|
@ -44,10 +51,12 @@ __all__ = [
|
|||
"SemanticStateError",
|
||||
"StateKey",
|
||||
"StateTransition",
|
||||
"accumulation_ledger_worlds",
|
||||
"build_accumulation_ledger",
|
||||
"classify_change_polarity",
|
||||
"continues_anchor_referent",
|
||||
"leading_subject_token",
|
||||
"replay_accumulation_ledger",
|
||||
"select_change_cue",
|
||||
"semantic_state_candidates",
|
||||
]
|
||||
|
|
|
|||
139
generate/derivation/state/source.py
Normal file
139
generate/derivation/state/source.py
Normal file
|
|
@ -0,0 +1,139 @@
|
|||
"""ADR-0184 §7 S4 — the semantic candidate-source boundary.
|
||||
|
||||
The single module through which semantic-ledger worlds become derivation candidates.
|
||||
World enumeration (which readings exist for a problem) lives here; conversion to the
|
||||
arithmetic proof object goes only through :func:`replay_accumulation_ledger` (S2's
|
||||
sole bridge). The output is a tuple of inert ``GroundedDerivation`` values — this
|
||||
boundary holds no commit authority: acceptance, classification, and refusal happen
|
||||
only in the unchanged ``generate.derivation.verify`` / ``generate.derivation.pool``.
|
||||
|
||||
Boundary laws (each pinned by tests in
|
||||
``tests/test_adr_0184_s4_semantic_candidate_source.py``):
|
||||
|
||||
* nothing under ``generate/derivation/state/`` imports verify/pool or names a commit
|
||||
surface (structural scan);
|
||||
* a world that cannot be built, or a replay that refuses, contributes nothing —
|
||||
fail-closed, never a synthesized candidate;
|
||||
* enumeration order is deterministic (strict, distractor-skip, anchor-skip) and
|
||||
byte-identical to the pre-S4 ``accumulation_candidates`` enumeration, duplicates
|
||||
included (de-dup remains the pool's job).
|
||||
|
||||
Sealed (no ``chat/`` import); deterministic; refuse-preferring.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import re
|
||||
from typing import Final
|
||||
|
||||
from generate.derivation.clauses import segment_clauses
|
||||
from generate.derivation.extract import extract_quantities
|
||||
from generate.derivation.model import GroundedDerivation
|
||||
from generate.derivation.state.ledger import build_accumulation_ledger
|
||||
from generate.derivation.state.model import SemanticLedger
|
||||
from generate.derivation.state.replay import replay_accumulation_ledger
|
||||
|
||||
|
||||
def _quantity_clauses(problem_text: str) -> list[str]:
|
||||
"""Sentence-level clauses that carry extracted quantities (the ledger anchor +
|
||||
change-clause sequence)."""
|
||||
return [c for c in segment_clauses(problem_text) if extract_quantities(c)]
|
||||
|
||||
|
||||
def accumulation_world(
|
||||
problem_text: str, *, drop_isolated_foreign: bool
|
||||
) -> SemanticLedger | None:
|
||||
"""The single-referent accumulation reading of ``problem_text`` as a ledger.
|
||||
|
||||
``drop_isolated_foreign`` (ADR-0182): when a change clause carries more than
|
||||
one quantity, drop those with a **non-empty unit foreign to the anchor's unit**
|
||||
(a candidate distractor — ``studies for 3 hours`` among ``pencils``) and proceed
|
||||
if exactly one same-unit/unitless change remains. With the flag off this is the
|
||||
strict GB-3b.1 reading (a multi-quantity change clause refuses). The
|
||||
distractor-skip reading is **never committed alone** — it only ever enters the
|
||||
pool to force a disagreement refusal (see :mod:`generate.derivation.pool`).
|
||||
"""
|
||||
return build_accumulation_ledger(
|
||||
_quantity_clauses(problem_text), drop_isolated_foreign=drop_isolated_foreign
|
||||
)
|
||||
|
||||
|
||||
# ADR-0182 anchor-skip: sub-clause split on conjunctions. A single sentence can pack
|
||||
# a state and its change ("Tom has 8 tickets and buys 4 more tickets") — the
|
||||
# sentence-level segmenter (used everywhere; not changed) keeps them together. This
|
||||
# finer split is *local* to the ungated candidate generator, so it cannot move
|
||||
# GB-1/GB-2/serving/practice (which never call it). Lexeme-level (ADR-0165): it names
|
||||
# coordinating conjunctions, it does not parse grammar.
|
||||
_CONJUNCTION_SPLIT: Final[re.Pattern[str]] = re.compile(r",?\s+(?:and then|and|then)\s+")
|
||||
|
||||
|
||||
def _sub_clauses(problem_text: str) -> list[str]:
|
||||
"""Sentence clauses, each further split on coordinating conjunctions."""
|
||||
parts: list[str] = []
|
||||
for clause in segment_clauses(problem_text):
|
||||
parts.extend(p.strip() for p in _CONJUNCTION_SPLIT.split(clause) if p.strip())
|
||||
return parts
|
||||
|
||||
|
||||
def anchor_skip_world(problem_text: str) -> SemanticLedger | None:
|
||||
"""ADR-0182 — the accumulation-over-sub-clauses reading, skipping a leading
|
||||
all-foreign block, as a ledger.
|
||||
|
||||
Reads ``A train travels 60 mph for 2 hours. Tom has 8 tickets and buys 4 more
|
||||
tickets.`` by skipping the (anchor-position) train block — its quantities cannot
|
||||
seed an anchor (≠1 quantity) — and anchoring on the first single-quantity
|
||||
sub-clause (``Tom has 8 tickets``), then chaining its conjunction-mate change
|
||||
(``buys 4 more`` → +4). The skipped block's quantities go unused; the pool's
|
||||
isolated-foreign exemption then classifies the reading ``exempt`` (commit-
|
||||
ineligible), so it can only force a disagreement refusal, never commit.
|
||||
|
||||
``drop_isolated_foreign`` stays off here — the anchor-skip reading drops a whole
|
||||
leading block, not an in-clause foreign quantity.
|
||||
"""
|
||||
sub_clauses = [(s, extract_quantities(s)) for s in _sub_clauses(problem_text)]
|
||||
quantity_subs = [(s, qs) for s, qs in sub_clauses if qs]
|
||||
if len(quantity_subs) < 2:
|
||||
return None
|
||||
|
||||
# Anchor = first single-quantity sub-clause; leading non-anchorable (≠1
|
||||
# quantity) sub-clauses are skipped (candidate distractor blocks). The anchor and
|
||||
# its trailing change sub-clauses are then read by the same semantic ledger as the
|
||||
# sentence-level path: same referent guard, same one-change-per-clause rule, same
|
||||
# polarity gate.
|
||||
anchor_idx = next((i for i, (_, qs) in enumerate(quantity_subs) if len(qs) == 1), None)
|
||||
if anchor_idx is None:
|
||||
return None
|
||||
selected = [sub for sub, _ in quantity_subs[anchor_idx:]]
|
||||
return build_accumulation_ledger(selected, drop_isolated_foreign=False)
|
||||
|
||||
|
||||
def accumulation_ledger_worlds(problem_text: str) -> tuple[SemanticLedger, ...]:
|
||||
"""Every accumulation-backed semantic world for ``problem_text``, in the fixed
|
||||
enumeration order: strict, distractor-skip, anchor-skip. A world that cannot be
|
||||
built is simply absent — fail-closed."""
|
||||
worlds: list[SemanticLedger] = []
|
||||
for drop in (False, True):
|
||||
world = accumulation_world(problem_text, drop_isolated_foreign=drop)
|
||||
if world is not None:
|
||||
worlds.append(world)
|
||||
anchor_skip = anchor_skip_world(problem_text)
|
||||
if anchor_skip is not None:
|
||||
worlds.append(anchor_skip)
|
||||
return tuple(worlds)
|
||||
|
||||
|
||||
def semantic_state_candidates(problem_text: str) -> tuple[GroundedDerivation, ...]:
|
||||
"""ADR-0184 §7 S4 — the semantic candidate source for cross-composer pooling.
|
||||
|
||||
Replays every semantic world through the S2 bridge and returns the resulting
|
||||
ungated candidates. Byte-identical to the pre-S4 ``accumulation_candidates``
|
||||
enumeration: the pool classifies each (``complete`` commits, ``exempt``
|
||||
refuses-only) and the disagreement rule does the wrong=0 work. A refused replay
|
||||
contributes nothing (fail-closed). Deterministic; de-dup is the pool's job.
|
||||
"""
|
||||
candidates: list[GroundedDerivation] = []
|
||||
for world in accumulation_ledger_worlds(problem_text):
|
||||
derivation = replay_accumulation_ledger(world)
|
||||
if derivation is not None:
|
||||
candidates.append(derivation)
|
||||
return tuple(candidates)
|
||||
190
tests/test_adr_0184_s4_semantic_candidate_source.py
Normal file
190
tests/test_adr_0184_s4_semantic_candidate_source.py
Normal file
|
|
@ -0,0 +1,190 @@
|
|||
"""ADR-0184 §7 S4 — the semantic candidate-source boundary tests.
|
||||
|
||||
The boundary (:mod:`generate.derivation.state.source`) is the single surface through
|
||||
which semantic-ledger worlds become derivation candidates, and ``pool.py`` now sources
|
||||
the accumulation readings through it. These tests pin the boundary laws
|
||||
(CLAUDE.md "Schema-Defined Proof Obligations" — each must fail loudly if exactly its
|
||||
guard is removed):
|
||||
|
||||
* **byte-equivalence** — the boundary enumeration is identical to the legacy
|
||||
``accumulation_candidates`` enumeration (order, duplicates, refusals included);
|
||||
* **authority unchanged** — a boundary candidate commits only through verify/pool:
|
||||
acceptance requires classification, rejection fails closed (no world -> no
|
||||
candidate -> refusal or fall-through, never a synthesized answer);
|
||||
* **no direct commit path** — nothing under ``generate/derivation/state/`` imports
|
||||
the verifier or the pool (structural scan, with a predicate self-test so the scan
|
||||
cannot be vacuous);
|
||||
* **legacy surfaces preserved** — ``compose_accumulation`` / ``accumulation_candidates``
|
||||
behave exactly as before the swap.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import ast
|
||||
from pathlib import Path
|
||||
|
||||
from generate.derivation import pool
|
||||
from generate.derivation.accumulate import accumulation_candidates, compose_accumulation
|
||||
from generate.derivation.model import GroundedDerivation
|
||||
from generate.derivation.pool import resolve_pooled
|
||||
from generate.derivation.state.source import (
|
||||
accumulation_ledger_worlds,
|
||||
semantic_state_candidates,
|
||||
)
|
||||
from generate.derivation.verify import Resolution, classify_derivation
|
||||
|
||||
_CLEAN_GAIN = "Sam has 14 apples. He buys 9 more apples. How many apples does Sam have?"
|
||||
_CLEAN_LOSS = "Anna has 25 stickers. She gives 10 away. How many stickers does Anna have?"
|
||||
_NEW_ACTOR = "Sam has 14 apples. Tom buys 9 more apples. How many apples does Sam have?"
|
||||
_DISTRACTOR_0014 = (
|
||||
"Kate has 20 pencils. She studies for 3 hours and then buys 5 more pencils. "
|
||||
"How many pencils does Kate have?"
|
||||
)
|
||||
_ANCHOR_SKIP_0016 = (
|
||||
"A train travels at 60 miles per hour for 2 hours. Tom has 8 tickets and "
|
||||
"he buys 4 more tickets. How many tickets does Tom have?"
|
||||
)
|
||||
_NO_QUANTITIES = "Sam walked to the library and read a book."
|
||||
|
||||
_BATTERY = (
|
||||
_CLEAN_GAIN,
|
||||
_CLEAN_LOSS,
|
||||
_NEW_ACTOR,
|
||||
_DISTRACTOR_0014,
|
||||
_ANCHOR_SKIP_0016,
|
||||
_NO_QUANTITIES,
|
||||
)
|
||||
|
||||
|
||||
class TestBoundaryEquivalence:
|
||||
"""The boundary is a re-plumbing, not a new reading."""
|
||||
|
||||
def test_legacy_wrapper_delegates_byte_identically(self) -> None:
|
||||
for text in _BATTERY:
|
||||
assert accumulation_candidates(text) == semantic_state_candidates(text)
|
||||
|
||||
def test_enumeration_order_is_strict_then_skip_readings(self) -> None:
|
||||
# The distractor problem yields the strict refusal (absent) then the
|
||||
# distractor-skip reading; the anchor-skip problem yields the anchor-skip
|
||||
# reading. Order changes would change which derivation object a commit
|
||||
# reports — pinned here.
|
||||
skip = semantic_state_candidates(_DISTRACTOR_0014)
|
||||
assert [d.answer for d in skip] == [25.0]
|
||||
anchor = semantic_state_candidates(_ANCHOR_SKIP_0016)
|
||||
assert anchor and anchor[-1].answer == 12.0
|
||||
|
||||
def test_clean_problem_emits_duplicate_readings(self) -> None:
|
||||
# On a clean problem the strict, distractor-skip, AND anchor-skip worlds all
|
||||
# coincide; the legacy enumeration emitted all three (pool dedups).
|
||||
# Collapsing them here would silently change pool input multiplicity.
|
||||
candidates = semantic_state_candidates(_CLEAN_GAIN)
|
||||
assert len(candidates) == 3
|
||||
assert len(set(candidates)) == 1
|
||||
|
||||
def test_every_world_starts_with_set(self) -> None:
|
||||
# The builder can only emit replayable accumulation shapes — a non-SET-start
|
||||
# world would be silently dropped by replay; prove the enumeration never
|
||||
# produces one (fail-closed is for hand-built ledgers, not a leak here).
|
||||
for text in _BATTERY:
|
||||
for world in accumulation_ledger_worlds(text):
|
||||
assert world.transitions[0].op == "set"
|
||||
|
||||
def test_compose_accumulation_unchanged(self) -> None:
|
||||
result = compose_accumulation(_CLEAN_GAIN)
|
||||
assert result is not None and result.answer == 23.0
|
||||
assert compose_accumulation(_NEW_ACTOR) is None
|
||||
|
||||
|
||||
class TestAuthorityUnchanged:
|
||||
"""Semantic candidates pass through verify/pool or do not pass at all."""
|
||||
|
||||
def test_boundary_emits_only_inert_value_objects(self) -> None:
|
||||
for text in _BATTERY:
|
||||
for candidate in semantic_state_candidates(text):
|
||||
assert isinstance(candidate, GroundedDerivation)
|
||||
assert not isinstance(candidate, Resolution)
|
||||
|
||||
def test_pool_sources_the_boundary_function(self) -> None:
|
||||
assert pool.semantic_state_candidates is semantic_state_candidates
|
||||
|
||||
def test_acceptance_still_requires_pool_commit_rules(self) -> None:
|
||||
resolution = resolve_pooled(_CLEAN_GAIN)
|
||||
assert resolution is not None and resolution.answer == 23.0
|
||||
# the committed derivation is one the boundary emitted and verify classified
|
||||
assert classify_derivation(resolution.derivation, _CLEAN_GAIN) == "complete"
|
||||
|
||||
def test_unverifiable_semantic_candidate_never_commits(self) -> None:
|
||||
# A boundary candidate evaluated against text it is not grounded in fails
|
||||
# the verifier — the boundary cannot vouch for its own output.
|
||||
candidate = semantic_state_candidates(_CLEAN_GAIN)[0]
|
||||
foreign_text = "Lily has 3 books. She buys 2 more books."
|
||||
assert classify_derivation(candidate, foreign_text) is None
|
||||
|
||||
def test_rejection_fails_closed(self) -> None:
|
||||
# No expressible world -> empty tuple -> downstream refusal/fall-through;
|
||||
# never a placeholder candidate.
|
||||
assert semantic_state_candidates(_NEW_ACTOR) == ()
|
||||
assert semantic_state_candidates(_NO_QUANTITIES) == ()
|
||||
|
||||
def test_distractor_disagreement_still_refuses(self) -> None:
|
||||
assert resolve_pooled(_DISTRACTOR_0014) is None
|
||||
|
||||
def test_anchor_skip_reading_is_still_exempt_only(self) -> None:
|
||||
# ADR-0182's refusals depend on the exempt rival reading surviving the swap.
|
||||
anchor = semantic_state_candidates(_ANCHOR_SKIP_0016)[-1]
|
||||
assert classify_derivation(anchor, _ANCHOR_SKIP_0016) == "exempt"
|
||||
|
||||
|
||||
_STATE_DIR = Path(__file__).resolve().parent.parent / "generate" / "derivation" / "state"
|
||||
_FORBIDDEN_MODULES = ("generate.derivation.verify", "generate.derivation.pool")
|
||||
_FORBIDDEN_NAMES = frozenset(
|
||||
{
|
||||
"Resolution",
|
||||
"classify_derivation",
|
||||
"resolve_pooled",
|
||||
"select_self_verified",
|
||||
"self_verifies",
|
||||
}
|
||||
)
|
||||
|
||||
|
||||
def _authority_imports(source: str) -> list[str]:
|
||||
"""Names a module imports from the verifier/pool authority surfaces."""
|
||||
violations: list[str] = []
|
||||
tree = ast.parse(source)
|
||||
for node in ast.walk(tree):
|
||||
if isinstance(node, ast.Import):
|
||||
violations.extend(
|
||||
alias.name for alias in node.names if alias.name in _FORBIDDEN_MODULES
|
||||
)
|
||||
elif isinstance(node, ast.ImportFrom):
|
||||
module = node.module or ""
|
||||
if module in _FORBIDDEN_MODULES:
|
||||
violations.append(module)
|
||||
else:
|
||||
violations.extend(
|
||||
alias.name for alias in node.names if alias.name in _FORBIDDEN_NAMES
|
||||
)
|
||||
return violations
|
||||
|
||||
|
||||
class TestNoDirectCommitPath:
|
||||
"""Structural: the semantic-state package cannot reach commit authority."""
|
||||
|
||||
def test_state_package_never_imports_verifier_or_pool(self) -> None:
|
||||
scanned = 0
|
||||
for path in sorted(_STATE_DIR.glob("*.py")):
|
||||
violations = _authority_imports(path.read_text())
|
||||
assert not violations, f"{path.name} imports commit authority: {violations}"
|
||||
scanned += 1
|
||||
assert scanned >= 6, "state/ package moved? scan would be vacuous"
|
||||
|
||||
def test_scan_predicate_flags_module_import(self) -> None:
|
||||
# Predicate self-test (non-vacuity): both import forms must be caught.
|
||||
assert _authority_imports("from generate.derivation.verify import Resolution")
|
||||
assert _authority_imports("import generate.derivation.pool")
|
||||
|
||||
def test_scan_predicate_flags_indirect_name_import(self) -> None:
|
||||
# Re-exported authority names are caught even via a laundering module.
|
||||
assert _authority_imports("from generate.derivation import resolve_pooled")
|
||||
assert _authority_imports("from generate.derivation import Resolution")
|
||||
Loading…
Reference in a new issue