Merge pull request #627 from AssetOverflow/feat/r2-reader

feat(constraint): R2 Pack C — two-category reader (the capability) + ledger
This commit is contained in:
Shay 2026-06-07 08:32:11 -07:00 committed by GitHub
commit 51b4a6e37d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 492 additions and 5 deletions

View file

@ -0,0 +1,94 @@
# R2 finite-integer constraint-compiler inventory ledger
**As of:** R2 C5C9 (reader landed), on `main @ 0e6a7f9a` + `feat/r2-constraint-setup-compiler`
**Lane state:**
- R2 reader (setup): **10 setup_correct / 0 setup_wrong / 0 missed** + **3 correct reader-refusals**
- R2 answers: **7 solved / 0 wrong** + **3 solver-refused** + **3 reader-refused**
- R2 gold validation: **13 / 13 valid**
- R1 unchanged: **7 / 0 / 3** · 15-case **15 / 0 / 0**
This is the R2 twin of the R1 ledger: a decision artifact recording exactly which constraint
families the off-serving organ now *reads, solves, and verifies*, which it *refuses*, and the
gate protecting each. R2 is disjoint from the GSM8K serving path (imports no
`generate.derivation` / `core.reliability_gate`), so none of this moves the sealed serving
metric. See ADR-0211 for the contract.
## Reproduce
```bash
.venv/bin/python -m evals.constraint_oracle # gold validation -> 13/13 valid
.venv/bin/python -m evals.constraint_oracle reader # reader grading -> setup_wrong 0
.venv/bin/python -m pytest tests/test_constraint_reader.py tests/test_constraint_solver.py \
tests/test_answer_choices.py tests/test_constraint_oracle.py \
tests/test_constraint_comprehension_model.py -q
```
## The pipeline (per the north star)
```text
prose -> read_constraint_problem -> ConstraintProblem -> solve (Cramer, exact int) -> answer
-> verify_answer_choice (tie to one option / flag a wrong key)
```
Four independent gates, each wired to fail loudly (the wrong=0 boundary):
| Gate | Module | Refuses |
|---|---|---|
| reader | `generate/constraint_comprehension/reader.py` | `too_many_categories`, `missing_total_count`, `missing_weighted_total` (+ defensive `coefficient_unit_mismatch`, `query_target_not_a_category`) |
| setup oracle | `evals/constraint_oracle/signature.py` | any drift in unknowns/facts/constraints/query vs gold ⇒ `setup_wrong` |
| solver | `generate/constraint_comprehension/solver.py` | `indistinguishable_weights`, `non_integer_solution`, `negative_solution`, `verification_failed` |
| answer-choice | `generate/answer_choices/verify.py` | `no_matching_option`, `ambiguous_options`, `unknown_provided_label`; flags `contradiction` |
## Per-fixture ledger (13 fixtures)
| Fixture | Family | Reader (setup) | Solver | Answer |
|---|---|---|---|---|
| `r2-001-buses` | buses / seats | ✅ correct | `large=4` | C ✅ |
| `r2-002-chickens` | animals / legs | ✅ correct | `chicken=11` | A ✅ |
| `r2-003-tickets` | tickets / price | ✅ correct | `adult=20` | B ✅ |
| `r2-004-coins` | coins / value | ✅ correct | `dime=9` | A ✅ |
| `r2-005-boxes` | boxes / capacity | ✅ correct | `large=4` | A ✅ |
| `r2-006-vehicles` | vehicles / wheels | ✅ correct | `car=6` | B ✅ |
| `r2-007-pens` | tools / price | ✅ correct | `pen=9` | B ✅ |
| `r2-008-negative` | buses / seats | ✅ correct | ⛔ `negative_solution` | — |
| `r2-009-non-integer` | items / price | ✅ correct | ⛔ `non_integer_solution` | — |
| `r2-010-indistinguishable` | vehicles / wheels | ✅ correct | ⛔ `indistinguishable_weights` | — |
| `r2-011-missing-total-count` | (incomplete) | ⛔ `missing_total_count` | — | — |
| `r2-012-missing-weighted-total` | (incomplete) | ⛔ `missing_weighted_total` | — | — |
| `r2-013-too-many-categories` | (ambiguous) | ⛔ `too_many_categories` | — | — |
**Key reconciliation:** the three `solver_refuses` fixtures (008010) read **setup_correct**
the reader's job is the *setup*, not solvability. Equal coefficients (010) are not a reader
refusal; they are the solver's `indistinguishable_weights`. So the reader reads all ten
well-formed setups and the solver owns the three unsolvable ones. This is the load-bearing
division of labor that keeps the reader's wrong=0 boundary clean.
## Covered families (the near-term milestone)
The six two-category count/weight families the user named are all read → solved → verified
with `setup_wrong = 0`, `answer_wrong = 0`, and answer-key contradictions flaggable:
```text
bus / seat chicken / leg ticket / price
coin / value box / capacity vehicle / wheel (+ tool / price)
```
## Deferred to R3 (NOT in this batch — see ADR-0211 §2)
- ≥3 categories, inequalities, multi-step / mixed constraints, distractor exclusion,
rates / unit conversion.
- The **typed contemplation loop + reviewed-failure learning** (plan Phases 67). When built,
the failure-learning half routes through the existing `teaching/*` proposal-only flywheel
(ADR-0055/0056/0057) — never a parallel correction path.
- Generalization to **real** GSM8K constraint prose (this gold is curated synthetic v1; the
reader recognizes structural patterns, not fixed strings, but real-corpus validation is R3).
## Decision and trajectory
R2 v1 is the off-serving finite-integer two-category constraint setup compiler, complete on
the C0C9 ladder. It is a meaningful capability leap (constraint *systems*, not relational
arithmetic) built on the same disciplined ladder as R1 — gold → setup oracle → solver →
answer verifier → reader — and it earns each family only where the gold + oracle + refusal
tests already license it. No guessed math, no silent correction, no answer without a proven
setup. Next axis (a later batch): R3 / the typed contemplation + reviewed-failure-learning
bridge to the L11 flywheel.

