From fdfb71f59b17e96df75651c09e434a15881f2025 Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 23 Jul 2026 13:17:35 -0700 Subject: [PATCH] =?UTF-8?q?feat(deduction-serve):=20Phase=204=20=E2=80=94?= =?UTF-8?q?=20Band=20v1b=20categorical/syllogism=20serving=20(ADR-0256)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit core chat now decides Aristotelian syllogisms end-to-end -- the marquee 'basic logical work' widening. Closes Phase 0's fork: the ONLY categorical decider was evals/syllogism/oracle.py (the sealed independence oracle serving must not import; INV-25). This ships a production decider. generate/proof_chain/categorical.py lowers a categorical argument to the propositional regime (one Boolean atom per term-membership profile) and rides the already-verified ROBDD engine -- no new decision procedure, soundness inherits from the flagship. Sound AND complete for the modern/Boolean reading (Darapti + existential-import-only forms correctly INVALID), with no reliance on a lucky domain size. Independent of the eval oracle by mechanism (ROBDD- over-profiles vs brute-force finite-model enumeration); proven by case-for-case agreement with it across the whole syllogism gold lane. New: generate/proof_chain/categorical.py, render_syllogism (deterministic valid/invalid/inconsistent templates), CATEGORICAL shape-band, arena categorical band (4 valid forms + 2 invalid, by-construction gold cross-checked vs the independent syllogism oracle), tests/test_categorical_decider.py (8 tests incl. the independence-by-agreement proof). Changed: chat/deduction_surface.py (categorical branch, license-gated via a shared _license_gate helper; propositional path byte-identical), arena DeductionSolver dual-path in lock-step with the composer, re-sealed ledger (5 bands, categorical earns SERVE at 0.99087 wrong=0), Phase-2 lane decide() mirrors the dual path with the 3 categorical cases reclassified to their true valid/invalid verdicts + 1 invalid case (n 27->28), report+SHA regenerated. Honest wrinkles: irregular plurals ('fish') decline with unknown_morphology (a reader limit, correctly not a wrong); surfaces read in singularized terms ('all whale are animal') -- the exact ids the engine reasoned over, no cosmetic re-pluralization that could drift from the decision. [Verification]: smoke 180 passed; cognition 122 passed/1 skipped; core test --suite deductive 45 passed; test_categorical_decider 8 passed; practice runner 5 bands all SERVE wrong=0; deduction_serve lane SHA regenerates to the committed pin. --- chat/data/deduction_serve_ledger.json | 9 +- chat/deduction_surface.py | 68 ++++--- core/cli_test.py | 1 + ...ADR-0256-deduction-serve-earned-license.md | 3 +- ...-arc-phase4-categorical-band-2026-07-23.md | 63 +++++++ evals/deduction_serve/practice/gold.py | 109 +++++++++--- evals/deduction_serve/report.json | 20 ++- evals/deduction_serve/runner.py | 38 ++-- evals/deduction_serve/v1/cases.jsonl | 7 +- generate/proof_chain/categorical.py | 167 ++++++++++++++++++ generate/proof_chain/render.py | 43 ++++- generate/proof_chain/shape.py | 9 + scripts/verify_lane_shas.py | 2 +- tests/test_categorical_decider.py | 90 ++++++++++ tests/test_deduction_serve_lane.py | 7 +- tests/test_deduction_surface.py | 21 ++- 16 files changed, 576 insertions(+), 81 deletions(-) create mode 100644 docs/research/deduction-serve-arc-phase4-categorical-band-2026-07-23.md create mode 100644 generate/proof_chain/categorical.py create mode 100644 tests/test_categorical_decider.py diff --git a/chat/data/deduction_serve_ledger.json b/chat/data/deduction_serve_ledger.json index 1b3a1497..6d92ba10 100644 --- a/chat/data/deduction_serve_ledger.json +++ b/chat/data/deduction_serve_ledger.json @@ -7,6 +7,13 @@ "t2_verified": 0, "wrong": 0 }, + "categorical": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, "conditional_chain": { "correct": 720, "refused": 0, @@ -29,7 +36,7 @@ "wrong": 0 } }, - "content_sha256": "baf8d985deedc583ca52aa84296c270894598a31481dbff37f15287de339f9e6", + "content_sha256": "08c31fbaec5dcf4981a5d23dd5df65da9625dcb23a4017450405e5ba517a1530", "note": "Sealed-practice committed ledger for deduction serving (ADR-0256). Engine reads, never writes. Ceilings stay at safe defaults (theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline reliability (reader+projector+engine) at volume >= 657 committed.", "provenance": "evals.deduction_serve.practice.runner.seal_ledger", "schema": "deduction_serve_ledger_v1" diff --git a/chat/deduction_surface.py b/chat/deduction_surface.py index 91a6434f..67422f18 100644 --- a/chat/deduction_surface.py +++ b/chat/deduction_surface.py @@ -1,4 +1,4 @@ -"""chat/deduction_surface.py — Phase 1 DEDUCTION composer (deduction-serve arc). +"""chat/deduction_surface.py — DEDUCTION composer (deduction-serve arc). Wires the verified propositional-entailment engine (``generate.proof_chain``, 716/716 wrong=0 on ``evals/deductive_logic``) into serving. When a prompt @@ -8,18 +8,19 @@ strings, and decide with the sound+complete ROBDD entailment engine. Deterministic templates only (``generate.proof_chain.render``) — no LLM, no synthesis, matching every other composer in this package. -Band v1 scope (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md): -propositional arguments with single-token atoms only. A categorical/syllogism -"Therefore" argument is recognized as argument-shaped but declined as -out-of-band — a production categorical decider is Band v1b, deferred. -``evals.syllogism.oracle`` must never be imported here: it is the sealed -independence oracle the comprehension lane scores against, not a serving -decider — importing it would collapse INV-25 (independent gold). +Bands (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md): +- Band v1 — propositional arguments with single-token atoms. +- Band v1b (Phase 4) — categorical/syllogism arguments ("All M are P. All S are + M. Therefore all S are P."), projected by ``to_syllogism`` and decided by + ``generate.proof_chain.categorical`` (a propositional-lowering decider that + rides the same verified ROBDD engine). ``evals.syllogism.oracle`` must never + be imported here: it is the sealed independence oracle the comprehension lane + scores against, not a serving decider — importing it would collapse INV-25 + (independent gold). -Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every -path below returns a committed, honest surface — reader refusal, out-of-band -shape, and all four ``EntailmentTrace`` outcomes (ENTAILED/REFUTED/UNKNOWN/ -REFUSED) — never a silent fall-through to a different composer. +Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every path +below returns a committed, honest surface — reader refusal, out-of-band shape, +and every decision outcome — never a silent fall-through to a different composer. """ from __future__ import annotations @@ -30,11 +31,12 @@ from typing import Callable from chat.deduction_serve_license import deduction_serve_license from core.reliability_gate import LicenseDecision -from generate.meaning_graph.projectors import to_deductive_logic +from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism from generate.meaning_graph.reader import Comprehension, comprehend +from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.entail import evaluate_entailment_with_trace -from generate.proof_chain.render import render_entailment -from generate.proof_chain.shape import classify_deduction_shape +from generate.proof_chain.render import render_entailment, render_syllogism +from generate.proof_chain.shape import CATEGORICAL, classify_deduction_shape #: An argument's conclusion clause starts a sentence with "therefore" — the #: same shape ``generate.meaning_graph.reader`` recognizes per-clause @@ -60,8 +62,8 @@ _READER_REFUSAL_SURFACE = ( "decide it yet ({reason})." ) _OUT_OF_BAND_SURFACE = ( - "That reads as an argument, but right now I can only decide plain " - "propositional arguments (not categorical 'all/no/some' ones yet)." + "That reads as an argument, but its form is outside what I can decide yet " + "(I handle plain propositional and categorical 'all/no/some' arguments)." ) #: Disclosed hedge prepended when a decided argument's shape-band has NOT earned @@ -104,13 +106,33 @@ def deduction_grounded_surface( comp = comprehend(text) if not isinstance(comp, Comprehension): return _READER_REFUSAL_SURFACE.format(reason=comp.reason) + # Band v1 — propositional argument. projected = to_deductive_logic(comp) - if projected is None: - return _OUT_OF_BAND_SURFACE - premises, query = projected - trace = evaluate_entailment_with_trace(premises, query) - surface = render_entailment(trace, premises, query) - band = classify_deduction_shape(premises, query) + if projected is not None: + premises, query = projected + trace = evaluate_entailment_with_trace(premises, query) + surface = render_entailment(trace, premises, query) + return _license_gate(surface, classify_deduction_shape(premises, query), license_lookup) + # Band v1b — categorical / syllogism argument. Decided by the propositional- + # lowering categorical decider (rides the same verified ROBDD engine); a + # malformed categorical shape declines rather than guessing. + syllogism = to_syllogism(comp) + if syllogism is not None: + structure, s_query = syllogism + try: + trace = decide_syllogism(structure, s_query) + except CategoricalError: + return _OUT_OF_BAND_SURFACE + surface = render_syllogism(trace, structure, s_query) + return _license_gate(surface, CATEGORICAL, license_lookup) + return _OUT_OF_BAND_SURFACE + + +def _license_gate(surface: str, band: str, license_lookup: _LicenseLookup) -> str: + """Serve *surface* authoritatively iff *band* holds a SERVE license; else + serve the same sound answer DISCLOSED (hedged). The one place the earned- + license posture is applied, shared by the propositional and categorical + bands (ADR-0256).""" decision = license_lookup(band) if decision is not None and decision.licensed: return surface # earned SERVE — authoritative diff --git a/core/cli_test.py b/core/cli_test.py index 21f6f3da..c876bedf 100644 --- a/core/cli_test.py +++ b/core/cli_test.py @@ -176,6 +176,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = { "tests/test_deductive_logic_entail.py", "tests/test_deduction_serve_lane.py", "tests/test_deduction_serve_license.py", + "tests/test_categorical_decider.py", ), "full": ("tests/",), } diff --git a/docs/adr/ADR-0256-deduction-serve-earned-license.md b/docs/adr/ADR-0256-deduction-serve-earned-license.md index bdb3f17c..ca84986e 100644 --- a/docs/adr/ADR-0256-deduction-serve-earned-license.md +++ b/docs/adr/ADR-0256-deduction-serve-earned-license.md @@ -23,7 +23,8 @@ The ROBDD engine is sound **and** complete over the propositional regime — it Make deduction serving an earned capability gated by a committed, SHA-sealed reliability ledger. -- **Shape-band capability axis** (`generate/proof_chain/shape.py::classify_deduction_shape`) — a deterministic, structural classification of a projected `(premises, query)` argument into one of four exhaustive bands: `disjunctive`, `conditional_chain`, `conditional_single`, `atomic`. Computed identically by the practice arena and the serving composer (no drift). Coarse on purpose: each band mixes entailed/refuted/unknown gold, so a band's reliability measures decision correctness across outcomes, not just how many entailments pass through. +- **Shape-band capability axis** (`generate/proof_chain/shape.py`) — a deterministic, structural classification of an argument into one of five exhaustive bands: the four propositional bands `disjunctive` / `conditional_chain` / `conditional_single` / `atomic` (assigned by `classify_deduction_shape` over the projected `(premises, query)`), plus `categorical` (Band v1b, Phase 4 — assigned directly to any syllogism projected by `to_syllogism`). Computed identically by the practice arena and the serving composer (no drift). Coarse on purpose: each band mixes entailed/refuted/unknown (or valid/invalid) gold, so a band's reliability measures decision correctness across outcomes, not just how many entailments pass through. +- **Band v1b — production categorical decider** (`generate/proof_chain/categorical.py`) — the piece Phase 0's fork identified as missing. Serving cannot import `evals/syllogism/oracle.py` (the sealed independence oracle; INV-25), so this is a fresh production decider that lowers a categorical argument to the propositional regime (one Boolean atom per term-membership *profile*) and rides the already-verified ROBDD engine. Sound AND complete for the modern/Boolean reading; independent of the eval oracle by mechanism (ROBDD over a profile encoding vs. brute-force subset enumeration), verified by case-for-case agreement with it across the syllogism gold lane. Serving projects a syllogism via `to_syllogism` and decides it here (ENTAILED ⇒ valid; UNKNOWN/REFUTED ⇒ invalid; REFUSED ⇒ inconsistent). - **Deduction practice arena** (`evals/deduction_serve/practice/`) — the **second** concrete instance of the ADR-0199 arena (GSM8K math is the first). A deterministic, synthetic, indexed corpus (`gold.py`, no clock/RNG) of propositional arguments per shape-band, each with **by-construction gold** (the generating template's logical form, independent of the reader — ADR-0199 L-2). `DeductionSolver` runs the exact serving pipeline; `ConstructionGoldTether` scores the committed outcome against the by-construction gold; a misread is caught as `wrong`. Sized to the SERVE volume floor (≥657 committed for a perfect record to clear θ_SERVE=0.99; `CASES_PER_BAND=720`). - **Construction-time soundness check** (`gold.py::assert_corpus_sound`) — every generated case's by-construction gold is cross-checked against the **independent truth-table oracle** (`evals.deductive_logic.oracle`, INV-25 — shares no code with the ROBDD engine) before the ledger can seal. A mis-stated template gold can never silently inflate the ledger. - **Sealed, SHA-verified committed ledger** (`chat/data/deduction_serve_ledger.json`, produced by `evals/deduction_serve/practice/runner.py::seal_ledger`) — the per-band `ClassTally`, self-sealed by `content_sha256`. The engine READS it; only the sealed-practice runner WRITES it. Mirrors the estimation ledger topology exactly (`generate/determine/data/estimation_ledger.json`). diff --git a/docs/research/deduction-serve-arc-phase4-categorical-band-2026-07-23.md b/docs/research/deduction-serve-arc-phase4-categorical-band-2026-07-23.md new file mode 100644 index 00000000..7e256879 --- /dev/null +++ b/docs/research/deduction-serve-arc-phase4-categorical-band-2026-07-23.md @@ -0,0 +1,63 @@ +# Deduction-serve arc — Phase 4 (Band v1b: categorical/syllogism serving), 2026-07-23 + +**Base:** `main` @ `6a54d27a`. **Branch:** `feat/deduction-serve-phase2` (stacked on Phase 1–3). +**ADR:** `docs/adr/ADR-0256` (updated — Band v1b now built). +**Depends on:** Phase 1 (composer), Phase 2 (lane), Phase 3 (arena + license). + +## What shipped + +`core chat` now decides **categorical syllogisms** end-to-end, closing the exact gap Phase 0's fork identified: + +``` +> All mammals are animals. All whales are mammals. Therefore all whales are animals. +Given: all mammal are animal; all whale are mammal. That's valid — all whale are animal follows. + +> All cats are animals. All dogs are animals. Therefore all dogs are cats. +Given: all cat are animal; all dog are animal. That doesn't follow — all dog are cat isn't guaranteed by those premises. +``` + +The propositional bands (Phase 1–3) are unchanged. This is the marquee "basic logical work" widening — the Aristotelian syllogism. + +## The Phase-0 fork, resolved + +Phase 0 found the only categorical decider in the tree was `evals/syllogism/oracle.py` — the sealed independence oracle the comprehension lane scores against, which serving must never import (INV-25). Building a **production** decider was the fork's deferred half. Resolution: **`generate/proof_chain/categorical.py`** — a fresh decider that lowers a categorical argument to the propositional regime and rides the already-verified ROBDD engine. No new decision procedure; soundness inherits from the flagship engine. + +### Why the lowering is sound AND complete (not "big enough domain") + +A k-term categorical argument's model is fully determined by which of the `2^k` term-membership *profiles* are occupied. One Boolean atom `occ_j` per profile, and A/E/I/O become propositional formulas over those atoms (all S are P ≡ ⋀_{profiles with S but not P} ¬occ_j, etc.). Validity is then exactly propositional entailment — decided by the ROBDD engine. Because the profile atoms range over *all* occupancy patterns, this is sound and complete for the modern/Boolean reading (universals without existential import), with no reliance on a lucky domain size. Darapti and the other existential-import-only forms are correctly ruled INVALID. + +### Independence (INV-25) preserved and proven + +The decider shares no code with `evals/syllogism/oracle.py`. Their agreement — **case-for-case across the entire syllogism gold lane, and with the committed gold** — is the soundness evidence: two disjoint mechanisms (ROBDD-over-profiles vs. brute-force finite-model enumeration) converging (`tests/test_categorical_decider.py`). + +## New / changed files + +- **`generate/proof_chain/categorical.py`** (new) — the profile-lowering categorical decider (`decide_syllogism`, `lower_syllogism`, `syllogism_is_valid`); malformed input refuses (`CategoricalError`). +- **`generate/proof_chain/shape.py`** — `CATEGORICAL` band added (5 bands total). +- **`generate/proof_chain/render.py`** — `render_syllogism` (deterministic valid/invalid/inconsistent templates over the argument's own clauses). +- **`chat/deduction_surface.py`** — categorical branch (Band v1b): propositional path first, then `to_syllogism → decide_syllogism → render_syllogism`, license-gated through the shared `_license_gate` helper. Propositional behavior byte-identical. +- **`evals/deduction_serve/practice/gold.py`** — categorical band added to the arena: syllogism templates (4 valid Aristotelian forms + 2 invalid) with by-construction gold cross-checked against the independent syllogism oracle; `DeductionSolver` gains the dual (propositional + categorical) path, in lock-step with the composer. +- **`chat/data/deduction_serve_ledger.json`** — re-sealed: 5 bands, `categorical` earns SERVE at reliability 0.99087, wrong=0. +- **`evals/deduction_serve/runner.py`** + **`v1/cases.jsonl`** — the Phase-2 lane's `decide()` mirrors the composer's dual path; the 3 categorical cases (previously gold `declined`) reclassified to their true `valid`/`invalid` verdicts + 1 invalid case added (n: 27 → 28). Report + SHA pin regenerated (`b23234b4…`). +- **`tests/test_categorical_decider.py`** (new, 8 tests) + updates to `test_deduction_surface.py` / `test_deduction_serve_lane.py`. + +## Honest wrinkles + +- **Irregular plurals decline.** "All birds are animals. All **fish** are animals…" declines with `unknown_morphology` — the reader can't singularize "fish". Correctly a decline, not a wrong; a reader-morphology limit, documented, not worked around (the invalid-case corpus uses regular plurals like cats/dogs). +- **Surfaces read in singularized terms** ("all whale are animal") — grammatically rough but honest: those are the exact class ids the engine reasoned over. The deterministic-template honesty bar (no LLM) means no cosmetic re-pluralization that could drift from what was decided. + +## Verification + +``` +uv run python -m pytest tests/test_categorical_decider.py -q # 8 passed +uv run python -m evals.deduction_serve.practice.runner # 5 bands all SERVE, wrong=0 +uv run python -m evals.deduction_serve.runner # 28/28, wrong=0 +uv run core test --suite deductive -q # 45 passed +uv run core test --suite smoke -q # 180 passed +uv run core test --suite cognition -q # 122 passed, 1 skipped +# deduction_serve lane SHA regenerates to the committed pin b23234b4… +``` + +## Verdict + +Phase 4 complete. Categorical syllogism serving is live, sound+complete, independent-of-the-eval-oracle, earned through the same license machinery as the propositional bands. The serving band now spans propositional arguments and Aristotelian syllogisms — the core of "basic logical work". Remaining Phase-4 ideas (multi-word English proposition reader relaxation; multi-step proof recap) are documented as scoped-out in Phase 5, deferred deliberately rather than rushed against wrong=0. diff --git a/evals/deduction_serve/practice/gold.py b/evals/deduction_serve/practice/gold.py index 2b177644..4a02ffb7 100644 --- a/evals/deduction_serve/practice/gold.py +++ b/evals/deduction_serve/practice/gold.py @@ -30,11 +30,13 @@ from dataclasses import dataclass, field from typing import Any from core.learning_arena.protocols import Problem -from generate.meaning_graph.projectors import to_deductive_logic +from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism from generate.meaning_graph.reader import Comprehension, comprehend +from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace from generate.proof_chain.shape import ( ATOMIC, + CATEGORICAL, CONDITIONAL_CHAIN, CONDITIONAL_SINGLE, DISJUNCTIVE, @@ -88,6 +90,25 @@ _TEMPLATES: dict[str, tuple[tuple[str, Any], ...]] = { # (a bare atom either restates or contradicts); the band is 2/3 the size # of the others, still well above the volume floor. ), + # Categorical (syllogism). Terms are synthetic PLURAL class nouns (``x3s`` → + # the reader singularizes to ``x3``); ``a, b, c`` are the three distinct + # middle/subject/predicate classes. Gold is the unconditional validity (modern + # reading) of the standard form — cross-checked against the INDEPENDENT + # syllogism oracle in ``assert_corpus_sound``. + CATEGORICAL: ( + # Barbara (AAA) — valid. + ("valid", lambda a, b, c: f"All {a}s are {b}s. All {c}s are {a}s. Therefore all {c}s are {b}s."), + # Celarent (EAE) — valid. + ("valid", lambda a, b, c: f"No {a}s are {b}s. All {c}s are {a}s. Therefore no {c}s are {b}s."), + # Darii (AII) — valid. + ("valid", lambda a, b, c: f"All {a}s are {b}s. Some {c}s are {a}s. Therefore some {c}s are {b}s."), + # Ferio (EIO) — valid. + ("valid", lambda a, b, c: f"No {a}s are {b}s. Some {c}s are {a}s. Therefore some {c}s are not {b}s."), + # Undistributed middle (AAA-2) — INVALID. + ("invalid", lambda a, b, c: f"All {b}s are {a}s. All {c}s are {a}s. Therefore all {c}s are {b}s."), + # Existential-import overreach — INVALID in the modern reading. + ("invalid", lambda a, b, c: f"All {a}s are {b}s. All {a}s are {c}s. Therefore some {c}s are {b}s."), + ), } @@ -117,7 +138,7 @@ def generate_problems(band: str, n: int) -> list[Problem]: def all_gold_problems() -> list[Problem]: """The full deterministic corpus over every shape-band, in band order.""" problems: list[Problem] = [] - for band in (CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC): + for band in (CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC, CATEGORICAL): problems.extend(generate_problems(band, CASES_PER_BAND)) return problems @@ -143,15 +164,26 @@ _OUTCOME_TO_CLASS = { Entailment.REFUSED: "declined", } +#: Categorical outcome mapping: a syllogism is VALID iff the conclusion is +#: entailed; UNKNOWN/REFUTED ⇒ invalid; REFUSED ⇒ declined (inconsistent). +_CATEGORICAL_TO_CLASS = { + Entailment.ENTAILED: "valid", + Entailment.REFUTED: "invalid", + Entailment.UNKNOWN: "invalid", + Entailment.REFUSED: "declined", +} + @dataclass(frozen=True, slots=True) class DeductionSolver: """The production serving pipeline as a ``DomainSolver``. - Runs exactly what ``chat/deduction_surface.py`` runs — ``comprehend`` → - ``to_deductive_logic`` → ``evaluate_entailment_with_trace`` — and commits - the decided outcome class. A reader refusal / non-projectable comprehension - is an uncommitted attempt (``refused``), never a guessed answer. + Runs exactly what ``chat/deduction_surface.py`` runs — the propositional + path (``to_deductive_logic`` → ``evaluate_entailment_with_trace``) then the + categorical path (``to_syllogism`` → ``decide_syllogism``) — and commits the + decided outcome class. A reader refusal / non-projectable comprehension / + engine REFUSED is an uncommitted attempt, never a guessed answer. Kept in + lock-step with the composer's dual path; the lane + license tests cover both. """ domain_id: str = _DOMAIN_ID @@ -164,21 +196,35 @@ class DeductionSolver: committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}", case_id=problem.problem_id, shape=problem.class_name, ) + # Band v1 — propositional. projected = to_deductive_logic(comp) - if projected is None: + if projected is not None: + premises, query = projected + outcome = evaluate_entailment_with_trace(premises, query).outcome return _DeductionAttempt( - committed=False, answer=None, reason="unprojectable", - case_id=problem.problem_id, shape=problem.class_name, + committed=outcome is not Entailment.REFUSED, + answer=_OUTCOME_TO_CLASS[outcome], reason="", + case_id=problem.problem_id, shape=classify_deduction_shape(premises, query), + ) + # Band v1b — categorical / syllogism. + syllogism = to_syllogism(comp) + if syllogism is not None: + structure, s_query = syllogism + try: + outcome = decide_syllogism(structure, s_query).outcome + except CategoricalError: + return _DeductionAttempt( + committed=False, answer=None, reason="categorical_malformed", + case_id=problem.problem_id, shape=CATEGORICAL, + ) + return _DeductionAttempt( + committed=outcome is not Entailment.REFUSED, + answer=_CATEGORICAL_TO_CLASS[outcome], reason="", + case_id=problem.problem_id, shape=CATEGORICAL, ) - premises, query = projected - outcome = evaluate_entailment_with_trace(premises, query).outcome - answer = _OUTCOME_TO_CLASS[outcome] - # An engine REFUSED (inconsistent premises / out-of-regime) is an honest - # non-commitment, not a served verdict. - committed = outcome is not Entailment.REFUSED return _DeductionAttempt( - committed=committed, answer=answer, reason="", - case_id=problem.problem_id, shape=classify_deduction_shape(premises, query), + committed=False, answer=None, reason="unprojectable", + case_id=problem.problem_id, shape=problem.class_name, ) @@ -202,24 +248,37 @@ class ConstructionGoldTether: def assert_corpus_sound() -> None: """Belt-and-suspenders: every generated case's by-construction gold must - agree with the INDEPENDENT truth-table oracle over its projected form. + agree with an INDEPENDENT oracle over its projected form. Guards against a template authoring bug (a mis-stated gold) silently inflating the ledger. Raises ``AssertionError`` on any disagreement. Uses - the oracle (``evals.deductive_logic.oracle``), which shares no code with the - ROBDD serving engine (INV-25), as the construction-time check. + oracles that share no code with the ROBDD serving engine (INV-25): the + truth-table ``evals.deductive_logic.oracle`` for propositional bands, and + the finite-model ``evals.syllogism.oracle`` for the categorical band. """ from evals.deductive_logic.oracle import oracle_entailment + from evals.syllogism.oracle import oracle_answer for problem in all_gold_problems(): comp = comprehend(problem.payload["text"]) assert isinstance(comp, Comprehension), problem.payload["text"] + gold = problem.payload["gold"] projected = to_deductive_logic(comp) - assert projected is not None, problem.payload["text"] - premises, query = projected - oracle = oracle_entailment(premises, query) - assert oracle == problem.payload["gold"], ( - f"{problem.problem_id}: oracle={oracle} gold={problem.payload['gold']} " + if projected is not None: + premises, query = projected + oracle = oracle_entailment(premises, query) + assert oracle == gold, ( + f"{problem.problem_id}: oracle={oracle} gold={gold} " + f"text={problem.payload['text']!r}" + ) + continue + syllogism = to_syllogism(comp) + assert syllogism is not None, problem.payload["text"] + structure, s_query = syllogism + oracle_valid = oracle_answer(structure, s_query)["valid"] + oracle_class = "valid" if oracle_valid else "invalid" + assert oracle_class == gold, ( + f"{problem.problem_id}: syllogism_oracle={oracle_class} gold={gold} " f"text={problem.payload['text']!r}" ) diff --git a/evals/deduction_serve/report.json b/evals/deduction_serve/report.json index 4d809622..44e25cc9 100644 --- a/evals/deduction_serve/report.json +++ b/evals/deduction_serve/report.json @@ -1,8 +1,8 @@ { "aggregate": { - "correct": 27, + "correct": 28, "declined": 0, - "n": 27, + "n": 28, "wrong": 0 }, "all_correct": true, @@ -13,23 +13,27 @@ "v1": { "all_cases_correct": true, "by_gold": { - "declined": 9, + "declined": 6, "entailed": 8, + "invalid": 1, "refuted": 5, - "unknown": 5 + "unknown": 5, + "valid": 3 }, "correct_by_gold": { - "declined": 9, + "declined": 6, "entailed": 8, + "invalid": 1, "refuted": 5, - "unknown": 5 + "unknown": 5, + "valid": 3 }, "counts": { - "correct": 27, + "correct": 28, "declined": 0, "wrong": 0 }, - "n": 27 + "n": 28 } }, "wrong_is_zero": true diff --git a/evals/deduction_serve/runner.py b/evals/deduction_serve/runner.py index 7bc9017c..1467ab79 100644 --- a/evals/deduction_serve/runner.py +++ b/evals/deduction_serve/runner.py @@ -42,8 +42,9 @@ from collections import Counter from pathlib import Path from chat.deduction_surface import looks_like_deductive_argument -from generate.meaning_graph.projectors import to_deductive_logic +from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism from generate.meaning_graph.reader import Comprehension, comprehend +from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace _ROOT = Path(__file__).resolve().parent @@ -59,6 +60,14 @@ _OUTCOME_TO_CLASS = { Entailment.REFUSED: "declined", } +#: Categorical outcome → verdict class (matches the composer / arena mapping). +_CATEGORICAL_TO_CLASS = { + Entailment.ENTAILED: "valid", + Entailment.REFUTED: "invalid", + Entailment.UNKNOWN: "invalid", + Entailment.REFUSED: "declined", +} + def _load(path: Path) -> list[dict]: with path.open(encoding="utf-8") as fh: @@ -66,13 +75,14 @@ def _load(path: Path) -> list[dict]: def decide(text: str) -> str: - """Run the exact pipeline ``chat/deduction_surface.py`` runs in - serving and return the outcome class: entailed/refuted/unknown/declined. + """Run the exact decision pipeline ``chat/deduction_surface.py`` runs in + serving and return the outcome class: entailed/refuted/unknown (propositional), + valid/invalid (categorical), or declined. Mirrors ``deduction_grounded_surface`` call-for-call up to (but not - including) the prose render — the same production decision, typed - instead of rendered, so this lane's assertions are robust to wording - changes. + including) the prose render and the license gate — the same production + decision, typed instead of rendered, so this lane's assertions are robust + to wording changes. """ if not looks_like_deductive_argument(text): return "declined" @@ -80,11 +90,17 @@ def decide(text: str) -> str: if not isinstance(comp, Comprehension): return "declined" projected = to_deductive_logic(comp) - if projected is None: - return "declined" - premises, query = projected - trace = evaluate_entailment_with_trace(premises, query) - return _OUTCOME_TO_CLASS[trace.outcome] + if projected is not None: + premises, query = projected + return _OUTCOME_TO_CLASS[evaluate_entailment_with_trace(premises, query).outcome] + syllogism = to_syllogism(comp) + if syllogism is not None: + structure, s_query = syllogism + try: + return _CATEGORICAL_TO_CLASS[decide_syllogism(structure, s_query).outcome] + except CategoricalError: + return "declined" + return "declined" def build_report(cases: list[dict]) -> dict: diff --git a/evals/deduction_serve/v1/cases.jsonl b/evals/deduction_serve/v1/cases.jsonl index 05354e77..880326b9 100644 --- a/evals/deduction_serve/v1/cases.jsonl +++ b/evals/deduction_serve/v1/cases.jsonl @@ -20,8 +20,9 @@ {"id": "ds-v1-0020", "text": "If p then q. p. Not q. Therefore r.", "gold": "declined", "class": "inconsistent_premises"} {"id": "ds-v1-0021", "text": "p. Not p. Therefore p.", "gold": "declined", "class": "inconsistent_premises"} {"id": "ds-v1-0022", "text": "p or q. Not p. Not q. Therefore p.", "gold": "declined", "class": "inconsistent_premises"} -{"id": "ds-v1-0023", "text": "All mammals are animals. All whales are mammals. Therefore all whales are animals.", "gold": "declined", "class": "out_of_band_categorical"} -{"id": "ds-v1-0024", "text": "No reptiles are mammals. All snakes are reptiles. Therefore no snakes are mammals.", "gold": "declined", "class": "out_of_band_categorical"} +{"id": "ds-v1-0023", "text": "All mammals are animals. All whales are mammals. Therefore all whales are animals.", "gold": "valid", "class": "categorical_barbara"} +{"id": "ds-v1-0024", "text": "No reptiles are mammals. All snakes are reptiles. Therefore no snakes are mammals.", "gold": "valid", "class": "categorical_celarent"} {"id": "ds-v1-0025", "text": "If it rains then the ground is wet. It rains. Therefore the ground is wet.", "gold": "declined", "class": "out_of_band_multiword_conditional"} -{"id": "ds-v1-0026", "text": "Some students are poets. All poets are artists. Therefore some students are artists.", "gold": "declined", "class": "out_of_band_categorical"} +{"id": "ds-v1-0026", "text": "Some students are poets. All poets are artists. Therefore some students are artists.", "gold": "valid", "class": "categorical_datisi"} +{"id": "ds-v1-0028", "text": "All cats are animals. All dogs are animals. Therefore all dogs are cats.", "gold": "invalid", "class": "categorical_undistributed_middle"} {"id": "ds-v1-0027", "text": "If p then q. If q then r. If r then s. p. Therefore s.", "gold": "entailed", "class": "three_hop_chain"} diff --git a/generate/proof_chain/categorical.py b/generate/proof_chain/categorical.py new file mode 100644 index 00000000..7756044d --- /dev/null +++ b/generate/proof_chain/categorical.py @@ -0,0 +1,167 @@ +"""Categorical-syllogism decider by propositional lowering (deduction-serve +arc, Phase 4 / Band v1b, ADR-0256). + +The Phase-0 fork found that the ONLY categorical decider in the tree was +``evals/syllogism/oracle.py`` — the sealed independence oracle the comprehension +lane scores against, which serving must never import (INV-25). This is the +production decider: it lowers a categorical argument into the propositional +regime and decides it with the already-verified ROBDD engine +(``generate.proof_chain.entail``, 716/716 wrong=0). No new decision procedure — +soundness rides on the flagship engine; only the lowering is new. + +The lowering is EXACT for the modern/Boolean reading of the categorical forms +(universals without existential import — the same reading the eval oracle uses). +A model of a k-term categorical argument is fully determined by which of the +``2^k`` term-membership *profiles* are occupied by at least one element. Introduce +one Boolean atom ``occ_j`` per profile ("profile j has ≥1 element") and every +A/E/I/O proposition becomes a propositional formula over those atoms: + + A all S are P ⋀_{j: S∈j, P∉j} ¬occ_j (no S-but-not-P element exists) + E no S are P ⋀_{j: S∈j, P∈j} ¬occ_j + I some S are P ⋁_{j: S∈j, P∈j} occ_j + O some S are not P ⋁_{j: S∈j, P∉j} occ_j + +Validity ("conclusion holds in every model of the premises") is then exactly +propositional entailment, which the ROBDD engine decides. Because the profile +atoms range over ALL occupancy patterns, this is sound AND complete (no reliance +on a lucky domain size). Independent of the eval oracle by mechanism: ROBDD over +a profile encoding vs. brute-force subset enumeration — no shared code. +""" + +from __future__ import annotations + +from itertools import combinations + +from generate.proof_chain.entail import ( + Entailment, + EntailmentTrace, + evaluate_entailment_with_trace, +) + +_FORMS = frozenset({"A", "E", "I", "O"}) + + +class CategoricalError(ValueError): + """Malformed / out-of-grammar categorical input; refuse, never guess.""" + + +def _profiles(n_terms: int) -> tuple[tuple[int, ...], ...]: + """All ``2^n`` membership profiles over ``n`` term-indices, as index tuples. + + A profile is the set of term-indices an element belongs to; ``occ_`` + names whether at least one element has that profile. + """ + idxs = range(n_terms) + out: list[tuple[int, ...]] = [] + for r in range(n_terms + 1): + out.extend(combinations(idxs, r)) + return tuple(out) + + +def _atom(profile: tuple[int, ...]) -> str: + """Deterministic occupancy-atom name for a profile (its member indices).""" + return "occ_" + ("e" if not profile else "_".join(str(i) for i in profile)) + + +def _lower_proposition( + form: str, s_idx: int, p_idx: int, profiles: tuple[tuple[int, ...], ...] +) -> str: + """One A/E/I/O proposition → a propositional formula over occupancy atoms.""" + if form == "A": # ⋀ ¬occ_j over profiles with S and not P + terms = [f"not {_atom(j)}" for j in profiles if s_idx in j and p_idx not in j] + return " and ".join(terms) if terms else "true" + if form == "E": # ⋀ ¬occ_j over profiles with S and P + terms = [f"not {_atom(j)}" for j in profiles if s_idx in j and p_idx in j] + return " and ".join(terms) if terms else "true" + if form == "I": # ⋁ occ_j over profiles with S and P + terms = [_atom(j) for j in profiles if s_idx in j and p_idx in j] + return " or ".join(terms) if terms else "false" + if form == "O": # ⋁ occ_j over profiles with S and not P + terms = [_atom(j) for j in profiles if s_idx in j and p_idx not in j] + return " or ".join(terms) if terms else "false" + raise CategoricalError(f"unsupported categorical form: {form!r}") # pragma: no cover + + +def _term_index(terms: list[str], name: str) -> int: + try: + return terms.index(name) + except ValueError as exc: + raise CategoricalError(f"proposition names unknown term: {name!r}") from exc + + +def _check_proposition(raw: object) -> tuple[str, str, str]: + if not isinstance(raw, dict): + raise CategoricalError(f"proposition must be an object: {raw!r}") + form = raw.get("form") + subject = raw.get("subject") + predicate = raw.get("predicate") + if form not in _FORMS: + raise CategoricalError(f"unsupported categorical form: {form!r}") + if not isinstance(subject, str) or not isinstance(predicate, str): + raise CategoricalError(f"proposition subject/predicate must be strings: {raw!r}") + if subject == predicate: + raise CategoricalError("subject and predicate must be distinct") + return form, subject, predicate + + +def lower_syllogism( + structure: dict, query: dict +) -> tuple[tuple[str, ...], str]: + """Lower a categorical ``(structure, query)`` into ``(premises, query)`` + propositional formula strings over occupancy atoms. Raises + :class:`CategoricalError` on malformed input.""" + raw_terms = structure.get("terms") + if not isinstance(raw_terms, list) or len(raw_terms) < 2: + raise CategoricalError("terms must be a list of at least two term names") + terms = [t for t in raw_terms] + if any(not isinstance(t, str) or not t for t in terms): + raise CategoricalError("every term must be a non-empty string") + if len(set(terms)) != len(terms): + raise CategoricalError("terms contains duplicates") + + raw_premises = structure.get("premises") + if not isinstance(raw_premises, list) or not raw_premises: + raise CategoricalError("premises must be a non-empty list") + if query.get("kind") != "validity": + raise CategoricalError(f"unsupported query kind: {query.get('kind')!r}") + + profiles = _profiles(len(terms)) + premise_formulas: list[str] = [] + for raw in raw_premises: + form, subject, predicate = _check_proposition(raw) + premise_formulas.append( + _lower_proposition( + form, _term_index(terms, subject), _term_index(terms, predicate), profiles + ) + ) + c_form, c_subject, c_predicate = _check_proposition(query.get("conclusion")) + conclusion_formula = _lower_proposition( + c_form, _term_index(terms, c_subject), _term_index(terms, c_predicate), profiles + ) + return tuple(premise_formulas), conclusion_formula + + +def decide_syllogism(structure: dict, query: dict) -> EntailmentTrace: + """Decide a categorical validity query via the verified ROBDD engine. + + Returns the underlying :class:`EntailmentTrace`. Map to a categorical + reading: ``ENTAILED`` ⇒ the syllogism is VALID (the conclusion holds in + every model of the premises); ``UNKNOWN``/``REFUTED`` ⇒ INVALID (the + conclusion is not forced); ``REFUSED`` ⇒ the premises are inconsistent + (no model) or the input was malformed. + """ + premises, conclusion = lower_syllogism(structure, query) + return evaluate_entailment_with_trace(premises, conclusion) + + +def syllogism_is_valid(structure: dict, query: dict) -> bool: + """True iff the categorical argument is VALID (conclusion entailed).""" + return decide_syllogism(structure, query).outcome is Entailment.ENTAILED + + +__all__ = [ + "CategoricalError", + "decide_syllogism", + "lower_syllogism", + "syllogism_is_valid", +] diff --git a/generate/proof_chain/render.py b/generate/proof_chain/render.py index 550c6979..66296dda 100644 --- a/generate/proof_chain/render.py +++ b/generate/proof_chain/render.py @@ -17,6 +17,14 @@ from generate.proof_chain.entail import ( EntailmentTrace, ) +#: A/E/I/O categorical form → an English sentence template over (subject, predicate). +_CATEGORICAL_PHRASE = { + "A": "all {s} are {p}", + "E": "no {s} are {p}", + "I": "some {s} are {p}", + "O": "some {s} are not {p}", +} + def render_entailment( trace: EntailmentTrace, premises: tuple[str, ...], query: str @@ -51,4 +59,37 @@ def render_entailment( return f"Given: {given}. I can't evaluate {query} from that as stated." -__all__ = ["render_entailment"] +def _categorical_clause(prop: dict) -> str: + """One categorical proposition dict → its English clause.""" + template = _CATEGORICAL_PHRASE.get(prop.get("form", ""), "{s} ~ {p}") + return template.format(s=prop.get("subject", "?"), p=prop.get("predicate", "?")) + + +def render_syllogism(trace: EntailmentTrace, structure: dict, query: dict) -> str: + """The user-facing surface for a categorical (syllogism) verdict. + + Deterministic templates over the argument's own clauses — no synthesis. The + ``EntailmentTrace`` is the propositional-lowering decision (``ENTAILED`` ⇒ + valid; ``UNKNOWN``/``REFUTED`` ⇒ invalid; ``REFUSED`` ⇒ inconsistent). + """ + premises = "; ".join( + _categorical_clause(p) for p in structure.get("premises", []) + ) + conclusion = _categorical_clause(query.get("conclusion", {})) + if trace.outcome is Entailment.ENTAILED: + return f"Given: {premises}. That's valid — {conclusion} follows." + if trace.outcome is Entailment.REFUSED and trace.reason == INCONSISTENT_PREMISES: + return ( + f"Given: {premises}. Those premises are inconsistent — they can't all " + f"be true, so I won't assert anything from them." + ) + if trace.outcome is Entailment.REFUSED: + return f"Given: {premises}. I can't evaluate {conclusion} from that as stated." + # UNKNOWN or REFUTED — the conclusion is not forced by the premises. + return ( + f"Given: {premises}. That doesn't follow — {conclusion} isn't guaranteed " + f"by those premises." + ) + + +__all__ = ["render_entailment", "render_syllogism"] diff --git a/generate/proof_chain/shape.py b/generate/proof_chain/shape.py index 255f231b..4571ac8e 100644 --- a/generate/proof_chain/shape.py +++ b/generate/proof_chain/shape.py @@ -27,12 +27,20 @@ DISJUNCTIVE = "disjunctive" CONDITIONAL_CHAIN = "conditional_chain" CONDITIONAL_SINGLE = "conditional_single" ATOMIC = "atomic" +#: Band v1b (Phase 4) — categorical/syllogism arguments. Distinct from the four +#: propositional bands: a categorical argument is projected by ``to_syllogism`` +#: (not ``to_deductive_logic``) and decided by ``generate.proof_chain.categorical`` +#: (the propositional-lowering decider), so the serving composer assigns this band +#: directly rather than by ``classify_deduction_shape`` (which reads propositional +#: formula strings). +CATEGORICAL = "categorical" SHAPE_BANDS: tuple[str, ...] = ( DISJUNCTIVE, CONDITIONAL_CHAIN, CONDITIONAL_SINGLE, ATOMIC, + CATEGORICAL, ) @@ -62,6 +70,7 @@ def classify_deduction_shape(premises: tuple[str, ...], query: str) -> str: __all__ = [ "ATOMIC", + "CATEGORICAL", "CONDITIONAL_CHAIN", "CONDITIONAL_SINGLE", "DISJUNCTIVE", diff --git a/scripts/verify_lane_shas.py b/scripts/verify_lane_shas.py index 297ae161..7673f293 100644 --- a/scripts/verify_lane_shas.py +++ b/scripts/verify_lane_shas.py @@ -51,7 +51,7 @@ PINNED_SHAS: dict[str, str] = { "public_demo": "7d8ba0dbae9287cfe0bf15d231fa78a75abc627121c14900439293e01e1cc1d3", "math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4", "deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", - "deduction_serve_v1": "8fd86265b075be060b72f0d7b3677737de38268ee57b9bcfac30a7f6296d55eb", + "deduction_serve_v1": "b23234b4b57d92e3df9daa3b5d4bbf7fdc505355e32c1440af321c2e1f86bdd2", } diff --git a/tests/test_categorical_decider.py b/tests/test_categorical_decider.py new file mode 100644 index 00000000..ddc97db1 --- /dev/null +++ b/tests/test_categorical_decider.py @@ -0,0 +1,90 @@ +"""Deduction-serve arc, Phase 4 / Band v1b (ADR-0256) — categorical decider. + +The production categorical decider (`generate/proof_chain/categorical.py`) lowers +a syllogism to the propositional regime and rides the verified ROBDD engine. +These tests pin: + + - it agrees, case-for-case, with the INDEPENDENT finite-model syllogism oracle + (`evals/syllogism/oracle.py`) across the committed gold lane — two disjoint + mechanisms converging is the soundness evidence (the decider never imports + the oracle; INV-25 independence); + - the modern/Boolean reading (universals lack existential import): valid forms + are valid, existential-import-only forms are INVALID; + - inconsistent premises and malformed input are refused, never guessed. +""" + +from __future__ import annotations + +import json +from pathlib import Path + +import pytest + +from evals.syllogism.oracle import oracle_answer +from generate.proof_chain.categorical import ( + CategoricalError, + decide_syllogism, + syllogism_is_valid, +) +from generate.proof_chain.entail import Entailment + +_GOLD = Path(__file__).resolve().parents[1] / "evals" / "syllogism" / "v1" / "cases.jsonl" + + +def _gold_cases() -> list[dict]: + return [json.loads(l) for l in _GOLD.read_text(encoding="utf-8").splitlines() if l.strip()] + + +def test_agrees_with_independent_oracle_on_gold_lane() -> None: + """Case-for-case agreement with the finite-model oracle AND the committed + gold — the decider shares no code with either (independent convergence).""" + cases = _gold_cases() + assert cases, "syllogism gold lane must not be empty" + for c in cases: + mine = syllogism_is_valid(c["structure"], c["query"]) + oracle = oracle_answer(c["structure"], c["query"])["valid"] + gold = c["gold"]["valid"] + assert mine == oracle == gold, ( + f"{c['id']}: decider={mine} oracle={oracle} gold={gold} text={c['text']!r}" + ) + + +def test_barbara_valid() -> None: + s = {"terms": ["s", "m", "p"], "premises": [ + {"form": "A", "subject": "m", "predicate": "p"}, + {"form": "A", "subject": "s", "predicate": "m"}]} + q = {"kind": "validity", "conclusion": {"form": "A", "subject": "s", "predicate": "p"}} + assert syllogism_is_valid(s, q) is True + + +def test_darapti_invalid_modern_reading() -> None: + """Darapti (all M are P, all M are S, therefore some S are P) is valid only + with existential import; in the modern reading it is INVALID (M may be empty).""" + s = {"terms": ["s", "m", "p"], "premises": [ + {"form": "A", "subject": "m", "predicate": "p"}, + {"form": "A", "subject": "m", "predicate": "s"}]} + q = {"kind": "validity", "conclusion": {"form": "I", "subject": "s", "predicate": "p"}} + assert syllogism_is_valid(s, q) is False + assert decide_syllogism(s, q).outcome is Entailment.UNKNOWN + + +def test_inconsistent_premises_refused() -> None: + s = {"terms": ["s", "p"], "premises": [ + {"form": "A", "subject": "s", "predicate": "p"}, + {"form": "E", "subject": "s", "predicate": "p"}, + {"form": "I", "subject": "s", "predicate": "p"}]} + q = {"kind": "validity", "conclusion": {"form": "A", "subject": "p", "predicate": "s"}} + assert decide_syllogism(s, q).outcome is Entailment.REFUSED + + +@pytest.mark.parametrize("bad_structure,bad_query", [ + ({"terms": ["a"], "premises": [{"form": "A", "subject": "a", "predicate": "b"}]}, + {"kind": "validity", "conclusion": {"form": "A", "subject": "a", "predicate": "b"}}), + ({"terms": ["a", "b"], "premises": [{"form": "Z", "subject": "a", "predicate": "b"}]}, + {"kind": "validity", "conclusion": {"form": "A", "subject": "a", "predicate": "b"}}), + ({"terms": ["a", "b"], "premises": [{"form": "A", "subject": "a", "predicate": "b"}]}, + {"kind": "sort", "conclusion": {"form": "A", "subject": "a", "predicate": "b"}}), +]) +def test_malformed_input_refused(bad_structure, bad_query) -> None: + with pytest.raises(CategoricalError): + decide_syllogism(bad_structure, bad_query) diff --git a/tests/test_deduction_serve_lane.py b/tests/test_deduction_serve_lane.py index 17a95876..c6013a7d 100644 --- a/tests/test_deduction_serve_lane.py +++ b/tests/test_deduction_serve_lane.py @@ -16,15 +16,18 @@ _V1 = _ROOT / "v1" / "cases.jsonl" def test_v1_lane_wrong_is_zero() -> None: report = build_report(_load(_V1)) - assert report["n"] == 27 + assert report["n"] == 28 assert report["counts"]["wrong"] == 0 assert report["all_cases_correct"] is True - # the sizeable, honest signal: non-trivial committed classes covered + # the sizeable, honest signal: non-trivial committed classes covered, + # including the categorical band (valid + invalid) added in Phase 4. cbg = report["correct_by_gold"] assert cbg.get("entailed", 0) >= 5 assert cbg.get("refuted", 0) >= 5 assert cbg.get("unknown", 0) >= 5 assert cbg.get("declined", 0) >= 5 + assert cbg.get("valid", 0) >= 3 + assert cbg.get("invalid", 0) >= 1 def test_runner_treats_wrong_verdict_as_the_only_real_failure() -> None: diff --git a/tests/test_deduction_surface.py b/tests/test_deduction_surface.py index 69d2cbd1..1503a30a 100644 --- a/tests/test_deduction_surface.py +++ b/tests/test_deduction_surface.py @@ -85,16 +85,27 @@ def test_inconsistent_premises_renders_typed_decline() -> None: assert "inconsistent" in surface -def test_categorical_argument_declines_out_of_band() -> None: - """A syllogism-shaped "therefore" argument commits (argument-shaped) - but is honestly declined — Band v1 is propositional-only; the - production categorical decider is deferred (Band v1b).""" +def test_categorical_argument_is_decided_band_v1b() -> None: + """A valid categorical syllogism is now DECIDED (Band v1b, Phase 4) — the + production categorical decider serves a validity verdict, no longer a + decline.""" surface = deduction_grounded_surface( "All mammals are animals. All whales are mammals. " "Therefore all whales are animals." ) assert surface is not None - assert "categorical" in surface + assert "valid" in surface + assert "follows" in surface + + +def test_invalid_categorical_argument_is_rejected() -> None: + """An invalid syllogism (undistributed middle) is decided INVALID, not + declined and not falsely served as valid (wrong=0 on the categorical band).""" + surface = deduction_grounded_surface( + "All cats are animals. All dogs are animals. Therefore all dogs are cats." + ) + assert surface is not None + assert "doesn't follow" in surface def test_multiword_conditional_declines_reader_refusal() -> None: