diff --git a/docs/decisions/ADR-0211-r2-finite-integer-constraint-compiler.md b/docs/decisions/ADR-0211-r2-finite-integer-constraint-compiler.md new file mode 100644 index 00000000..e7ac2f7c --- /dev/null +++ b/docs/decisions/ADR-0211-r2-finite-integer-constraint-compiler.md @@ -0,0 +1,170 @@ +# ADR-0211 — R2: Finite-Integer Linear-Constraint Setup Compiler (off-serving) + +**Status:** Accepted (ratified 2026-06-07) +**Date:** 2026-06-07 +**Author:** Shay +**Anchor:** [[thesis-decoding-not-generating]] +**Current execution state:** IR (C1) + setup oracle / gold (C2) landed with this ADR; +the integer solver (C3), answer-choice verifier (C4), and reader (C5–C9) execute against +the gates below. R1 stays frozen at 7/0/3 (ADR-0207 surface untouched). +**Builds on (does not replace):** ADR-0207 (GSM8K substrate), ADR-0175 (calibrated +learning), ADR-0083 (transitive chain — the one executing R1 reasoning primitive). + +--- + +## 1. The shift this ratifies + +R1 grew one reader template per problem shape (`more_than`, `times_as_many`, `half`, +partition, aggregate-query, inverse). That ladder is now **closed** (R1 = 7/0/3; see +`docs/analysis/r1-inventory-ledger-2026-06-07.md`) and the per-shape path does not +generalize to harder problems. R2 changes the unit of work from + +```text +one problem shape -> one reader patch +``` + +to a **small algebra of reusable setup primitives**: + +```text +problem text -> entities -> quantities -> relations -> CONSTRAINTS -> goal -> solver -> verifier +``` + +A new problem family is admitted only when it can be expressed as **known primitive +composition + setup oracle + answer verifier + refusal tests** — never as a bespoke matcher. +This is the same discipline ADR-0207 ratified for the comprehension substrate, extended one +level up to constraint *systems*. + +> If anyone proposes a "new GSM8K reader" or a per-shape matcher for two-category constraint +> problems after this ADR, it is redundant with this document. Redirect here. + +## 2. Scope — R2 v1 + +**In:** a single **two-category, finite-integer linear system** of exactly two equations: + +```text +x + y = N (total count) +a·x + b·y = T (weighted total) +x, y ∈ nonnegative integers +``` + +covering buses/seats, chickens/legs, tickets/prices, coins/values, boxes/items, +vehicles/wheels — anything that reduces to this shape. The deliverable is a **verified +setup first**, then an exact integer solve, then answer-choice verification. + +**Deferred to R3 (explicitly NOT in this batch):** ≥3 categories, inequalities, multi-step / +mixed constraints, distractor exclusion, rates / unit conversion, and the **typed +contemplation loop + reviewed-failure learning** (the plan's Phases 6–7). When the +failure-learning half is built it routes through the existing `teaching/*` proposal-only +flywheel (ADR-0055/0056/0057) — it MUST NOT become a parallel correction path (CLAUDE.md). + +## 3. The IR — `generate/constraint_comprehension` + +Strings are serialization only; meaning lives in typed, frozen, slotted dataclasses (the R2 +twin of `generate.quantitative_expr`): + +- `expr.py` — `LinearExpr(terms: ((symbol, coeff), …), constant)`, `LinearConstraint(lhs, + relation="eq", rhs, source_span?)`. Integers only; no floats representable. +- `model.py` — `Unknown(symbol, entity, unit, domain)` with `domain ∈ {nonnegative_integer, + integer}`; `AttributeFact(category, measured_unit, value)` (per-category coefficient + provenance); `ConstraintQuery(symbol, unit)`; `ConstraintProblem(unknowns, facts, + constraints, query)`. + +The query is a dedicated `ConstraintQuery`, **not** R1's `BoundUnknown` — R2 has no +state-index / question-form axis, and forcing R1's type would be a degenerate fit. + +## 4. The ruler — `evals/constraint_oracle` (independent) + +The setup oracle grades a comprehended `ConstraintProblem` against independent gold by a +**span-free canonical signature** (`signature.py`): unknowns `(symbol, unit, domain)`, +attribute coefficients, the canonical linear system (terms merged + sorted, the lhs constant +folded into the rhs, source spans stripped), and the query. Two setups are equal iff every +component matches; a mismatch localizes the diverging axis. This is the R2 twin of +`evals.setup_oracle.signature`, and — like it — imports **no** `generate.derivation` / +`core.reliability_gate` (§6). + +The gold (`r2_gold.jsonl`, 13 fixtures) carries a **closed `expect` taxonomy**: + +| `expect` | meaning | gold | graded by | +|---|---|---|---| +| `solved` | well-formed setup; integer answer; `options[answer] == gold` | int | reader (C5–C9) + solver (C3) + answer-choice (C4) | +| `solver_refuses` | well-formed setup, but no nonnegative-integer answer | none | solver (C3) | +| `reader_refuses` | incomplete/ambiguous prose the reader must not assemble | none | reader (C5–C9) | + +Closed refusal sets (grow only by ratified extension, each with its fixture): + +- `solver_reason ∈ {indistinguishable_weights, non_integer_solution, negative_solution, + verification_failed}` +- `reader_reason ∈ {missing_total_count, missing_weighted_total, too_many_categories}` + (C6/C8 may add coefficient-level reasons — equal coefficients, unit mismatch — each + ratified with a fixture). + +C2 ships a **gold-validation lane** only (no reader yet): every fixture deserializes into the +IR, canonicalizes deterministically, has a closed taxonomy, and — for `solved` — a coherent +answer key. `python -m evals.constraint_oracle` exits 0 iff `invalid == 0` (currently 13/13). + +## 5. The wrong=0 contract + +R2 carries the same invariant as the rest of the engine: **never emit a wrong answer; refuse +instead.** It is enforced at four independent gates, each wired to fail loudly: + +1. **Setup oracle** — any drift in unknowns/units/constraints/query vs gold ⇒ `setup_wrong` + (the reader must refuse an unsupported shape, never misread it as a simpler one). +2. **Reader** — incomplete or ambiguous prose (missing a constraint, >2 categories) ⇒ a typed + refusal at assembly time, never a fabricated constraint. +3. **Solver (C3)** — exact integer arithmetic only: `indistinguishable_weights` (equal + coefficients), `non_integer_solution` (`numer % denom ≠ 0` — never rounds), + `negative_solution`, and a final `verification_failed` re-substitution check. No floats, + no nearest-option snapping. +4. **Answer-choice verifier (C4)** — exactly one option may match the proven value; + `0`/`>1` matches refuse; a provided key that disagrees with the proven value is **flagged + as a contradiction**, not silently accepted (truth discipline: "the math says A; the key + says C — the key is wrong"). + +### Schema-proof obligations (per CLAUDE.md) + +Each gate above is real only because a test fails under the violation it catches: the C2 +validator has per-branch meaningful-fail tests (incoherent answer key, three categories, +constraint referencing an unknown symbol, refusal carrying a gold, unknown reason/expect); +C3/C4 ship the same for their refusals. A gate without such a test is decoration, not proof. + +## 6. Off-serving disjointness + +`generate/constraint_comprehension` and `evals/constraint_oracle` import **no** +`generate.derivation` and **no** `core.reliability_gate` — the GSM8K serving path. R2 is a +parallel organ graded by its own independent oracle, so it **cannot regress** the sealed +serving metric (`train_sample`) or any pinned lane SHA. Consequently the per-commit gate is +`pytest` on the R2 files + the R1/15-case regression, **not** the pinned-SHA lane; the SHA +gate runs once at PR-submission to confirm zero serving drift. + +## 7. Build ladder + +| Commit | Adds | Local gate | +|---|---|---| +| C1 | constraint IR (`expr`, `model`) | IR tests | +| C2 | gold + signature + validation runner + **this ADR** | `constraint_oracle` 13/13 valid | +| C3 | two-variable integer solver + refusal tests | buses→4, chickens→11; refusals fire | +| C4 | answer-choice parse + verify (contradiction flag) | computed-vs-key contradiction test | +| C5–C9 | reader: category-pair → coefficients → total-count → weighted-total → query-target | setup_wrong stays 0; supported fixtures flip | + +After C9: R2 setup nonzero-correct / **0 wrong** / rest refused; answers likewise; answer-key +contradictions flagged; serving unchanged. (Plan Phases 6–7 are a later batch — §2.) + +## 8. What this reuses, and does not reinvent + +- **ADR-0207** — R2 is the constraint-systems layer *above* the comprehension substrate, off + the serving path; it does not touch `generate.derivation`. +- **ADR-0175** — a new capability family is admitted only with gold + oracle + refusal tests; + R2 adds no per-shape matcher and no serving bridge. +- **ADR-0083** — the R1 transitive chain is the one executing R1 reasoning primitive; R2 adds + *linear-system solving* as a new, independently-verified primitive (the C3 solver). +- **`evals.setup_oracle` pattern** — R2 mirrors the R1 ruler (signature + gold + runner) + rather than inventing a new scoring mechanism. +- **ADR-0055/0056/0057** — the future failure-learning half (R3) routes through the existing + proposal-only teaching flywheel; no parallel correction path. + +## 9. Decision + +Build R2 v1 as the off-serving finite-integer constraint setup compiler on the C1–C9 ladder. +The contract is pinned by the gold and this ADR; capability grows only where the gold + +oracle + refusal tests already license it. No guessed math, no silent correction, no answer +without a proven setup. diff --git a/evals/constraint_oracle/__init__.py b/evals/constraint_oracle/__init__.py new file mode 100644 index 00000000..69164b70 --- /dev/null +++ b/evals/constraint_oracle/__init__.py @@ -0,0 +1,7 @@ +"""R2 constraint setup oracle (off-serving) — the independent ruler for the R2 organ. + +Grades a comprehended :class:`ConstraintProblem` against independent gold by a span-free +canonical signature (``signature``), backed by a reviewable gold corpus (``r2_gold.jsonl``) +and a validation runner (``runner``). The R2 twin of ``evals.setup_oracle``. Imports no +``generate.derivation`` / ``core.reliability_gate`` — disjoint from the GSM8K serving path. +""" diff --git a/evals/constraint_oracle/__main__.py b/evals/constraint_oracle/__main__.py new file mode 100644 index 00000000..99667f1b --- /dev/null +++ b/evals/constraint_oracle/__main__.py @@ -0,0 +1,20 @@ +"""CLI: validate the R2 constraint gold. + + python -m evals.constraint_oracle # validate r2_gold.jsonl; exit 0 iff invalid == 0 +""" + +from __future__ import annotations + +import json + +from evals.constraint_oracle.runner import run + + +def main() -> int: + report = run() + print(json.dumps(report, indent=2, default=str)) + return 0 if report["invalid"] == 0 else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/evals/constraint_oracle/r2_gold.jsonl b/evals/constraint_oracle/r2_gold.jsonl new file mode 100644 index 00000000..ac8327c7 --- /dev/null +++ b/evals/constraint_oracle/r2_gold.jsonl @@ -0,0 +1,13 @@ +{"id": "r2-001-buses", "expect": "solved", "text": "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 large buses are there?", "unknowns": [{"symbol": "large_bus", "entity": "large bus", "unit": "bus", "domain": "nonnegative_integer"}, {"symbol": "small_bus", "entity": "small bus", "unit": "bus", "domain": "nonnegative_integer"}], "facts": [{"category": "large_bus", "measured_unit": "student", "value": 50}, {"category": "small_bus", "measured_unit": "student", "value": 30}], "constraints": [{"terms": [["large_bus", 1], ["small_bus", 1]], "relation": "eq", "rhs": 6}, {"terms": [["large_bus", 50], ["small_bus", 30]], "relation": "eq", "rhs": 260}], "query": {"symbol": "large_bus", "unit": "bus"}, "gold": 4, "options": {"A": 2, "B": 3, "C": 4, "D": 5}, "answer": "C", "notes": "Canonical two-category count/weight system: large+small=6, 50*large+30*small=260 -> large=4, small=2."} +{"id": "r2-002-chickens", "expect": "solved", "text": "A farm has 18 animals, all chickens and cows. Altogether the animals have 50 legs. Each chicken has 2 legs and each cow has 4 legs. How many chickens are there?", "unknowns": [{"symbol": "chicken", "entity": "chicken", "unit": "animal", "domain": "nonnegative_integer"}, {"symbol": "cow", "entity": "cow", "unit": "animal", "domain": "nonnegative_integer"}], "facts": [{"category": "chicken", "measured_unit": "leg", "value": 2}, {"category": "cow", "measured_unit": "leg", "value": 4}], "constraints": [{"terms": [["chicken", 1], ["cow", 1]], "relation": "eq", "rhs": 18}, {"terms": [["chicken", 2], ["cow", 4]], "relation": "eq", "rhs": 50}], "query": {"symbol": "chicken", "unit": "animal"}, "gold": 11, "options": {"A": 11, "B": 7, "C": 9, "D": 13}, "answer": "A", "notes": "chicken+cow=18, 2*chicken+4*cow=50 -> chicken=11, cow=7."} +{"id": "r2-003-tickets", "expect": "solved", "text": "A family buys 40 tickets in total, some adult and some child. Each adult ticket costs 12 dollars and each child ticket costs 8 dollars. The tickets cost 400 dollars in total. How many adult tickets are there?", "unknowns": [{"symbol": "adult_ticket", "entity": "adult ticket", "unit": "ticket", "domain": "nonnegative_integer"}, {"symbol": "child_ticket", "entity": "child ticket", "unit": "ticket", "domain": "nonnegative_integer"}], "facts": [{"category": "adult_ticket", "measured_unit": "dollar", "value": 12}, {"category": "child_ticket", "measured_unit": "dollar", "value": 8}], "constraints": [{"terms": [["adult_ticket", 1], ["child_ticket", 1]], "relation": "eq", "rhs": 40}, {"terms": [["adult_ticket", 12], ["child_ticket", 8]], "relation": "eq", "rhs": 400}], "query": {"symbol": "adult_ticket", "unit": "ticket"}, "gold": 20, "options": {"A": 15, "B": 20, "C": 25, "D": 10}, "answer": "B", "notes": "adult+child=40, 12*adult+8*child=400 -> adult=20, child=20."} +{"id": "r2-004-coins", "expect": "solved", "text": "A jar holds 20 coins, all nickels and dimes. A nickel is worth 5 cents and a dime is worth 10 cents. The coins are worth 145 cents in total. How many dimes are there?", "unknowns": [{"symbol": "nickel", "entity": "nickel", "unit": "coin", "domain": "nonnegative_integer"}, {"symbol": "dime", "entity": "dime", "unit": "coin", "domain": "nonnegative_integer"}], "facts": [{"category": "nickel", "measured_unit": "cent", "value": 5}, {"category": "dime", "measured_unit": "cent", "value": 10}], "constraints": [{"terms": [["nickel", 1], ["dime", 1]], "relation": "eq", "rhs": 20}, {"terms": [["nickel", 5], ["dime", 10]], "relation": "eq", "rhs": 145}], "query": {"symbol": "dime", "unit": "coin"}, "gold": 9, "options": {"A": 9, "B": 11, "C": 7, "D": 13}, "answer": "A", "notes": "nickel+dime=20, 5*nickel+10*dime=145 -> nickel=11, dime=9. Query asks the SECOND category (dime), guarding against a solver that only returns the first variable."} +{"id": "r2-005-boxes", "expect": "solved", "text": "A warehouse packs 12 boxes, some large and some small. Each large box holds 20 items and each small box holds 8 items. The boxes hold 144 items in total. How many large boxes are there?", "unknowns": [{"symbol": "large_box", "entity": "large box", "unit": "box", "domain": "nonnegative_integer"}, {"symbol": "small_box", "entity": "small box", "unit": "box", "domain": "nonnegative_integer"}], "facts": [{"category": "large_box", "measured_unit": "item", "value": 20}, {"category": "small_box", "measured_unit": "item", "value": 8}], "constraints": [{"terms": [["large_box", 1], ["small_box", 1]], "relation": "eq", "rhs": 12}, {"terms": [["large_box", 20], ["small_box", 8]], "relation": "eq", "rhs": 144}], "query": {"symbol": "large_box", "unit": "box"}, "gold": 4, "options": {"A": 4, "B": 6, "C": 8, "D": 2}, "answer": "A", "notes": "large+small=12, 20*large+8*small=144 -> large=4, small=8."} +{"id": "r2-006-vehicles", "expect": "solved", "text": "A parking lot has 10 vehicles, all cars and motorcycles. Each car has 4 wheels and each motorcycle has 2 wheels. Together the vehicles have 32 wheels. How many cars are there?", "unknowns": [{"symbol": "car", "entity": "car", "unit": "vehicle", "domain": "nonnegative_integer"}, {"symbol": "motorcycle", "entity": "motorcycle", "unit": "vehicle", "domain": "nonnegative_integer"}], "facts": [{"category": "car", "measured_unit": "wheel", "value": 4}, {"category": "motorcycle", "measured_unit": "wheel", "value": 2}], "constraints": [{"terms": [["car", 1], ["motorcycle", 1]], "relation": "eq", "rhs": 10}, {"terms": [["car", 4], ["motorcycle", 2]], "relation": "eq", "rhs": 32}], "query": {"symbol": "car", "unit": "vehicle"}, "gold": 6, "options": {"A": 4, "B": 6, "C": 8, "D": 5}, "answer": "B", "notes": "car+motorcycle=10, 4*car+2*motorcycle=32 -> car=6, motorcycle=4."} +{"id": "r2-007-pens", "expect": "solved", "text": "A store sells 15 writing tools, all pens and pencils. Each pen costs 3 dollars and each pencil costs 1 dollar. The tools cost 33 dollars in total. How many pens are there?", "unknowns": [{"symbol": "pen", "entity": "pen", "unit": "tool", "domain": "nonnegative_integer"}, {"symbol": "pencil", "entity": "pencil", "unit": "tool", "domain": "nonnegative_integer"}], "facts": [{"category": "pen", "measured_unit": "dollar", "value": 3}, {"category": "pencil", "measured_unit": "dollar", "value": 1}], "constraints": [{"terms": [["pen", 1], ["pencil", 1]], "relation": "eq", "rhs": 15}, {"terms": [["pen", 3], ["pencil", 1]], "relation": "eq", "rhs": 33}], "query": {"symbol": "pen", "unit": "tool"}, "gold": 9, "options": {"A": 6, "B": 9, "C": 7, "D": 12}, "answer": "B", "notes": "pen+pencil=15, 3*pen+1*pencil=33 -> pen=9, pencil=6."} +{"id": "r2-008-negative", "expect": "solver_refuses", "solver_reason": "negative_solution", "text": "A school rents 6 buses. Each large bus holds 50 students and each small bus holds 30 students. The buses carry 400 students in total. How many large buses are there?", "unknowns": [{"symbol": "large_bus", "entity": "large bus", "unit": "bus", "domain": "nonnegative_integer"}, {"symbol": "small_bus", "entity": "small bus", "unit": "bus", "domain": "nonnegative_integer"}], "facts": [{"category": "large_bus", "measured_unit": "student", "value": 50}, {"category": "small_bus", "measured_unit": "student", "value": 30}], "constraints": [{"terms": [["large_bus", 1], ["small_bus", 1]], "relation": "eq", "rhs": 6}, {"terms": [["large_bus", 50], ["small_bus", 30]], "relation": "eq", "rhs": 400}], "query": {"symbol": "large_bus", "unit": "bus"}, "gold": null, "notes": "Well-formed setup but 400 students needs large=11 > 6 buses -> small=-5 < 0. The solver REFUSES (negative_solution); no nonnegative-integer answer exists."} +{"id": "r2-009-non-integer", "expect": "solver_refuses", "solver_reason": "non_integer_solution", "text": "A shop sells 10 items, all pens and notebooks. Each pen costs 3 dollars and each notebook costs 5 dollars. The items cost 37 dollars in total. How many pens are there?", "unknowns": [{"symbol": "pen", "entity": "pen", "unit": "item", "domain": "nonnegative_integer"}, {"symbol": "notebook", "entity": "notebook", "unit": "item", "domain": "nonnegative_integer"}], "facts": [{"category": "pen", "measured_unit": "dollar", "value": 3}, {"category": "notebook", "measured_unit": "dollar", "value": 5}], "constraints": [{"terms": [["pen", 1], ["notebook", 1]], "relation": "eq", "rhs": 10}, {"terms": [["pen", 3], ["notebook", 5]], "relation": "eq", "rhs": 37}], "query": {"symbol": "pen", "unit": "item"}, "gold": null, "notes": "pen+notebook=10, 3*pen+5*notebook=37 -> pen=6.5: no integer solution. The solver REFUSES (non_integer_solution), never rounds."} +{"id": "r2-010-indistinguishable", "expect": "solver_refuses", "solver_reason": "indistinguishable_weights", "text": "A lot has 8 vehicles, all cars and trucks. Each car has 4 wheels and each truck has 4 wheels. Together the vehicles have 32 wheels. How many cars are there?", "unknowns": [{"symbol": "car", "entity": "car", "unit": "vehicle", "domain": "nonnegative_integer"}, {"symbol": "truck", "entity": "truck", "unit": "vehicle", "domain": "nonnegative_integer"}], "facts": [{"category": "car", "measured_unit": "wheel", "value": 4}, {"category": "truck", "measured_unit": "wheel", "value": 4}], "constraints": [{"terms": [["car", 1], ["truck", 1]], "relation": "eq", "rhs": 8}, {"terms": [["car", 4], ["truck", 4]], "relation": "eq", "rhs": 32}], "query": {"symbol": "car", "unit": "vehicle"}, "gold": null, "notes": "Equal coefficients (4 == 4): the weighted total carries no information beyond the count, so the system is underdetermined. The solver REFUSES (indistinguishable_weights)."} +{"id": "r2-011-missing-total-count", "expect": "reader_refuses", "reader_reason": "missing_total_count", "text": "Each large bus holds 50 students and each small bus holds 30 students. The buses carry 260 students in total. How many large buses are there?", "gold": null, "notes": "The weighted total (260 students) is given but the total number of buses is NOT. With only one constraint the system is underdetermined; the reader must REFUSE to assemble it (missing_total_count), never invent a count."} +{"id": "r2-012-missing-weighted-total", "expect": "reader_refuses", "reader_reason": "missing_weighted_total", "text": "A school rents 6 buses. Each large bus holds 50 students and each small bus holds 30 students. How many large buses are there?", "gold": null, "notes": "The total bus count (6) is given but no student total. Only the count constraint exists; the system is underdetermined. The reader must REFUSE (missing_weighted_total)."} +{"id": "r2-013-too-many-categories", "expect": "reader_refuses", "reader_reason": "too_many_categories", "text": "A lot has 10 vehicles: cars, motorcycles, and trucks. 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?", "gold": null, "notes": "Three categories — v1 admits exactly two. A two-variable count/weight solver cannot determine three unknowns from two totals; the reader must REFUSE (too_many_categories)."} diff --git a/evals/constraint_oracle/runner.py b/evals/constraint_oracle/runner.py new file mode 100644 index 00000000..eeb049b5 --- /dev/null +++ b/evals/constraint_oracle/runner.py @@ -0,0 +1,172 @@ +"""R2 constraint setup-oracle runner — the RULER, before any reader capability (C2). + +There is no R2 reader yet (it lands C5+). This lane validates that the independent gold is +internally coherent and canonicalizes stably: every fixture deserializes into the typed +:class:`ConstraintProblem` IR, its setup signature is deterministic, its taxonomy is closed, +and — for ``solved`` fixtures — the provided multiple-choice key agrees with the gold value. +When the reader lands, a grading lane compares the reader's signature against these same gold +signatures; the solver lane (C3) verifies that each ``solved`` setup actually computes ``gold``. + +Exit 0 iff ``invalid == 0``. "Zero capability" is the point: this proves the ruler, not a reader. + +Gold fixture ``expect`` taxonomy (closed): + - ``solved`` — well-formed two-category / two-constraint setup; ``gold`` is the int + answer; ``options[answer] == gold`` (coherent key). + - ``solver_refuses`` — well-formed setup, but unsolvable; ``solver_reason`` says why; no gold. + - ``reader_refuses`` — incomplete/ambiguous prose the reader must refuse to assemble; + ``reader_reason`` says why; no setup fields required, no gold. +""" + +from __future__ import annotations + +import json +from pathlib import Path +from typing import Any + +from evals.constraint_oracle.signature import constraint_setup_signature +from generate.constraint_comprehension.expr import LinearConstraint, LinearExpr +from generate.constraint_comprehension.model import ( + AttributeFact, + ConstraintProblem, + ConstraintQuery, + Unknown, +) + +_R2_GOLD_PATH = Path(__file__).resolve().parent / "r2_gold.jsonl" + +#: Closed taxonomies. ``READER_REASONS`` grows as reader slices (C6/C8) add coefficient-level +#: refusals (equal coefficients, unit mismatch, …); each addition is ratified with its fixture. +EXPECTATIONS = frozenset({"solved", "solver_refuses", "reader_refuses"}) +SOLVER_REASONS = frozenset( + {"indistinguishable_weights", "non_integer_solution", "negative_solution", "verification_failed"} +) +READER_REASONS = frozenset({"missing_total_count", "missing_weighted_total", "too_many_categories"}) +DOMAINS = frozenset({"nonnegative_integer", "integer"}) + + +def _load_r2_gold() -> list[dict[str, Any]]: + return [ + json.loads(line) + for line in _R2_GOLD_PATH.read_text(encoding="utf-8").splitlines() + if line.strip() + ] + + +def gold_to_problem(fx: dict[str, Any]) -> ConstraintProblem: + """Deserialize a gold fixture's setup fields into the typed ConstraintProblem IR. + + Terms arrive as ``[symbol, coefficient]`` pairs (the pinned serialization). Raises the + standard ``KeyError``/``TypeError``/``ValueError`` on a malformed fixture — the validator + turns that into an ``invalid`` outcome rather than a crash. + """ + unknowns = tuple( + Unknown(u["symbol"], u["entity"], u["unit"], u["domain"]) for u in fx["unknowns"] + ) + facts = tuple( + AttributeFact(f["category"], f["measured_unit"], int(f["value"])) + for f in fx.get("facts", []) + ) + constraints = tuple( + LinearConstraint( + LinearExpr( + tuple((str(s), int(c)) for s, c in con["terms"]), + int(con.get("constant", 0)), + ), + con["relation"], + int(con["rhs"]), + ) + for con in fx["constraints"] + ) + q = fx["query"] + return ConstraintProblem(unknowns, facts, constraints, ConstraintQuery(q["symbol"], q["unit"])) + + +def validate_fixture(fx: dict[str, Any]) -> tuple[str, str | None]: + """Validate one gold fixture's internal coherence. Returns ``(outcome, reason)`` where + ``outcome`` is ``"valid"`` or ``"invalid"`` and ``reason`` names the failing check.""" + expect = fx.get("expect") + if expect not in EXPECTATIONS: + return "invalid", f"unknown_expect:{expect!r}" + + if expect == "reader_refuses": + if fx.get("reader_reason") not in READER_REASONS: + return "invalid", f"unknown_reader_reason:{fx.get('reader_reason')!r}" + if fx.get("gold") is not None: + return "invalid", "reader_refuses_has_gold" + return "valid", None + + # solved | solver_refuses both require a well-formed two-category, two-constraint setup. + try: + problem = gold_to_problem(fx) + except (KeyError, TypeError, ValueError) as exc: + return "invalid", f"malformed_setup:{exc}" + + symbols = {u.symbol for u in problem.unknowns} + if len(problem.unknowns) != 2 or len(symbols) != 2: + return "invalid", "v1_requires_exactly_two_distinct_categories" + if any(u.domain not in DOMAINS for u in problem.unknowns): + return "invalid", "bad_domain" + if len(problem.constraints) != 2: + return "invalid", "v1_requires_exactly_two_constraints" + if any(sym not in symbols for c in problem.constraints for sym, _ in c.lhs.terms): + return "invalid", "constraint_references_unknown_symbol" + if any(f.category not in symbols for f in problem.facts): + return "invalid", "fact_references_unknown_symbol" + if problem.query.symbol not in symbols: + return "invalid", "query_target_not_a_category" + if constraint_setup_signature(problem) != constraint_setup_signature(problem): + return "invalid", "nondeterministic_signature" # pragma: no cover - determinism guard + + if expect == "solver_refuses": + if fx.get("solver_reason") not in SOLVER_REASONS: + return "invalid", f"unknown_solver_reason:{fx.get('solver_reason')!r}" + if fx.get("gold") is not None: + return "invalid", "solver_refuses_has_gold" + return "valid", None + + # solved: an integer gold and a coherent multiple-choice key. + gold = fx.get("gold") + if not isinstance(gold, int) or isinstance(gold, bool): + return "invalid", "solved_needs_int_gold" + options, answer = fx.get("options"), fx.get("answer") + if not isinstance(options, dict) or answer not in options: + return "invalid", "missing_or_unlabeled_answer" + if options[answer] != gold: + return "invalid", "answer_key_incoherent" + return "valid", None + + +def run() -> dict[str, Any]: + """Validate every R2 gold fixture. Exit-0 criterion for the lane is ``invalid == 0``.""" + fixtures = _load_r2_gold() + valid = invalid = 0 + by_expect: dict[str, int] = {} + details: list[dict[str, Any]] = [] + for fx in fixtures: + outcome, reason = validate_fixture(fx) + expect = fx.get("expect", "?") + by_expect[expect] = by_expect.get(expect, 0) + 1 + if outcome == "valid": + valid += 1 + details.append({"id": fx.get("id"), "outcome": "valid", "expect": expect}) + else: + invalid += 1 + details.append({"id": fx.get("id"), "outcome": "invalid", "reason": reason}) + return { + "lane": "constraint_oracle_gold_validation", + "total": len(fixtures), + "valid": valid, + "invalid": invalid, + "by_expect": by_expect, + "details": details, + } + + +__all__ = [ + "EXPECTATIONS", + "READER_REASONS", + "SOLVER_REASONS", + "gold_to_problem", + "run", + "validate_fixture", +] diff --git a/evals/constraint_oracle/signature.py b/evals/constraint_oracle/signature.py new file mode 100644 index 00000000..c0ccb2d5 --- /dev/null +++ b/evals/constraint_oracle/signature.py @@ -0,0 +1,89 @@ +"""Span-free canonical signatures for the R2 constraint setup oracle. + +A *signature* is a deterministic, order-independent, span-free projection of a constraint +SETUP — what a reader claims a problem says, stripped of input spans and surface tokens. Two +setups are equivalent iff their signatures are equal. Used to compare a reader's comprehended +:class:`ConstraintProblem` against the independent gold (and, until the reader lands in C5+, +to prove the gold itself canonicalizes stably). + +The R2 twin of ``evals.setup_oracle.signature``. Pure, deterministic; no clock, no randomness. +""" + +from __future__ import annotations + +from typing import Any + +from generate.constraint_comprehension.expr import LinearConstraint, LinearExpr +from generate.constraint_comprehension.model import ( + AttributeFact, + ConstraintProblem, + ConstraintQuery, + Unknown, +) + + +def canonical_linear(expr: LinearExpr) -> tuple[tuple[tuple[str, int], ...], int]: + """Merge duplicate symbols, drop zero coefficients, sort by symbol -> ``(terms, constant)``.""" + merged: dict[str, int] = {} + for symbol, coeff in expr.terms: + merged[symbol] = merged.get(symbol, 0) + coeff + terms = tuple(sorted((s, c) for s, c in merged.items() if c != 0)) + return terms, expr.constant + + +def canonical_constraint(c: LinearConstraint) -> tuple[tuple[tuple[str, int], ...], str, int]: + """A span-free canonical equation: ``(merged sorted lhs terms, relation, rhs - lhs constant)``. + + Folding the lhs constant into the rhs makes ``x + y + 0 = 6`` and ``x + y = 6`` equal; the + source span never participates — two constraints are setup-equal iff lhs/relation/rhs match. + """ + terms, constant = canonical_linear(c.lhs) + return terms, c.relation, c.rhs - constant + + +def unknowns_signature(unknowns: tuple[Unknown, ...]) -> tuple[tuple[str, str, str], ...]: + """Sorted ``(symbol, unit, domain)`` per unknown — surface ``entity`` is provenance, excluded.""" + return tuple(sorted((u.symbol, u.unit, u.domain) for u in unknowns)) + + +def constraints_signature( + constraints: tuple[LinearConstraint, ...], +) -> tuple[tuple[tuple[tuple[str, int], ...], str, int], ...]: + """Order-independent canonical signature of the whole linear system.""" + return tuple(sorted((canonical_constraint(c) for c in constraints), key=repr)) + + +def query_signature(query: ConstraintQuery) -> tuple[str, str]: + return (query.symbol, query.unit) + + +def attribute_facts_signature( + facts: tuple[AttributeFact, ...], +) -> tuple[tuple[str, str, int], ...]: + """Sorted ``(category, measured_unit, value)`` — the per-category coefficient provenance.""" + return tuple(sorted((f.category, f.measured_unit, f.value) for f in facts)) + + +def constraint_setup_signature(problem: ConstraintProblem) -> dict[str, Any]: + """The composite setup signature: unknowns ∧ facts ∧ constraints ∧ query. + + A reader matches gold iff every component is equal. Returned as a dict so a mismatch + localizes which axis diverged (mirroring the R1 setup oracle's per-axis ``*_match`` detail). + """ + return { + "unknowns": unknowns_signature(problem.unknowns), + "facts": attribute_facts_signature(problem.facts), + "constraints": constraints_signature(problem.constraints), + "query": query_signature(problem.query), + } + + +__all__ = [ + "attribute_facts_signature", + "canonical_constraint", + "canonical_linear", + "constraint_setup_signature", + "constraints_signature", + "query_signature", + "unknowns_signature", +] diff --git a/tests/test_constraint_oracle.py b/tests/test_constraint_oracle.py new file mode 100644 index 00000000..65c48a0a --- /dev/null +++ b/tests/test_constraint_oracle.py @@ -0,0 +1,131 @@ +"""Tests for the R2 constraint setup oracle (C2) — the ruler before reader capability. + +The runner validates the gold's internal coherence; these tests pin that the validator is +NON-VACUOUS — each ``invalid`` branch fires loudly when its violation is introduced (the +schema-proof-obligation discipline: a gate is real only if a test would fail under the +violation it is written to catch). Also pins signature order-independence + constant folding. +""" + +from __future__ import annotations + +import copy +from typing import Any + +from evals.constraint_oracle.runner import ( + READER_REASONS, + SOLVER_REASONS, + _load_r2_gold, + gold_to_problem, + run, + validate_fixture, +) +from evals.constraint_oracle.signature import ( + canonical_constraint, + constraint_setup_signature, +) +from generate.constraint_comprehension.expr import LinearConstraint, LinearExpr +from generate.constraint_comprehension.model import ConstraintProblem + + +def _solved_fixture() -> dict[str, Any]: + return copy.deepcopy(next(f for f in _load_r2_gold() if f["expect"] == "solved")) + + +def test_run_validates_all_gold() -> None: + r = run() + assert r["invalid"] == 0 + assert r["valid"] == r["total"] == 13 + assert r["by_expect"] == {"solved": 7, "solver_refuses": 3, "reader_refuses": 3} + + +def test_gold_to_problem_roundtrips_bus() -> None: + fx = next(f for f in _load_r2_gold() if f["id"] == "r2-001-buses") + p = gold_to_problem(fx) + assert {u.symbol for u in p.unknowns} == {"large_bus", "small_bus"} + assert all(u.domain == "nonnegative_integer" for u in p.unknowns) + assert p.query.symbol == "large_bus" + assert len(p.constraints) == 2 + + +def test_signature_is_order_independent() -> None: + p = gold_to_problem(next(f for f in _load_r2_gold() if f["id"] == "r2-001-buses")) + shuffled = ConstraintProblem( + unknowns=tuple(reversed(p.unknowns)), + facts=tuple(reversed(p.facts)), + constraints=tuple( + LinearConstraint( + LinearExpr(tuple(reversed(c.lhs.terms)), c.lhs.constant), c.relation, c.rhs + ) + for c in reversed(p.constraints) + ), + query=p.query, + ) + assert constraint_setup_signature(shuffled) == constraint_setup_signature(p) + + +def test_canonical_constraint_folds_constant_and_merges_terms() -> None: + # x + y + 0x + 5 = 11 canonicalizes to ((x,1),(y,1)), "eq", 6 — constant folded into the + # rhs, the duplicate x merged, the zero-coefficient term dropped. + c = LinearConstraint(LinearExpr((("x", 1), ("y", 1), ("x", 0)), 5), "eq", 11) + assert canonical_constraint(c) == ((("x", 1), ("y", 1)), "eq", 6) + + +def test_reader_and_solver_reasons_in_gold_are_closed() -> None: + for fx in _load_r2_gold(): + if fx["expect"] == "solver_refuses": + assert fx["solver_reason"] in SOLVER_REASONS + elif fx["expect"] == "reader_refuses": + assert fx["reader_reason"] in READER_REASONS + + +# --- meaningful-fail: each invalid branch must fire under exactly its violation -------- # + + +def test_validator_rejects_incoherent_answer_key() -> None: + fx = _solved_fixture() + fx["answer"] = next(k for k in fx["options"] if fx["options"][k] != fx["gold"]) + assert validate_fixture(fx) == ("invalid", "answer_key_incoherent") + + +def test_validator_rejects_three_categories() -> None: + fx = _solved_fixture() + fx["unknowns"].append( + {"symbol": "z", "entity": "z", "unit": fx["unknowns"][0]["unit"], "domain": "nonnegative_integer"} + ) + assert validate_fixture(fx) == ("invalid", "v1_requires_exactly_two_distinct_categories") + + +def test_validator_rejects_constraint_referencing_unknown_symbol() -> None: + fx = _solved_fixture() + fx["constraints"][0]["terms"][0][0] = "ghost" + assert validate_fixture(fx) == ("invalid", "constraint_references_unknown_symbol") + + +def test_validator_rejects_query_not_a_category() -> None: + fx = _solved_fixture() + fx["query"]["symbol"] = "ghost" + assert validate_fixture(fx) == ("invalid", "query_target_not_a_category") + + +def test_validator_rejects_solved_without_int_gold() -> None: + fx = _solved_fixture() + fx["gold"] = None + assert validate_fixture(fx) == ("invalid", "solved_needs_int_gold") + + +def test_validator_rejects_reader_refuse_carrying_gold() -> None: + fx = copy.deepcopy(next(f for f in _load_r2_gold() if f["expect"] == "reader_refuses")) + fx["gold"] = 4 + assert validate_fixture(fx) == ("invalid", "reader_refuses_has_gold") + + +def test_validator_rejects_unknown_solver_reason() -> None: + fx = copy.deepcopy(next(f for f in _load_r2_gold() if f["expect"] == "solver_refuses")) + fx["solver_reason"] = "made_up" + assert validate_fixture(fx)[0] == "invalid" + + +def test_validator_rejects_unknown_expect() -> None: + fx = _solved_fixture() + fx["expect"] = "teleported" + assert validate_fixture(fx)[0] == "invalid"