From 3389cc68c3d899e6ff248d78dc0a6fc6f1d40a7c Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 4 Jun 2026 08:37:51 -0700 Subject: [PATCH] feat: add deductive proof evidence gates --- core/cli.py | 3 + core/cognition/pipeline.py | 66 +++++++++-- evals/deductive_logic/contract.md | 24 ++-- evals/deductive_logic/external/v1/cases.jsonl | 16 +++ evals/deductive_logic/refusal/v1/cases.jsonl | 4 + evals/deductive_logic/runner.py | 26 ++++- evals/gsm8k_math/holdout_dev/v1/README.md | 12 +- evals/gsm8k_math/holdout_dev/v1/report.json | 5 + evals/gsm8k_math/holdout_dev/v1/runner.py | 41 ++++++- generate/proof_chain/__init__.py | 24 ++++ generate/proof_chain/entail.py | 106 ++++++++++++++++-- tests/test_cli_test_suites.py | 22 ++++ tests/test_cognitive_turn_pipeline.py | 35 ++++++ tests/test_deductive_logic_entail.py | 73 ++++++++++++ tests/test_holdout_dev_lane.py | 12 ++ 15 files changed, 432 insertions(+), 37 deletions(-) create mode 100644 evals/deductive_logic/external/v1/cases.jsonl create mode 100644 evals/deductive_logic/refusal/v1/cases.jsonl diff --git a/core/cli.py b/core/cli.py index 6801b6ec..92b48a4a 100644 --- a/core/cli.py +++ b/core/cli.py @@ -165,6 +165,9 @@ _TEST_SUITES: dict[str, tuple[str, ...]] = { "math": ( "tests/test_adr_0126_train_sample_runner.py", ), + "deductive": ( + "tests/test_deductive_logic_entail.py", + ), "full": ("tests/",), } diff --git a/core/cognition/pipeline.py b/core/cognition/pipeline.py index b26382cb..a2541d3b 100644 --- a/core/cognition/pipeline.py +++ b/core/cognition/pipeline.py @@ -47,6 +47,7 @@ from generate.operators import ( multi_relation_walk, transitive_walk, ) +from generate.proof_chain import EntailmentTrace, evaluate_entailment_with_trace from teaching.correction import CorrectionCandidate, extract_correction from teaching.epistemic import EpistemicStatus from teaching.review import ReviewedTeachingExample, review_correction @@ -122,7 +123,7 @@ class CognitiveTurnPipeline: ) -> None: # runtime: ChatRuntime (no import cycle) self.runtime = runtime self._last_node_id: str | None = None - self.teaching_store = teaching_store or TeachingStore() + self.teaching_store = teaching_store if teaching_store is not None else TeachingStore() if recognizer is not None: self._recognizer = recognizer elif hasattr(runtime, "first_admitted_recognizer"): @@ -304,6 +305,8 @@ class CognitiveTurnPipeline: ): compose_surface = CognitiveTurnPipeline._render_compose_surface(compose_result) + entailment_trace = self._maybe_entailment_trace(intent, triples) + resolved = resolve_surface( canonical_surface=canonical, pre_decoration_surface=pre_decoration, @@ -393,13 +396,14 @@ class CognitiveTurnPipeline: epistemic_status = proposal.epistemic_status.value if proposal is not None else "" walk_serialised = CognitiveTurnPipeline._serialize_operator(walk_result) compose_serialised = CognitiveTurnPipeline._serialize_operator(compose_result) - # Deterministic concatenation: walk record, then compose record. - # Empty strings are dropped so single-operator turns keep their - # existing trace_hash byte-for-byte. - operator_invocation = ( - f"{walk_serialised}|{compose_serialised}" - if compose_serialised - else walk_serialised + entailment_serialised = CognitiveTurnPipeline._serialize_entailment_trace( + entailment_trace + ) + # Deterministic concatenation: walk, compose, then entailment. Empty + # strings are dropped so unaffected turns keep existing trace bytes. + operator_invocation = "|".join( + s for s in (walk_serialised, compose_serialised, entailment_serialised) + if s ) # ADR-0023 — admissibility trace + ratification provenance. # Comb pass 2026-05-21 — direct attribute access; the fields @@ -690,6 +694,39 @@ class CognitiveTurnPipeline: relation=intent.relation, ) + def _maybe_entailment_trace( + self, + intent, + triples: tuple[tuple[str, str, str], ...], + ) -> EntailmentTrace | None: + """Compile exact verification triples into propositional entailment. + + Telemetry-only v1: the result is folded into ``operator_invocation`` and + never changes the user-facing surface. Runs only when classification + exposes a precise positive ``subject relation object`` shape. + """ + if intent.tag is not IntentTag.VERIFICATION: + return None + if intent.negated or not intent.relation or not intent.object: + return None + head = self._proof_atom(intent.subject) + tail = self._proof_atom(intent.object) + if not head or not tail: + return None + + relation = intent.relation.strip().lower() + premises: list[str] = [] + for h, r, t in triples: + if r.strip().lower() != relation: + continue + h_atom = self._proof_atom(h) + t_atom = self._proof_atom(t) + if h_atom and t_atom: + premises.append(f"{h_atom} -> {t_atom}") + if not premises: + return None + return evaluate_entailment_with_trace(tuple(premises), f"{head} -> {tail}") + @staticmethod def _render_compose_surface(compose: FrameComposeResult) -> str: """Render a frame-transfer composition suffix without selecting authority.""" @@ -721,6 +758,19 @@ class CognitiveTurnPipeline: return "" return json.dumps(op.as_dict(), sort_keys=True, ensure_ascii=False) + @staticmethod + def _serialize_entailment_trace(trace: EntailmentTrace | None) -> str: + if trace is None: + return "" + return f"entailment:{trace.canonical_json()}" + + @staticmethod + def _proof_atom(text: str) -> str: + parts = [p for p in _SUBJECT_SPLIT_RE.split(text.lower()) if p] + if not parts: + return "" + return "atom_" + "_".join(parts) + @staticmethod def _render_walk_surface(walk: WalkResult) -> str: """Render a chain-aware walk suffix without selecting authority.""" diff --git a/evals/deductive_logic/contract.md b/evals/deductive_logic/contract.md index e4261b61..efe9ecf4 100644 --- a/evals/deductive_logic/contract.md +++ b/evals/deductive_logic/contract.md @@ -23,14 +23,16 @@ make stochastic. ## The numbers (2026-06-04) -| Set | n | correct | wrong | of which non-trivial (entailed + refuted) | -|---|---:|---:|---:|---:| -| dev | 200 | 200 | **0** | 74 | -| **holdout v1** | 500 | **500** | **0** | **227** (117 entailed + 110 refuted) | -| fuzz (fresh random, engine vs oracle) | 7,340 | 7,340 | **0** | 3,360 | +| Set | n | correct | wrong | refused | of which non-trivial (entailed + refuted) | +|---|---:|---:|---:|---:|---:| +| 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 | -**100% correct with `wrong = 0`**, and the correct answers include hundreds of -non-trivial multi-hop entailments and refutations — not just `unknown` pass-throughs. +**100% correct with `wrong = 0` and `refused = 0` on committed in-regime +cases**, and the correct answers include hundreds of non-trivial multi-hop +entailments and refutations — not just `unknown` pass-throughs. ## Why the gold is trustworthy (the GSM8K lesson applied) @@ -40,7 +42,9 @@ enumeration over all 2^k assignments, sharing **no code** with the ROBDD engine. independently-coded sound procedures agreeing on **8,000** fresh random problems with **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. +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 +tested separately. ## Honesty boundary (load-bearing — do not overclaim) @@ -70,7 +74,7 @@ wrong ones). A single engine/oracle disagreement fails the test suite. ## Run ```bash -PYTHONPATH=. .venv/bin/python -m evals.deductive_logic.runner # dev + holdout, exits 1 if wrong>0 +PYTHONPATH=. .venv/bin/python -m evals.deductive_logic.runner # dev + holdout + external; exits 1 unless every in-regime case is correct PYTHONPATH=. .venv/bin/python -m evals.deductive_logic.generate # regenerate committed cases (deterministic) PYTHONPATH=. .venv/bin/python -m pytest tests/test_deductive_logic_entail.py -q ``` @@ -85,4 +89,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 + refusal/v1/cases.jsonl # refusal-boundary cases, tested separately ``` diff --git a/evals/deductive_logic/external/v1/cases.jsonl b/evals/deductive_logic/external/v1/cases.jsonl new file mode 100644 index 00000000..d26b8513 --- /dev/null +++ b/evals/deductive_logic/external/v1/cases.jsonl @@ -0,0 +1,16 @@ +{"gold":"entailed","id":"dl-external-v1-0001","premises":["cat_furry -> mammal_warm","mammal_warm -> needs_food","cat_furry"],"query":"needs_food"} +{"gold":"refuted","id":"dl-external-v1-0002","premises":["penguin -> ~flies","penguin"],"query":"flies"} +{"gold":"unknown","id":"dl-external-v1-0003","premises":["student -> studies"],"query":"graduates"} +{"gold":"entailed","id":"dl-external-v1-0004","premises":["red | blue","~red"],"query":"blue"} +{"gold":"entailed","id":"dl-external-v1-0005","premises":["p","q","(p & q) -> r"],"query":"r"} +{"gold":"unknown","id":"dl-external-v1-0006","premises":["p","(p & q) -> r"],"query":"r"} +{"gold":"entailed","id":"dl-external-v1-0007","premises":["a -> b","b -> c"],"query":"a -> c"} +{"gold":"refuted","id":"dl-external-v1-0008","premises":["a -> ~b","a"],"query":"a & b"} +{"gold":"entailed","id":"dl-external-v1-0009","premises":["~(a | b)"],"query":"~a & ~b"} +{"gold":"unknown","id":"dl-external-v1-0010","premises":["a | b"],"query":"a"} +{"gold":"entailed","id":"dl-external-v1-0011","premises":["rough_cat -> animal_cat","animal_cat -> living_cat","rough_cat"],"query":"living_cat"} +{"gold":"refuted","id":"dl-external-v1-0012","premises":["round_rock -> heavy_rock","heavy_rock -> ~floating_rock","round_rock"],"query":"floating_rock"} +{"gold":"entailed","id":"dl-external-v1-0013","premises":["green_frog | brown_frog","~green_frog"],"query":"brown_frog"} +{"gold":"entailed","id":"dl-external-v1-0014","premises":["teaches_lee -> helps_lee","helps_lee -> learns_lee","teaches_lee"],"query":"learns_lee"} +{"gold":"unknown","id":"dl-external-v1-0015","premises":["kind_ada -> trusted_ada"],"query":"trusted_ada"} +{"gold":"refuted","id":"dl-external-v1-0016","premises":["open_gate -> safe_room","~safe_room"],"query":"open_gate"} diff --git a/evals/deductive_logic/refusal/v1/cases.jsonl b/evals/deductive_logic/refusal/v1/cases.jsonl new file mode 100644 index 00000000..177d2441 --- /dev/null +++ b/evals/deductive_logic/refusal/v1/cases.jsonl @@ -0,0 +1,4 @@ +{"gold":"refused","id":"dl-refusal-v1-0001","premises":["p","~p"],"query":"q"} +{"gold":"refused","id":"dl-refusal-v1-0002","premises":["forall x. p"],"query":"p"} +{"gold":"refused","id":"dl-refusal-v1-0003","premises":["rough(x)"],"query":"p"} +{"gold":"refused","id":"dl-refusal-v1-0004","premises":["p"],"query":"p & & q"} diff --git a/evals/deductive_logic/runner.py b/evals/deductive_logic/runner.py index 938d72e9..cd652d2b 100644 --- a/evals/deductive_logic/runner.py +++ b/evals/deductive_logic/runner.py @@ -9,14 +9,15 @@ Counts: ``unknown``). * ``wrong`` — engine outcome != gold and engine did not refuse (a confabulated deduction — this MUST stay 0). -* ``refused`` — engine returned ``refused`` (should not happen on these - well-formed, consistent, propositional cases; counted separately, never as wrong). +* ``refused`` — engine returned ``refused`` on a committed in-regime case. This + is a capability failure for this lane, not a safety success. A breakdown by gold class (entailed / refuted / unknown) is reported so the "sizeable numbers" are visible: how many non-trivial entailments/refutations the engine decides correctly, not just how many ``unknown``s it passes through. -Exits non-zero if ``wrong > 0`` (the floor). +Exits non-zero unless every committed in-regime case is correct. Refusal-boundary +cases live in unit tests, not in these dev/holdout formula splits. """ from __future__ import annotations @@ -41,6 +42,7 @@ def build_report(cases: list[dict]) -> dict: by_gold: Counter[str] = Counter() correct_by_gold: Counter[str] = Counter() wrong_examples: list[dict] = [] + refused_examples: list[dict] = [] for case in cases: gold = case["gold"] @@ -52,6 +54,11 @@ def build_report(cases: list[dict]) -> dict: correct_by_gold[gold] += 1 elif verdict.outcome is Entailment.REFUSED: counts["refused"] += 1 + if len(refused_examples) < 10: + refused_examples.append( + {"id": case["id"], "gold": gold, "reason": verdict.reason, + "premises": case["premises"], "query": case["query"]} + ) else: counts["wrong"] += 1 if len(wrong_examples) < 10: @@ -60,12 +67,15 @@ def build_report(cases: list[dict]) -> dict: "premises": case["premises"], "query": case["query"]} ) + all_cases_correct = counts["correct"] == len(cases) return { "n": len(cases), "counts": dict(counts), "by_gold": dict(by_gold), "correct_by_gold": dict(correct_by_gold), + "all_cases_correct": all_cases_correct, "wrong_examples": wrong_examples, + "refused_examples": refused_examples, } @@ -85,6 +95,11 @@ def _run(name: str, path: Path) -> dict: for w in report["wrong_examples"]: print(f" {w['id']}: gold={w['gold']} got={w['got']} " f"premises={w['premises']} query={w['query']}") + if report["refused_examples"]: + print(" REFUSED examples:") + for r in report["refused_examples"]: + print(f" {r['id']}: gold={r['gold']} reason={r['reason']} " + f"premises={r['premises']} query={r['query']}") return report @@ -92,6 +107,9 @@ if __name__ == "__main__": reports = { "dev": _run("dev", _ROOT / "dev" / "cases.jsonl"), "holdout-v1": _run("holdout-v1", _ROOT / "holdout" / "v1" / "cases.jsonl"), + "external-v1": _run("external-v1", _ROOT / "external" / "v1" / "cases.jsonl"), } total_wrong = sum(r["counts"]["wrong"] for r in reports.values()) - sys.exit(1 if total_wrong > 0 else 0) + 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) diff --git a/evals/gsm8k_math/holdout_dev/v1/README.md b/evals/gsm8k_math/holdout_dev/v1/README.md index e144a0be..4d3bae8a 100644 --- a/evals/gsm8k_math/holdout_dev/v1/README.md +++ b/evals/gsm8k_math/holdout_dev/v1/README.md @@ -40,4 +40,14 @@ untouched. PYTHONPATH=. .venv/bin/python -m evals.gsm8k_math.holdout_dev.v1.runner ``` -Exits non-zero if `wrong > 0` (the floor). Current baseline: **0 / 0 / 500**. +Default execution exits non-zero only if `wrong > 0` (the safety floor). Current +baseline: **0 / 0 / 500**. + +Capability-promotion runs must opt into a correctness threshold: + +```bash +PYTHONPATH=. .venv/bin/python -m evals.gsm8k_math.holdout_dev.v1.runner --min-correct 1 +``` + +That command fails today, by design. A GSM8K capability PR updates the threshold only +when held-out `correct` rises while `wrong == 0` remains true. diff --git a/evals/gsm8k_math/holdout_dev/v1/report.json b/evals/gsm8k_math/holdout_dev/v1/report.json index e6b3ab10..deb23c4a 100644 --- a/evals/gsm8k_math/holdout_dev/v1/report.json +++ b/evals/gsm8k_math/holdout_dev/v1/report.json @@ -1,10 +1,14 @@ { + "baseline_correct": 0, + "capability_pass": false, "counts": { "correct": 0, "refused": 500, "wrong": 0 }, "lane": "gsm8k_math/holdout_dev/v1", + "min_correct": null, + "min_correct_pass": true, "n": 500, "note": "Open held-out dev metric: cases CORE was NOT built against. Iterate here; the sealed TEST (1,319) is the final arbiter. wrong=0 is the floor; correct rising is the goal (refuse-everything is the failing baseline, not a pass).", "per_case": [ @@ -2009,6 +2013,7 @@ "verdict": "refused" } ], + "safety_pass": true, "schema_version": 1, "source": "openai/gsm8k train split, minus the 50 train_sample, deterministic sha256(question) sort, first 500" } diff --git a/evals/gsm8k_math/holdout_dev/v1/runner.py b/evals/gsm8k_math/holdout_dev/v1/runner.py index 7929068d..53389ee3 100644 --- a/evals/gsm8k_math/holdout_dev/v1/runner.py +++ b/evals/gsm8k_math/holdout_dev/v1/runner.py @@ -23,6 +23,7 @@ Deterministic; no network (reads the committed `cases.jsonl`). from __future__ import annotations +import argparse import json from pathlib import Path from typing import Any @@ -32,6 +33,7 @@ from evals.gsm8k_math.runner import _score_one_candidate_graph _HERE = Path(__file__).resolve().parent _CASES_PATH = _HERE / "cases.jsonl" _REPORT_PATH = _HERE / "report.json" +BASELINE_CORRECT = 0 def _load_cases() -> list[dict[str, Any]]: @@ -42,7 +44,11 @@ def _load_cases() -> list[dict[str, Any]]: ] -def build_report(cases: list[dict[str, Any]] | None = None) -> dict[str, Any]: +def build_report( + cases: list[dict[str, Any]] | None = None, + *, + min_correct: int | None = None, +) -> dict[str, Any]: cases = cases if cases is not None else _load_cases() counts = {"correct": 0, "wrong": 0, "refused": 0} per_case: list[dict[str, str]] = [] @@ -50,6 +56,9 @@ def build_report(cases: list[dict[str, Any]] | None = None) -> dict[str, Any]: outcome = _score_one_candidate_graph(case) counts[outcome.outcome] = counts.get(outcome.outcome, 0) + 1 per_case.append({"case_id": outcome.case_id, "verdict": outcome.outcome}) + safety_pass = counts["wrong"] == 0 + capability_pass = counts["correct"] > BASELINE_CORRECT + min_correct_pass = True if min_correct is None else counts["correct"] >= min_correct return { "schema_version": 1, "lane": "gsm8k_math/holdout_dev/v1", @@ -59,6 +68,11 @@ def build_report(cases: list[dict[str, Any]] | None = None) -> dict[str, Any]: ), "n": len(cases), "counts": counts, + "baseline_correct": BASELINE_CORRECT, + "safety_pass": safety_pass, + "capability_pass": capability_pass, + "min_correct": min_correct, + "min_correct_pass": min_correct_pass, "note": ( "Open held-out dev metric: cases CORE was NOT built against. Iterate here; " "the sealed TEST (1,319) is the final arbiter. wrong=0 is the floor; correct " @@ -72,12 +86,31 @@ def write_report(report: dict[str, Any]) -> None: _REPORT_PATH.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8") -def main() -> int: - report = build_report() +def _parser() -> argparse.ArgumentParser: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--min-correct", + type=int, + default=None, + help=( + "Optional promotion gate. Default reports safety only; when set, " + "the process also fails unless correct >= MIN_CORRECT." + ), + ) + return parser + + +def main(argv: list[str] | None = None) -> int: + args = _parser().parse_args(argv) + report = build_report(min_correct=args.min_correct) write_report(report) c = report["counts"] print(f"holdout_dev: correct={c['correct']} wrong={c['wrong']} refused={c['refused']} (n={report['n']})") - return 0 if c["wrong"] == 0 else 1 # the floor: wrong must be 0 + if not report["safety_pass"]: + return 1 + if not report["min_correct_pass"]: + return 1 + return 0 if __name__ == "__main__": # pragma: no cover diff --git a/generate/proof_chain/__init__.py b/generate/proof_chain/__init__.py index 3a15a037..3bc2efa0 100644 --- a/generate/proof_chain/__init__.py +++ b/generate/proof_chain/__init__.py @@ -33,6 +33,19 @@ from .rules import ( evaluate_modus_ponens, evaluate_proof_conclusion, ) +from .entail import ( + ENTAILMENT_REASONS, + INCONSISTENT_PREMISES, + OUT_OF_REGIME_OR_MALFORMED, + TAUTOLOGICAL_IMPLICATION, + TAUTOLOGICAL_REFUTATION, + UNDETERMINED, + Entailment, + EntailmentTrace, + EntailmentVerdict, + evaluate_entailment, + evaluate_entailment_with_trace, +) __all__ = ( "CONCLUSION_DISAGREEMENT", @@ -48,9 +61,20 @@ __all__ = ( "ProofError", "ProofGraph", "ProofNode", + "ENTAILMENT_REASONS", + "Entailment", + "EntailmentTrace", + "EntailmentVerdict", + "INCONSISTENT_PREMISES", + "OUT_OF_REGIME_OR_MALFORMED", + "TAUTOLOGICAL_IMPLICATION", + "TAUTOLOGICAL_REFUTATION", "UNESTABLISHED_ANTECEDENT", + "UNDETERMINED", "UNIQUE_CANONICAL_CONCLUSION", "build_proof_graph", + "evaluate_entailment", + "evaluate_entailment_with_trace", "evaluate_modus_ponens", "evaluate_proof_conclusion", "proof_from_premises", diff --git a/generate/proof_chain/entail.py b/generate/proof_chain/entail.py index c1683a9c..6d711b3b 100644 --- a/generate/proof_chain/entail.py +++ b/generate/proof_chain/entail.py @@ -30,6 +30,7 @@ propositional and in scope; an ungrounded ``forall x. P(x)`` is not. from __future__ import annotations +import json from dataclasses import dataclass from enum import Enum from typing import Final @@ -66,6 +67,33 @@ class EntailmentVerdict: reason: str +@dataclass(frozen=True, slots=True) +class EntailmentTrace: + """Deterministic proof evidence for a propositional entailment decision.""" + + outcome: Entailment + reason: str + premise_keys: tuple[str, ...] + conjunction_key: str | None + query_key: str | None + entailment_check_key: str | None + refutation_check_key: str | None + + def as_dict(self) -> dict[str, object]: + return { + "outcome": self.outcome.value, + "reason": self.reason, + "premise_keys": self.premise_keys, + "conjunction_key": self.conjunction_key, + "query_key": self.query_key, + "entailment_check_key": self.entailment_check_key, + "refutation_check_key": self.refutation_check_key, + } + + def canonical_json(self) -> str: + return json.dumps(self.as_dict(), sort_keys=True, separators=(",", ":")) + + def _conjoin(premises: tuple[str, ...]) -> str: """Fully-parenthesized conjunction of the premise formulas (``true`` if empty). @@ -82,27 +110,83 @@ def evaluate_entailment(premises: tuple[str, ...], query: str) -> EntailmentVerd Sound and complete over the propositional regime; refusal-first on anything outside it. Never raises on a logic-domain error — every ``LogicError`` (and its regime/budget subclasses) maps to a typed ``REFUSED`` verdict.""" + trace = evaluate_entailment_with_trace(premises, query) + return EntailmentVerdict(trace.outcome, trace.reason) + + +def evaluate_entailment_with_trace( + premises: tuple[str, ...], + query: str, +) -> EntailmentTrace: + """Decide entailment and return deterministic proof evidence. + + This is the evidence-bearing API; :func:`evaluate_entailment` intentionally + remains the stable verdict-only wrapper for existing callers.""" + premise_keys_list: list[str] = [] + conjunction_key: str | None = None + query_key: str | None = None + entailment_check_key: str | None = None + refutation_check_key: str | None = None + try: + for premise in premises: + premise_keys_list.append(canonicalize(premise).canonical_key) conj = _conjoin(premises) conj_canon = canonicalize(conj) + conjunction_key = conj_canon.canonical_key if conj_canon.is_contradiction: # No model satisfies the premises: from a contradiction everything # follows. We decline rather than assert a vacuous entailment. - return EntailmentVerdict(Entailment.REFUSED, INCONSISTENT_PREMISES) + return EntailmentTrace( + outcome=Entailment.REFUSED, + reason=INCONSISTENT_PREMISES, + premise_keys=tuple(premise_keys_list), + conjunction_key=conjunction_key, + query_key=None, + entailment_check_key=None, + refutation_check_key=None, + ) # Force the query through the canonicalizer too, so a malformed / out-of- # regime query refuses even when the implication check would shortcut. - canonicalize(query) - entailed = canonicalize(f"({conj}) -> ({query})").is_tautology - refuted = canonicalize(f"({conj}) -> (~({query}))").is_tautology + query_canon = canonicalize(query) + query_key = query_canon.canonical_key + entail_canon = canonicalize(f"({conj}) -> ({query})") + entailment_check_key = entail_canon.canonical_key + refute_canon = canonicalize(f"({conj}) -> (~({query}))") + refutation_check_key = refute_canon.canonical_key + entailed = entail_canon.is_tautology + refuted = refute_canon.is_tautology except LogicError: - return EntailmentVerdict(Entailment.REFUSED, OUT_OF_REGIME_OR_MALFORMED) + return EntailmentTrace( + outcome=Entailment.REFUSED, + reason=OUT_OF_REGIME_OR_MALFORMED, + premise_keys=tuple(premise_keys_list), + conjunction_key=conjunction_key, + query_key=query_key, + entailment_check_key=entailment_check_key, + refutation_check_key=refutation_check_key, + ) if entailed and refuted: # Only possible if the premises are inconsistent, already handled above; # defensive — never assert a contradiction-derived answer. - return EntailmentVerdict(Entailment.REFUSED, INCONSISTENT_PREMISES) - if entailed: - return EntailmentVerdict(Entailment.ENTAILED, TAUTOLOGICAL_IMPLICATION) - if refuted: - return EntailmentVerdict(Entailment.REFUTED, TAUTOLOGICAL_REFUTATION) - return EntailmentVerdict(Entailment.UNKNOWN, UNDETERMINED) + outcome = Entailment.REFUSED + reason = INCONSISTENT_PREMISES + elif entailed: + outcome = Entailment.ENTAILED + reason = TAUTOLOGICAL_IMPLICATION + elif refuted: + outcome = Entailment.REFUTED + reason = TAUTOLOGICAL_REFUTATION + else: + outcome = Entailment.UNKNOWN + reason = UNDETERMINED + return EntailmentTrace( + outcome=outcome, + reason=reason, + premise_keys=tuple(premise_keys_list), + conjunction_key=conjunction_key, + query_key=query_key, + entailment_check_key=entailment_check_key, + refutation_check_key=refutation_check_key, + ) diff --git a/tests/test_cli_test_suites.py b/tests/test_cli_test_suites.py index ae6a8dbc..1005c0a8 100644 --- a/tests/test_cli_test_suites.py +++ b/tests/test_cli_test_suites.py @@ -17,6 +17,7 @@ def test_core_test_lists_curated_suites(capsys) -> None: assert "cognition" in captured.out.splitlines() assert "teaching" in captured.out.splitlines() assert "packs" in captured.out.splitlines() + assert "deductive" in captured.out.splitlines() assert "full" in captured.out.splitlines() @@ -61,6 +62,27 @@ def test_core_test_fast_suite_expands_to_iteration_lane(monkeypatch) -> None: assert "tests/" not in command +def test_core_test_deductive_suite_expands_to_entailment_lane(monkeypatch) -> None: + calls: list[tuple[str, ...]] = [] + + def fake_run(*args: str, check: bool = False, cwd=None) -> int: + calls.append(args) + return 0 + + monkeypatch.setattr(cli, "_run", fake_run) + + rc = cli.main(["test", "--suite", "deductive", "-q"]) + + assert rc == 0 + assert calls[0] == ( + cli.sys.executable, + "-m", + "pytest", + "tests/test_deductive_logic_entail.py", + "-q", + ) + + def test_core_test_suite_accepts_pytest_flags_without_separator(monkeypatch) -> None: calls: list[tuple[str, ...]] = [] diff --git a/tests/test_cognitive_turn_pipeline.py b/tests/test_cognitive_turn_pipeline.py index e82bdb08..54d03368 100644 --- a/tests/test_cognitive_turn_pipeline.py +++ b/tests/test_cognitive_turn_pipeline.py @@ -15,6 +15,8 @@ from core.cognition import CognitiveTurnPipeline, CognitiveTurnResult from core.cognition.trace import trace_hash_from_result from generate.intent import IntentTag from generate.graph_planner import RhetoricalMove +from teaching.source import ProposalSource +from teaching.store import PackMutationProposal, TeachingStore # --------------------------------------------------------------------------- @@ -240,3 +242,36 @@ def test_pipeline_chat_response_contract_unchanged(pipeline: CognitiveTurnPipeli assert isinstance(result.vault_hits, int) assert result.proposition is not None assert result.articulation is not None + + +def test_verification_turn_records_entailment_operator_telemetry() -> None: + store = TeachingStore() + store._proposals.extend([ # noqa: SLF001 - focused operator substrate seed + PackMutationProposal( + proposal_id="p1", + candidate_id="c1", + subject="wisdom", + correction_text="wisdom precedes knowledge", + prior_surface="", + source=ProposalSource.operator(emitted_at_revision="test"), + triple=("wisdom", "precedes", "knowledge"), + ), + PackMutationProposal( + proposal_id="p2", + candidate_id="c2", + subject="knowledge", + correction_text="knowledge precedes recall", + prior_surface="", + source=ProposalSource.operator(emitted_at_revision="test"), + triple=("knowledge", "precedes", "recall"), + ), + ]) + pipeline = CognitiveTurnPipeline(ChatRuntime(), teaching_store=store) + + result = pipeline.run("wisdom precedes recall.", max_tokens=6) + + assert result.intent is not None + assert result.intent.tag is IntentTag.VERIFICATION + assert "entailment:" in result.operator_invocation + assert '"outcome":"entailed"' in result.operator_invocation + assert result.trace_hash == trace_hash_from_result(result) diff --git a/tests/test_deductive_logic_entail.py b/tests/test_deductive_logic_entail.py index aa711581..c12e72f1 100644 --- a/tests/test_deductive_logic_entail.py +++ b/tests/test_deductive_logic_entail.py @@ -22,11 +22,14 @@ import pytest from evals.deductive_logic.generate import _make_case from evals.deductive_logic.oracle import oracle_entailment from evals.deductive_logic.runner import _ROOT, _load, build_report +from generate.logic_canonical import LogicBudgetError from generate.proof_chain.entail import ( INCONSISTENT_PREMISES, OUT_OF_REGIME_OR_MALFORMED, + TAUTOLOGICAL_IMPLICATION, Entailment, evaluate_entailment, + evaluate_entailment_with_trace, ) @@ -81,6 +84,44 @@ def test_malformed_query_refuses() -> None: assert evaluate_entailment(("P",), "P & & Q").outcome is Entailment.REFUSED +def test_budget_error_refuses_typed(monkeypatch) -> None: + def boom(_formula: str): + raise LogicBudgetError("too many nodes") + + monkeypatch.setattr("generate.proof_chain.entail.canonicalize", boom) + + v = evaluate_entailment(("P",), "Q") + assert v.outcome is Entailment.REFUSED + assert v.reason == OUT_OF_REGIME_OR_MALFORMED + + +def test_entailment_trace_is_deterministic_evidence() -> None: + t1 = evaluate_entailment_with_trace(("P", "P -> Q"), "Q") + t2 = evaluate_entailment_with_trace(("P", "P -> Q"), "Q") + + assert t1.outcome is Entailment.ENTAILED + assert t1.reason == TAUTOLOGICAL_IMPLICATION + assert t1.premise_keys + assert t1.conjunction_key is not None + assert t1.query_key is not None + assert t1.entailment_check_key == "T" + assert t1.refutation_check_key is not None + assert t1.canonical_json() == t2.canonical_json() + assert "premise_keys" in t1.canonical_json() + + +def test_refused_trace_preserves_available_canonical_evidence() -> None: + trace = evaluate_entailment_with_trace(("P",), "P & & Q") + + assert trace.outcome is Entailment.REFUSED + assert trace.reason == OUT_OF_REGIME_OR_MALFORMED + assert trace.premise_keys + assert trace.conjunction_key is not None + assert trace.query_key is None + assert trace.entailment_check_key is None + assert trace.refutation_check_key is None + + # --- 3a. wrong=0 vs the independent oracle (deterministic fuzz) ------------- def test_engine_matches_independent_oracle_fuzz() -> None: @@ -128,6 +169,8 @@ def test_holdout_lane_wrong_is_zero() -> None: report = build_report(_load(_ROOT / "holdout" / "v1" / "cases.jsonl")) assert report["n"] == 500 assert report["counts"]["wrong"] == 0 + assert report["counts"]["refused"] == 0 + assert report["all_cases_correct"] is True # the sizeable, honest signal: non-trivial deductions decided correctly cbg = report["correct_by_gold"] assert cbg.get("entailed", 0) >= 50 @@ -138,3 +181,33 @@ def test_dev_lane_wrong_is_zero() -> None: report = build_report(_load(_ROOT / "dev" / "cases.jsonl")) assert report["n"] == 200 assert report["counts"]["wrong"] == 0 + assert report["counts"]["refused"] == 0 + assert report["all_cases_correct"] is True + + +def test_external_mirror_lane_matches_independent_oracle() -> None: + cases = _load(_ROOT / "external" / "v1" / "cases.jsonl") + report = build_report(cases) + assert report["n"] == 16 + assert report["all_cases_correct"] is True + assert report["counts"] == {"correct": 16, "wrong": 0, "refused": 0} + for case in cases: + assert oracle_entailment(tuple(case["premises"]), case["query"]) == case["gold"] + + +def test_refusal_boundary_split_refuses_every_case() -> None: + cases = _load(_ROOT / "refusal" / "v1" / "cases.jsonl") + assert len(cases) == 4 + for case in cases: + verdict = evaluate_entailment(tuple(case["premises"]), case["query"]) + assert case["gold"] == "refused" + assert verdict.outcome is Entailment.REFUSED + + +def test_runner_treats_committed_refusal_as_capability_failure() -> None: + report = build_report([ + {"id": "bad-refusal", "premises": ["P", "~P"], "query": "Q", "gold": "entailed"} + ]) + assert report["counts"]["wrong"] == 0 + assert report["counts"]["refused"] == 1 + assert report["all_cases_correct"] is False diff --git a/tests/test_holdout_dev_lane.py b/tests/test_holdout_dev_lane.py index 646cfc45..88004750 100644 --- a/tests/test_holdout_dev_lane.py +++ b/tests/test_holdout_dev_lane.py @@ -25,6 +25,7 @@ def test_wrong_is_zero_the_floor() -> None: """FOREVER: never confabulate on held-out data. If this ever fails, a committing path is wrong on real GSM8K — exactly the breach class that hid behind train_sample.""" assert _REPORT["counts"]["wrong"] == 0 + assert _REPORT["safety_pass"] is True def test_current_baseline_snapshot() -> None: @@ -38,3 +39,14 @@ def test_current_baseline_snapshot() -> None: f"holdout_dev moved to {_REPORT['counts']} — if a real capability change landed, " f"update this snapshot AND confirm wrong=0 on the sealed test before claiming lift" ) + assert _REPORT["baseline_correct"] == 0 + assert _REPORT["capability_pass"] is False + assert _REPORT["min_correct"] is None + assert _REPORT["min_correct_pass"] is True + + +def test_min_correct_promotion_gate_is_optional() -> None: + report = build_report(_load_cases(), min_correct=1) + assert report["safety_pass"] is True + assert report["min_correct"] == 1 + assert report["min_correct_pass"] is False