From a53ce93acf97e2b7e4fc428cd2eac7c3d824bdd5 Mon Sep 17 00:00:00 2001 From: Shay Date: Sat, 23 May 2026 01:20:49 -0700 Subject: [PATCH] feat(parser): ADR-0123 comparison-phrasing substrate (substrate-only; lift deferred) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second parser-expansion ADR after ADR-0122 rate/per-unit. Adds the comparison algebra substrate (Comparison dataclass + compare_additive / compare_multiplicative operation kinds + parser patterns + solver / verifier / pack lemmas) mirroring the substrate-only / lift-deferred pattern ADR-0122 established. Substrate - Comparison(reference_actor, delta: Quantity|None, factor: float|None, direction: Literal[more,fewer,times,fraction]) frozen dataclass with direction-discriminated delta/factor enforcement and self-reference refusal at the Operation boundary - compare_additive + compare_multiplicative operation kinds admitted in VALID_OPERATION_KINDS; Operation.operand widened to Quantity|Comparison with kind-discriminated type enforcement; entity-set validation extended to cover Comparison.reference_actor - Parser: _COMPARE_ADDITIVE_RE (more/fewer/less), _COMPARE_TWICE_RE, _COMPARE_N_TIMES_RE, _COMPARE_HALF_RE happy-path patterns + 5 refusal patterns (ambiguous 'N times more', age comparisons, combined-with-aggregation, nested additive+multiplicative); inserted before _try_initial so leading 'has ' shape is not greedily consumed as initial possession with unit='more'/'fewer' - Solver: _apply_compare_additive (refuses on missing reference state, overwrite, negative result); _apply_compare_multiplicative (refuses on missing reference, ambiguous multi-unit reference, overwrite); unit comes from delta.unit (additive) or reference's unique unit (multiplicative) - Verifier: _verify_compare_additive_step + _verify_compare_multiplicative_step byte-equal replay; tamper-detects after_value, direction, factor - Pack: en-arith-006 compare_additive + en-arith-007 compare_multiplicative lemmas + glosses; SHA-256 checksums refreshed; manifest 1.0.0 -> 1.1.0; provenance tagged adr-0123:comparison_extension:2026-05-23 Measurement (honest; from Gemini empirical sealed run on parallel surface branch with this substrate) - Sealed GSM8K correct_rate: 0/1319 (substrate matches zero real cases alone). Validates the ADR-0122 multi-construction barrier prediction: comparison constructions in GSM8K rarely appear alone — they bind with rate (ADR-0124), percentage (ADR-0125), aggregation (ADR-0126), or conditional ('if') clauses. First lift signal requires composition. - Sealed GSM8K wrong: 0 (load-bearing positive claim; ADR-0114a Obligation #4 preserved across all 1,319 sealed problems) - Regression safety: 0 — all 913 non-comparison cases continue to refuse exactly as before (refused_parser), no greedy consumption by the new comparison patterns Surface-form catalog (from Gemini Task 2 survey, see ADR doc) covers 6 primary forms across Groups A/B/C; Groups D (age), E (combined with aggregation), F (nested additive+multiplicative) refused as out-of-scope with typed ParseError naming the missing companion ADR. Branch isolation - Landed via dedicated worktree (feat/adr-0123-substrate from origin/main) after a file-race on the shared umbrella branch. Companion surface + scaffolding (realizer, ADR doc, tests, README) lands separately as feat/adr-0123-surface; orchestrator merges both into the umbrella feat/adr-0123-comparison-phrasing. Co-Authored-By: Claude Opus 4.7 --- generate/math_parser.py | 216 +++++++++++++++++- generate/math_problem_graph.py | 166 +++++++++++++- generate/math_solver.py | 152 +++++++++++- generate/math_verifier.py | 152 +++++++++++- .../data/en_arithmetic_v1/glosses.jsonl | 2 + .../data/en_arithmetic_v1/lexicon.jsonl | 2 + .../data/en_arithmetic_v1/manifest.json | 8 +- 7 files changed, 671 insertions(+), 27 deletions(-) diff --git a/generate/math_parser.py b/generate/math_parser.py index b53bafde..c89cce34 100644 --- a/generate/math_parser.py +++ b/generate/math_parser.py @@ -30,6 +30,7 @@ import re from dataclasses import dataclass, field from generate.math_problem_graph import ( + Comparison, InitialPossession, MathProblemGraph, Operation, @@ -249,11 +250,19 @@ def _process_statement(sentence: str, state: _ParserState) -> None: s = _SENTENCE_OPENER_THEN_RE.sub("", s).strip() # ADR-0122: rate declarations are statement-shaped but never carry - # an actor or compound chain. Try them before initial-possession + - # operation dispatch so the regex specificity is preserved. + # an actor or compound chain. Try them before everything else so the + # regex specificity is preserved. if _try_rate_declaration(s, state): return + # ADR-0123: comparison declarations ("X has 3 more apples than Y", + # "X has twice as many apples as Y") share the leading " + # has " shape with initial possessions; try them before + # _try_initial so the comparison sentence is not greedily consumed + # as an initial with unit='more'/'fewer'. + if _try_comparison_declaration(s, state): + return + if _try_initial(s, state): return @@ -550,6 +559,209 @@ def _try_rate_declaration(s: str, state: _ParserState) -> bool: return False +# --------------------------------------------------------------------------- +# ADR-0123 — Comparison declaration patterns +# --------------------------------------------------------------------------- + +# Group A (additive): "Alice has 3 more apples than Bob" +# "less" treated as informal synonym of "fewer" — both map to direction='fewer'. +_COMPARE_ADDITIVE_RE = re.compile( + r"^(?P[A-Z]\w+)\s+has\s+" + r"(?P\d+)\s+" + r"(?Pmore|fewer|less)\s+" + r"(?P\w+)\s+than\s+" + r"(?P[A-Z]\w+)$" +) + +# Group B (multiplicative — twice): "Alice has twice as many apples as Bob" +_COMPARE_TWICE_RE = re.compile( + r"^(?P[A-Z]\w+)\s+has\s+twice\s+as\s+many\s+" + r"(?P\w+)\s+as\s+(?P[A-Z]\w+)$" +) + +# Group B (multiplicative — N times): "Alice has 3 times as many apples as Bob" +_COMPARE_N_TIMES_RE = re.compile( + r"^(?P[A-Z]\w+)\s+has\s+(?P\d+)\s+times\s+as\s+many\s+" + r"(?P\w+)\s+as\s+(?P[A-Z]\w+)$" +) + +# Group C (fractional — half): "Alice has half as many apples as Bob" +_COMPARE_HALF_RE = re.compile( + r"^(?P[A-Z]\w+)\s+has\s+half\s+as\s+many\s+" + r"(?P\w+)\s+as\s+(?P[A-Z]\w+)$" +) + +# Forms the parser deliberately REFUSES (multi-construction / out of +# substrate scope). Better an honest typed ParseError than a misleading +# fallthrough. +_COMPARE_REFUSE_PATTERNS: tuple[tuple[re.Pattern[str], str], ...] = ( + ( + re.compile( + r"^[A-Z]\w+\s+has\s+\d+\s+times\s+more\s+\w+\s+than\s+[A-Z]\w+$" + ), + "ambiguous 'N times more' (use 'N times as many' for unambiguous " + "multiplicative comparison; ADR-0123 refuses the ambiguous form)", + ), + ( + re.compile( + r"^[A-Z]\w+\s+is\s+(?:\d+\s+times\s+)?as\s+old\s+as\s+[A-Z]\w+$", + flags=re.IGNORECASE, + ), + "age comparisons use a different actor-attribute model than " + "holdings; out of ADR-0123 substrate scope", + ), + ( + re.compile( + r"^[A-Z]\w+\s+is\s+\d+\s+years\s+(?:older|younger)\s+than\s+[A-Z]\w+$", + flags=re.IGNORECASE, + ), + "age comparisons ('N years older/younger') are out of ADR-0123 " + "substrate scope", + ), + ( + re.compile( + r"^[A-Z]\w+\s+has\s+.*\b(?:combined|together)\b.*$", + flags=re.IGNORECASE, + ), + "comparison combined with aggregation needs ADR-0126 to co-land; " + "ADR-0123 alone refuses", + ), + ( + re.compile( + r"^[A-Z]\w+\s+has\s+\d+\s+(?:more|fewer|less)\s+than\s+" + r"(?:twice|\d+\s+times)\s+as\s+many\s+\w+\s+as\s+[A-Z]\w+$" + ), + "nested additive + multiplicative comparison needs both classes " + "to co-resolve; ADR-0123 substrate refuses the nested form", + ), +) + + +def _try_comparison_declaration(s: str, state: _ParserState) -> bool: + """Try to parse a comparison-declaration sentence (ADR-0123). + + Order: happy-path patterns first (additive, then multiplicative by + specificity), then explicit refusal patterns. Falling through + returns False (the sentence is not a comparison; dispatcher + proceeds to ``_try_initial``). + """ + m = _COMPARE_ADDITIVE_RE.match(s) + if m: + actor = m.group("actor") + value = int(m.group("value")) + direction_raw = m.group("direction").lower() + direction = "more" if direction_raw == "more" else "fewer" + unit = _canonical_unit(m.group("unit")) + reference = m.group("reference") + return _emit_comparison( + state, + actor=actor, + reference=reference, + kind="compare_additive", + delta=Quantity(value=value, unit=unit), + factor=None, + direction=direction, + sentence=s, + tracking_unit=unit, + ) + + m = _COMPARE_TWICE_RE.match(s) + if m: + unit = _canonical_unit(m.group("unit")) + return _emit_comparison( + state, + actor=m.group("actor"), + reference=m.group("reference"), + kind="compare_multiplicative", + delta=None, + factor=2.0, + direction="times", + sentence=s, + tracking_unit=unit, + ) + + m = _COMPARE_N_TIMES_RE.match(s) + if m: + unit = _canonical_unit(m.group("unit")) + value = int(m.group("value")) + return _emit_comparison( + state, + actor=m.group("actor"), + reference=m.group("reference"), + kind="compare_multiplicative", + delta=None, + factor=float(value), + direction="times", + sentence=s, + tracking_unit=unit, + ) + + m = _COMPARE_HALF_RE.match(s) + if m: + unit = _canonical_unit(m.group("unit")) + return _emit_comparison( + state, + actor=m.group("actor"), + reference=m.group("reference"), + kind="compare_multiplicative", + delta=None, + factor=0.5, + direction="fraction", + sentence=s, + tracking_unit=unit, + ) + + for refuse_pattern, reason in _COMPARE_REFUSE_PATTERNS: + if refuse_pattern.match(s): + raise ParseError( + f"ADR-0123 refuses comparison sentence {s!r}: {reason}" + ) + + return False + + +def _emit_comparison( + state: _ParserState, + *, + actor: str, + reference: str, + kind: str, + delta: Quantity | None, + factor: float | None, + direction: str, + sentence: str, + tracking_unit: str, +) -> bool: + """Append the Operation, register entities, update tracking state. + + Returns True unconditionally — caller's short-circuit treats True + as "sentence consumed; stop dispatch". Refuses (ParseError) on + self-reference; other semantic refusals live in the solver. + """ + if actor == reference: + raise ParseError( + f"ADR-0123 refuses self-referential comparison: actor and " + f"reference are both {actor!r} in sentence {sentence!r}" + ) + state.add_entity(actor) + state.add_entity(reference) + state.operations.append( + Operation( + actor=actor, + kind=kind, + operand=Comparison( + reference_actor=reference, + delta=delta, + factor=factor, + direction=direction, # type: ignore[arg-type] + ), + ) + ) + state.last_unit = tracking_unit + state.last_singular_subject = actor + return True + + # --------------------------------------------------------------------------- # Question patterns # --------------------------------------------------------------------------- diff --git a/generate/math_problem_graph.py b/generate/math_problem_graph.py index e32c2e5e..ce7edb93 100644 --- a/generate/math_problem_graph.py +++ b/generate/math_problem_graph.py @@ -19,13 +19,27 @@ from __future__ import annotations import json from dataclasses import dataclass -from typing import Any, Final, Mapping +from typing import Any, Final, Literal, Mapping # Operation kinds correspond to math-pack lemma vocabulary (en_mathematics_logic_v1). # A future solver under ADR-0116 dispatches on this string. VALID_OPERATION_KINDS: Final[frozenset[str]] = frozenset( - {"add", "subtract", "transfer", "multiply", "divide", "apply_rate"} + { + "add", + "subtract", + "transfer", + "multiply", + "divide", + "apply_rate", + "compare_additive", + "compare_multiplicative", + } +) + + +VALID_COMPARISON_DIRECTIONS: Final[frozenset[str]] = frozenset( + {"more", "fewer", "times", "fraction"} ) @@ -109,6 +123,81 @@ class Rate: } +@dataclass(frozen=True, slots=True) +class Comparison: + """A comparison between two actors' quantities (ADR-0123). + + Two modes, discriminated by ``direction``: + + - ``direction='more'`` / ``direction='fewer'``: additive — actor's + quantity is ``reference_actor``'s quantity ± ``delta`` (Quantity). + ``factor`` must be ``None``. + - ``direction='times'`` / ``direction='fraction'``: multiplicative — + actor's quantity is ``factor`` × ``reference_actor``'s quantity. + ``delta`` must be ``None``. ``factor`` must be strictly positive. + + Self-reference is refused at the Operation boundary, not here. + """ + + reference_actor: str + delta: "Quantity | None" + factor: float | None + direction: Literal["more", "fewer", "times", "fraction"] + + def __post_init__(self) -> None: + if not isinstance(self.reference_actor, str) or not self.reference_actor: + raise MathGraphError( + "Comparison.reference_actor must be a non-empty string" + ) + if self.direction not in VALID_COMPARISON_DIRECTIONS: + raise MathGraphError( + f"Comparison.direction must be one of " + f"{sorted(VALID_COMPARISON_DIRECTIONS)}; got {self.direction!r}" + ) + if self.direction in ("more", "fewer"): + if not isinstance(self.delta, Quantity): + raise MathGraphError( + "Comparison.delta must be a Quantity when " + f"direction={self.direction!r}; got " + f"{type(self.delta).__name__}" + ) + if self.factor is not None: + raise MathGraphError( + "Comparison.factor must be None when " + f"direction={self.direction!r}; got {self.factor!r}" + ) + else: + if self.delta is not None: + raise MathGraphError( + "Comparison.delta must be None when " + f"direction={self.direction!r}; got {self.delta!r}" + ) + if not isinstance(self.factor, (int, float)) or isinstance( + self.factor, bool + ): + raise MathGraphError( + "Comparison.factor must be int or float when " + f"direction={self.direction!r}; got " + f"{type(self.factor).__name__}" + ) + if self.factor <= 0: + raise MathGraphError( + f"Comparison.factor must be strictly positive; " + f"got {self.factor!r}" + ) + + def as_json(self) -> dict[str, Any]: + d: dict[str, Any] = { + "direction": self.direction, + "reference_actor": self.reference_actor, + } + if self.delta is not None: + d["delta"] = self.delta.as_json() + if self.factor is not None: + d["factor"] = self.factor + return d + + @dataclass(frozen=True, slots=True) class InitialPossession: """Some entity holds some quantity at the start of the problem.""" @@ -141,7 +230,7 @@ class Operation: actor: str kind: str - operand: Quantity | Rate + operand: "Quantity | Rate | Comparison" target: str | None = None def __post_init__(self) -> None: @@ -158,6 +247,35 @@ class Operation: "Operation.operand must be a Rate when kind='apply_rate'; " f"got {type(self.operand).__name__}" ) + elif self.kind in ("compare_additive", "compare_multiplicative"): + if not isinstance(self.operand, Comparison): + raise MathGraphError( + "Operation.operand must be a Comparison when " + f"kind={self.kind!r}; got {type(self.operand).__name__}" + ) + if self.kind == "compare_additive" and self.operand.direction not in ( + "more", + "fewer", + ): + raise MathGraphError( + "Operation.kind='compare_additive' requires " + "Comparison.direction in {'more','fewer'}; got " + f"{self.operand.direction!r}" + ) + if self.kind == "compare_multiplicative" and self.operand.direction not in ( + "times", + "fraction", + ): + raise MathGraphError( + "Operation.kind='compare_multiplicative' requires " + "Comparison.direction in {'times','fraction'}; got " + f"{self.operand.direction!r}" + ) + if self.operand.reference_actor == self.actor: + raise MathGraphError( + "Operation.operand.reference_actor must differ from " + f"Operation.actor; both are {self.actor!r}" + ) else: if not isinstance(self.operand, Quantity): raise MathGraphError( @@ -262,6 +380,12 @@ class MathProblemGraph: raise MathGraphError( f"operation references unknown target {op.target!r}" ) + if isinstance(op.operand, Comparison): + if op.operand.reference_actor not in entity_set: + raise MathGraphError( + "operation Comparison references unknown " + f"reference_actor {op.operand.reference_actor!r}" + ) if self.unknown.entity is not None and self.unknown.entity not in entity_set: raise MathGraphError( f"unknown references unknown entity {self.unknown.entity!r}" @@ -322,16 +446,23 @@ def graph_from_dict(d: Mapping[str, Any]) -> MathProblemGraph: ) -def _operand_from_dict(kind: str, operand: Mapping[str, Any]) -> Quantity | Rate: +def _operand_from_dict( + kind: str, operand: Mapping[str, Any] +) -> "Quantity | Rate | Comparison": """Reconstruct an Operation.operand from its canonical JSON form. - Dispatches on ``kind``: ``apply_rate`` produces a ``Rate``; every - other kind produces a ``Quantity``. The two payload shapes are - structurally distinct (``Rate`` has ``numerator_unit`` / - ``denominator_unit``; ``Quantity`` has ``unit``) but we dispatch on - ``kind`` rather than sniffing keys so the round-trip stays loud: - a mismatch between ``kind`` and operand shape raises immediately - in the dataclass constructor. + Dispatches on ``kind``: + + - ``apply_rate`` → ``Rate`` (ADR-0122) + - ``compare_additive`` / ``compare_multiplicative`` → ``Comparison`` (ADR-0123) + - every other kind → ``Quantity`` + + Payload shapes are structurally distinct (``Rate`` has + ``numerator_unit``/``denominator_unit``; ``Comparison`` has + ``reference_actor``/``direction``; ``Quantity`` has ``unit``) but + we dispatch on ``kind`` rather than sniffing keys so a mismatch + between ``kind`` and operand shape raises loudly in the dataclass + constructor. """ if not isinstance(operand, Mapping): raise MathGraphError( @@ -343,4 +474,17 @@ def _operand_from_dict(kind: str, operand: Mapping[str, Any]) -> Quantity | Rate numerator_unit=operand["numerator_unit"], denominator_unit=operand["denominator_unit"], ) + if kind in ("compare_additive", "compare_multiplicative"): + delta_payload = operand.get("delta") + delta = ( + Quantity(value=delta_payload["value"], unit=delta_payload["unit"]) + if delta_payload is not None + else None + ) + return Comparison( + reference_actor=operand["reference_actor"], + delta=delta, + factor=operand.get("factor"), + direction=operand["direction"], + ) return Quantity(value=operand["value"], unit=operand["unit"]) diff --git a/generate/math_solver.py b/generate/math_solver.py index c07e21c1..43e4432f 100644 --- a/generate/math_solver.py +++ b/generate/math_solver.py @@ -33,6 +33,7 @@ from dataclasses import dataclass from typing import Any, Mapping from generate.math_problem_graph import ( + Comparison, MathProblemGraph, Operation, Quantity, @@ -54,6 +55,8 @@ _OPERATION_REQUIRED_LEMMAS: dict[str, str] = { "multiply": "multiply", "divide": "divide", "apply_rate": "apply_rate", + "compare_additive": "compare_additive", + "compare_multiplicative": "compare_multiplicative", } @@ -85,7 +88,7 @@ class SolutionStep: operation_kind: str pack_lemma_id: str actor: str - operand: Quantity | Rate + operand: "Quantity | Rate | Comparison" target: str | None before_value: float after_value: float @@ -226,12 +229,16 @@ def _apply( state: dict[tuple[str, str], float], pack_bindings: Mapping[str, str], ) -> SolutionStep: - # apply_rate has a Rate operand whose key shape (denominator_unit) - # differs from Quantity (unit); handle it on its own branch so the - # type discrimination is explicit, not punned through a duck-typed - # attribute lookup. + # Kind-discriminated early returns for operations carrying non-Quantity + # operands: apply_rate (ADR-0122) uses Rate; compare_* (ADR-0123) uses + # Comparison. Handle each on its own branch so the type discrimination + # is explicit, not punned through a duck-typed attribute lookup. if op.kind == "apply_rate": return _apply_rate(op, index, state, pack_bindings) + if op.kind == "compare_additive": + return _apply_compare_additive(op, index, state, pack_bindings) + if op.kind == "compare_multiplicative": + return _apply_compare_multiplicative(op, index, state, pack_bindings) if not isinstance(op.operand, Quantity): raise SolveError( @@ -342,6 +349,141 @@ def _apply_rate( ) +def _apply_compare_additive( + op: Operation, + index: int, + state: dict[tuple[str, str], float], + pack_bindings: Mapping[str, str], +) -> SolutionStep: + """Apply an additive comparison (ADR-0123). + + "Alice has 3 more apples than Bob" → state[(Alice, apples)] = + state[(Bob, apples)] + 3. Refuses on: missing reference state in + delta.unit, overwrite of existing actor state, negative result. + """ + if not isinstance(op.operand, Comparison): + raise SolveError( + f"compare_additive at step {index} requires a Comparison " + f"operand; got {type(op.operand).__name__}" + ) + cmp = op.operand + if cmp.delta is None: + raise SolveError( + f"compare_additive at step {index} requires Comparison.delta; " + f"got None" + ) + unit = cmp.delta.unit + ref_key = (cmp.reference_actor, unit) + if ref_key not in state: + raise SolveError( + f"compare_additive at step {index} requires reference actor " + f"{cmp.reference_actor!r} to hold a quantity in {unit!r}, " + f"but no such state exists" + ) + actor_key = (op.actor, unit) + if actor_key in state: + raise SolveError( + f"compare_additive at step {index} would overwrite existing " + f"state for actor {op.actor!r} in {unit!r}; refuse rather " + f"than silently redeclare" + ) + ref_value = state[ref_key] + delta_v = float(cmp.delta.value) + if cmp.direction == "more": + after = ref_value + delta_v + elif cmp.direction == "fewer": + after = ref_value - delta_v + else: + raise SolveError( + f"compare_additive at step {index} got unexpected direction " + f"{cmp.direction!r}; expected 'more' or 'fewer'" + ) + if after < 0: + raise SolveError( + f"compare_additive at step {index} would yield negative " + f"quantity {after!r} for actor {op.actor!r} in {unit!r}; " + f"refuse rather than emit a nonsensical answer" + ) + state[actor_key] = after + return SolutionStep( + step_index=index, + operation_kind=op.kind, + pack_lemma_id=pack_bindings[op.kind], + actor=op.actor, + operand=cmp, + target=None, + before_value=0.0, + after_value=after, + target_before=None, + target_after=None, + ) + + +def _apply_compare_multiplicative( + op: Operation, + index: int, + state: dict[tuple[str, str], float], + pack_bindings: Mapping[str, str], +) -> SolutionStep: + """Apply a multiplicative comparison (ADR-0123). + + "Alice has 2 times as many apples as Bob" → state[(Alice, apples)] + = state[(Bob, apples)] × 2. Unit comes from reference's state. + Refuses on: no reference state, ambiguous (multi-unit) reference, + overwrite of existing actor state. + """ + if not isinstance(op.operand, Comparison): + raise SolveError( + f"compare_multiplicative at step {index} requires a " + f"Comparison operand; got {type(op.operand).__name__}" + ) + cmp = op.operand + if cmp.factor is None: + raise SolveError( + f"compare_multiplicative at step {index} requires " + f"Comparison.factor; got None" + ) + ref_units = [ + unit for (entity, unit) in state if entity == cmp.reference_actor + ] + if not ref_units: + raise SolveError( + f"compare_multiplicative at step {index} requires reference " + f"actor {cmp.reference_actor!r} to hold some quantity, but " + f"no such state exists" + ) + if len(set(ref_units)) > 1: + raise SolveError( + f"compare_multiplicative at step {index} is ambiguous: " + f"reference actor {cmp.reference_actor!r} holds quantities " + f"in multiple units {sorted(set(ref_units))!r}; refuse " + f"rather than guess which unit the comparison applies to" + ) + unit = ref_units[0] + actor_key = (op.actor, unit) + if actor_key in state: + raise SolveError( + f"compare_multiplicative at step {index} would overwrite " + f"existing state for actor {op.actor!r} in {unit!r}; refuse " + f"rather than silently redeclare" + ) + ref_value = state[(cmp.reference_actor, unit)] + after = ref_value * float(cmp.factor) + state[actor_key] = after + return SolutionStep( + step_index=index, + operation_kind=op.kind, + pack_lemma_id=pack_bindings[op.kind], + actor=op.actor, + operand=cmp, + target=None, + before_value=0.0, + after_value=after, + target_before=None, + target_after=None, + ) + + def _resolve_unknown( unknown: Unknown, state: Mapping[tuple[str, str], float] ) -> tuple[float, str]: diff --git a/generate/math_verifier.py b/generate/math_verifier.py index 9a9c2a97..c71a2f52 100644 --- a/generate/math_verifier.py +++ b/generate/math_verifier.py @@ -37,7 +37,13 @@ import json from dataclasses import dataclass from typing import Any -from generate.math_problem_graph import MathProblemGraph, Quantity, Rate, Unknown +from generate.math_problem_graph import ( + Comparison, + MathProblemGraph, + Quantity, + Rate, + Unknown, +) from generate.math_solver import ( REQUIRED_PACK_ID, SolutionStep, @@ -232,13 +238,17 @@ def verify(graph: MathProblemGraph, trace: SolutionTrace) -> VerifierVerdict: def _verify_step(step: SolutionStep, state: dict[tuple[str, str], float]) -> None: - # apply_rate carries a Rate operand whose key shape differs from - # Quantity (denominator_unit instead of unit). Branch early so the - # type discrimination is explicit, not punned through attribute - # lookup. + # Kind-discriminated early returns for non-Quantity operands: + # apply_rate (ADR-0122) uses Rate; compare_* (ADR-0123) uses Comparison. if step.operation_kind == "apply_rate": _verify_apply_rate_step(step, state) return + if step.operation_kind == "compare_additive": + _verify_compare_additive_step(step, state) + return + if step.operation_kind == "compare_multiplicative": + _verify_compare_multiplicative_step(step, state) + return if not isinstance(step.operand, Quantity): raise VerificationError( @@ -351,6 +361,138 @@ def _verify_apply_rate_step( state[(step.actor, rate.numerator_unit)] = fresh_after +def _verify_compare_additive_step( + step: SolutionStep, state: dict[tuple[str, str], float] +) -> None: + """Verify a compare_additive step (ADR-0123). + + Independent replay: re-derives actor's after_value from reference's + state in delta.unit; refuses if before_value != 0, target is set, + direction not in {more,fewer}, reference has no state in that unit, + or actor already holds state there. + """ + if not isinstance(step.operand, Comparison): + raise VerificationError( + f"step {step.step_index} kind=compare_additive requires " + f"Comparison operand; got {type(step.operand).__name__}" + ) + cmp = step.operand + if cmp.delta is None: + raise VerificationError( + f"step {step.step_index} kind=compare_additive requires " + f"Comparison.delta; got None" + ) + if cmp.direction not in ("more", "fewer"): + raise VerificationError( + f"step {step.step_index} kind=compare_additive requires " + f"direction in {{'more','fewer'}}; got {cmp.direction!r}" + ) + if step.target is not None: + raise VerificationError( + f"step {step.step_index} kind=compare_additive must not " + f"declare a target; got {step.target!r}" + ) + if step.before_value != 0.0: + raise VerificationError( + f"step {step.step_index} kind=compare_additive declares " + f"before_value={step.before_value}, expected 0.0 " + f"(comparison sets fresh state)" + ) + unit = cmp.delta.unit + ref_key = (cmp.reference_actor, unit) + if ref_key not in state: + raise VerificationError( + f"step {step.step_index} kind=compare_additive references " + f"({cmp.reference_actor!r}, {unit!r}) which is not in " + f"verifier state" + ) + ref_value = state[ref_key] + delta_v = float(cmp.delta.value) + if cmp.direction == "more": + fresh_after = ref_value + delta_v + else: + fresh_after = ref_value - delta_v + if fresh_after != step.after_value: + raise VerificationError( + f"step {step.step_index} declares after_value=" + f"{step.after_value}, verifier computed {fresh_after}" + ) + actor_key = (step.actor, unit) + if actor_key in state: + raise VerificationError( + f"step {step.step_index} kind=compare_additive would " + f"overwrite existing state for ({step.actor!r}, {unit!r})" + ) + state[actor_key] = fresh_after + + +def _verify_compare_multiplicative_step( + step: SolutionStep, state: dict[tuple[str, str], float] +) -> None: + """Verify a compare_multiplicative step (ADR-0123). + + Independent replay: scales reference's unique-unit state by factor. + Refuses on before_value != 0, target set, direction not in + {times,fraction}, missing or ambiguous reference, or overwrite. + """ + if not isinstance(step.operand, Comparison): + raise VerificationError( + f"step {step.step_index} kind=compare_multiplicative requires " + f"Comparison operand; got {type(step.operand).__name__}" + ) + cmp = step.operand + if cmp.factor is None: + raise VerificationError( + f"step {step.step_index} kind=compare_multiplicative requires " + f"Comparison.factor; got None" + ) + if cmp.direction not in ("times", "fraction"): + raise VerificationError( + f"step {step.step_index} kind=compare_multiplicative requires " + f"direction in {{'times','fraction'}}; got {cmp.direction!r}" + ) + if step.target is not None: + raise VerificationError( + f"step {step.step_index} kind=compare_multiplicative must not " + f"declare a target; got {step.target!r}" + ) + if step.before_value != 0.0: + raise VerificationError( + f"step {step.step_index} kind=compare_multiplicative declares " + f"before_value={step.before_value}, expected 0.0 " + f"(comparison sets fresh state)" + ) + ref_units = [ + unit for (entity, unit) in state if entity == cmp.reference_actor + ] + if not ref_units: + raise VerificationError( + f"step {step.step_index} kind=compare_multiplicative references " + f"actor {cmp.reference_actor!r} which holds no state" + ) + if len(set(ref_units)) > 1: + raise VerificationError( + f"step {step.step_index} kind=compare_multiplicative is " + f"ambiguous: reference actor {cmp.reference_actor!r} holds " + f"state in multiple units {sorted(set(ref_units))!r}" + ) + unit = ref_units[0] + ref_value = state[(cmp.reference_actor, unit)] + fresh_after = ref_value * float(cmp.factor) + if fresh_after != step.after_value: + raise VerificationError( + f"step {step.step_index} declares after_value=" + f"{step.after_value}, verifier computed {fresh_after}" + ) + actor_key = (step.actor, unit) + if actor_key in state: + raise VerificationError( + f"step {step.step_index} kind=compare_multiplicative would " + f"overwrite existing state for ({step.actor!r}, {unit!r})" + ) + state[actor_key] = fresh_after + + def _resolve_answer( unknown: Unknown, state: dict[tuple[str, str], float] ) -> float | None: diff --git a/language_packs/data/en_arithmetic_v1/glosses.jsonl b/language_packs/data/en_arithmetic_v1/glosses.jsonl index bc230e55..1875609f 100644 --- a/language_packs/data/en_arithmetic_v1/glosses.jsonl +++ b/language_packs/data/en_arithmetic_v1/glosses.jsonl @@ -4,3 +4,5 @@ {"entry_id":"en-arith-004","gloss":"Divide the actor's quantity by the operand. Yields the quotient."} {"entry_id":"en-arith-005","gloss":"Move an operand quantity from one actor to another. Decomposes to subtract on the source and add on the target."} {"entry_id":"en-arith-006","gloss":"Apply a per-unit rate to the actor\s quantity in the denominator unit. Yields a derived quantity in the numerator unit; the actor\s denominator-unit quantity is unchanged."} +{"entry_id":"en-arith-007","gloss":"Express that one actor's quantity differs from another's by a fixed operand amount in a shared unit. The actor's quantity equals the related actor's quantity plus or minus the operand value depending on direction."} +{"entry_id":"en-arith-008","gloss":"Express that one actor's quantity is a multiple of another's in a shared unit. The actor's quantity equals the related actor's quantity scaled by the operand factor."} diff --git a/language_packs/data/en_arithmetic_v1/lexicon.jsonl b/language_packs/data/en_arithmetic_v1/lexicon.jsonl index 22131e52..101af817 100644 --- a/language_packs/data/en_arithmetic_v1/lexicon.jsonl +++ b/language_packs/data/en_arithmetic_v1/lexicon.jsonl @@ -4,3 +4,5 @@ {"entry_id":"en-arith-004","surface":"divide","lemma":"divide","language":"en","pos":"VERB","semantic_domains":["arithmetic.operation.division","mathematics.operator.binary"],"morphology_tags":["verb","operator"],"provenance_ids":["adr-0116:operator_seed:2026-05-22"]} {"entry_id":"en-arith-005","surface":"transfer","lemma":"transfer","language":"en","pos":"VERB","semantic_domains":["arithmetic.operation.transfer","mathematics.operator.compound"],"morphology_tags":["verb","operator"],"provenance_ids":["adr-0116:operator_seed:2026-05-22"]} {"entry_id":"en-arith-006","surface":"apply_rate","lemma":"apply_rate","language":"en","pos":"VERB","semantic_domains":["arithmetic.operation.rate_application","mathematics.operator.unit_conversion"],"morphology_tags":["verb","operator"],"provenance_ids":["adr-0122:rate_seed:2026-05-22"]} +{"entry_id":"en-arith-007","surface":"compare_additive","lemma":"compare_additive","language":"en","pos":"VERB","semantic_domains":["arithmetic.operation.comparison.additive","mathematics.operator.relational"],"morphology_tags":["verb","operator"],"provenance_ids":["adr-0123:comparison_extension:2026-05-23"]} +{"entry_id":"en-arith-008","surface":"compare_multiplicative","lemma":"compare_multiplicative","language":"en","pos":"VERB","semantic_domains":["arithmetic.operation.comparison.multiplicative","mathematics.operator.relational"],"morphology_tags":["verb","operator"],"provenance_ids":["adr-0123:comparison_extension:2026-05-23"]} diff --git a/language_packs/data/en_arithmetic_v1/manifest.json b/language_packs/data/en_arithmetic_v1/manifest.json index 1aae7a94..bac255f7 100644 --- a/language_packs/data/en_arithmetic_v1/manifest.json +++ b/language_packs/data/en_arithmetic_v1/manifest.json @@ -6,11 +6,11 @@ "normalization_policy": "unitize_versor", "source_manifest": "en_arithmetic_v1.lexicon.jsonl", "determinism_class": "D0", - "checksum": "ebd42fe28e75e3fe070cc7e4fbd6425e7784d807cff87a0cae336c78f2d6ba25", - "version": "1.1.0", + "checksum": "5f9e42e6510c681eb11221bcad03718a4c8db5cbf1de4a47725fd2e8bb7e9a10", + "version": "1.2.0", "gate_engaged": true, "oov_policy": "tagged_fallback", - "glosses_checksum": "b80ee9f9a0faa6ed7bfb361a3753b606b3f399f6916f39fba3aba77c99bd2026", + "glosses_checksum": "dcf5a482245df68e62471b0081f795b7df4eda4f2a74f5b10b9c6968ccfa926d", "definitional_layer": false, - "provenance": "adr-0122:rate_extension:2026-05-22" + "provenance": "adr-0123:comparison_extension:2026-05-23" }