View file

@ -1,19 +1,28 @@
"""CLI: validate the R2 constraint gold.
"""CLI: validate the R2 gold, or grade the R2 reader against it.
python -m evals.constraint_oracle # validate r2_gold.jsonl; exit 0 iff invalid == 0
python -m evals.constraint_oracle # validate r2_gold.jsonl; exit 0 iff invalid == 0
python -m evals.constraint_oracle reader # grade the reader; exit 0 iff setup_wrong == 0
# and reason_mismatch == 0
"""
from __future__ import annotations
import json
import sys
from evals.constraint_oracle.runner import run
from evals.constraint_oracle.runner import run, run_reader
def main() -> int:
report = run()
lane = sys.argv[1] if len(sys.argv) > 1 else ""
if lane == "reader":
report = run_reader()
ok = report["setup_wrong"] == 0 and report["reason_mismatch"] == 0
else:
report = run()
ok = report["invalid"] == 0
print(json.dumps(report, indent=2, default=str))
return 0 if report["invalid"] == 0 else 1
return 0 if ok else 1
if __name__ == "__main__":

View file

@ -162,11 +162,73 @@ def run() -> dict[str, Any]:
}
def run_reader() -> dict[str, Any]:
"""Grade the R2 reader against the gold (C5C9).
Well-formed fixtures (``solved`` / ``solver_refuses``) must read to a setup whose canonical
signature equals the gold's — ``setup_correct``; a refusal is a miss (``setup_refused``); a
mismatch is ``setup_wrong`` (the wrong=0-critical count). ``reader_refuses`` fixtures must
refuse with EXACTLY the gold's ``reader_reason`` (``refused_correct``); a refusal with the
wrong reason is ``reason_mismatch``; producing a setup at all is ``setup_wrong`` (over-read).
Exit-0 criterion: ``setup_wrong == 0 and reason_mismatch == 0`` (and, once C9 lands, the
well-formed fixtures are all correct, so ``setup_refused == 0``).
"""
from generate.constraint_comprehension.reader import read_constraint_problem
from generate.meaning_graph.reader import Refusal
fixtures = _load_r2_gold()
setup_correct = setup_wrong = setup_refused = refused_correct = reason_mismatch = 0
details: list[dict[str, Any]] = []
for fx in fixtures:
out = read_constraint_problem(fx["text"])
fid = fx.get("id")
if fx["expect"] in ("solved", "solver_refuses"):
if isinstance(out, Refusal):
setup_refused += 1
details.append({"id": fid, "outcome": "setup_refused", "reason": out.reason})
elif constraint_setup_signature(out) == constraint_setup_signature(gold_to_problem(fx)):
setup_correct += 1
details.append({"id": fid, "outcome": "setup_correct"})
else:
setup_wrong += 1
details.append(
{
"id": fid,
"outcome": "setup_WRONG",
"reader": constraint_setup_signature(out),
"gold": constraint_setup_signature(gold_to_problem(fx)),
}
)
else: # reader_refuses
if isinstance(out, Refusal) and out.reason == fx["reader_reason"]:
refused_correct += 1
details.append({"id": fid, "outcome": "refused_correct", "reason": out.reason})
elif isinstance(out, Refusal):
reason_mismatch += 1
details.append(
{"id": fid, "outcome": "reason_mismatch", "got": out.reason, "want": fx["reader_reason"]}
)
else:
setup_wrong += 1
details.append({"id": fid, "outcome": "setup_WRONG_over_read"})
return {
"lane": "constraint_oracle_reader",
"total": len(fixtures),
"setup_correct": setup_correct,
"setup_wrong": setup_wrong,
"setup_refused": setup_refused,
"refused_correct": refused_correct,
"reason_mismatch": reason_mismatch,
"details": details,
}
__all__ = [
"EXPECTATIONS",
"READER_REASONS",
"SOLVER_REASONS",
"gold_to_problem",
"run",
"run_reader",
"validate_fixture",
]

View file

@ -0,0 +1,205 @@
"""Two-category constraint-problem reader (R2 C5C9): prose -> ``ConstraintProblem``.
Recognizes the four pieces of a finite-integer two-category problem and assembles the typed
setup, REFUSING (never mis-assembling) when a piece is missing or there are not exactly two
categories. Off-serving; deterministic. The reader does NOT solve solvability (singular /
non-integer / negative systems) is the solver's boundary (C3): an equal-coefficient problem
(e.g. 4 wheels each) still reads setup_correct and is refused *downstream* by the solver. (This
reconciles the design sketch's "no equal coefficients" note: equal coefficients are a SOLVER
refusal, ``indistinguishable_weights``, not a reader refusal the gold classifies that fixture
``solver_refuses``, so the reader must read it.)
Recognizers and their wrong=0 guards:
C5 category pair the two categories come from the per-category coefficient clauses (exactly
two distinct; >2 -> ``too_many_categories``).
C6 coefficient ``Each <cat> (holds|has|costs|is worth) <N> <measured_unit>``; the two
coefficients must share one measured unit (else ``coefficient_unit_mismatch``).
C7 total count a ``<N> <collective>`` sentence whose unit is the collective (not the
measured unit) -> ``x + y = N``; absent -> ``missing_total_count``.
C8 weighted total a ``<T> <measured_unit>`` sentence -> ``a·x + b·y = T`` (coefficients from
C6); absent -> ``missing_weighted_total``.
C9 query target ``How many <category> are there?`` -> the asked unknown (one of the two;
else ``query_target_not_a_category``).
``too_many_categories`` / ``missing_total_count`` / ``missing_weighted_total`` are the gold's
closed ``reader_reason`` set (ADR-0211). ``coefficient_unit_mismatch`` / ``category_pair_not_found``
/ ``query_target_not_a_category`` are defensive guards with no gold fixture (tested by
construction); they never fire on the gold corpus.
"""
from __future__ import annotations
from generate.constraint_comprehension.expr import LinearConstraint, LinearExpr
from generate.constraint_comprehension.model import (
AttributeFact,
ConstraintProblem,
ConstraintQuery,
Unknown,
)
from generate.meaning_graph.reader import Refusal, _split_sentences
#: Coefficient-clause verbs. The category words sit between the article and the first of these;
#: ``worth`` follows ``is`` and is skipped. Totals use other verbs (rents/buys/carry/…) and are
#: classified separately by their noun, so they never reach coefficient parsing.
_COEFF_VERBS = frozenset({"holds", "hold", "has", "have", "costs", "cost", "is", "are"})
#: Tokens that close the noun phrase after a count/weighted digit.
_NP_STOP = frozenset({"in", "for", "all", "some", "and", "to", "of", "with", "that"})
_DOMAIN = "nonnegative_integer"
def _singular(noun: str) -> str:
"""Conservative singularization (``buses``->``bus``, ``boxes``->``box``, ``legs``->``leg``)."""
noun = noun.strip(".,?!")
if noun.endswith("es") and noun[:-2].endswith(("x", "s", "z", "ch", "sh")):
return noun[:-2]
if noun.endswith("s") and len(noun) > 1:
return noun[:-1]
return noun
def _parse_coefficient_clause(clause: str) -> tuple[str, list[str], str, int] | None:
"""``(symbol, category_words, measured_unit, value)`` for a coefficient clause, else ``None``.
A coefficient clause starts with ``each`` (any category) or with ``a`` **and** contains
``worth`` (``A nickel is worth 5 cents``). The ``a``-without-``worth`` form is a framing /
total sentence (``A jar holds 20 coins``) and is rejected here so it is classified as a total.
"""
toks = clause.lower().split()
if not toks or toks[0] not in ("each", "a"):
return None
if toks[0] == "a" and "worth" not in toks:
return None
verb_i = next((i for i in range(1, len(toks)) if toks[i] in _COEFF_VERBS), None)
if verb_i is None or verb_i == 1:
return None
category_words = toks[1:verb_i]
digit_i = next((j for j in range(verb_i + 1, len(toks)) if toks[j].strip(".,").isdigit()), None)
if digit_i is None or digit_i + 1 >= len(toks):
return None
value = int(toks[digit_i].strip(".,"))
measured_unit = _singular(toks[digit_i + 1])
return "_".join(category_words), category_words, measured_unit, value
def _split_coeff_clauses(sentence: str) -> list[str]:
"""Split a coefficient sentence into clauses on commas and ``and`` (``Each X … and each Y …``)."""
parts: list[str] = []
for chunk in sentence.split(","):
parts.extend(chunk.split(" and "))
return [p.strip() for p in parts if p.strip()]
def _digit_and_head(sentence: str) -> tuple[str | None, int | None]:
"""The first integer in *sentence* and the singular head noun of the phrase that follows it."""
toks = sentence.lower().rstrip("?.!").split()
for i, tok in enumerate(toks):
if tok.strip(".,").isdigit():
value = int(tok.strip(".,"))
phrase: list[str] = []
for nxt in toks[i + 1:]:
if nxt.endswith(","):
phrase.append(nxt[:-1])
break
if nxt in _NP_STOP:
break
phrase.append(nxt)
if not phrase:
return None, None
return _singular(phrase[-1]), value
return None, None
def _query_symbol(toks: list[str]) -> str | None:
"""``How many <category> are there?`` -> the (singularized, joined) category symbol."""
if "are" not in toks:
return None
words = toks[2 : toks.index("are")]
if not words:
return None
return "_".join(words[:-1] + [_singular(words[-1])])
def read_constraint_problem(text: str) -> ConstraintProblem | Refusal:
"""Comprehend two-category constraint prose into a typed :class:`ConstraintProblem`, or refuse."""
if not text or not text.strip():
return Refusal("empty")
coefficients: list[tuple[str, list[str], str, int]] = []
query_words: str | None = None
leftover: list[str] = []
for body, _term, _start, _end in _split_sentences(text):
toks = body.lower().rstrip("?.!").split()
if len(toks) >= 2 and toks[0] == "how" and toks[1] == "many":
query_words = _query_symbol(toks)
continue
parsed_any = False
for clause in _split_coeff_clauses(body):
pc = _parse_coefficient_clause(clause)
if pc is not None:
coefficients.append(pc)
parsed_any = True
if not parsed_any:
leftover.append(body)
# C5 — exactly two distinct categories (order preserved).
coeff_value: dict[str, int] = {}
coeff_unit: dict[str, str] = {}
entity: dict[str, str] = {}
order: list[str] = []
for symbol, words, mu, value in coefficients:
if symbol in coeff_value and coeff_value[symbol] != value:
return Refusal("coefficient_conflict", symbol)
if symbol not in coeff_value:
order.append(symbol)
coeff_value[symbol], coeff_unit[symbol], entity[symbol] = value, mu, " ".join(words)
if len(order) > 2:
return Refusal("too_many_categories", f"{order}")
if len(order) != 2:
return Refusal("category_pair_not_found", f"{order}")
# C6 — the two coefficients must share one measured unit.
if len({coeff_unit[s] for s in order}) != 1:
return Refusal("coefficient_unit_mismatch", f"{[coeff_unit[s] for s in order]}")
measured_unit = coeff_unit[order[0]]
# C7 / C8 — classify the leftover digit sentences: collective unit -> count; measured -> weighted.
total_count: int | None = None
collective: str | None = None
weighted_total: int | None = None
for sentence in leftover:
head, value = _digit_and_head(sentence)
if value is None:
continue
if head == measured_unit:
weighted_total = value
else:
total_count, collective = value, head
if total_count is None or collective is None:
return Refusal("missing_total_count")
if weighted_total is None:
return Refusal("missing_weighted_total")
# C9 — the query must name one of the two categories.
if query_words is None or query_words not in order:
return Refusal("query_target_not_a_category", f"{query_words}")
s0, s1 = order
unknowns = tuple(
Unknown(symbol=s, entity=entity[s], unit=collective, domain=_DOMAIN) for s in order
)
facts = tuple(
AttributeFact(category=s, measured_unit=measured_unit, value=coeff_value[s]) for s in order
)
constraints = (
LinearConstraint(LinearExpr(((s0, 1), (s1, 1))), "eq", total_count),
LinearConstraint(
LinearExpr(((s0, coeff_value[s0]), (s1, coeff_value[s1]))), "eq", weighted_total
),
)
return ConstraintProblem(unknowns, facts, constraints, ConstraintQuery(query_words, collective))
__all__ = ["read_constraint_problem"]

View file

@ -68,6 +68,13 @@ def test_no_matching_option_refuses() -> None:
assert isinstance(out, Refusal) and out.reason == "no_matching_option"
def test_exact_match_only_never_nearest() -> None:
# Hazard: a proven value with no exact option REFUSES — it never snaps to the nearest
# (10 or 12). Exact-or-refuse is the wrong=0 boundary for answer-choice tie-in.
out = verify_answer_choice(11, {"A": 10, "B": 12, "C": 13, "D": 14}, "B")
assert isinstance(out, Refusal) and out.reason == "no_matching_option"
def test_ambiguous_duplicate_options_refuse() -> None:
out = verify_answer_choice(4, {"A": 4, "B": 4}, None)
assert isinstance(out, Refusal) and out.reason == "ambiguous_options"

View file

@ -0,0 +1,110 @@
"""Tests for the R2 two-category reader (C5C9).
Pins the wrong=0 reader contract: every well-formed fixture reads to EXACTLY the gold setup
signature, every ``reader_refuses`` fixture refuses with its gold reason, and proving each
reader slice end to end every solved fixture reads -> solves -> ties to its labeled answer.
The defensive guards (coefficient unit mismatch, off-category query) are exercised by
construction; the too-many-categories guard is shown meaningful-fail against a 2-category twin.
"""
from __future__ import annotations
from evals.constraint_oracle.runner import _load_r2_gold, gold_to_problem, run_reader
from evals.constraint_oracle.signature import constraint_setup_signature
from generate.answer_choices.verify import ChoiceVerdict, verify_answer_choice
from generate.constraint_comprehension.reader import read_constraint_problem
from generate.constraint_comprehension.solver import answer_constraint_problem
from generate.meaning_graph.reader import Refusal
def _by_expect(expect: str) -> list[dict]:
return [f for f in _load_r2_gold() if f["expect"] == expect]
def test_reader_lane_is_wrong_zero_and_complete() -> None:
r = run_reader()
assert r["setup_wrong"] == 0
assert r["reason_mismatch"] == 0
assert r["setup_refused"] == 0 # every well-formed fixture reads at C9
assert r["setup_correct"] == 10 # 7 solved + 3 solver_refuses (all have valid setups)
assert r["refused_correct"] == 3 # the three reader_refuses fixtures
def test_reader_reads_every_well_formed_fixture_to_gold_signature() -> None:
for fx in _by_expect("solved") + _by_expect("solver_refuses"):
out = read_constraint_problem(fx["text"])
assert not isinstance(out, Refusal), f"{fx['id']} refused: {getattr(out, 'reason', '')}"
assert constraint_setup_signature(out) == constraint_setup_signature(gold_to_problem(fx)), fx["id"]
def test_reader_refuses_every_reader_refuse_fixture_with_its_reason() -> None:
for fx in _by_expect("reader_refuses"):
out = read_constraint_problem(fx["text"])
assert isinstance(out, Refusal), fx["id"]
assert out.reason == fx["reader_reason"], f"{fx['id']}: {out.reason} != {fx['reader_reason']}"
def test_read_solve_verify_end_to_end_for_solved() -> None:
# The full chain a reader slice must prove: read -> solve -> tie to the labeled option.
for fx in _by_expect("solved"):
problem = read_constraint_problem(fx["text"])
assert not isinstance(problem, Refusal), fx["id"]
value = answer_constraint_problem(problem)
assert value == fx["gold"], fx["id"]
verdict = verify_answer_choice(value, fx["options"], fx["answer"], noun=problem.query.unit)
assert isinstance(verdict, ChoiceVerdict) and verdict.status == "consistent"
assert verdict.computed_label == fx["answer"]
def test_read_then_solver_refuses_for_solver_refuse_fixtures() -> None:
# The reader reads the setup; the SOLVER owns solvability — read correct, solve refuses.
for fx in _by_expect("solver_refuses"):
problem = read_constraint_problem(fx["text"])
assert not isinstance(problem, Refusal), fx["id"]
out = answer_constraint_problem(problem)
assert isinstance(out, Refusal) and out.reason == fx["solver_reason"], fx["id"]
# --- defensive guards (no gold fixture; exercised by construction) --------------------- #
def test_coefficient_unit_mismatch_refuses() -> None:
out = read_constraint_problem(
"A shop has 5 things, all cars and trucks. Each car has 4 wheels and each truck costs "
"3 dollars. The things total 20 wheels. How many cars are there?"
)
assert isinstance(out, Refusal) and out.reason == "coefficient_unit_mismatch"
def test_weighted_total_in_wrong_unit_refuses() -> None:
# Hazard: the weighted total's unit must match the coefficient unit. Coefficients are in
# students; a total in DOLLARS matches no coefficient unit, so the weighted equation is
# never assembled -> missing_weighted_total. The reader never sums across units.
out = read_constraint_problem(
"A school rents 6 buses. Each large bus holds 50 students and each small bus holds "
"30 students. The buses cost 260 dollars in total. How many large buses are there?"
)
assert isinstance(out, Refusal) and out.reason == "missing_weighted_total"
def test_off_category_query_refuses() -> None:
out = read_constraint_problem(
"A school rents 6 buses for a trip. Each large bus holds 50 students and each small bus "
"holds 30 students. The buses carry 260 students in total. How many vans are there?"
)
assert isinstance(out, Refusal) and out.reason == "query_target_not_a_category"
def test_too_many_categories_is_meaningful_fail_against_two_category_twin() -> None:
# The 3-category text refuses; the SAME template with exactly two categories reads.
three = read_constraint_problem(
"A lot has 10 vehicles. Each car has 4 wheels, each motorcycle has 2 wheels, and each "
"truck has 6 wheels. Together the vehicles have 34 wheels. How many cars are there?"
)
assert isinstance(three, Refusal) and three.reason == "too_many_categories"
two = read_constraint_problem(
"A lot has 10 vehicles. Each car has 4 wheels and each motorcycle has 2 wheels. "
"Together the vehicles have 32 wheels. How many cars are there?"
)
assert not isinstance(two, Refusal)
assert {u.symbol for u in two.unknowns} == {"car", "motorcycle"}