From a447dce5d199ac0a11d4cc24b19960a333dcf4a0 Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 4 Jun 2026 15:56:28 -0700 Subject: [PATCH 1/2] feat: ratify independent-gold invariant (INV-25) + SHA-pin deductive lane INV-25 makes the GSM8K lesson structural: no capability claim is valid unless its gold is computed by a procedure sharing no code with the system under test. Three meaningfully-failing checks (proven able to fail): 25a oracle imports no SUT module (AST); 25b every committed deductive gold is reproduced by the independent oracle AND matched by the engine; 25c an unsound engine disagrees on committed cases. SHA-pin the deductive lane (deductive_logic_v1, dev+holdout+external 716/716, wrong=0, refused=0) via a deterministic --report writer + run_as_module (the lane dir's local generate.py shadows the package in script mode) + CLAIMS regen. Fix drift the review surfaced: contract.md + pivot doc claimed an 8,000/7,340 fuzz and an 'external mirror' -> corrected to the real gated 3,000-case fuzz (2,796 definite) and 'hand-authored, NOT a published-benchmark mirror'; pivot doc GSM8K holdout 0->5 (all 5 are R1 reconstruction; composer scored 0). Validated: smoke 78, deductive 23, proof 29, invariants 44, lane-sha+claims 9. --- CLAIMS.md | 1 + .../pivot-to-deductive-logic-2026-06-04.md | 27 ++- evals/deductive_logic/contract.md | 19 +- evals/deductive_logic/report.json | 73 ++++++ evals/deductive_logic/runner.py | 82 ++++++- scripts/generate_claims.py | 4 + scripts/verify_lane_shas.py | 21 +- tests/test_architectural_invariants.py | 210 ++++++++++++++++++ tests/test_lane_sha_verifier.py | 1 + 9 files changed, 422 insertions(+), 16 deletions(-) create mode 100644 evals/deductive_logic/report.json diff --git a/CLAIMS.md b/CLAIMS.md index fad1ac0a..c34774f9 100644 --- a/CLAIMS.md +++ b/CLAIMS.md @@ -42,6 +42,7 @@ is a CI failure (`.github/workflows/lane-shas.yml`). | ADR-0099 | `public_demo` | Public showcase runs deterministically under 30s; all claims supported | `evals/public_demo/results/v1_dev.json` | `e323adb35ea17987991395424c603ff93bca08c11bc2713bd9f6338e86bb269f` | | ADR-0104 | `curriculum_loop_closure` | Curriculum-sourced proposals route through single reviewed teaching path | `evals/curriculum_loop_closure/results/v1_dev.json` | `b46d56b2d209172cc3ffaf3776dc8dcfe55093f13587c5cb67372be6dfa23e8d` | | ADR-0131 | `math_teaching_corpus_v1` | Math teaching corpus replays deterministically; all chains pass exit criterion (correct_rate=1.0, wrong=0) | `evals/math_teaching_corpus/v1/report.json` | `eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4` | +| ADR-0206 | `deductive_logic_v1` | Propositional entailment scored against an independent truth-table oracle; dev+holdout+external 716/716 correct, wrong=0, refused=0 | `evals/deductive_logic/report.json` | `97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f` | ## Verification diff --git a/docs/analysis/pivot-to-deductive-logic-2026-06-04.md b/docs/analysis/pivot-to-deductive-logic-2026-06-04.md index 22b8b451..d0b04e71 100644 --- a/docs/analysis/pivot-to-deductive-logic-2026-06-04.md +++ b/docs/analysis/pivot-to-deductive-logic-2026-06-04.md @@ -1,4 +1,4 @@ - + # The pivot to deductive logic — what went wrong, and the path now @@ -48,11 +48,20 @@ three sets, same day: | Set | correct | wrong | what it is | |---|---:|---:|---| | `train_sample` (50) | 4 | 0 | the data CORE was **built on** — overfit, no predictive validity | -| `holdout_dev` (500) | **0** | 0 | real GSM8K **never built-against** — the honest baseline | +| `holdout_dev` (500) | 5† | 0 | real GSM8K **never built-against** — the composer scored **0**; the 5 are the narrow R1 reconstruction | | sealed test (1,319) | 0 | 0 | the final exam | -**Real GSM8K capability was 0%.** The four train "correct" generalised to *zero* of -500 held-out cases. Serving held `wrong = 0` only because it refused everything real. +† Committed `evals/gsm8k_math/holdout_dev/v1/report.json` reads **5 correct / 0 wrong +/ 495 refused**. All 5 come from the narrow, verifier-gated **R1 comparative-total +reconstruction** (a typed reader, not the composer), which landed the same day; the +composer (`resolve_pooled`) generalised to **0** of 500. The "0%" below is the +composer's number — the subject of this post-mortem. (The original snapshot read +`0/500`; it predated the R1 landing and is corrected here to match the committed +artifact.) + +**The composer's real GSM8K capability was 0%.** Its four train "correct" generalised +to *zero* of 500 held-out cases (the 5 committed held-out correct are the separate R1 +reconstruction, above). Serving held `wrong = 0` only because it refused everything real. **The deeper finding — the composer is *unsound*, not just narrow.** The derivation composer (`resolve_pooled`), the reader the whole composition program was built around @@ -116,12 +125,16 @@ by design (propositional regime only). |---|---:|---:|---:|---:| | dev | 200 | 200 | **0** | 74 | | **holdout v1** | 500 | **500** | **0** | **227** | -| fuzz (fresh random, engine vs **independent** oracle) | 7,340 | 7,340 | **0** | 3,360 | +| fuzz (seed 424242, engine vs **independent** oracle) | 2,796 | 2,796 | **0** | 1,241 | The gold is computed by an **independent truth-table oracle** (`evals/deductive_logic/oracle.py`) sharing **no code** with the ROBDD engine. -**8,000 fresh random problems, two independent sound decision procedures, zero -disagreements** — the soundness evidence the GSM8K composer could never produce. +The committed gate (`test_engine_matches_independent_oracle_fuzz`) runs a +deterministic **3,000-case** fuzz of which **2,796** are in-regime/definite, with +**zero** engine-vs-oracle disagreements (a complementary 4,000-case fuzz exercises +inconsistent-premise refusal) — the soundness evidence the GSM8K composer could +never produce. INV-25 (`tests/test_architectural_invariants.py`) ratifies that +independence structurally. **Honest caveat (state it plainly):** propositional validity is *decidable*, so 100% is the expected ceiling for a correct implementation. The value is not "solved diff --git a/evals/deductive_logic/contract.md b/evals/deductive_logic/contract.md index efe9ecf4..93ec21af 100644 --- a/evals/deductive_logic/contract.md +++ b/evals/deductive_logic/contract.md @@ -1,4 +1,4 @@ - + # deductive-logic eval lane (ADR-0206) @@ -27,8 +27,14 @@ make stochastic. |---|---:|---:|---:|---:|---:| | dev | 200 | 200 | **0** | **0** | 74 | | **holdout v1** | 500 | **500** | **0** | **0** | **227** (117 entailed + 110 refuted) | -| external mirror v1 | 16 | **16** | **0** | **0** | 12 | -| fuzz (fresh random, engine vs oracle) | 7,340 | 7,340 | **0** | **0** | 3,360 | +| external (hand-authored, illustrative) v1 | 16 | **16** | **0** | **0** | 12 | +| fuzz (seed 424242, engine vs oracle) | 2,796 | 2,796 | **0** | **0** | 1,241 | + +(The fuzz row is the deterministic `test_engine_matches_independent_oracle_fuzz` +gate: 3,000 random formulas, 2,796 of them in-regime/definite, **0** +engine-vs-oracle disagreements; a complementary 4,000-case fuzz exercises +inconsistent-premise refusal. The property holds far more broadly than the +committed gate — these are the numbers CI actually pins, not a headline count.) **100% correct with `wrong = 0` and `refused = 0` on committed in-regime cases**, and the correct answers include hundreds of non-trivial multi-hop @@ -39,8 +45,9 @@ entailments and refutations — not just `unknown` pass-throughs. The gold is **not** computed by the engine under test. It comes from an *independent* truth-table decision procedure (`oracle.py`): a separate parser + brute-force model enumeration over all 2^k assignments, sharing **no code** with the ROBDD engine. Two -independently-coded sound procedures agreeing on **8,000** fresh random problems with -**zero disagreements** is real soundness evidence — exactly the property the GSM8K +independently-coded sound procedures agreeing on every committed case plus a +deterministic 3,000-case fuzz (2,796 definite, **zero disagreements**) is real +soundness evidence — exactly the property the GSM8K composer could never establish (it could not tell its 2 right answers from its 87 wrong ones). A single engine/oracle disagreement fails the test suite. A refusal on a committed in-regime case is also a lane failure; refusal-boundary cases are @@ -89,6 +96,6 @@ evals/deductive_logic/ runner.py # engine vs gold; correct/wrong/refused + class breakdown dev/cases.jsonl # seed 20260604, 200 cases holdout/v1/cases.jsonl # seed 70260604, 500 cases (disjoint) - external/v1/cases.jsonl # frozen finite-entity/proposition mirror cases + external/v1/cases.jsonl # frozen hand-authored propositional cases (illustrative; NOT a published-benchmark mirror) refusal/v1/cases.jsonl # refusal-boundary cases, tested separately ``` diff --git a/evals/deductive_logic/report.json b/evals/deductive_logic/report.json new file mode 100644 index 00000000..612c9ca3 --- /dev/null +++ b/evals/deductive_logic/report.json @@ -0,0 +1,73 @@ +{ + "adr": "ADR-0206", + "aggregate": { + "correct": 716, + "n": 716, + "refused": 0, + "wrong": 0 + }, + "all_correct": true, + "lane": "deductive_logic", + "refused_is_zero": true, + "schema_version": 1, + "splits": { + "dev": { + "all_cases_correct": true, + "by_gold": { + "entailed": 37, + "refuted": 37, + "unknown": 126 + }, + "correct_by_gold": { + "entailed": 37, + "refuted": 37, + "unknown": 126 + }, + "counts": { + "correct": 200, + "refused": 0, + "wrong": 0 + }, + "n": 200 + }, + "external_v1": { + "all_cases_correct": true, + "by_gold": { + "entailed": 8, + "refuted": 4, + "unknown": 4 + }, + "correct_by_gold": { + "entailed": 8, + "refuted": 4, + "unknown": 4 + }, + "counts": { + "correct": 16, + "refused": 0, + "wrong": 0 + }, + "n": 16 + }, + "holdout_v1": { + "all_cases_correct": true, + "by_gold": { + "entailed": 117, + "refuted": 110, + "unknown": 273 + }, + "correct_by_gold": { + "entailed": 117, + "refuted": 110, + "unknown": 273 + }, + "counts": { + "correct": 500, + "refused": 0, + "wrong": 0 + }, + "n": 500 + } + }, + "wrong_is_zero": true +} diff --git a/evals/deductive_logic/runner.py b/evals/deductive_logic/runner.py index cd652d2b..faf47ddd 100644 --- a/evals/deductive_logic/runner.py +++ b/evals/deductive_logic/runner.py @@ -22,6 +22,7 @@ cases live in unit tests, not in these dev/holdout formula splits. from __future__ import annotations +import argparse import json import sys from collections import Counter @@ -31,6 +32,14 @@ from generate.proof_chain.entail import Entailment, evaluate_entailment _ROOT = Path(__file__).resolve().parent +# The committed splits this lane scores (refusal-boundary cases live in unit +# tests, not here). Order is fixed for deterministic report bytes. +_SPLITS: tuple[tuple[str, Path], ...] = ( + ("dev", _ROOT / "dev" / "cases.jsonl"), + ("holdout_v1", _ROOT / "holdout" / "v1" / "cases.jsonl"), + ("external_v1", _ROOT / "external" / "v1" / "cases.jsonl"), +) + def _load(path: Path) -> list[dict]: with path.open(encoding="utf-8") as fh: @@ -103,7 +112,72 @@ def _run(name: str, path: Path) -> dict: return report -if __name__ == "__main__": +def build_combined_report() -> dict: + """Deterministic per-split + aggregate report over the committed splits. + + Pure over the committed ``cases.jsonl`` files: same inputs → byte-identical + JSON (no examples lists, no timestamps), so it is safe to SHA-pin + (``scripts/verify_lane_shas.py``). The human-facing ``_run`` stdout view + keeps the example breakdowns; the pinned artifact carries only the counts + that constitute the capability claim. + """ + splits: dict[str, dict] = {} + aggregate = {"n": 0, "correct": 0, "wrong": 0, "refused": 0} + for name, path in _SPLITS: + report = build_report(_load(path)) + splits[name] = { + "n": report["n"], + "counts": report["counts"], + "by_gold": report["by_gold"], + "correct_by_gold": report["correct_by_gold"], + "all_cases_correct": report["all_cases_correct"], + } + aggregate["n"] += report["n"] + for key in ("correct", "wrong", "refused"): + aggregate[key] += report["counts"][key] + return { + "schema_version": 1, + "lane": "deductive_logic", + "adr": "ADR-0206", + "splits": splits, + "aggregate": aggregate, + "wrong_is_zero": aggregate["wrong"] == 0, + "refused_is_zero": aggregate["refused"] == 0, + "all_correct": all(s["all_cases_correct"] for s in splits.values()), + } + + +def write_combined_report(path: Path) -> dict: + report = build_combined_report() + path.write_text( + json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8" + ) + return report + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--report", + type=Path, + default=None, + help=( + "write the deterministic combined JSON report to this path " + "(used by scripts/verify_lane_shas.py); default prints the " + "human-facing per-split breakdown to stdout" + ), + ) + args = parser.parse_args(argv) + + if args.report is not None: + report = write_combined_report(args.report) + gate_ok = ( + report["wrong_is_zero"] + and report["refused_is_zero"] + and report["all_correct"] + ) + return 0 if gate_ok else 1 + reports = { "dev": _run("dev", _ROOT / "dev" / "cases.jsonl"), "holdout-v1": _run("holdout-v1", _ROOT / "holdout" / "v1" / "cases.jsonl"), @@ -112,4 +186,8 @@ if __name__ == "__main__": total_wrong = sum(r["counts"]["wrong"] for r in reports.values()) total_refused = sum(r["counts"]["refused"] for r in reports.values()) all_correct = all(r["all_cases_correct"] for r in reports.values()) - sys.exit(0 if total_wrong == 0 and total_refused == 0 and all_correct else 1) + return 0 if total_wrong == 0 and total_refused == 0 and all_correct else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/generate_claims.py b/scripts/generate_claims.py index c3b85523..ec86a63b 100644 --- a/scripts/generate_claims.py +++ b/scripts/generate_claims.py @@ -70,6 +70,10 @@ _LANE_ADR: dict[str, tuple[str, str]] = { "ADR-0131", "Math teaching corpus replays deterministically; all chains pass exit criterion (correct_rate=1.0, wrong=0)", ), + "deductive_logic_v1": ( + "ADR-0206", + "Propositional entailment scored against an independent truth-table oracle; dev+holdout+external 716/716 correct, wrong=0, refused=0", + ), } diff --git a/scripts/verify_lane_shas.py b/scripts/verify_lane_shas.py index 65388332..5ffe78b7 100644 --- a/scripts/verify_lane_shas.py +++ b/scripts/verify_lane_shas.py @@ -41,6 +41,7 @@ PINNED_SHAS: dict[str, str] = { "demo_composition": "3a3d09f3a87462737e615c2dd3481b9e13e5ff8fadee0043c37873494ded556d", "public_demo": "e323adb35ea17987991395424c603ff93bca08c11bc2713bd9f6338e86bb269f", "math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4", + "deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", } @@ -51,11 +52,20 @@ class LaneSpec: report_relative: str accepts_report_flag: bool = True extra_args: tuple[str, ...] = field(default_factory=tuple) + # Run via ``python -m pkg.mod`` instead of ``python path/to/runner.py``. + # Required when the runner's own directory holds a module that would shadow + # an absolute import in script mode — e.g. the deductive lane's local + # ``generate.py`` shadows the ``generate`` package when run as a script. + run_as_module: bool = False @property def runner_path(self) -> Path: return REPO_ROOT / self.runner_module + @property + def runner_dotted(self) -> str: + return self.runner_module.removesuffix(".py").replace("/", ".") + @property def canonical_report(self) -> Path: return REPO_ROOT / self.report_relative @@ -105,6 +115,12 @@ LANE_SPECS: tuple[LaneSpec, ...] = ( report_relative="evals/math_teaching_corpus/v1/report.json", accepts_report_flag=False, ), + LaneSpec( + lane_id="deductive_logic_v1", + runner_module="evals/deductive_logic/runner.py", + report_relative="evals/deductive_logic/report.json", + run_as_module=True, + ), ) @@ -112,7 +128,10 @@ def _invoke_runner(spec: LaneSpec, *, target_path: Path | None = None) -> Path: import os env = {"PYTHONPATH": str(REPO_ROOT), **os.environ} - args: list[str] = [sys.executable, str(spec.runner_path)] + if spec.run_as_module: + args = [sys.executable, "-m", spec.runner_dotted] + else: + args = [sys.executable, str(spec.runner_path)] if target_path is not None and spec.accepts_report_flag: args.extend(["--report", str(target_path)]) args.extend(spec.extra_args) diff --git a/tests/test_architectural_invariants.py b/tests/test_architectural_invariants.py index 01460afd..ed357627 100644 --- a/tests/test_architectural_invariants.py +++ b/tests/test_architectural_invariants.py @@ -1032,3 +1032,213 @@ class TestINV24VaultRecallRegistry: f"Registered recall site(s) no longer call vault.recall(): " f"{sorted(unused)}\nRemove from VAULT_RECALL_SITES." ) + + +# =========================================================================== +# INV-25 Independent gold — a promotable-capability lane scores against an +# oracle that shares NO code with the system under test (SUT) +# =========================================================================== +# +# Claim (the GSM8K post-mortem made structural, docs/analysis/ +# pivot-to-deductive-logic-2026-06-04.md §"the GSM8K lesson"): +# +# No capability claim is valid unless the gold it is measured against is +# computed by a procedure INDEPENDENT of the engine that produced the +# answer. A "gold" that shares code with the engine only proves the engine +# agrees with itself — exactly the blind spot that let the GSM8K composer +# serve 87 wrong held-out answers it could not tell from its 2 right ones. +# +# The deductive-logic lane is the first lane to earn a real correct number +# (holdout 500/500, wrong=0), and it earns it honestly because its gold is an +# independent truth-table oracle (evals/deductive_logic/oracle.py): a separate +# tokenizer + recursive-descent parser + brute-force 2^k model enumeration +# that imports NONE of the ROBDD engine under test. This invariant ratifies +# that independence as a structural, meaningfully-failing property: +# +# 25a (structural). Each registered oracle module imports none of its SUT's +# modules. Fails the moment an oracle is "simplified" to reuse the +# engine — the single change that would turn independent gold into +# self-agreement. +# 25b (behavioral). Every committed deductive case's gold is reproduced by +# the independent oracle AND matched by the engine: engine == oracle == +# committed gold. This is the anti-overfit firewall — it fails if any +# committed gold were ever engine-derived and diverged from the oracle. +# 25c (non-vacuity). An unsound engine (entailed<->refuted flipped) is shown +# to disagree with the oracle on committed cases, proving 25b can fail. +# +# A new lane that claims a promotable/checkable capability MUST register its +# (oracle, SUT) pair here. The CI failure is the prompt to do so. + +from typing import NamedTuple + +_REPO_ROOT = PROJECT_ROOT_FOR_INV21 + + +class IndependentGoldLane(NamedTuple): + """A lane whose gold must be independent of its system under test.""" + + name: str + oracle_module: str # path relative to repo root + sut_import_prefixes: tuple[str, ...] # modules the oracle MUST NOT import + + +# The engine under test for the deductive lane is generate.proof_chain.entail, +# built on the generate.logic_canonical ROBDD stack. The oracle must share no +# code with any of it (it is a stdlib-only truth-table procedure today). +INDEPENDENT_GOLD_LANES: tuple[IndependentGoldLane, ...] = ( + IndependentGoldLane( + name="deductive_logic", + oracle_module="evals/deductive_logic/oracle.py", + sut_import_prefixes=( + "generate.proof_chain", + "generate.logic_canonical", + "generate.logic_equivalence", + ), + ), +) + +_DEDUCTIVE_CASE_FILES: tuple[str, ...] = ( + "evals/deductive_logic/dev/cases.jsonl", + "evals/deductive_logic/holdout/v1/cases.jsonl", + "evals/deductive_logic/external/v1/cases.jsonl", +) + + +def _module_imports(path: Path) -> set[str]: + """Every absolute module name imported by ``path``. + + Uses AST so a forbidden module mentioned only in a docstring/comment/string + cannot trigger a false positive, and a real ``import generate.proof_chain`` + cannot hide from a substring grep. + """ + try: + tree = ast.parse(path.read_text()) + except (OSError, SyntaxError): + return set() + mods: set[str] = set() + for node in ast.walk(tree): + if isinstance(node, ast.Import): + for alias in node.names: + mods.add(alias.name) + elif isinstance(node, ast.ImportFrom): + # Absolute imports only (level == 0); a relative import cannot reach + # the SUT package from the evals oracle. + if node.module and node.level == 0: + mods.add(node.module) + return mods + + +def _imports_any_prefix(mods: set[str], prefixes: tuple[str, ...]) -> list[str]: + hits: list[str] = [] + for mod in sorted(mods): + for prefix in prefixes: + if mod == prefix or mod.startswith(prefix + "."): + hits.append(mod) + break + return hits + + +def _load_deductive_cases() -> list[dict[str, Any]]: + cases: list[dict[str, Any]] = [] + for rel in _DEDUCTIVE_CASE_FILES: + path = _REPO_ROOT / rel + for line in path.read_text(encoding="utf-8").splitlines(): + if line.strip(): + cases.append(json.loads(line)) + return cases + + +class TestINV25IndependentGold: + """A promotable-capability lane's gold must share no code with its SUT, + and its committed gold must be reproducible by that independent oracle.""" + + def test_registered_oracle_modules_exist(self): + """Drift guard: a registered oracle path that no longer exists means + the registry is stale and the structural check below is vacuous.""" + missing = [ + lane.oracle_module + for lane in INDEPENDENT_GOLD_LANES + if not (_REPO_ROOT / lane.oracle_module).is_file() + ] + assert not missing, ( + "Registered independent-gold oracle module(s) not found: " + f"{missing}\nUpdate INDEPENDENT_GOLD_LANES in " + "tests/test_architectural_invariants.py." + ) + + def test_oracle_shares_no_code_with_sut(self): + """25a — the load-bearing structural guarantee. If any registered + oracle imports a module of the engine it is supposed to check + independently, the gold is not independent and this fails.""" + offenders: list[str] = [] + for lane in INDEPENDENT_GOLD_LANES: + mods = _module_imports(_REPO_ROOT / lane.oracle_module) + hits = _imports_any_prefix(mods, lane.sut_import_prefixes) + if hits: + offenders.append(f"{lane.oracle_module} imports SUT module(s) {hits}") + assert not offenders, ( + "Independent-gold oracle shares code with its system under test:\n " + + "\n ".join(offenders) + + "\n\nThe oracle must be an independent decision procedure (a 'gold' " + "that imports the engine only proves the engine agrees with itself — " + "the GSM8K blind spot, INV-25). Re-implement the check independently, " + "or — if this import is genuinely unrelated to the decision — narrow " + "sut_import_prefixes in INDEPENDENT_GOLD_LANES with a justification." + ) + + def test_committed_gold_is_independently_reproducible(self): + """25b — engine == oracle == committed gold on every committed case. + Reproducing the committed gold with the *independent* oracle is the + anti-overfit firewall: it fails if any gold were engine-derived and + diverged, or if the engine ever confabulated a verdict.""" + from evals.deductive_logic.oracle import oracle_entailment + from generate.proof_chain.entail import evaluate_entailment + + cases = _load_deductive_cases() + assert cases, "no committed deductive cases found — INV-25b would be vacuous" + + oracle_mismatch: list[str] = [] + engine_mismatch: list[str] = [] + for case in cases: + premises = tuple(case["premises"]) + query = case["query"] + gold = case["gold"] + if oracle_entailment(premises, query) != gold: + oracle_mismatch.append(case["id"]) + if evaluate_entailment(premises, query).outcome.value != gold: + engine_mismatch.append(case["id"]) + + assert not oracle_mismatch, ( + "Committed gold is NOT reproduced by the independent oracle " + f"(first few: {oracle_mismatch[:5]}). The gold may be engine-derived " + "or the case file drifted — regenerate gold from the oracle." + ) + assert not engine_mismatch, ( + "Engine disagrees with committed independent gold " + f"(first few: {engine_mismatch[:5]}). This is a wrong==0 breach on a " + "lane that claims a promotable capability." + ) + + def test_differential_is_non_vacuous(self): + """25c — proves 25b can fail. An unsound engine (entailed<->refuted + flipped) MUST disagree with the independent oracle on committed cases; + if it did not, 25b would be decoration (CLAUDE.md schema-defined proof + obligations).""" + from evals.deductive_logic.oracle import oracle_entailment + + flip = {"entailed": "refuted", "refuted": "entailed"} + cases = _load_deductive_cases() + disagreements = 0 + for case in cases: + premises = tuple(case["premises"]) + query = case["query"] + gold = oracle_entailment(premises, query) + unsound = flip.get(gold, gold) + if unsound != gold: + disagreements += 1 + assert disagreements > 0, ( + "A deliberately unsound (entailed<->refuted) engine disagreed with " + "the oracle on ZERO committed cases — the committed set has no " + "entailed/refuted signal, so INV-25b cannot catch a soundness break. " + "Add non-trivial cases before claiming the lane proves capability." + ) diff --git a/tests/test_lane_sha_verifier.py b/tests/test_lane_sha_verifier.py index f40c29c1..6a9bfc17 100644 --- a/tests/test_lane_sha_verifier.py +++ b/tests/test_lane_sha_verifier.py @@ -91,6 +91,7 @@ class TestExpectedLaneCoverage: "public_demo", # ADR-0099 "curriculum_loop_closure", "math_teaching_corpus_v1", # ADR-0131 + "deductive_logic_v1", # ADR-0206 — independent-oracle entailment lane } ) From 0ac725ccfdcf59650bd246ee5cf4239bde78f6ee Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 4 Jun 2026 15:56:28 -0700 Subject: [PATCH 2/2] =?UTF-8?q?docs:=20plan=20=E2=80=94=20universal=20stru?= =?UTF-8?q?cture=20+=20field<->symbol=20coherence=20gate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Planning-only design doc for the comprehension->structure->solve->verify spine: converge reading onto the binding-graph interlingua; field comprehends, structure bridges, symbol verifies; their AGREEMENT is the wrong=0 gate and the genuine second derivation that unblocks t2_precision. Field-as-reasoner must EARN each domain against independent gold (Phase 1.5 wedge: field-decides-entailment vs ROBDD oracle); never asserted unfalsifiably. INV-25 is Phase 0. --- ...-field-symbol-coherence-gate-2026-06-04.md | 187 ++++++++++++++++++ 1 file changed, 187 insertions(+) create mode 100644 docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md diff --git a/docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md b/docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md new file mode 100644 index 00000000..0a4a475d --- /dev/null +++ b/docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md @@ -0,0 +1,187 @@ + + +# Universal structure + the field↔symbol coherence gate + +A plan for the most robust, clean, logical, and masterful path to **breaking +reading and inputs of any modality into a logical structure** — so the engine can +comprehend, articulate, and solve a problem in any field for which it has adequate +packs. GSM8K (math logic) is the first proving ground; the same spine must lift +GSM8K *and* be confirmed by independent problem-solving in other fields. + +This document is planning-only. It assigns no ADR number, changes no serving path, +and introduces no capability claim. It records the architecture so later, gated +PRs can build it without re-deriving the rationale. + +## 0. End goal + +```text +input (any modality) + -> comprehended into ONE logical structure + -> reasoned over to produce a solution AND an articulated "understanding" + (what the problem is, the approach) + -> verified against INDEPENDENT gold + -> refuses when grounding is incomplete +``` + +Success = held-out GSM8K rises **drastically** with `wrong == 0`, **and** the +identical machinery clears an independent gold in ≥2 other fields. + +## 1. The honest grounding (what exists today) + +**The bottleneck is comprehension→structure, not arithmetic.** The GSM8K composer +is epistemically *unsafe* on real data (`resolve_pooled` = 2 right / 87 wrong on +holdout); bespoke per-shape readers do not compose. Capability is *real* only where +the conclusion is **checkable against independent gold** — deductive propositional +entailment (ROBDD) vs. an independent truth-table oracle: dev 200/200, holdout +500/500, `wrong = 0`. + +**There are several disjoint problem-structure representations:** + +- `generate/math_problem_graph.py::MathProblemGraph` — the GSM8K candidate-graph solver IR. +- `generate/derivation/model.py::GroundedDerivation` — the (unsafe-as-serving) derivation reader IR. +- `generate/binding_graph/SemanticSymbolicBindingGraph` (ADR-0132/0133/0134/0135) — + a **field-agnostic, unit-aware, provenance-carrying, acyclic, refusal-first** + semantic-symbolic DAG. It already unifies two domains: math (`bind_math_problem_graph`) + and proofs (`generate/proof_chain/builder.py`, ADR-0204 — "the binding graph's first consumer"). +- `generate/proof_chain` + `generate/logic_canonical.py` (ROBDD) — the deductive decision IR. +- `generate/graph_planner.py::PropositionGraph -> ArticulationTarget` — the *articulation* IR (for saying the answer), separate from reasoning. + +**The reasoning readers have zero field/algebra dependency.** `generate/derivation`, +`generate/proof_chain`, `math_solver`, `math_candidate_graph` import no +`versor_apply` / `cga_inner` / `holonomy` / `field.propagate`. The CL(4,1) field +engine participates in the **cognition turn loop** (capture field state, ratify +intent, recall, identity) — **not** in problem reasoning. Any claim of +"field-as-reasoner" is therefore currently *unverified*. + +**The dormant lever.** The reliability gate (ADR-0175) already exposes +`checker="t2_precision"` ("widening past gold"), but it is inert: no genuinely +structurally-distinct second derivation exists, and nothing consumes it. + +## 2. The synthesis — field comprehends, structure bridges, symbol verifies + +The correct architecture is not "field OR symbol." It is a precise division of +labor with a **checkable handshake**: + +- **Field/manifold engine = comprehension & constraint-resolution master (right-mode).** + A problem's entities/relations embed as geometric objects in CGA; solving = + propagating constraints via `versor_apply` until the configuration is *coherent* + (`versor_condition < 1e-6`). The converged field **is** the holistic understanding — + apprehended as a whole, context-first, in CORE's *native* operations. +- **Binding-graph DAG = interlingua / corpus callosum.** The typed, unit-checked, + provenance-carrying form the field configuration is read **into and out of**: the + inspectable, checkable commitment where holistic apprehension hands off to analysis + and analysis hands corrections back. Not master, not mere servant. +- **Symbolic servants (parser, ROBDD, solver, oracle) = analyze & dispose.** They + verify the structure against independent gold, refute incoherence, articulate. + They never originate truth. + +### 2.1 Why this is correct, not a compromise + +**The field-derivation and the symbolic-derivation are two structurally-distinct +canonical decodings of the same problem. Their *agreement* is the `wrong = 0` gate.** + +1. **It operationalizes the deepest axiom — "Truth is coherent."** Two independent + canonical decodings (geometric field + algebraic ROBDD) agreeing is coherence + across vantage points. Agreement → admit; disagreement → **refuse**. This is + exactly McGilchrist's "right apprehends, left analyzes, right re-integrates." +2. **It is the genuine second derivation that is currently missing.** The Tier-2 + spine and `t2_precision` lever are inert because solver-vs-verifier shares + structure (decoration) and the two GSM8K readers never co-fire. **Field ⟂ symbol + is that second derivation.** Activating the field as a reasoner is *what unblocks + the dormant capability lever* — mechanism, not metaphor. +3. **It makes the field earn its role checkably (conforms to `wrong = 0` / no + decoration).** The field is load-bearing *only where its answer agrees with an + independent symbolic/gold derivation*. It can never serve an unagreed answer — + disagreement refuses. This is INV-25 (Phase 0) generalized. + +### 2.2 Conformance to the governing axes + +| Axis | Conformance | +|---|---| +| Philosophical ("decoding, not generating") | Field & symbol are two canonical decodings of a reality that already is; agreement = it tracks the canonical form. | +| Axiomatic | Reasoning *is* `versor_apply` + `cga_inner` + `versor_condition` (the actual primitives); exact recall stays exact. | +| Ethical / `wrong = 0` | The field never serves an unagreed answer; refusal is the correction surface. | +| Mechanical sympathy | Field does vectorized geometric propagation (native strength, Rust-parity-ready); symbol does discrete checks. | +| Logical per "intelligence" | Holistic grasp + analytic check + refuse-on-incoherence is what integrated understanding *is*, with the non-negotiable twist that both modes must cohere or it declines. | + +## 3. The earning path (the field must *prove* it reasons) + +Today the readers have zero field dependency, so field-as-reasoner is a research arc +that earns its role on the **safest checkable micro-domain first**. A negative +result is an acceptable, honest outcome: where the field cannot earn agreement, it +**stays a servant** and the symbolic path carries that domain, refusing where it +cannot verify. **No unfalsifiable "the field knows" claim ever enters the codebase.** + +**The wedge (Phase 1.5):** *Can the field decide propositional entailment +geometrically and agree with the ROBDD oracle on held-out, `wrong = 0`?* Logic is +the ideal first test — the ROBDD + independent oracle already give a rock-solid gold +(500/500). Embed atoms/clauses as geometric objects; decide entailment by +incidence/coherence; require `field_verdict == ROBDD_verdict == oracle` on a +held-out set. Agree → the field has earned a reasoning role and we have our first +genuine second derivation. Cannot → we learned it cheaply and honestly. + +## 4. Phased plan + +- **Phase 0 — independent-gold discipline. ✅ SHIPPED.** INV-25 + (`tests/test_architectural_invariants.py`): no capability claim without an + independent gold sharing no code with the SUT; deductive lane SHA-pinned + (`deductive_logic_v1`). The foundation every later phase rides on. +- **Phase 1 — canonize the universal structure.** Promote + `SemanticSymbolicBindingGraph` to *the* documented problem-structure interlingua; + resolve its closed-vocab placeholder (`semantic_role="unknown"`) only when a + load-bearing consumer defines it. Add a **hemisphere-role invariant**: servant + modules (parsers, metrics, vault) may not bypass the structure's consistency + checks. (The taxonomy is a proposal to validate before the enforcing INV lands.) +- **Phase 1.5 — the keystone wedge.** Field-decides-entailment vs. ROBDD oracle on + the deductive lane. Prove (or honestly refute) field-as-reasoner on the safest + gold. Gate to everything geometric. +- **Phase 2 — comprehension compiler → binding graph** (finite-entity grounding + first), with **field ⟂ symbol agreement** as the admission gate from the moment + Phase 1.5 succeeds. +- **Phase 3 — activate `t2_precision`.** The field⟂symbol agreement *is* the t2 + signal; wire the propose-loop consuming `checker="t2_precision"`. No invented + second derivation needed — it is real now. +- **Phase 4 — GSM8K on the universal structure** (the drastic-lift phase), gated by + field⟂symbol agreement + independent gold + held-out/sealed validation (never + train_sample — the overfit firewall). Safe by construction. +- **Phase 5 — cross-domain confirmation.** Systems/software arena (execution = a + third independent decoding; ADR-0199's first non-math arena), then a second + non-executable field with a proof-checker gold. The generalization proof. +- **Phase 6 — multimodal grounding.** Connect the sensorium modality compilers + (`sensorium/compiler` `CompilerLike`/`CompilationUnitLike`) → binding graph. A + modality becomes "just another reader" grounding into the universal structure; + stays afferent/gated per ADR-0198. + +### Cross-cutting (every phase) — checkable budgets, adjoints, phenomenology + +- **Distortion budgets as first-class CI gates**, but *only checkable ones*: + grounding completeness %, unit-proof coverage, acyclicity, and **structural + perturbation stability** (paraphrase/reorder the input → the binding graph and + answer are invariant, or it refuses). Regressions gate the build as hard as + accuracy. This is the antidote to metric-capture (the train_sample trap). +- **Adjoint-per-operator.** Every new transform ships with its verifier/correction + pass + a test that it reduces a *structural* error, not just a string. +- **Phenomenology harness.** Sample full structured articulations (the + "understanding": problem restatement + approach) for periodic trusted review; + qualitative depth as an explicit but *subordinate* signal (never a new truth + criterion — that would re-open left-mode capture under a different name). + +## 5. Risks & honest tensions + +- **HIGH — Phase 4 `wrong = 0`.** GSM8K serving breached it before. Mitigation: + agreement gate + independent gold + held-out/sealed + pre-push verification + (auto-merge pipeline). +- **MEDIUM — field-reasoning may not pan out** in a given domain. Expected and + acceptable: it stays a servant there; the symbolic path carries it, refusing where + unverifiable. +- **MEDIUM — McGilchrist over-reach.** "Field as master of reasoning" is realized + only through the *checkable* agreement gate; never asserted as unfalsifiable fact. +- **MEDIUM — IR convergence cost.** Converge the disjoint reasoning IRs incrementally + (adapters first, direct targeting later), never a big-bang rewrite. + +## 6. What this supersedes + +The earlier 554/555/556 sequence is reframed: 554 (Tier-2 verifier) was inert → +Phase 3 done *right* (field⟂symbol is the genuine second derivation); 555 +(target-slot composition) was unsafe via the composer → Phase 4 (comprehension on +the universal structure, gated); 556 (systems/software arena) → Phase 5.