From 85781f0f4ca61ce63ac2c16badc996aa8374f47d Mon Sep 17 00:00:00 2001 From: Shay Date: Sun, 19 Jul 2026 19:10:05 -0700 Subject: [PATCH] =?UTF-8?q?fix(trackb):=20pure-S1=20gate=20=E2=80=94=20ref?= =?UTF-8?q?use=20total=20supersets=20and=20extra=20contains?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mapper required only that total include {a,b}; rebuild-from-binding then dropped third entities and could emit a certified wrong answer (e.g. 15 instead of 115). Require exact total part-set {a,b}, refuse any contain outside reference a, and agree with original-graph classical solve before emit. Adds multi-entity refuse unit tests. --- docs/research/trackb-s1-slice-2026-07-20.md | 28 +++- generate/structure_mapping/mapper.py | 77 ++++++---- generate/structure_mapping/solve_s1.py | 56 ++++++++ tests/test_trackb_s1_structure_mapping.py | 148 ++++++++++++++++++++ 4 files changed, 278 insertions(+), 31 deletions(-) diff --git a/docs/research/trackb-s1-slice-2026-07-20.md b/docs/research/trackb-s1-slice-2026-07-20.md index 156a9211..b78ff0df 100644 --- a/docs/research/trackb-s1-slice-2026-07-20.md +++ b/docs/research/trackb-s1-slice-2026-07-20.md @@ -151,7 +151,31 @@ Post-edit: same smoke suite (off-serving code only; serving modules diff empty). --- -## 6. Explicit non-claims / STOP gate +## 6. Pure-S1 integrity fix (reviewer-critical) + +An early mapper draft accepted totals that *included* `{a,b}` among other parts +and only blocked an independent contain on `b`. Combined with rebuild-from-binding +solve, that could emit a certified **wrong** answer (drop third entity): + +```text +# A=5, C=100, B=2×A, total all → classical 115; buggy pure rebuild → 15 +$ uv run python -c '...' # see measure-s1-pure-gate-repro +map=StructureMapRefuse reason=total_parts_not_exactly_a_b +emit=False ans=None refuse=structure_map_refuse:total_parts_not_exactly_a_b mr=False +REPRO FIXED +``` + +**Fix (shipped):** +1. `map_to_s1` requires total part-set **exactly** `{a,b}` (`total_parts_not_exactly_a_b`). +2. Any `contain` on an entity other than `a` is refused (`extra_contain_not_pure_s1:*` / `b_has_independent_contain_not_pure_s1`). +3. `try_s1_structure_map_and_solve(graph=…)` additionally requires classical solve of the **original** graph to agree with the pure-S1 rebuild before emit (fail-closed backstop). + +Unit tests: `test_mapper_refuses_total_superset_with_extra_entity`, +`test_mapper_refuses_extra_contain_even_if_total_were_ab_only`, +`test_multi_entity_slice_never_emits_wrong_certified_answer`, +`test_multi_entity_small_c_same_trap` (20 tests total). + +## 7. Explicit non-claims / STOP gate - **Not claimed**: geometric SME revival; S2–S4 coverage; serving cutover; sealed-test movement. - **Not claimed**: holdout non-S1 graph-level separability beyond the vacuous parse layer — only synthetic + other-corpus graphs. @@ -160,7 +184,7 @@ Post-edit: same smoke suite (off-serving code only; serving modules diff empty). --- -## 7. Inventory: proven vs assumed +## 8. Inventory: proven vs assumed | Item | Status | | --- | --- | diff --git a/generate/structure_mapping/mapper.py b/generate/structure_mapping/mapper.py index bcf93ca8..54ca13bd 100644 --- a/generate/structure_mapping/mapper.py +++ b/generate/structure_mapping/mapper.py @@ -6,6 +6,12 @@ role matching** (predicate kinds + systematicity). Surface attributes Blind: never reads gold structure labels. Refuse is a first-class outcome. Deterministic: single compare-total pattern, fixed role assignment rules. + +Pure-S1 gate (Increment 1): the problem must be *exactly* two roles +``a`` (seeded) and ``b`` (defined by ``k×a``) with total over ``{a,b}``. +A total that merely *includes* ``a`` and ``b`` among other parts, or any +seeded ``contain`` on a third entity, is refused — never bound and rebuilt +as a smaller pure-S1 problem (that would emit a wrong certified answer). """ from __future__ import annotations @@ -14,7 +20,7 @@ from dataclasses import dataclass from typing import Mapping from generate.structure_mapping.canonicals import S1_CANONICAL -from generate.structure_mapping.role_predicate import RoleGraph, RolePredicate, RoleTerm +from generate.structure_mapping.role_predicate import RoleGraph @dataclass(frozen=True, slots=True) @@ -42,17 +48,15 @@ class StructureMapRefuse: def map_to_s1(role_graph: RoleGraph) -> StructureMapResult | StructureMapRefuse: """Map ``role_graph`` to the S1 canonical or refuse. - Algorithm (deterministic, systematicity-first): + Algorithm (deterministic, systematicity-first, pure-S1 only): 1. Require exactly one ``compare`` predicate (multiplicative factor present). - 2. Require at least one ``total`` whose part-set includes both compare roles. + 2. Require exactly one admissible ``total`` whose **part-set equals** + ``{a, b}`` (not a superset — extras would be dropped by rebuild solve). 3. Require a ``contain`` on the compare reference entity (role ``a``) with a known quantity — the seed. - 4. Refuse if a competing independent ``contain`` on ``b`` contradicts - pure definition-by-compare (b defined only via k×a). We *allow* a - contain on b only when absent; if present with a value, refuse this - slice (not pure S1). - 5. Refuse on transfer/rate co-presence that would make the family multi-frontier - (Increment 1 is single-family pure S1). + 4. Refuse any ``contain`` whose entity is not ``a`` (including ``b`` and + any third entity ``c``). ``b`` is defined only via the compare. + 5. Refuse on transfer/rate co-presence (multi-frontier; out of Increment 1). Gold labels are never consulted. """ @@ -98,40 +102,55 @@ def map_to_s1(role_graph: RoleGraph) -> StructureMapResult | StructureMapRefuse: return StructureMapRefuse(reason="compare_self_reference") k = float(k_term.value) + expected_parts = frozenset({a_name, b_name}) - # Total must mention both a and b as parts (sum slot is last arg). - total_ok = False + # Pure S1: total part-set must equal {a, b} exactly — not a superset. + # A total that merely includes a,b among other parts is multi-entity and + # must refuse; rebuilding a+b alone would emit the wrong problem's answer. + exact_total = False for total in totals: - part_names = {t.name for t in total.args[:-1] if t.kind == "entity"} - if a_name in part_names and b_name in part_names: - total_ok = True + part_names = frozenset( + t.name for t in total.args[:-1] if t.kind == "entity" + ) + if part_names == expected_parts: + exact_total = True break - if not total_ok: + if not exact_total: + # Distinguish "missing roles" vs "extra parts" for auditability. + any_cover = any( + a_name in (t.name for t in total.args[:-1] if t.kind == "entity") + and b_name in (t.name for t in total.args[:-1] if t.kind == "entity") + for total in totals + ) + if any_cover: + return StructureMapRefuse(reason="total_parts_not_exactly_a_b") return StructureMapRefuse(reason="total_does_not_cover_compare_roles") - # contain(a, qty) required. + # contain(a, qty) required; no other entity may carry a seed contain. a_value: float | None = None unit: str | None = None for c in contains: ent, qty = c.args - if ent.kind == "entity" and ent.name == a_name and qty.kind == "quantity": - if qty.value is None: - continue + if ent.kind != "entity" or qty.kind != "quantity": + continue + if qty.value is None: + continue + if ent.name == a_name: a_value = float(qty.value) unit = qty.unit - break + continue + # Any contain on b or a third entity is not pure S1. + if ent.name == b_name: + return StructureMapRefuse( + reason="b_has_independent_contain_not_pure_s1" + ) + return StructureMapRefuse( + reason=f"extra_contain_not_pure_s1:{ent.name}" + ) + if a_value is None: return StructureMapRefuse(reason="missing_contain_on_reference_a") - # Pure S1: b should not have an independent seed contain. - for c in contains: - ent, qty = c.args - if ent.kind == "entity" and ent.name == b_name and qty.kind == "quantity": - if qty.value is not None: - return StructureMapRefuse( - reason="b_has_independent_contain_not_pure_s1" - ) - binding: dict[str, object] = { "a": a_name, "b": b_name, diff --git a/generate/structure_mapping/solve_s1.py b/generate/structure_mapping/solve_s1.py index dd6c62f5..8652715c 100644 --- a/generate/structure_mapping/solve_s1.py +++ b/generate/structure_mapping/solve_s1.py @@ -234,6 +234,12 @@ def try_s1_structure_map_and_solve( Accepts either a surface graph or a prebuilt role graph. Never takes a gold structure label. + + When the original ``MathProblemGraph`` is supplied, an additional + integrity gate runs after a successful binding solve: the original graph + must classically solve to the same answer as the pure-S1 rebuild. This + is a fail-closed backstop so a mapper bug that drops entities cannot + emit a certified wrong answer for a different problem. """ if role_graph is None: if graph is None: @@ -262,6 +268,56 @@ def try_s1_structure_map_and_solve( ) assert isinstance(mapped, StructureMapResult) out = solve_s1_binding(mapped.binding) + + # Original-graph integrity backstop (when available). + if ( + out.emitted + and out.answer is not None + and graph is not None + ): + try: + original_trace = solve(graph) + original_verdict = verify(graph, original_trace) + except (SolveError, VerificationError, ValueError) as exc: + return S1SolveOutcome( + emitted=False, + answer=None, + refusal_reason=( + f"original_graph_solve_failed:{type(exc).__name__}:{exc}" + ), + binding=out.binding, + derivation=out.derivation, + multi_register_certified=out.multi_register_certified, + classical_verified=False, + source_graph_hash=role_graph.source_graph_hash, + ) + if not original_verdict.passed: + return S1SolveOutcome( + emitted=False, + answer=None, + refusal_reason="original_graph_verifier_rejected", + binding=out.binding, + derivation=out.derivation, + multi_register_certified=out.multi_register_certified, + classical_verified=False, + source_graph_hash=role_graph.source_graph_hash, + ) + orig_ans = float(original_trace.answer_value) + if abs(orig_ans - float(out.answer)) > 1e-6 * max(1.0, abs(orig_ans)): + return S1SolveOutcome( + emitted=False, + answer=None, + refusal_reason=( + f"original_graph_disagreement:original={orig_ans}," + f"s1_rebuild={out.answer}" + ), + binding=out.binding, + derivation=out.derivation, + multi_register_certified=out.multi_register_certified, + classical_verified=out.classical_verified, + source_graph_hash=role_graph.source_graph_hash, + ) + return S1SolveOutcome( emitted=out.emitted, answer=out.answer, diff --git a/tests/test_trackb_s1_structure_mapping.py b/tests/test_trackb_s1_structure_mapping.py index 8b90b176..269840a8 100644 --- a/tests/test_trackb_s1_structure_mapping.py +++ b/tests/test_trackb_s1_structure_mapping.py @@ -282,3 +282,151 @@ def test_scoring_labels_isolated_and_loadable() -> None: assert sc["tp"] is True sc_fp = score_label("gsm8k-holdout-dev-v1-0101", False, labels) assert sc_fp["fn"] is True + + +def _multi_entity_compare_total_graph( + *, + a_value: float = 5.0, + c_value: float = 100.0, + k: float = 2.0, +) -> MathProblemGraph: + """A=a_value seeded, C=c_value seeded, B=k×A; unknown = total of all. + + True answer is a_value + k*a_value + c_value (e.g. 5+10+100=115). + A buggy pure-S1 rebuild that drops C would emit a_value*(1+k) (=15). + """ + return MathProblemGraph( + entities=("A", "B", "C"), + initial_state=( + InitialPossession(entity="A", quantity=Quantity(value=a_value, unit="x")), + InitialPossession(entity="C", quantity=Quantity(value=c_value, unit="x")), + ), + operations=( + Operation( + actor="B", + kind="compare_multiplicative", + operand=Comparison( + reference_actor="A", + delta=None, + factor=k, + direction="times", + ), + ), + ), + unknown=Unknown(entity=None, unit="x"), + ) + + +def test_mapper_refuses_total_superset_with_extra_entity() -> None: + """total parts must equal {a,b}; superset is not pure S1.""" + g = _multi_entity_compare_total_graph() + rg = graph_to_role_graph(g) + # Converter should surface contain on C and total over A,B,C. + assert any( + p.kind == "contain" and p.args[0].name == "C" for p in rg.predicates + ) + total_parts = None + for p in rg.of_kind("total"): + total_parts = {t.name for t in p.args[:-1] if t.kind == "entity"} + assert total_parts == {"A", "B", "C"} + + mapped = map_to_s1(rg) + assert isinstance(mapped, StructureMapRefuse) + assert mapped.reason in ( + "total_parts_not_exactly_a_b", + "extra_contain_not_pure_s1:C", + ) + + +def test_mapper_refuses_extra_contain_even_if_total_were_ab_only() -> None: + """Seed contain on a third entity is not pure S1.""" + from generate.structure_mapping.role_predicate import ( + RoleGraph, + RolePredicate, + RoleTerm, + ) + + # Hand-built role graph: total is exactly {A,B} but C is also seeded. + rg = RoleGraph( + predicates=( + RolePredicate( + kind="contain", + args=( + RoleTerm(kind="entity", name="A"), + RoleTerm(kind="quantity", name="qa", value=5.0, unit="x"), + ), + ), + RolePredicate( + kind="contain", + args=( + RoleTerm(kind="entity", name="C"), + RoleTerm(kind="quantity", name="qc", value=10.0, unit="x"), + ), + ), + RolePredicate( + kind="compare", + args=( + RoleTerm(kind="entity", name="B"), + RoleTerm(kind="entity", name="A"), + RoleTerm(kind="quantity", name="factor", value=2.0, unit=None), + ), + ), + RolePredicate( + kind="total", + args=( + RoleTerm(kind="entity", name="A"), + RoleTerm(kind="entity", name="B"), + RoleTerm(kind="quantity", name="sum_query", value=0.0, unit="x"), + ), + ), + ) + ) + mapped = map_to_s1(rg) + assert isinstance(mapped, StructureMapRefuse) + assert mapped.reason == "extra_contain_not_pure_s1:C" + + +def test_multi_entity_slice_never_emits_wrong_certified_answer() -> None: + """Repro of skeptic finding: A=5,C=100,B=2×A,total must not emit 15. + + Must refuse at map time (preferred) or refuse at integrity gate. + Must never emit 15 with multi_register_certified=True. + """ + g = _multi_entity_compare_total_graph(a_value=5.0, c_value=100.0, k=2.0) + # True classical answer of the original graph. + from generate.math_solver import solve as classical_solve + + true_ans = float(classical_solve(g).answer_value) + assert true_ans == pytest.approx(115.0) + + out = try_s1_structure_map_and_solve(graph=g) + # Never emit the dropped-entity wrong answer. + assert not (out.emitted and out.answer is not None and abs(float(out.answer) - 15.0) < 1e-6) + # Prefer refuse; if ever emitted, must match original 115 (not wrong). + if out.emitted: + assert out.answer == pytest.approx(true_ans) + else: + assert out.refusal_reason is not None + assert ( + "total_parts" in out.refusal_reason + or "extra_contain" in out.refusal_reason + or "original_graph" in out.refusal_reason + or "structure_map_refuse" in out.refusal_reason + ) + # Certificate must not green-light a wrong answer. + if out.answer is not None and abs(float(out.answer) - 15.0) < 1e-6: + assert out.multi_register_certified is False + assert out.emitted is False + + +def test_multi_entity_small_c_same_trap() -> None: + """Second repro: A=5,C=10,B=2×A → true 25; buggy rebuild 15.""" + g = _multi_entity_compare_total_graph(a_value=5.0, c_value=10.0, k=2.0) + from generate.math_solver import solve as classical_solve + + true_ans = float(classical_solve(g).answer_value) + assert true_ans == pytest.approx(25.0) + out = try_s1_structure_map_and_solve(graph=g) + assert out.emitted is False + assert out.answer is None + assert out.refusal_reason is not None