feat(parser): ADR-0123 comparison-phrasing substrate (substrate-only; lift deferred)
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 <N>' 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 <noreply@anthropic.com>
This commit is contained in:
Shay
parent
2659b569b0
commit
a53ce93acf
7 changed files with 671 additions and 27 deletions
|
|
@ -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 "<Entity>
|
||||
# has <N>" 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<actor>[A-Z]\w+)\s+has\s+"
|
||||
r"(?P<value>\d+)\s+"
|
||||
r"(?P<direction>more|fewer|less)\s+"
|
||||
r"(?P<unit>\w+)\s+than\s+"
|
||||
r"(?P<reference>[A-Z]\w+)$"
|
||||
)
|
||||
|
||||
# Group B (multiplicative — twice): "Alice has twice as many apples as Bob"
|
||||
_COMPARE_TWICE_RE = re.compile(
|
||||
r"^(?P<actor>[A-Z]\w+)\s+has\s+twice\s+as\s+many\s+"
|
||||
r"(?P<unit>\w+)\s+as\s+(?P<reference>[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<actor>[A-Z]\w+)\s+has\s+(?P<value>\d+)\s+times\s+as\s+many\s+"
|
||||
r"(?P<unit>\w+)\s+as\s+(?P<reference>[A-Z]\w+)$"
|
||||
)
|
||||
|
||||
# Group C (fractional — half): "Alice has half as many apples as Bob"
|
||||
_COMPARE_HALF_RE = re.compile(
|
||||
r"^(?P<actor>[A-Z]\w+)\s+has\s+half\s+as\s+many\s+"
|
||||
r"(?P<unit>\w+)\s+as\s+(?P<reference>[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
|
||||
# ---------------------------------------------------------------------------
|
||||
|
|
|
|||
|
|
@ -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"])
|
||||
|
|
|
|||
|
|
@ -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]:
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -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."}
|
||||
|
|
|
|||
|
|
@ -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"]}
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue