feat(constraint): R2 setup oracle + gold + ADR-0211 — the ruler (R2 C2)
evals/constraint_oracle: span-free canonical setup signature (unknowns/facts/constraints/query; terms merged+sorted, lhs constant folded into rhs), a 13-fixture gold (7 solved / 3 solver_refuses / 3 reader_refuses) with a closed expect+refusal taxonomy, and a gold-validation runner. No reader yet — this proves the ruler is coherent (13/13 valid), not capability. ADR-0211 ratifies the R2 finite-integer two-category constraint compiler: the IR, the canonical signature, the closed taxonomy, the four wrong=0 gates (setup oracle / reader refusal / exact solver / answer-choice contradiction flag), off-serving disjointness, and the C1-C9 ladder. Cross-refs ADR-0207/0175/0083/0055-0057; reuses the R1 setup_oracle pattern. Off-serving (no generate.derivation / reliability_gate). 13 oracle tests incl. per-branch meaningful-fail.
This commit is contained in:
Shay
parent
e71531c0c9
commit
a098519bc1
7 changed files with 602 additions and 0 deletions
170
docs/decisions/ADR-0211-r2-finite-integer-constraint-compiler.md
Normal file
170
docs/decisions/ADR-0211-r2-finite-integer-constraint-compiler.md
Normal file
|
|
@ -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.
|
||||
7
evals/constraint_oracle/__init__.py
Normal file
7
evals/constraint_oracle/__init__.py
Normal file
|
|
@ -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.
|
||||
"""
|
||||
20
evals/constraint_oracle/__main__.py
Normal file
20
evals/constraint_oracle/__main__.py
Normal file
|
|
@ -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())
|
||||
13
evals/constraint_oracle/r2_gold.jsonl
Normal file
13
evals/constraint_oracle/r2_gold.jsonl
Normal file
|
|
@ -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)."}
|
||||
172
evals/constraint_oracle/runner.py
Normal file
172
evals/constraint_oracle/runner.py
Normal file
|
|
@ -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",
|
||||
]
|
||||
89
evals/constraint_oracle/signature.py
Normal file
89
evals/constraint_oracle/signature.py
Normal file
|
|
@ -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",
|
||||
]
|
||||
131
tests/test_constraint_oracle.py
Normal file
131
tests/test_constraint_oracle.py
Normal file
|
|
@ -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"
|
||||
Loading…
Reference in a new issue