From a447dce5d199ac0a11d4cc24b19960a333dcf4a0 Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 4 Jun 2026 15:56:28 -0700 Subject: [PATCH] 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 } )