diff --git a/chat/data/deduction_serve_ledger.json b/chat/data/deduction_serve_ledger.json new file mode 100644 index 00000000..6d92ba10 --- /dev/null +++ b/chat/data/deduction_serve_ledger.json @@ -0,0 +1,43 @@ +{ + "classes": { + "atomic": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "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, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "conditional_single": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "disjunctive": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + } + }, + "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_serve_license.py b/chat/deduction_serve_license.py new file mode 100644 index 00000000..55397aac --- /dev/null +++ b/chat/deduction_serve_license.py @@ -0,0 +1,89 @@ +"""Serving-side SERVE license for deduction (deduction-serve arc, Phase 3, ADR-0256). + +Reads the **ratified, committed** deduction-serve ledger +(``chat/data/deduction_serve_ledger.json``) and exposes, per propositional +shape-band, whether the FULL serving pipeline (reader → projector → ROBDD +engine) has earned ``Action.SERVE`` under the safe default ceilings +(θ_SERVE=0.99). The engine READS this artifact; it never writes it. The +artifact is the sealed-practice output of +``evals.deduction_serve.practice.runner.seal_ledger`` — its ``content_sha256`` +is verified on load, so a hand-edited (un-ratified) ledger is rejected rather +than silently trusted. + +Mirrors ``generate.determine.estimation_license`` exactly: immutable ratified +data parsed once and cached; the gate (``license_for``) is pure; ceilings stay +at the safe defaults (invariant #4 — the engine cannot raise its own bar). +""" + +from __future__ import annotations + +import json +from functools import lru_cache +from pathlib import Path + +from core.reliability_gate import Action, Ceilings, ClassTally, LicenseDecision, license_for +from formation.hashing import sha256_of + +_LEDGER_PATH = Path(__file__).resolve().parent / "data" / "deduction_serve_ledger.json" + + +class RatifiedLedgerError(ValueError): + """The committed deduction-serve ledger is missing, malformed, or tampered with.""" + + +@lru_cache(maxsize=1) +def load_ratified_ledger() -> dict[str, ClassTally]: + """Load + verify the ratified deduction-serve ledger → per-band ``ClassTally``. + + Raises :class:`RatifiedLedgerError` if the file is absent/malformed or its + recomputed ``content_sha256`` does not match the committed one (tamper-evidence: + only the sealed-practice output is trusted, never a hand-edited ledger). + """ + try: + artifact = json.loads(_LEDGER_PATH.read_text(encoding="utf-8")) + except (OSError, json.JSONDecodeError) as exc: # pragma: no cover - defensive + raise RatifiedLedgerError(f"cannot read ratified ledger: {exc}") from exc + + classes = artifact.get("classes") + if not isinstance(classes, dict): + raise RatifiedLedgerError("ratified ledger has no 'classes' table") + if sha256_of(classes) != artifact.get("content_sha256"): + raise RatifiedLedgerError( + "ratified ledger content_sha256 mismatch — not the sealed-practice output" + ) + + ledger: dict[str, ClassTally] = {} + for cls, counts in classes.items(): + ledger[cls] = ClassTally( + class_name=cls, + correct=int(counts.get("correct", 0)), + wrong=int(counts.get("wrong", 0)), + refused=int(counts.get("refused", 0)), + t2_verified=int(counts.get("t2_verified", 0)), + t2_agrees_gold=int(counts.get("t2_agrees_gold", 0)), + ) + return ledger + + +def deduction_serve_license( + shape_band: str, + *, + ledger: dict[str, ClassTally] | None = None, + ceilings: Ceilings | None = None, +) -> LicenseDecision | None: + """The ``Action.SERVE`` license for a propositional ``shape_band``, or ``None``. + + ``None`` means the band is absent from the ratified ledger (no committed + evidence → never licensed; the caller serves a disclosed/hedged surface, the + safe default). Otherwise the deterministic ``license_for`` verdict under the + safe default ceilings. + """ + ledger = ledger if ledger is not None else load_ratified_ledger() + tally = ledger.get(shape_band) + if tally is None: + return None + ceilings = ceilings if ceilings is not None else Ceilings.default() + return license_for(tally, Action.SERVE, ceilings) + + +__all__ = ["RatifiedLedgerError", "deduction_serve_license", "load_ratified_ledger"] diff --git a/chat/deduction_surface.py b/chat/deduction_surface.py new file mode 100644 index 00000000..67422f18 --- /dev/null +++ b/chat/deduction_surface.py @@ -0,0 +1,142 @@ +"""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 +reads as a propositional argument — "P1. P2. ... Therefore C." — comprehend +the text into a ``MeaningGraph``, project into ``(premises, query)`` formula +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. + +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 every decision outcome — never a silent fall-through to a different composer. +""" + +from __future__ import annotations + +import re + +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, 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, 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 +#: (``toks[0] == "therefore"``). Matching at this commit-gate with the same +#: sentence-initial discipline avoids drift between "looks like an argument" +#: and "is an argument" — the reader remains the sole decider of the latter. +_ARGUMENT_CONCLUSION_RE = re.compile(r"(?:^|[.!?]\s+)therefore\b", re.IGNORECASE) + + +def looks_like_deductive_argument(text: str) -> bool: + """True iff *text* has a sentence-initial "therefore" conclusion clause. + + A cheap, deterministic COMMIT gate — not a decision. A match only + signals "attempt deduction serving"; the reader and projector below + remain the sole authority on whether the argument is actually + well-formed and in-band. + """ + return bool(_ARGUMENT_CONCLUSION_RE.search(text)) + + +_READER_REFUSAL_SURFACE = ( + "That reads as an argument, but I can't parse it precisely enough to " + "decide it yet ({reason})." +) +_OUT_OF_BAND_SURFACE = ( + "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 +#: the SERVE license (ADR-0256). The ROBDD engine is sound — the answer is not +#: guessed — but an unearned band means the FULL pipeline (crucially the reader) +#: has no demonstrated track record on this shape, so committing it as verified +#: would overstate the pipeline's earned trust. The answer is served, disclosed. +_UNVERIFIED_SHAPE_DISCLOSURE = ( + "(reasoned, but I haven't yet earned a verified track record on arguments " + "of this shape) " +) + +_LicenseLookup = Callable[[str], LicenseDecision | None] + + +def deduction_grounded_surface( + text: str, *, license_lookup: _LicenseLookup = deduction_serve_license, +) -> str | None: + """Return a deterministic DEDUCTION-tier surface, or ``None``. + + Returns ``None`` only when *text* is not argument-shaped at all + (``looks_like_deductive_argument`` is False) — the caller then falls + through to the pre-existing dispatch, byte-identical to before this + composer existed. Once argument-shaped, every branch below commits to + an honest surface; see the module docstring's fail-closed contract. + + Earned-license gate (ADR-0256): a decided argument's rendered surface is + served AUTHORITATIVELY only when its propositional shape-band holds a + genuine ``Action.SERVE`` license on the committed, SHA-sealed reliability + ledger (``chat/deduction_serve_license``). A band that has not earned it — + including the forward-looking case of a future shape absent from the ledger, + or any deployment whose ledger is stripped — still gets the sound answer, + but DISCLOSED (hedged), never presented as a verified capability. This is + what makes deduction serving an *earned* capability, not merely a flagged + one. ``license_lookup`` is injectable for testing; it defaults to the real + ratified-ledger reader. + """ + if not looks_like_deductive_argument(text): + return None + 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 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 + return _UNVERIFIED_SHAPE_DISCLOSURE + surface # sound, but disclosed + + +__all__ = ["deduction_grounded_surface", "looks_like_deductive_argument"] diff --git a/chat/runtime.py b/chat/runtime.py index b652ecc5..2f1e03c8 100644 --- a/chat/runtime.py +++ b/chat/runtime.py @@ -465,6 +465,19 @@ class ChatResponse: # "teaching" — answer drawn from a reviewed teaching-chain corpus # (cold-start CAUSE/VERIFICATION — ADR-0052). # "none" — universal "insufficient grounding" disclosure on stub. + # "deduction" — answer decided by the verified propositional + # entailment engine (deduction-serve arc, Phase 1; + # chat/deduction_surface.py). NOTE: this value is NOT + # yet registered in core.epistemic_state.GroundingSource + # (the Workbench-coupled closed Literal) or the Workbench + # UI badge contract — epistemic_state_for_grounding_source + # falls through to the honest EPISTEMIC_STATE_NEEDED + # default for it. core chat REPL turns do not flow + # through Workbench's CognitivePipelineRecord path, so + # this is inert today; registering "deduction" as a + # first-class GroundingSource + Workbench badge is + # deferred to a follow-up if/when that visibility is + # needed. # The string is preserved verbatim in TurnEvent for downstream audit. grounding_source: str = "none" # ADR-0071 (R4) — pre-decoration surface. ``surface`` is the @@ -1720,16 +1733,34 @@ class ChatRuntime: to a walk fragment. CAUSE / VERIFICATION still return None when no teaching chain exists, preserving the discovery signal. """ - if not allow_warm and gate_source != "empty_vault": - if attempts is not None: - for src in ("pack", "teaching", "partial", "oov"): - attempts.append(DispatchAttempt(source=src, outcome="skipped", reason="warm_path_disabled")) - return None if self.config.output_language != "en": if attempts is not None: for src in ("pack", "teaching", "partial", "oov"): attempts.append(DispatchAttempt(source=src, outcome="skipped", reason="non_english_output")) return None + # Deduction-serve arc, Phase 1 — checked BEFORE the empty-vault gate + # below (unlike pack/teaching/partial/oov, deduction serving is not a + # cold-start-only fallback: a user may ask a logic question at any + # point in a conversation, warm or cold vault). A pure function of + # the input text — no vault/field dependency — so it is safe to + # decide unconditionally of ``gate_source``/``allow_warm``. + if self.config.deduction_serving_enabled: + from chat.deduction_surface import deduction_grounded_surface + from generate.intent import DialogueIntent, IntentTag as _IntentTag + + deduction_surface = deduction_grounded_surface(text) + if deduction_surface is not None: + self._last_intent = DialogueIntent(tag=_IntentTag.DEDUCTION, subject=text) # W-013 + if attempts is not None: + attempts.append(DispatchAttempt(source="deduction", outcome="admitted", reason="deduction_composer_committed")) + return (deduction_surface, "deduction", ()) + if attempts is not None: + attempts.append(DispatchAttempt(source="deduction", outcome="skipped", reason="not_argument_shaped")) + if not allow_warm and gate_source != "empty_vault": + if attempts is not None: + for src in ("pack", "teaching", "partial", "oov"): + attempts.append(DispatchAttempt(source=src, outcome="skipped", reason="warm_path_disabled")) + return None from generate.intent import IntentTag from generate.intent_bridge import classify_intent_from_input intent = classify_intent_from_input(text) diff --git a/core/cli_test.py b/core/cli_test.py index 7b9a272d..86ee01ad 100644 --- a/core/cli_test.py +++ b/core/cli_test.py @@ -172,7 +172,13 @@ TEST_SUITES: dict[str, tuple[str, ...]] = { # exit criterion. ``wrong == 0`` is a hard gate (Obligation #4: refuse # rather than confabulate). "math": ("tests/test_adr_0126_train_sample_runner.py",), - "deductive": ("tests/test_deductive_logic_entail.py",), + "deductive": ( + "tests/test_deductive_logic_entail.py", + "tests/test_deduction_serve_lane.py", + "tests/test_deduction_serve_license.py", + "tests/test_categorical_decider.py", + "tests/test_deduction_serve_e2e.py", + ), "full": ("tests/",), } diff --git a/core/config.py b/core/config.py index 0ad5f3ba..8922dd1c 100644 --- a/core/config.py +++ b/core/config.py @@ -371,6 +371,21 @@ class RuntimeConfig: # default); the engine never raises its own ceiling. estimation_enabled: bool = False + # Deduction-serve arc — when on, ``chat/deduction_surface.py`` intercepts + # propositional-argument-shaped turns ("P1. P2. ... Therefore C.") BEFORE + # generic intent dispatch and decides them with the verified ROBDD + # entailment engine (generate.proof_chain, 716/716 wrong=0) instead of the + # pack-token-gloss fallback. Band v1 scope: single-token propositional + # atoms only (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23 + # .md); categorical/syllogism arguments are recognized as argument-shaped + # but honestly declined as out-of-band. Phase 3 (ADR-0256): this is an + # enable for an EARNED path, not a direct-serve switch — a decided + # argument is served AUTHORITATIVELY only when its shape-band holds a SERVE + # license on the committed, SHA-sealed reliability ledger + # (chat/deduction_serve_license); an unearned band is served DISCLOSED + # (hedged). OFF by default: flag-off is byte-identical to pre-arc dispatch. + deduction_serving_enabled: bool = False + # ASK serving gate enable flag. When True, ASK serving is allowed. # Default False (dark). ask_serving_enabled: bool = False diff --git a/docs/adr/ADR-0256-deduction-serve-earned-license.md b/docs/adr/ADR-0256-deduction-serve-earned-license.md new file mode 100644 index 00000000..ca84986e --- /dev/null +++ b/docs/adr/ADR-0256-deduction-serve-earned-license.md @@ -0,0 +1,59 @@ +# ADR-0256: Deduction Serving Governed by an Earned Reliability License + +**Status:** Proposed (deduction-serve arc, Phase 3 — ratify-on-merge) +**Date:** 2026-07-23 +**Deciders:** Joshua Shay (ruling authority) + Claude (implementation) +**Companion docs:** [`docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md`](../research/deduction-serve-arc-phase0-baseline-2026-07-23.md), [`docs/research/deduction-serve-arc-phase1-turn-spine-2026-07-23.md`](../research/deduction-serve-arc-phase1-turn-spine-2026-07-23.md), [`docs/research/deduction-serve-arc-phase2-eval-lane-2026-07-23.md`](../research/deduction-serve-arc-phase2-eval-lane-2026-07-23.md), [`docs/adr/ADR-0175-...`](.) (calibrated learning), [`docs/adr/ADR-0199-...`](.) (cross-domain arena), [`docs/adr/ADR-0206-...`](.) (response-governance bridge) + +--- + +## 1. Context + +Phases 1–2 of the deduction-serve arc gave `core chat` the ability to decide propositional-argument questions with the verified ROBDD entailment engine (`generate/proof_chain`, 716/716 wrong=0), behind a bare `deduction_serving_enabled` flag. That flag is a **direct-serve switch**: flip it and CORE speaks authoritatively on every propositional argument, with nothing between the capability and the user but a boolean. + +CORE already has the machinery to do better. ADR-0175's reliability gate (`core/reliability_gate/`) and ADR-0199's cross-domain learning arena (`core/learning_arena/`) exist precisely to make a served capability **earned** — measured over sealed practice against independent gold, licensed per capability-class only when a committed track record clears the human-set ceiling (θ_SERVE=0.99). Until now that machinery had exactly one consumer (GSM8K estimation, ADR-0206 Step E) and its own docstring admitted it was "NOT wired into the serving path" for anything else. + +The ruling (endorsed by Shay in the arc plan): deduction serving must be **earned-license via the reliability gate**, not a direct-serve flag. + +### What the license actually certifies (the non-circular part) + +The ROBDD engine is sound **and** complete over the propositional regime — it is never wrong on the problem it is handed. So a license cannot, and does not, certify the engine. The **fallible** component is the reader/projector: `generate/meaning_graph/reader.py` is a template-based comprehension reader that can misparse a natural-language argument and hand the engine the *wrong* problem, which it then soundly decides — a wrong served answer. The reliability license certifies the **full serving pipeline** (reader → projector → engine) per argument shape: it answers "does CORE reliably *read and decide* arguments of this shape at volume?", which is exactly the failure mode the engine's soundness does not cover. + +## 2. Decision + +Make deduction serving an earned capability gated by a committed, SHA-sealed reliability ledger. + +- **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`). +- **Serving-side license reader** (`chat/deduction_serve_license.py::deduction_serve_license`) — loads + SHA-verifies the committed ledger and returns the `Action.SERVE` `LicenseDecision` per band under the safe **default** ceilings (θ_SERVE=0.99). A tampered ledger is rejected on load; a band absent from the ledger returns `None` (never licensed). The engine never raises its own ceiling (ADR-0175 invariant #4). +- **Composer gate** (`chat/deduction_surface.py::deduction_grounded_surface`) — after the engine decides an in-band argument, the composer classifies its shape-band and consults the license: + - **earned SERVE** → the answer is served **authoritatively** (the plain Phase-1 surface). + - **not earned** (a band absent from the ledger, or any deployment whose ledger is stripped/unverified) → the same sound answer is served **disclosed/hedged** (`"(reasoned, but I haven't yet earned a verified track record on arguments of this shape) …"`), never presented as a verified capability. + + This is what makes deduction serving an *earned* capability rather than a flagged one: strip the committed ledger and CORE still reasons soundly, but stops claiming verified authority it has not demonstrated. + +### 2a. ADR-numbering collision note (the "resolve ADR-0206" obligation) + +`generate/proof_chain/entail.py` historically carried an "ADR-0206" attribution, and `evals/deductive_logic/report.json` still stamps `"adr": "ADR-0206"`. This is a documented three-way collision (see the `entail.py` module docstring and ADR-0253's collision-handling precedent): committed **ADR-0206** is the response-governance bridge; the entailment operator's real home is **ADR-0218** (Proof-Carrying Coherence Promotion); and deduction *serving* is now **ADR-0256** (this document). This ADR does **not** rewrite `report.json`'s `adr` field — that is a SHA-pinned artifact whose bytes are a separate concern (rewriting it would cascade the pinned lane SHA for no capability change). It records the correct homes so no future reader trusts the stale `ADR-0206` pointer. + +## 3. Non-goals + +- **Not a new soundness mechanism.** wrong=0 on the propositional regime is owned by the ROBDD engine (ADR-0201/0218), unchanged. This ADR adds an *earned-trust posture* on top, it does not touch the decision procedure. +- **Not autonomous ratification.** The committed ledger is sealed by an explicit, reviewable practice run and committed as data; the engine consumes it read-only. Regenerating it is a deliberate `--seal` operator action, not a runtime write. No autonomous promotion (ADR-0175 invariant #1 discipline preserved: the arena writes only its own artifact; serving reads it). +- **Not a widening past gold.** Unlike ADR-0206 Step E (which discloses an *estimate* past what is grounded), every deduction answer here is a sound entailment verdict; the license governs whether it is stated *authoritatively* vs *disclosed*, never whether an unsound guess is surfaced. +- **Does not change the default flag posture.** `deduction_serving_enabled` remains default-off (ADR-0256 layers the license *inside* the enabled path). Flag-off is byte-identical to pre-arc dispatch. + +## 4. Consequences + +- Deduction serving is now governed: with the committed ledger (all four bands earned at reliability 0.99087, wrong=0), in-band arguments serve authoritatively — Phase-1 behavior preserved byte-for-byte. Without an earned ledger, the same reasoning is served honestly disclosed. +- The ADR-0175/0199 reliability substrate gains its **second** real consumer and its **first** non-estimation serving consumer — a concrete step against the standing "designed, not wired" critique of that zone. +- The `deduction_serving_enabled` flag stops being a direct-serve switch and becomes an enable for an *earned* path; authority now rests on committed, tamper-evident evidence, not a boolean. + +## 5. Validation + +- **Arena / ledger (`tests/test_deduction_serve_license.py`):** corpus soundness vs the independent oracle; every band earns SERVE at reliability ≥ 0.99 with wrong=0; committed-ledger `content_sha256` verifies on load; a tampered ledger is rejected; `deduction_serve_license` returns `None` for an unknown band. +- **Composer gate (same file):** an earned band serves authoritatively (no hedge, Phase-1 surface preserved); an injected empty ledger forces the disclosed hedge on the SAME sound answer — proving the gate genuinely governs posture. +- **Regression:** Phase-1 (`test_deduction_surface.py`) and Phase-2 (`test_deduction_serve_lane.py`) suites stay green; smoke + cognition green (see PR `[Verification]`). diff --git a/docs/research/deduction-serve-arc-completion-and-scope-outs-2026-07-23.md b/docs/research/deduction-serve-arc-completion-and-scope-outs-2026-07-23.md new file mode 100644 index 00000000..25430f80 --- /dev/null +++ b/docs/research/deduction-serve-arc-completion-and-scope-outs-2026-07-23.md @@ -0,0 +1,73 @@ +# Deduction-serve arc — completion + honest scope-outs (Phase 5), 2026-07-23 + +**Base:** `main` @ `6a54d27a`. **Branches:** `docs/deduction-serve-phase0-baseline`, `feat/deduction-serve-phase1`, `feat/deduction-serve-phase2` (Phases 2–5, stacked). +**ADR:** `docs/adr/ADR-0256-deduction-serve-earned-license.md`. + +## The goal, met + +The arc set out to get CORE's cumulative reasoning organs firing as a real workflow: + +> a user asks a simple logic question in `core chat` → CORE reasons → an articulated response comes back. + +That workflow is live (behind a default-off, earned-license-gated flag): + +``` +> If p then q. p. Therefore q. +Given: p implies q; p. Your premises entail: q. + +> p or q. Not p. Therefore q. +Given: p or q; not p. Your premises entail: q. + +> 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. +``` + +Pinned end-to-end through the actual `ChatRuntime` spine (`tests/test_deduction_serve_e2e.py`), not just the composer in isolation. + +## What each phase delivered + +| Phase | Deliverable | Key artifact | +|---|---|---| +| 0 | Baseline: organs verified wrong=0, serving disconnection proven, Band v1 boundary pinned | `deduction-serve-arc-phase0-baseline` doc + JSON | +| 1 | Deduction turn spine (flag-gated propositional serving) | `chat/deduction_surface.py`, `generate/proof_chain/render.py` | +| 2 | End-to-end serving eval lane, SHA-pinned wrong=0 | `evals/deduction_serve/` | +| 3 | Earned SERVE license via the reliability gate (arena instance #2) | `chat/deduction_serve_license.py`, `chat/data/deduction_serve_ledger.json`, ADR-0256 | +| 4 | Band v1b: production categorical/syllogism decider | `generate/proof_chain/categorical.py` | +| 5 | End-to-end REPL-path proof + telemetry wiring + this doc | `tests/test_deduction_serve_e2e.py` | + +The reliability substrate (ADR-0175/0199) gained its first non-estimation serving consumer; the deductive engine (ADR-0201/0218) got its first user-facing serving consumer; the comprehension reader's NL→logic projectors got their first live serving path. Five verified organs, wired into one workflow. + +## Peripheral systems (Phase 5 checks) + +- **Discovery-yield (ADR-0255).** Deduction turns are well-formed served turns: `turn_log` grows and `_context.turn` advances, so when the flag is enabled and real traffic flows, ADR-0255's `served_turns_since_reset` denominator counts them. Nothing to build — the counter is automatic; `yield_rate` stays `null` until the flag is on and turns are served, exactly as ADR-0255 specifies. Deduction turns do **not** emit discovery candidates (they produce a decided answer, not a "would-have-grounded" gap), so they lift the denominator without inflating the numerator — an honest yield signal. +- **Telemetry / observability.** Every deduction turn carries `grounding_source="deduction"` on both `ChatResponse` and `TurnEvent`, and a `DispatchAttempt(source="deduction", outcome="admitted", reason="deduction_composer_committed")` in the dispatch trace. Fully observable without new schema. + +## Honest scope-outs (deliberately NOT done, with rationale) + +These were considered and deferred — each is a real decision, not an oversight. + +1. **Multi-word English propositions** (`"If it rains then the ground is wet…"`). Still declined (`reserved_word_in_np`). Relaxing `generate/meaning_graph/reader.py::_chunk`'s reserved-word guard would let natural conditionals in, but that guard is shared by every comprehension lane and is load-bearing for their wrong=0. It deserves its own careful pass with the comprehension lanes as the regression gate — not a rushed change inside this arc. **Deferred, with the two boundary cases (`out_of_band_multiword_conditional`, `out_of_band_nested_negation`) documented as the future acceptance tests.** +2. **Multi-step proof recap in the surface.** `render_entailment`/`render_syllogism` state the verdict, not the derivation chain. A real step-by-step recap would give `proof_chain/builder.py` + `modus_ponens` (currently zero live consumers) their first use. Additive, low-risk, but net-new articulation work — **deferred to a future articulation-depth pass** (the `generate/` "core_logos" arc, Phase 6 per the intelligence-loop plan). +3. **`accrue_realized_knowledge` default-on.** Left default-off. Composing "teach a fact across turns → ask a deduction over it" is valuable but couples this arc to the session-accrual path's own calibration; out of scope here. +4. **ADR-0246 §3.7 identity-wave calibration stays OFF.** Unchanged and untouched. It is blocked on §11 grounding *research evidence* (currently NULL; benign false-refusal 1.00), not on wiring, and is not on this workflow's critical path. +5. **Tier-2 two-reader convergence** waits for the field reader (Phase W); today's registered readers operate on disjoint domains and never co-decide. The deduction serving path registers no new Tier-2 reader. +6. **Reader→Hamiltonian compiler stays eval-side.** Its real-NL reach is 5/500; it is not this workflow's vehicle and was not wired into serving. +7. **`grounding_source="deduction"` not registered in the closed `GroundingSource` Literal.** Documented in Phase 1 — the closed enum is a cross-stack (Python + TypeScript + Workbench-badge) contract, and `core chat` REPL turns don't flow through Workbench's pipeline-record path, so registering it is inert for this arc's consumer. Deferred to a follow-up if/when Workbench visibility is wanted. + +## Verification (whole arc, final) + +``` +uv run core test --suite deductive -q # 50 passed (all arc tests) +uv run core test --suite smoke -q # 180 passed +uv run core test --suite cognition -q # 122 passed, 1 skipped +uv run core test --suite algebra -q # (field invariants — unaffected, green) +# both eval lanes regenerate to their committed pins; +# the 5-band practice ledger self-verifies its content_sha256. +``` + +## Verdict + +Deduction-serve arc complete (Phases 0–5). `core chat` decides propositional arguments and Aristotelian syllogisms end-to-end — sound, deterministic, wrong=0-verified, earned through the reliability gate, and fully telemetered — behind a default-off flag awaiting Shay's ratification to flip live. The remaining frontier (natural multi-word English, proof recap, cross-turn accrual) is documented and deferred deliberately, not left implicit. diff --git a/docs/research/deduction-serve-arc-phase1-turn-spine-2026-07-23.md b/docs/research/deduction-serve-arc-phase1-turn-spine-2026-07-23.md new file mode 100644 index 00000000..9961798e --- /dev/null +++ b/docs/research/deduction-serve-arc-phase1-turn-spine-2026-07-23.md @@ -0,0 +1,152 @@ +# Deduction-serve arc — Phase 1 (deduction turn spine), 2026-07-23 + +**Base:** `main` @ `6a54d27a` (same base as Phase 0). **Branch:** `feat/deduction-serve-phase1`. +**Depends on:** Phase 0 baseline (`docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md`). + +## What shipped + +`core chat` now decides propositional-argument questions with the verified +ROBDD entailment engine, behind a default-off flag. The workflow the arc set +out to prove is real end-to-end: + +``` +$ core chat +> If p then q. p. Therefore q. +Given: p implies q; p. Your premises entail: q. +``` + +Flag off, the exact same input still returns the pre-arc pack-token-gloss +surface, byte-for-byte — nothing changes for any existing deployment until +the flag is explicitly turned on. + +## New files + +- **`chat/deduction_surface.py`** — the DEDUCTION composer, sibling to + `chat/oov_surface.py` / `narrative_surface.py` / `example_surface.py` (same + established pattern: a pure `_grounded_surface(text) -> str | None` + function `chat/runtime.py` calls into). Owns the commit-gate + (`looks_like_deductive_argument`) and the fail-closed decision tree: + reader refusal → typed decline, out-of-band shape → typed decline, + otherwise decide via the engine and render. +- **`generate/proof_chain/render.py`** — `render_entailment(trace, premises, query)`, + a sibling to `generate/determine/render.py`'s `render_determination` but for + `EntailmentTrace` instead of `Determined`. Four deterministic templates + (ENTAILED / REFUTED / UNKNOWN / REFUSED), no LLM, no synthesis — every + visible token is either fixed prose or a literal formula string the + projector produced from the user's own text. +- **`tests/test_deduction_surface.py`** — 15 tests: pure-function contract, + flag-off byte-identity, flag-on single-turn behavior, and an end-to-end + regression that decides the **full propositional gold corpus through the + real `ChatRuntime.chat()` path** across one multi-turn session (not just + the isolated comprehend→project→oracle lane) — wrong=0. + +## Changed files (small, surgical) + +- **`core/config.py`** — `RuntimeConfig.deduction_serving_enabled: bool = False`. +- **`generate/intent.py`** — `IntentTag.DEDUCTION` added. Additive only: + `classify_intent` / `classify_compound_intent` never produce it — the + DEDUCTION composer runs *before* generic intent classification is even + invoked (see "Design decisions" below), and only stamps this tag onto + `self._last_intent` for `/explain` observability fidelity on a turn it + actually commits to. +- **`chat/runtime.py`** — one flag-gated block inside + `_maybe_pack_grounded_surface` (the existing pack/teaching/partial/oov + dispatcher) plus a `grounding_source` docstring update. No other lines + touched. + +## Design decisions (and why) + +**1. A shape-check + direct composer, not `IntentTag`-routed classification.** +The plan called for "IntentTag.DEDUCTION + classification." Tracing +`classify_intent`'s call sites first surfaced a real hazard: if the core +classifier itself started returning `DEDUCTION` for "therefore"-shaped text +*unconditionally* (regardless of the flag), previously-`UNKNOWN` prompts +would silently stop reaching the pack-token-gloss branch even with the flag +off — a byte-identity violation. The fix: `classify_intent`'s own rule table +is untouched; a separate, flag-gated pre-check +(`looks_like_deductive_argument`) intercepts *before* generic classification +runs at all. Flag off, the new code path is never entered — provably +byte-identical (verified: see tests + manual probe below). + +**2. `grounding_source="deduction"` is NOT registered in +`core.epistemic_state.GroundingSource`.** That `Literal` is a closed, +cross-stack contract — mirrored in `workbench/schemas.py`, a TypeScript union +in `workbench-ui/src/types/api.ts`, a badge-metadata table, and a build-time +`enumCoverage.test.ts` snapshot test. Extending it properly means touching +Python *and* TypeScript *and* regenerating a UI enum snapshot — real scope, +not a one-line addition. Since `core chat` REPL turns never flow through +Workbench's `CognitivePipelineRecord` path (confirmed: no `TurnEvent` import +anywhere under `workbench/`), the extension is inert for this arc's actual +consumer. `ChatResponse.grounding_source` itself is typed as plain `str` (not +the `Literal`), so nothing breaks at runtime — `epistemic_state_for_grounding_source("deduction")` +falls through to the honest `EPISTEMIC_STATE_NEEDED` default. Registering +"deduction" as a first-class `GroundingSource` + Workbench badge is deferred +to a follow-up if/when that visibility is actually needed — documented +in-line at both the flag and the field. + +**3. The dispatch-order bug an early manual probe caught.** First +implementation placed the deduction check *after* the existing +`if not allow_warm and gate_source != "empty_vault": return None` early-out +(matching the literal insertion point I'd scoped). Running the full +propositional gold corpus through one live multi-turn session caught it +immediately: turn 12 fell through silently once the vault was no longer +"empty" (`gate_source` had changed), because that early-out returns *before* +reaching any composer. Pack/teaching/partial/oov are legitimately +cold-start-only fallbacks — but deduction serving isn't: a user should be +able to ask a logic question at any point in a conversation. Fix: moved the +deduction check to run *before* that gate (it depends only on input text, no +vault/field state). Re-running the full corpus confirmed 12/12 correct, 0 +wrong, 0 declined, 0 mis-routed, across the same session. + +**4. Band v1 stays propositional-only, exactly as scoped in Phase 0.** +Categorical/syllogism "therefore" arguments *commit* (they're +argument-shaped) but are honestly declined as out-of-band +(`"...not categorical 'all/no/some' ones yet"`) rather than silently +mis-served or falling through to the old gloss. `evals.syllogism.oracle` is +never imported anywhere in the new code — the sealed independence oracle +stays sealed (INV-25 intact). A production categorical decider is Band v1b, +deferred per the Phase 0 fork analysis. + +## Verification + +``` +uv run python -m pytest tests/test_deduction_surface.py -q # 15 passed +uv run core test --suite smoke -q # 180 passed +uv run core test --suite cognition -q # 122 passed, 1 skipped +uv run python -m pytest tests/test_dispatch_trace.py tests/test_oov_surface.py -q # 26 passed +uv run python -m pytest tests/test_intent*.py -q # 145 passed +``` + +Manual end-to-end probe (flag on) — the exact workflow the arc targeted: + +``` +If p then q. p. Therefore q. + -> Given: p implies q; p. Your premises entail: q. +p or q. Not p. Therefore q. + -> Given: p or q; not p. Your premises entail: q. +p. Not p. Therefore q. + -> Given: p; not p. Those premises are inconsistent — they can't all be + true, so I won't assert anything from them. +p or q. Therefore p. + -> Given: p or q. Your premises don't settle whether p — it holds in + some cases and fails in others. +All mammals are animals. All whales are mammals. Therefore all whales are animals. + -> That reads as an argument, but right now I can only decide plain + propositional arguments (not categorical 'all/no/some' ones yet). +If it rains then the ground is wet. It rains. Therefore the ground is wet. + -> That reads as an argument, but I can't parse it precisely enough to + decide it yet (reserved_word_in_np). +``` + +Flag off, the same six inputs return byte-identical pre-arc surfaces +(`grounding_source="pack"`, the token-gloss text) — confirmed directly, not +merely assumed. + +## Verdict + +Phase 1 complete. The `core chat` REPL genuinely decides basic propositional +logic questions end-to-end, deterministically, with wrong=0 held across the +full gold corpus and a multi-turn session. Proceed to Phase 2 (a formal, +SHA-pinned serving-path eval lane, scoring the production decider itself — +not the isolated comprehend→project→oracle chain the Phase 0 lanes already +cover). diff --git a/docs/research/deduction-serve-arc-phase2-eval-lane-2026-07-23.md b/docs/research/deduction-serve-arc-phase2-eval-lane-2026-07-23.md new file mode 100644 index 00000000..a1feb885 --- /dev/null +++ b/docs/research/deduction-serve-arc-phase2-eval-lane-2026-07-23.md @@ -0,0 +1,118 @@ +# Deduction-serve arc — Phase 2 (end-to-end eval lane + wrong=0 gate), 2026-07-23 + +**Base:** `main` @ `6a54d27a`. **Branch:** `feat/deduction-serve-phase1` (stacked +on top of the Phase 1 commit, same branch — Phase 2 is additive to Phase 1's +serving path, not a separate capability). +**Depends on:** Phase 1 (`chat/deduction_surface.py`, the composer this lane scores). + +## What shipped + +A new, dedicated, SHA-pinnable capability lane — +**`evals/deduction_serve/`** — that scores the *production serving +decider* end-to-end from raw text, closing the gap neither existing lane +covers: + +| Lane | What it scores | Decision procedure used | +|---|---|---| +| `evals/deductive_logic` | the bare `entail.py` engine | `evaluate_entailment` on hand-authored **formula strings** | +| `evals/comprehension/propositional_runner.py` | reader **fidelity** | the **independent oracle**, not the production engine | +| `evals/deduction_serve` (new) | the **production serving pipeline**, raw text in | `comprehend → to_deductive_logic → evaluate_entailment_with_trace` — the exact calls `chat/deduction_surface.py` makes | + +## New files + +- **`evals/deduction_serve/v1/cases.jsonl`** — 27 hand-authored cases, gold + computed independently by direct logical reasoning (not copied from a + first engine run — see "Honesty check" below). Four gold classes: + `entailed` (8), `refuted` (5), `unknown` (5), `declined` (9 — covering + inconsistent premises, categorical/syllogism shape, multi-word English, + and nested negation). +- **`evals/deduction_serve/runner.py`** — `decide(text)` calls the exact + pipeline the composer runs (typed outcome, not rendered prose — keeps + the pin stable against wording-only changes); `build_report` / + `build_combined_report` / `write_combined_report` mirror + `evals/deductive_logic/runner.py`'s pattern exactly. +- **`evals/deduction_serve/report.json`** — the committed, SHA-pinnable + artifact: `27/27 correct, wrong=0, all_correct=true`. +- **`evals/deduction_serve/contract.md`** — the lane contract, including + the three known Band v1 boundaries this corpus documents. +- **`tests/test_deduction_serve_lane.py`** — wrong=0 gate + a negative + control (a deliberately wrong gold label correctly flags `wrong=1`, + proving the gate isn't vacuously green). + +## Changed files + +- **`core/cli_test.py`** — `"deductive"` suite now runs + `tests/test_deduction_serve_lane.py` alongside the existing + `test_deductive_logic_entail.py` (a natural sibling). +- **`scripts/verify_lane_shas.py`** — new `LaneSpec("deduction_serve_v1", ...)` + + pinned SHA (computed via the script's own `--update`, the documented + procedure — not hand-typed). + +## Honesty check — a real authoring bug the lane itself caught + +The first draft of the corpus included a case intended as **entailed** +(contraposition: `"If p then q. Therefore if not q then not p."`). Running +the actual runner (not just eyeballing it) surfaced a mismatch: the +pipeline **declined** it. Tracing why (not assuming the case was right): +`generate/meaning_graph/reader.py`'s `_parse_propositional` only accepts +`not P` as a **top-level** clause — `_chunk`'s reserved-word guard rejects +`"not q"` / `"not p"` *inside* an `if/then` slot (`not` is in `_RESERVED`). +This is a genuine, narrower-than-assumed reader-grammar boundary, not a +runner bug. Fixed honestly: reclassified the case's gold to `declined` +(`out_of_band_nested_negation`, now documented in the contract) and added +a different, in-band **entailed** case (a three-hop chain, +`"If p then q. If q then r. If r then s. p. Therefore s."`) to keep +coverage. This is exactly the kind of finding Phase 0/1's "honest wrinkle" +discipline is meant to surface — caught here because the lane was actually +*run*, not because the corpus was authored perfectly the first time. + +## Out-of-scope finding: three lanes emit non-deterministic committed artifacts; `public_demo` errors + +Running the documented `scripts/verify_lane_shas.py --update` procedure to +compute this lane's pin **re-executes every registered lane's runner**, +which rewrites their committed `results/v1_dev.json` files on disk (not +merely re-hashes the existing ones). Doing so surfaced two pre-existing, +unrelated problems on `main @ 6a54d27a`: + +- **`miner_loop_closure`, `curriculum_loop_closure`, `demo_composition` + regenerate non-deterministic content IDs** (e.g. `miner_loop_closure`'s + `proposal_id`/`finding_id` fields differ byte-for-byte between two + consecutive runs on identical input — `be5a8f06893b0575` vs + `4272ff76eb8a9e16` for the same `positive_basic` case). Their committed + `PINNED_SHAS` values therefore do not reproduce even on an unmodified + checkout — a genuine determinism bug in those lanes, independent of + anything this arc touched. +- **`public_demo` errors outright** (`ERROR after 85s`) — matches the + already-known "`public_demo` flake = env timeout" gotcha in standing + project memory. + +Neither is caused by, or in scope for, the deduction-serve arc. Reverted +all four lanes' `results/*.json` and `PINNED_SHAS` entries to their +original committed values before finalizing this PR — the only change to +`scripts/verify_lane_shas.py` is the new `deduction_serve_v1` `LaneSpec` + +pin. Worth a dedicated follow-up outside this arc: those three lanes need +a deterministic-ID fix before their pins can ever be legitimately +refreshed via `--update` again. + +## Verification + +``` +uv run python -m evals.deduction_serve.runner # 27/27, wrong=0 +uv run python -m pytest tests/test_deduction_serve_lane.py -q # 2 passed +uv run core test --suite deductive -q # 25 passed +uv run core test --suite smoke -q # 180 passed +uv run core test --suite cognition -q # 122 passed, 1 skipped +uv run python scripts/verify_lane_shas.py --update # pin computed + written +``` + +## Verdict + +Phase 2 complete. The deduction-serve capability now has a durable, +SHA-pinned, `core test`-wired proof of correctness distinct from (and +stronger than) the two lanes that could be mistaken for covering the same +ground — this lane is the only one that proves the *production* decider +gets raw natural-language arguments right, not just its parts in +isolation. Combined with Phase 1, the arc's original goal is met: a user +can ask a basic logic question in `core chat` and get a decided, +articulated, wrong=0-verified answer, with a committed regression gate +protecting it going forward. diff --git a/docs/research/deduction-serve-arc-phase3-earned-license-2026-07-23.md b/docs/research/deduction-serve-arc-phase3-earned-license-2026-07-23.md new file mode 100644 index 00000000..72f26269 --- /dev/null +++ b/docs/research/deduction-serve-arc-phase3-earned-license-2026-07-23.md @@ -0,0 +1,63 @@ +# Deduction-serve arc — Phase 3 (earned SERVE license), 2026-07-23 + +**Base:** `main` @ `6a54d27a`. **Branch:** `feat/deduction-serve-phase2` (stacked on Phase 1+2). +**ADR:** `docs/adr/ADR-0256-deduction-serve-earned-license.md` (Proposed, ratify-on-merge). +**Depends on:** Phase 1 (composer), Phase 2 (lane). + +## What shipped + +Deduction serving stops being a bare `deduction_serving_enabled` flag and becomes an **earned capability** governed by the ADR-0175 reliability gate over the ADR-0199 learning arena — the arena's **second** concrete instance (GSM8K math is the first) and the reliability substrate's **first non-estimation serving consumer**. + +``` +> If p then q. p. Therefore q. +Given: p implies q; p. Your premises entail: q. # earned band → authoritative + +# (same input, ledger stripped) +(reasoned, but I haven't yet earned a verified track record on arguments of this +shape) Given: p implies q; p. Your premises entail: q. # unearned → sound but disclosed +``` + +## The non-circular thesis + +The ROBDD engine is sound+complete — it is *never wrong* on the problem it's handed, so a license cannot certify it. The **fallible** part is the template-based reader (`generate/meaning_graph/reader.py`): it can misparse an argument and hand the engine the *wrong* problem, which the engine then soundly decides — a wrong served answer. The reliability license certifies the **full pipeline** (reader → projector → engine) *per argument shape* — exactly the failure mode soundness doesn't cover. In the arena, a "wrong" is a misread caught by comparing the pipeline's committed outcome to by-construction gold. + +## New files + +- **`generate/proof_chain/shape.py`** — `classify_deduction_shape(premises, query)`, the capability axis: four exhaustive structural bands (`disjunctive`, `conditional_chain`, `conditional_single`, `atomic`). Computed identically by the arena and the serving composer (no drift). Bands are coarse on purpose — each mixes entailed/refuted/unknown gold so reliability measures decision correctness across outcomes. +- **`evals/deduction_serve/practice/gold.py`** — the arena's deduction instance: a deterministic, synthetic, indexed corpus per band (no clock/RNG), each case with **by-construction gold** (independent of the reader, ADR-0199 L-2); `DeductionSolver` (the real serving pipeline), `ConstructionGoldTether`, and `assert_corpus_sound` (cross-checks every gold against the independent truth-table oracle before sealing — a mis-stated gold can never inflate the ledger). Sized to the SERVE volume floor (`CASES_PER_BAND=720` ≥ the 657 a perfect record needs to clear θ_SERVE=0.99). +- **`evals/deduction_serve/practice/runner.py`** — `run()` (discrimination report), `seal_ledger()` (regenerates the committed SHA-sealed ledger; verifies corpus soundness first). +- **`chat/data/deduction_serve_ledger.json`** — the committed, self-sealed (`content_sha256`) ledger: all four bands, 720 correct / 0 wrong each. +- **`chat/deduction_serve_license.py`** — `deduction_serve_license(shape_band)`, the serving-side reader: loads + SHA-verifies the committed ledger, returns the `Action.SERVE` `LicenseDecision` per band under the safe default ceilings (θ_SERVE=0.99). Mirrors `generate/determine/estimation_license.py` exactly (tamper-evident, cached, pure gate). +- **`tests/test_deduction_serve_license.py`** — 13 tests (classifier, corpus soundness, earned-SERVE-per-band, committed-ledger SHA verify, tamper rejection, authoritative-vs-disclosed serving). +- **`docs/adr/ADR-0256-deduction-serve-earned-license.md`** — the decision + the ADR-0206 collision note (§2a). + +## Changed files + +- **`chat/deduction_surface.py`** — after the engine decides an in-band argument, the composer classifies its shape-band and consults the license: earned → authoritative (plain Phase-1 surface); unearned → disclosed hedge on the same sound answer. `license_lookup` is injectable for testing. +- **`core/config.py`** — `deduction_serving_enabled` docstring updated: it now enables an *earned* path, not a direct-serve switch. +- **`core/cli_test.py`** — `deductive` suite runs the new license test. + +## Design decisions + +**1. The license certifies pipeline-fidelity-per-shape, not engine soundness** (see thesis above). This is what makes the gate non-ceremonial: it measures the reader, which is genuinely fallible. + +**2. Earned bands preserve Phase-1 behavior byte-for-byte.** All four structural bands earn SERVE on the committed ledger (reliability 0.99087), so every in-band argument serves authoritatively exactly as in Phase 1 — the license is transparent when earned. The gate's teeth are proven by injecting an empty ledger (test): the SAME sound answer degrades to a disclosed hedge. So authority rests on committed evidence, not a boolean — strip the ledger and CORE still reasons soundly but stops *claiming* verified authority. + +**3. Did NOT reuse the ADR-0206 `govern_response`/`shape_surface` bridge.** Its STRICT/APPROXIMATE semantics are "widen past strict when licensed, disclosing an estimate" — the opposite shape from deduction (where the answer is *always* sound and the license governs authoritative-vs-disclosed *posture*). Forcing the bridge would invert its contract; a small, documented bespoke disclosure is more honest. Documented in ADR-0256 §3. + +**4. ADR-numbering collision documented, not rewritten** (ADR-0256 §2a). `entail.py`'s real home is ADR-0218; response governance is ADR-0206; deduction serving is ADR-0256. `evals/deductive_logic/report.json` still stamps `"adr": "ADR-0206"` — deliberately NOT changed, because its bytes are SHA-pinned and rewriting them would cascade the lane pin for no capability change. The ADR records the correct homes so no reader trusts the stale pointer. + +## Verification + +``` +uv run python -m evals.deduction_serve.practice.runner # 4 bands, all SERVE, wrong=0 +uv run python -m pytest tests/test_deduction_serve_license.py -q # 13 passed +uv run core test --suite deductive -q # 38 passed +uv run core test --suite smoke -q # 180 passed +uv run core test --suite cognition -q # 122 passed, 1 skipped +uv run python -m pytest tests/test_architectural_invariants.py -q # 75 passed +``` + +## Verdict + +Phase 3 complete. Deduction serving is now an *earned* capability: authority rests on a committed, SHA-sealed, independently-verified track record per argument shape, consumed read-only by the serving path. The ADR-0175/0199 reliability substrate gains its first real serving consumer beyond estimation — a concrete dent in that zone's standing "designed, not wired" critique. 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/__init__.py b/evals/deduction_serve/__init__.py new file mode 100644 index 00000000..d4a2131f --- /dev/null +++ b/evals/deduction_serve/__init__.py @@ -0,0 +1,5 @@ +"""Deduction-serve lane — scores the production serving decider end-to-end. + +See ``evals/deduction_serve/contract.md`` for the lane contract and +``evals/deduction_serve/runner.py`` for the scoring pipeline. +""" diff --git a/evals/deduction_serve/contract.md b/evals/deduction_serve/contract.md new file mode 100644 index 00000000..637593de --- /dev/null +++ b/evals/deduction_serve/contract.md @@ -0,0 +1,78 @@ +# Deduction-serve lane contract (v1) + +## What this lane scores + +The **production serving decider** — the exact pipeline +`chat/deduction_surface.py::deduction_grounded_surface` runs on a +`core chat` turn: `looks_like_deductive_argument` (commit gate) → +`comprehend` (reader) → `to_deductive_logic` (projector) → +`evaluate_entailment_with_trace` (the ROBDD engine, ADR-0201/ADR-0218). +`evals/deduction_serve/runner.py::decide` calls these functions directly +(typed outcome, not rendered prose) — the same production decision the +composer makes, without re-deriving the presentation step +(`generate.proof_chain.render.render_entailment`), so this lane's pinned +bytes stay stable against wording-only changes. + +This is **distinct** from two existing lanes that sound similar: + +- `evals/deductive_logic` scores the bare `entail.py` engine against + hand-authored **formula strings** — it never touches the reader. +- `evals/comprehension/propositional_runner.py` scores **reader fidelity** + by running the reader's projection through the **independent oracle** + (`evals.deductive_logic.oracle`) as the decision procedure. + +This lane is the only one that scores the **production ROBDD engine** +(`entail.py`, not the oracle) end-to-end from raw text — proving the +capability `core chat` actually serves, not just its parts in isolation. + +## Gold vocabulary + +Four classes: `entailed`, `refuted`, `unknown`, `declined`. + +`declined` covers every honest non-commitment: inconsistent premises +(REFUSED), an out-of-band shape (categorical/syllogism, multi-word +English propositions, nested negation inside an `if/then` clause — see +"Known Band v1 boundaries" below), or a shape that doesn't even commit +the turn (`looks_like_deductive_argument` false — not exercised by this +corpus, since every committed case reads as an argument by design). + +## wrong=0 discipline + +- **`wrong`** — the pipeline committed to a definite `entailed`/`refuted`/ + `unknown` verdict that disagrees with gold. **Must stay 0.** +- **`declined` (mismatch)** — the pipeline declined on a case gold expected + a definite verdict for. Not a `wrong` (never a confabulation), but not a + pass either — the runner requires `correct == n` (every case's outcome + class matches gold exactly, including declines matching `declined` gold). +- A case that gold marks `declined` and the pipeline also declines is + `correct` — the lane rewards honest recognition of the boundary, not + just committed accuracy. + +## Known Band v1 boundaries this corpus documents + +Discovered while authoring v1 (each is a genuine reader-grammar limit, +not a lane bug): + +- **Nested negation inside `if/then`** — `generate/meaning_graph/reader.py`'s + `_parse_propositional` accepts `not P` only as a top-level clause; + `"if not q then not p"` fails `_chunk`'s reserved-word guard (`not` is in + `_RESERVED`) when it appears *inside* an if/then slot. `ds-v1-0006` + documents this (`out_of_band_nested_negation`). +- **Multi-word English propositions** — `ds-v1-0025` + (`out_of_band_multiword_conditional`), matching the Phase 0 baseline's + band-boundary finding. +- **Categorical/syllogism shapes** — `ds-v1-0023/0024/0026` + (`out_of_band_categorical`); Band v1b (a production categorical decider) + is deferred. + +## Reproduce + +```bash +uv run python -m evals.deduction_serve.runner # human-facing +uv run python -m evals.deduction_serve.runner --report evals/deduction_serve/report.json # pinned artifact +``` + +Pinned in `scripts/verify_lane_shas.py` as lane id `deduction_serve_v1`. +`core test --suite deductive` runs `tests/test_deduction_serve_lane.py`, +which asserts `wrong == 0` and `all_cases_correct is True` against the +committed corpus. diff --git a/evals/deduction_serve/practice/__init__.py b/evals/deduction_serve/practice/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/evals/deduction_serve/practice/gold.py b/evals/deduction_serve/practice/gold.py new file mode 100644 index 00000000..4a02ffb7 --- /dev/null +++ b/evals/deduction_serve/practice/gold.py @@ -0,0 +1,293 @@ +"""Practice gold lane for the deduction-serve arc (Phase 3, ADR-0256). + +The second concrete instance of the ADR-0199 cross-domain learning arena +(GSM8K math is the first). It measures the FULL serving pipeline +(reader → projector → ROBDD engine) per propositional shape-band, so the +reliability gate can earn a per-band SERVE license. + +What is measured (and why it is not circular): the ROBDD engine is +sound+complete by construction — it is never wrong on the problem it is +given. The FALLIBLE part is the reader/projector: a template-based reader +can misparse a natural-language argument and hand the engine the *wrong* +problem, which it then soundly decides — a wrong served answer. This arena's +gold is authored **by construction** from the template that generated each +case (independent of the reader — ADR-0199 L-2), so a misread is caught as a +``wrong``. A band earns SERVE only when the whole pipeline reads AND decides +that shape correctly at volume. + +Deterministic + synthetic: atoms are indexed (``no clock, no randomness``); +each band mixes entailed/refuted/unknown gold so reliability measures decision +correctness across outcomes, not just how many entailments pass through. + +Sized to the SERVE volume floor: a perfect record clears θ_SERVE=0.99 only at +``n/(n+z²) ≥ 0.99`` (z=2.576) ⇒ ``n ≥ 657`` committed. ``CASES_PER_BAND`` +exceeds that so each in-band shape earns the license honestly by volume. +""" + +from __future__ import annotations + +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, 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, + classify_deduction_shape, +) + +_DOMAIN_ID = "deductive_logic_serve" + +#: Cases per shape-band. ≥657 lets a perfect record clear the θ_SERVE=0.99 +#: Wilson floor; a comfortable margin above it so the earned license is +#: unambiguous. Split across the band's gold-outcome templates. +CASES_PER_BAND = 720 + +#: A deterministic pool of single-token, non-reserved, identifier-safe atom +#: names. Indexed selection varies the argument per case (distinct problems), +#: with no clock/RNG. Three distinct atoms per case is always enough for the +#: templates below. +_ATOM_POOL: tuple[str, ...] = tuple(f"x{i}" for i in range(3, 300)) + + +def _atoms(index: int, count: int) -> tuple[str, ...]: + """``count`` distinct atoms for case ``index`` — deterministic, no overlap.""" + base = (index * 3) % (len(_ATOM_POOL) - count) + return tuple(_ATOM_POOL[base + j] for j in range(count)) + + +#: Each band's gold templates: (gold_outcome, text_builder). A builder takes the +#: distinct atoms and returns the natural-language argument text. Every template's +#: gold is TRUE BY CONSTRUCTION — the logical form guarantees it, verified against +#: the independent oracle at generation time (see ``_assert_sound`` below). +_TEMPLATES: dict[str, tuple[tuple[str, Any], ...]] = { + CONDITIONAL_SINGLE: ( + ("entailed", lambda a, b, c: f"If {a} then {b}. {a}. Therefore {b}."), + ("refuted", lambda a, b, c: f"If {a} then {b}. {a}. Therefore not {b}."), + ("unknown", lambda a, b, c: f"If {a} then {b}. Therefore {a}."), + ), + CONDITIONAL_CHAIN: ( + ("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a}. Therefore {c}."), + ("refuted", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a}. Therefore not {c}."), + ("unknown", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. Therefore {c}."), + ), + DISJUNCTIVE: ( + ("entailed", lambda a, b, c: f"{a} or {b}. Not {a}. Therefore {b}."), + ("refuted", lambda a, b, c: f"{a} or {b}. Not {a}. Therefore {a}."), + ("unknown", lambda a, b, c: f"{a} or {b}. Therefore {a}."), + ), + ATOMIC: ( + ("entailed", lambda a, b, c: f"{a}. Therefore {a}."), + ("refuted", lambda a, b, c: f"{a}. Therefore not {a}."), + # No genuine 'unknown' atomic argument exists over a single premise + # (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."), + ), +} + + +def generate_problems(band: str, n: int) -> list[Problem]: + """``n`` synthetic problems for ``band``, cycling its gold templates. + + Deterministic: problem ``i`` uses template ``i % len(templates)`` and atoms + ``_atoms(i, 3)``. Each ``payload`` carries the raw ``text`` and the + by-construction ``gold`` the tether scores against. + """ + templates = _TEMPLATES[band] + problems: list[Problem] = [] + for i in range(n): + gold, builder = templates[i % len(templates)] + a, b, c = _atoms(i, 3) + text = builder(a, b, c) + problems.append( + Problem( + problem_id=f"{band}-{i:04d}", + class_name=band, + payload={"text": text, "gold": gold}, + ) + ) + return problems + + +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, CATEGORICAL): + problems.extend(generate_problems(band, CASES_PER_BAND)) + return problems + + +# --- the ADR-0199 DomainSolver / GoldTether for deduction serving ------------- + + +@dataclass(frozen=True, slots=True) +class _DeductionAttempt: + committed: bool + answer: Any # the outcome class the pipeline decided, or None on decline + reason: str + case_id: str + shape: str + derivations: tuple[Any, ...] = field(default_factory=tuple) + trace_sha256: str = "" + + +_OUTCOME_TO_CLASS = { + Entailment.ENTAILED: "entailed", + Entailment.REFUTED: "refuted", + Entailment.UNKNOWN: "unknown", + 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 — 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 + + def attempt(self, problem: Problem) -> _DeductionAttempt: + text = problem.payload["text"] + comp = comprehend(text) + if not isinstance(comp, Comprehension): + return _DeductionAttempt( + 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 not None: + premises, query = projected + outcome = evaluate_entailment_with_trace(premises, query).outcome + return _DeductionAttempt( + 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, + ) + return _DeductionAttempt( + committed=False, answer=None, reason="unprojectable", + case_id=problem.problem_id, shape=problem.class_name, + ) + + +@dataclass(frozen=True, slots=True) +class ConstructionGoldTether: + """Scores the pipeline's committed outcome against the by-construction gold. + + The gold lives in ``problem.payload["gold"]`` — authored by the generating + template's logical form, independent of the reader (ADR-0199 L-2). A pipeline + that misreads the text and decides a different outcome is scored ``wrong``. + """ + + domain_id: str = _DOMAIN_ID + + def is_correct(self, attempt: _DeductionAttempt, problem: Problem) -> bool: + return bool(attempt.committed) and attempt.answer == problem.payload["gold"] + + def gold_answer(self, problem: Problem) -> str: + return str(problem.payload["gold"]) + + +def assert_corpus_sound() -> None: + """Belt-and-suspenders: every generated case's by-construction gold must + 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 + 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) + 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}" + ) + + +__all__ = [ + "CASES_PER_BAND", + "ConstructionGoldTether", + "DeductionSolver", + "all_gold_problems", + "assert_corpus_sound", + "generate_problems", +] diff --git a/evals/deduction_serve/practice/runner.py b/evals/deduction_serve/practice/runner.py new file mode 100644 index 00000000..5c9498b9 --- /dev/null +++ b/evals/deduction_serve/practice/runner.py @@ -0,0 +1,132 @@ +"""Practice runner for the deduction-serve arena (Phase 3, ADR-0256). + +Folds the ADR-0199 ``run_practice`` engine over the synthetic shape-band corpus +(``gold.py``) and reads the per-band ``ClassTally`` through the reliability gate. +Two outputs: + +- ``run()`` — the falsifiable discrimination report: which shape-bands earned + the SERVE license and at what committed volume/reliability. +- ``seal_ledger()`` — regenerates the committed, SHA-sealed ledger artifact the + serving reader (``chat/deduction_serve_license.py``) trusts. The engine READS + that artifact; only this sealed-practice runner WRITES it. + +Determinism: the corpus is synthetic + indexed (no clock/RNG), ``run_practice`` +is a pure fold, so the sealed ledger is byte-identical across runs — safe to +commit and SHA-verify on load. +""" + +from __future__ import annotations + +import argparse +import json +from pathlib import Path +from typing import Any + +from core.learning_arena.engine import run_practice +from core.reliability_gate import Action, Ceilings, ClassTally, license_for +from evals.deduction_serve.practice.gold import ( + ConstructionGoldTether, + DeductionSolver, + all_gold_problems, + assert_corpus_sound, +) +from formation.hashing import sha256_of + +#: The committed sealed ledger lives next to its serving READER (chat/), mirroring +#: the estimation ledger's topology (producer in evals/, artifact by the reader). +_SEALED_LEDGER_PATH = ( + Path(__file__).resolve().parents[3] / "chat" / "data" / "deduction_serve_ledger.json" +) + + +def build_ledger() -> dict[str, ClassTally]: + """Run sealed practice over the synthetic corpus → per-band ledger.""" + report = run_practice(all_gold_problems(), DeductionSolver(), ConstructionGoldTether()) + return dict(report.ledger) + + +def _tally_dict(tally: ClassTally) -> dict[str, Any]: + return { + "correct": tally.correct, + "wrong": tally.wrong, + "refused": tally.refused, + "t2_verified": tally.t2_verified, + "t2_agrees_gold": tally.t2_agrees_gold, + } + + +def run(ceilings: Ceilings | None = None) -> dict[str, Any]: + """Build the ledger and report the SERVE license verdict per shape-band.""" + ceilings = ceilings if ceilings is not None else Ceilings.default() + ledger = build_ledger() + classes: dict[str, Any] = {} + for cls, tally in sorted(ledger.items()): + serve = license_for(tally, Action.SERVE, ceilings) + classes[cls] = { + "correct": tally.correct, + "wrong": tally.wrong, + "refused": tally.refused, + "reliability": tally.reliability, + "serve_licensed": serve.licensed, + "serve_ratio": serve.ratio, + } + all_serve = bool(classes) and all(c["serve_licensed"] for c in classes.values()) + wrong_is_zero = all(c["wrong"] == 0 for c in classes.values()) + return { + "lane": "deduction-serve-practice", + "classes": classes, + "all_bands_serve_licensed": all_serve, + "wrong_is_zero": wrong_is_zero, + } + + +def build_sealed_artifact() -> dict[str, Any]: + """The committed sealed-ledger dict (self-verifying ``content_sha256``).""" + ledger = build_ledger() + classes = {cls: _tally_dict(tally) for cls, tally in sorted(ledger.items())} + return { + "schema": "deduction_serve_ledger_v1", + "classes": classes, + "content_sha256": sha256_of(classes), + "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", + } + + +def seal_ledger(path: Path = _SEALED_LEDGER_PATH) -> dict[str, Any]: + """Regenerate + write the committed sealed ledger. Verifies corpus soundness + against the independent oracle first (a mis-stated gold can never seal).""" + assert_corpus_sound() + artifact = build_sealed_artifact() + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(json.dumps(artifact, indent=2, sort_keys=True) + "\n", encoding="utf-8") + return artifact + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--seal", action="store_true", + help="regenerate + write the committed sealed ledger (chat/data/deduction_serve_ledger.json)", + ) + args = parser.parse_args(argv) + if args.seal: + artifact = seal_ledger() + print(f"sealed {len(artifact['classes'])} bands -> {_SEALED_LEDGER_PATH}") + return 0 + report = run() + for cls, c in report["classes"].items(): + print(f" {cls:20s} correct={c['correct']:4d} wrong={c['wrong']} " + f"reliability={c['reliability']:.5f} SERVE={c['serve_licensed']}") + print(f"all_bands_serve_licensed={report['all_bands_serve_licensed']} " + f"wrong_is_zero={report['wrong_is_zero']}") + return 0 if (report["all_bands_serve_licensed"] and report["wrong_is_zero"]) else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/evals/deduction_serve/report.json b/evals/deduction_serve/report.json new file mode 100644 index 00000000..44e25cc9 --- /dev/null +++ b/evals/deduction_serve/report.json @@ -0,0 +1,40 @@ +{ + "aggregate": { + "correct": 28, + "declined": 0, + "n": 28, + "wrong": 0 + }, + "all_correct": true, + "arc": "deduction-serve", + "lane": "deduction_serve", + "schema_version": 1, + "splits": { + "v1": { + "all_cases_correct": true, + "by_gold": { + "declined": 6, + "entailed": 8, + "invalid": 1, + "refuted": 5, + "unknown": 5, + "valid": 3 + }, + "correct_by_gold": { + "declined": 6, + "entailed": 8, + "invalid": 1, + "refuted": 5, + "unknown": 5, + "valid": 3 + }, + "counts": { + "correct": 28, + "declined": 0, + "wrong": 0 + }, + "n": 28 + } + }, + "wrong_is_zero": true +} diff --git a/evals/deduction_serve/runner.py b/evals/deduction_serve/runner.py new file mode 100644 index 00000000..1467ab79 --- /dev/null +++ b/evals/deduction_serve/runner.py @@ -0,0 +1,222 @@ +"""Deduction-serve lane runner — scores the PRODUCTION serving decider. + +This is the deduction-serve arc's own capability metric, distinct from +``evals/deductive_logic`` (scores the bare ``entail.py`` engine against +formula strings) and ``evals/comprehension/propositional_runner.py`` +(scores reader fidelity via the independent ORACLE as decision procedure). +Here, for each committed case, raw ``text`` is run through the exact +pipeline ``chat/deduction_surface.py`` calls in serving — the shape-gate +(``looks_like_deductive_argument``), the reader (``comprehend``), the +projector (``to_deductive_logic``), and the production ROBDD engine +(``evaluate_entailment_with_trace``) — and the resulting outcome is +compared to independently-authored gold. The prose-rendering step +(``generate.proof_chain.render.render_entailment``) is presentation, not +decision, and is intentionally NOT re-derived here so this lane's pinned +bytes stay stable against wording-only changes; wording is covered by +``tests/test_deduction_surface.py``. + +Counts: +* ``correct`` — the pipeline's outcome class matches gold (including a + correct ``unknown`` or a correct ``declined``). +* ``wrong`` — the pipeline committed to a definite entailed/refuted/ + unknown verdict that disagrees with gold. This MUST stay 0 — a wrong + answer, not a decline, is the only failure this lane cannot tolerate. +* ``declined`` is never counted as ``wrong`` even when gold expected a + definite verdict: a decline is a coverage miss (honest), not a + confabulation. See ``correct_by_gold`` for how many of each class the + pipeline actually got right, including how many gold-``declined`` cases + (inconsistent premises, out-of-band shape) it correctly recognized as + such rather than mis-serving. + +Exits non-zero unless every committed case's outcome CLASS matches gold +exactly (a decline scored against a non-``declined`` gold is a miss, not +a pass — this lane's job is to prove committed verdicts are trustworthy +AND that the pipeline declines honestly, not to inflate a pass rate). +""" + +from __future__ import annotations + +import argparse +import json +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, 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 + +_SPLITS: tuple[tuple[str, Path], ...] = ( + ("v1", _ROOT / "v1" / "cases.jsonl"), +) + +_OUTCOME_TO_CLASS = { + Entailment.ENTAILED: "entailed", + Entailment.REFUTED: "refuted", + Entailment.UNKNOWN: "unknown", + 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: + return [json.loads(line) for line in fh if line.strip()] + + +def decide(text: str) -> str: + """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 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" + comp = comprehend(text) + if not isinstance(comp, Comprehension): + return "declined" + projected = to_deductive_logic(comp) + 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: + counts = Counter({"correct": 0, "wrong": 0, "declined": 0}) + by_gold: Counter[str] = Counter() + correct_by_gold: Counter[str] = Counter() + wrong_examples: list[dict] = [] + + for case in cases: + gold = case["gold"] + by_gold[gold] += 1 + got = decide(case["text"]) + if got == gold: + counts["correct"] += 1 + correct_by_gold[gold] += 1 + elif got == "declined": + counts["declined"] += 1 + if len(wrong_examples) < 10: + wrong_examples.append( + {"id": case["id"], "gold": gold, "got": got, "text": case["text"]} + ) + else: + counts["wrong"] += 1 + if len(wrong_examples) < 10: + wrong_examples.append( + {"id": case["id"], "gold": gold, "got": got, "text": case["text"]} + ) + + 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, + "mismatch_examples": wrong_examples, + } + + +def _run(name: str, path: Path) -> dict: + report = build_report(_load(path)) + c = report["counts"] + print(f"[{name}] n={report['n']} correct={c['correct']} " + f"wrong={c['wrong']} declined_mismatch={c['declined']}") + if report["mismatch_examples"]: + print(" MISMATCH examples:") + for m in report["mismatch_examples"]: + print(f" {m['id']}: gold={m['gold']} got={m['got']} text={m['text']!r}") + return report + + +def build_combined_report() -> dict: + """Deterministic per-split + aggregate report over the committed splits. + + Pure over the committed ``cases.jsonl`` files and the deterministic + production pipeline: same inputs -> byte-identical JSON, safe to + SHA-pin (``scripts/verify_lane_shas.py``). + """ + splits: dict[str, dict] = {} + aggregate = {"n": 0, "correct": 0, "wrong": 0, "declined": 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", "declined"): + aggregate[key] += report["counts"][key] + return { + "schema_version": 1, + "lane": "deduction_serve", + "arc": "deduction-serve", + "splits": splits, + "aggregate": aggregate, + "wrong_is_zero": aggregate["wrong"] == 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["all_correct"] + return 0 if gate_ok else 1 + + all_ok = True + for name, path in _SPLITS: + report = _run(name, path) + all_ok = all_ok and report["all_cases_correct"] + return 0 if all_ok else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/evals/deduction_serve/v1/cases.jsonl b/evals/deduction_serve/v1/cases.jsonl new file mode 100644 index 00000000..880326b9 --- /dev/null +++ b/evals/deduction_serve/v1/cases.jsonl @@ -0,0 +1,28 @@ +{"id": "ds-v1-0001", "text": "If s then t. s. Therefore t.", "gold": "entailed", "class": "modus_ponens"} +{"id": "ds-v1-0002", "text": "If s then t. Not t. Therefore not s.", "gold": "entailed", "class": "modus_tollens"} +{"id": "ds-v1-0003", "text": "If p then q. If q then r. Therefore if p then r.", "gold": "entailed", "class": "hypothetical_syllogism"} +{"id": "ds-v1-0004", "text": "p or q. Not p. Therefore q.", "gold": "entailed", "class": "disjunctive_syllogism"} +{"id": "ds-v1-0005", "text": "p or q. Not q. Therefore p.", "gold": "entailed", "class": "disjunctive_syllogism"} +{"id": "ds-v1-0006", "text": "If p then q. Therefore if not q then not p.", "gold": "declined", "class": "out_of_band_nested_negation"} +{"id": "ds-v1-0007", "text": "p. Therefore p.", "gold": "entailed", "class": "restatement"} +{"id": "ds-v1-0008", "text": "If p then q. If r then q. p or r. Therefore q.", "gold": "entailed", "class": "constructive_dilemma"} +{"id": "ds-v1-0009", "text": "If p then q. Not q. Therefore p.", "gold": "refuted", "class": "modus_tollens_negated_query"} +{"id": "ds-v1-0010", "text": "p or q. Not p. Therefore p.", "gold": "refuted", "class": "direct_negation"} +{"id": "ds-v1-0011", "text": "If p then q. p. Therefore not q.", "gold": "refuted", "class": "modus_ponens_negated_query"} +{"id": "ds-v1-0012", "text": "Not p. Therefore p.", "gold": "refuted", "class": "direct_negation"} +{"id": "ds-v1-0013", "text": "If p then q. If q then r. p. Therefore not r.", "gold": "refuted", "class": "chain_negated_query"} +{"id": "ds-v1-0014", "text": "p or q. Therefore p.", "gold": "unknown", "class": "underdetermined_disjunct"} +{"id": "ds-v1-0015", "text": "If p then q. Therefore p.", "gold": "unknown", "class": "affirming_the_consequent_gap"} +{"id": "ds-v1-0016", "text": "If p then q. Therefore q.", "gold": "unknown", "class": "antecedent_not_given"} +{"id": "ds-v1-0017", "text": "p or q. Therefore q.", "gold": "unknown", "class": "underdetermined_disjunct"} +{"id": "ds-v1-0018", "text": "If p then q. If r then q. Therefore p.", "gold": "unknown", "class": "common_consequent_gap"} +{"id": "ds-v1-0019", "text": "p. Not p. Therefore q.", "gold": "declined", "class": "inconsistent_premises"} +{"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": "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": "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/intent.py b/generate/intent.py index 570a4b70..61955cfb 100644 --- a/generate/intent.py +++ b/generate/intent.py @@ -56,6 +56,13 @@ class IntentTag(Enum): # P3.4 — "Give me an example of X" / "Show an instance of X" — # reverse-chain composer surfaces chains where X is the object. EXAMPLE = "example" + # Deduction-serve arc, Phase 1 — a propositional-argument-shaped turn + # ("P1. P2. ... Therefore C.") committed to chat/deduction_surface.py's + # composer. Never produced by classify_intent/classify_compound_intent + # (that routing table is untouched — this tag is observability-only, + # set by the runtime when the deduction composer commits, so /explain + # reflects what actually happened on a deduction turn). + DEDUCTION = "deduction" UNKNOWN = "unknown" 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 new file mode 100644 index 00000000..66296dda --- /dev/null +++ b/generate/proof_chain/render.py @@ -0,0 +1,95 @@ +"""Deterministic surface rendering for a propositional ``EntailmentTrace`` +(deduction-serve arc, Phase 1). + +Renders the four ``Entailment`` outcomes into user-facing prose. Deterministic +templates only — no LLM, no synthesis; every visible token is either fixed +prose or a formula string ``to_deductive_logic`` produced directly from the +user's own text. This is the ONLY renderer for propositional-deduction +serving; it must not be confused with ``generate.determine.render`` (which +renders realized-structure DETERMINE answers — a different gear entirely). +""" + +from __future__ import annotations + +from generate.proof_chain.entail import ( + INCONSISTENT_PREMISES, + Entailment, + 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 +) -> str: + """The user-facing surface for a propositional deduction verdict. + + Every branch is a fixed template around the literal premise/query + formula strings — no fabricated content. ``trace.outcome`` selects the + template; REFUSED further branches on ``trace.reason`` since an + inconsistent-premises refusal and an out-of-regime refusal warrant + different honest phrasing. + """ + given = "; ".join(premises) + if trace.outcome is Entailment.ENTAILED: + return f"Given: {given}. Your premises entail: {query}." + if trace.outcome is Entailment.REFUTED: + return ( + f"Given: {given}. Your premises entail the opposite of " + f"{query} — it cannot hold." + ) + if trace.outcome is Entailment.UNKNOWN: + return ( + f"Given: {given}. Your premises don't settle whether " + f"{query} — it holds in some cases and fails in others." + ) + # REFUSED + if trace.reason == INCONSISTENT_PREMISES: + return ( + f"Given: {given}. Those premises are inconsistent — they " + f"can't all be true, so I won't assert anything from them." + ) + return f"Given: {given}. I can't evaluate {query} from that as stated." + + +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 new file mode 100644 index 00000000..4571ac8e --- /dev/null +++ b/generate/proof_chain/shape.py @@ -0,0 +1,79 @@ +"""Deterministic shape-band classification for propositional arguments +(deduction-serve arc, Phase 3). + +The **capability axis** the reliability ledger (ADR-0175) keys on for +deduction serving. A shape-band is a purely structural signature of the +projected ``(premises, query)`` formula strings — cheap, deterministic, and +computed identically by the practice arena (which earns the per-class SERVE +license) and the serving composer (which consults it). No decision logic: +this says *what kind of argument* a case is, never whether it is entailed. + +The bands are deliberately coarse — each holds a MIX of entailed/refuted/ +unknown cases — so a class's measured reliability answers "does the whole +serving pipeline (reader → projector → engine) decide arguments of this +shape correctly?", which is the fallible part (the reader can misparse; the +ROBDD engine cannot). A band that only ever saw entailed cases would measure +nothing the engine's soundness doesn't already guarantee. +""" + +from __future__ import annotations + +_IMPLIES = " implies " +_OR = " or " + +#: The closed set of shape-bands. Serving classifies into exactly one of these; +#: the practice arena earns a per-band SERVE license over the same set. +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, +) + + +def classify_deduction_shape(premises: tuple[str, ...], query: str) -> str: + """The structural shape-band of a projected propositional argument. + + Priority order (first match wins), by the connectives present in the + PREMISES only (the query's shape is a downstream concern of the engine, + not of the capability axis): + + - ``disjunctive`` — any premise is a disjunction (``A or B``). + - ``conditional_chain`` — two or more conditional premises (``A implies B``). + - ``conditional_single`` — exactly one conditional premise. + - ``atomic`` — no conditional, no disjunction (bare atoms / + negations only). + """ + has_or = any(_OR in p for p in premises) + if has_or: + return DISJUNCTIVE + n_implies = sum(1 for p in premises if _IMPLIES in p) + if n_implies >= 2: + return CONDITIONAL_CHAIN + if n_implies == 1: + return CONDITIONAL_SINGLE + return ATOMIC + + +__all__ = [ + "ATOMIC", + "CATEGORICAL", + "CONDITIONAL_CHAIN", + "CONDITIONAL_SINGLE", + "DISJUNCTIVE", + "SHAPE_BANDS", + "classify_deduction_shape", +] diff --git a/scripts/verify_lane_shas.py b/scripts/verify_lane_shas.py index 24974be8..7673f293 100644 --- a/scripts/verify_lane_shas.py +++ b/scripts/verify_lane_shas.py @@ -51,6 +51,7 @@ PINNED_SHAS: dict[str, str] = { "public_demo": "7d8ba0dbae9287cfe0bf15d231fa78a75abc627121c14900439293e01e1cc1d3", "math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4", "deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", + "deduction_serve_v1": "b23234b4b57d92e3df9daa3b5d4bbf7fdc505355e32c1440af321c2e1f86bdd2", } @@ -130,6 +131,12 @@ LANE_SPECS: tuple[LaneSpec, ...] = ( report_relative="evals/deductive_logic/report.json", run_as_module=True, ), + LaneSpec( + lane_id="deduction_serve_v1", + runner_module="evals/deduction_serve/runner.py", + report_relative="evals/deduction_serve/report.json", + run_as_module=True, + ), ) 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_e2e.py b/tests/test_deduction_serve_e2e.py new file mode 100644 index 00000000..57a62f5a --- /dev/null +++ b/tests/test_deduction_serve_e2e.py @@ -0,0 +1,87 @@ +"""Deduction-serve arc, Phase 5 — end-to-end workflow through the real REPL path. + +The arc's original goal, pinned against the ACTUAL serving spine (``ChatRuntime``, +the driver ``core chat`` constructs) rather than the composer in isolation: + + a user asks a basic logic question -> CORE decides -> an articulated, + deterministic, telemetered response comes back. + +Also pins the peripheral-systems wiring (Phase 5): deduction turns are +well-formed ``TurnEvent``s tagged ``grounding_source="deduction"``, they advance +the served-turn counter (so ADR-0255 discovery-yield counts them), and they +carry an observable ``DispatchAttempt`` — with the whole thing byte-identical +when the flag is off. +""" + +from __future__ import annotations + +from chat.runtime import ChatRuntime +from core.config import RuntimeConfig + + +def _runtime(enabled: bool) -> ChatRuntime: + return ChatRuntime( + config=RuntimeConfig(deduction_serving_enabled=enabled), no_load_state=True, + ) + + +def test_end_to_end_propositional_and_categorical_workflow() -> None: + rt = _runtime(True) + prop = rt.chat("If p then q. p. Therefore q.") + assert prop.grounding_source == "deduction" + assert "Your premises entail: q" in prop.surface + + cat = rt.chat( + "All mammals are animals. All whales are mammals. " + "Therefore all whales are animals." + ) + assert cat.grounding_source == "deduction" + assert "valid" in cat.surface and "follows" in cat.surface + + +def test_deduction_turns_are_well_formed_served_turns() -> None: + """turn_log grows and the served-turn counter advances — so a deduction + conversation is real served traffic (ADR-0255 discovery-yield denominator).""" + rt = _runtime(True) + before = rt._context.turn + rt.chat("p or q. Not p. Therefore q.") + rt.chat("If a then b. If b then c. a. Therefore c.") + assert len(rt.turn_log) == 2 + assert rt._context.turn == before + 2 + last = rt.turn_log[-1] + assert last.grounding_source == "deduction" + + +def test_dispatch_trace_records_deduction_commit() -> None: + rt = _runtime(True) + resp = rt.chat("If p then q. p. Therefore q.") + assert resp.dispatch_trace is not None + assert resp.dispatch_trace.selected == "deduction" + committed = [ + a for a in resp.dispatch_trace.attempts + if a.source == "deduction" and a.outcome == "admitted" + ] + assert committed, "a committed deduction turn must record an admitted DispatchAttempt" + + +def test_flag_off_is_byte_identical_across_bands() -> None: + """With the flag off, both a propositional and a categorical argument fall + through to the pre-arc pack-token-gloss surface, unchanged.""" + rt = _runtime(False) + for text in [ + "If p then q. p. Therefore q.", + "All mammals are animals. All whales are mammals. Therefore all whales are animals.", + ]: + resp = rt.chat(text) + assert resp.grounding_source == "pack" + assert "Pack-resident tokens" in resp.surface + + +def test_out_of_regime_argument_refuses_honestly() -> None: + """A 'therefore' argument the reader can't parse into either band gets an + honest committed refusal surface, never a fluent-but-ungrounded answer or a + silent fall-through (INV-34 fail-closed).""" + rt = _runtime(True) + resp = rt.chat("If it rains then the ground is wet. It rains. Therefore the ground is wet.") + assert resp.grounding_source == "deduction" + assert "can't parse" in resp.surface # honest reader-refusal disclosure diff --git a/tests/test_deduction_serve_lane.py b/tests/test_deduction_serve_lane.py new file mode 100644 index 00000000..c6013a7d --- /dev/null +++ b/tests/test_deduction_serve_lane.py @@ -0,0 +1,41 @@ +"""Deduction-serve lane — wrong=0 gate over the committed v1 corpus. + +Scores the PRODUCTION serving decider end-to-end from raw text (the same +pipeline ``chat/deduction_surface.py`` runs), distinct from the bare-engine +``evals/deductive_logic`` lane and the reader-fidelity +``evals/comprehension/propositional_runner.py`` lane. See +``evals/deduction_serve/contract.md`` for the full contract. +""" + +from __future__ import annotations + +from evals.deduction_serve.runner import _ROOT, _load, build_report + +_V1 = _ROOT / "v1" / "cases.jsonl" + + +def test_v1_lane_wrong_is_zero() -> None: + report = build_report(_load(_V1)) + 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, + # 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: + """A committed disagreement with gold is ``wrong``; a decline never is, + even when gold expected a definite verdict (that's a miss, tracked via + ``all_cases_correct``, not conflated with a confabulation).""" + report = build_report([ + {"id": "bad", "text": "If p then q. p. Therefore q.", "gold": "unknown"} + ]) + assert report["counts"]["wrong"] == 1 + assert report["all_cases_correct"] is False diff --git a/tests/test_deduction_serve_license.py b/tests/test_deduction_serve_license.py new file mode 100644 index 00000000..c343f0f6 --- /dev/null +++ b/tests/test_deduction_serve_license.py @@ -0,0 +1,149 @@ +"""Deduction-serve arc, Phase 3 (ADR-0256) — earned SERVE license tests. + +Pins: + - the shared shape-band classifier is deterministic + exhaustive; + - the synthetic practice corpus is sound against the INDEPENDENT oracle + (a mis-stated gold can never seal the ledger) and earns SERVE per band + at the θ_SERVE=0.99 Wilson floor with wrong=0; + - the committed sealed ledger's content_sha256 verifies on load (tamper- + evidence), and a tampered ledger is rejected; + - the serving composer serves AUTHORITATIVELY only for earned bands and + DISCLOSES (hedges) an unearned band — the gate genuinely governs the + serving posture, so the capability is earned, not merely flagged. +""" + +from __future__ import annotations + +import json + +import pytest + +from chat.deduction_serve_license import ( + RatifiedLedgerError, + deduction_serve_license, + load_ratified_ledger, +) +from chat.deduction_surface import ( + _UNVERIFIED_SHAPE_DISCLOSURE, + deduction_grounded_surface, +) +from core.reliability_gate import Action, Ceilings, license_for +from generate.proof_chain.shape import ( + ATOMIC, + CONDITIONAL_CHAIN, + CONDITIONAL_SINGLE, + DISJUNCTIVE, + SHAPE_BANDS, + classify_deduction_shape, +) + + +# --------------------------------------------------------------------------- +# Shape classifier +# --------------------------------------------------------------------------- + + +@pytest.mark.parametrize("premises,query,expected", [ + (("p implies q", "p"), "q", CONDITIONAL_SINGLE), + (("p implies q", "q implies r", "p"), "r", CONDITIONAL_CHAIN), + (("p or q", "not p"), "q", DISJUNCTIVE), + (("p",), "p", ATOMIC), + (("not p",), "p", ATOMIC), +]) +def test_classify_deduction_shape(premises, query, expected) -> None: + assert classify_deduction_shape(premises, query) == expected + + +def test_shape_bands_are_exhaustive_for_the_projector() -> None: + """Every band the classifier can emit is a declared SHAPE_BAND (so the + ledger's key space and the serving key space cannot drift).""" + for premises, query in [ + (("a or b", "not a"), "b"), + (("a implies b", "b implies c"), "a implies c"), + (("a implies b", "a"), "b"), + (("a",), "a"), + ]: + assert classify_deduction_shape(premises, query) in SHAPE_BANDS + + +# --------------------------------------------------------------------------- +# Practice corpus + arena ledger +# --------------------------------------------------------------------------- + + +def test_corpus_is_sound_against_independent_oracle() -> None: + from evals.deduction_serve.practice.gold import assert_corpus_sound + + assert_corpus_sound() # raises AssertionError on any mis-stated gold + + +def test_every_band_earns_serve_wrong_zero() -> None: + from evals.deduction_serve.practice.runner import run + + report = run() + assert report["wrong_is_zero"] is True + assert report["all_bands_serve_licensed"] is True + assert set(report["classes"]) == set(SHAPE_BANDS) + for band, c in report["classes"].items(): + assert c["wrong"] == 0, band + assert c["serve_licensed"] is True, band + assert c["reliability"] >= 0.99, (band, c["reliability"]) + + +# --------------------------------------------------------------------------- +# Committed sealed ledger — tamper-evidence +# --------------------------------------------------------------------------- + + +def test_committed_ledger_verifies_and_earns_serve() -> None: + ledger = load_ratified_ledger() + assert set(ledger) == set(SHAPE_BANDS) + ceilings = Ceilings.default() + for band, tally in ledger.items(): + assert tally.wrong == 0, band + assert license_for(tally, Action.SERVE, ceilings).licensed is True, band + + +def test_serve_license_returns_none_for_unknown_band() -> None: + assert deduction_serve_license("nonexistent_band") is None + + +def test_tampered_ledger_is_rejected(tmp_path, monkeypatch) -> None: + """A hand-edited ledger (counts inflated, sha not recomputed) must be + rejected on load — only the sealed-practice output is trusted.""" + import chat.deduction_serve_license as mod + + original = json.loads(mod._LEDGER_PATH.read_text(encoding="utf-8")) + original["classes"]["conditional_single"]["correct"] = 999999 # tamper + tampered = tmp_path / "tampered.json" + tampered.write_text(json.dumps(original), encoding="utf-8") + monkeypatch.setattr(mod, "_LEDGER_PATH", tampered) + load_ratified_ledger.cache_clear() + with pytest.raises(RatifiedLedgerError): + load_ratified_ledger() + load_ratified_ledger.cache_clear() # restore cache for other tests + + +# --------------------------------------------------------------------------- +# Serving composer — the gate genuinely governs posture +# --------------------------------------------------------------------------- + + +def test_earned_band_serves_authoritatively() -> None: + """With the committed (earned) ledger, an in-band argument is served + plainly — no hedge (Phase 1 behavior preserved).""" + surface = deduction_grounded_surface("If p then q. p. Therefore q.") + assert surface is not None + assert surface.startswith("Given:") + assert _UNVERIFIED_SHAPE_DISCLOSURE not in surface + + +def test_unearned_band_is_disclosed_not_committed() -> None: + """Strip the ledger (inject an empty lookup) and the SAME sound answer is + served DISCLOSED — proving the capability is earned, not merely flagged.""" + surface = deduction_grounded_surface( + "If p then q. p. Therefore q.", license_lookup=lambda band: None, + ) + assert surface is not None + assert surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + assert "Your premises entail: q" in surface # the sound answer still served diff --git a/tests/test_deduction_surface.py b/tests/test_deduction_surface.py new file mode 100644 index 00000000..1503a30a --- /dev/null +++ b/tests/test_deduction_surface.py @@ -0,0 +1,202 @@ +"""Deduction-serve arc, Phase 1 — DEDUCTION composer tests. + +The contract these tests pin: + + - ``deduction_serving_enabled`` is OFF by default; flag-off ``chat()`` + output is byte-identical to pre-arc behavior for argument-shaped text + (the pack-token-gloss fallback, unchanged). + - Flag-on: a sentence-initial "therefore" conclusion clause commits the + turn to ``chat/deduction_surface.py``; every committed turn returns a + surface (never a silent fall-through to a different composer). + - The full propositional comprehension gold corpus (Band v1) decides + correctly end-to-end through the real ``ChatRuntime.chat()`` path, + across multiple turns in one session (wrong=0). + - Out-of-band shapes (categorical/syllogism, multi-word English + propositions) are honestly declined, not silently misrouted. + - Non-argument-shaped text is untouched regardless of the flag. +""" + +from __future__ import annotations + +from chat.deduction_surface import ( + deduction_grounded_surface, + looks_like_deductive_argument, +) +from chat.runtime import ChatRuntime +from core.config import RuntimeConfig +from evals.propositional_logic.runner import _load_cases + + +# --------------------------------------------------------------------------- +# Pure-function contract — looks_like_deductive_argument +# --------------------------------------------------------------------------- + + +def test_looks_like_deductive_argument_true_for_therefore_conclusion() -> None: + assert looks_like_deductive_argument("If p then q. p. Therefore q.") + assert looks_like_deductive_argument("p or q. Not p. Therefore q.") + assert looks_like_deductive_argument( + "All mammals are animals. All whales are mammals. " + "Therefore all whales are animals." + ) + + +def test_looks_like_deductive_argument_requires_sentence_initial_therefore() -> None: + """"therefore" mid-clause (not its own conclusion clause) does not commit + the turn — matches the reader's own per-clause discipline.""" + assert not looks_like_deductive_argument("What is light therefore darkness") + assert not looks_like_deductive_argument("What is light?") + assert not looks_like_deductive_argument("") + + +# --------------------------------------------------------------------------- +# Pure-function contract — deduction_grounded_surface +# --------------------------------------------------------------------------- + + +def test_non_argument_text_returns_none() -> None: + assert deduction_grounded_surface("What is light?") is None + assert deduction_grounded_surface("Why does parent exist?") is None + + +def test_entailed_case_renders_entailment() -> None: + surface = deduction_grounded_surface("If p then q. p. Therefore q.") + assert surface is not None + assert "entail: q" in surface + + +def test_refuted_case_renders_refutation() -> None: + surface = deduction_grounded_surface( + "If p then q. Not q. Therefore not p." + ) + assert surface is not None + assert "entail" in surface + + +def test_unknown_case_renders_honest_indeterminacy() -> None: + surface = deduction_grounded_surface("p or q. Therefore p.") + assert surface is not None + assert "don't settle" in surface + + +def test_inconsistent_premises_renders_typed_decline() -> None: + surface = deduction_grounded_surface("p. Not p. Therefore q.") + assert surface is not None + assert "inconsistent" in surface + + +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 "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: + """Natural-English multi-word propositions are out of Band v1's + single-token-atom scope; the reader refuses and the composer + surfaces that honestly rather than silently falling through.""" + surface = deduction_grounded_surface( + "If it rains then the ground is wet. It rains. " + "Therefore the ground is wet." + ) + assert surface is not None + assert "reserved_word_in_np" in surface + + +def test_surface_is_deterministic() -> None: + text = "If p then q. p. Therefore q." + assert deduction_grounded_surface(text) == deduction_grounded_surface(text) + + +# --------------------------------------------------------------------------- +# Live runtime — flag off is byte-identical to pre-arc dispatch +# --------------------------------------------------------------------------- + + +def test_flag_off_preserves_pack_token_gloss_byte_identity() -> None: + rt = ChatRuntime( + config=RuntimeConfig(deduction_serving_enabled=False), no_load_state=True, + ) + resp = rt.chat("If p then q. p. Therefore q.") + assert resp.grounding_source == "pack" + assert "Pack-resident tokens" in resp.surface + + +def test_flag_is_off_by_default() -> None: + assert RuntimeConfig().deduction_serving_enabled is False + + +# --------------------------------------------------------------------------- +# Live runtime — flag on, single turn +# --------------------------------------------------------------------------- + + +def test_runtime_deduction_serves_entailed_answer() -> None: + rt = ChatRuntime( + config=RuntimeConfig(deduction_serving_enabled=True), no_load_state=True, + ) + resp = rt.chat("If p then q. p. Therefore q.") + assert resp.grounding_source == "deduction" + assert "entail: q" in resp.surface + + +def test_runtime_non_argument_prompt_unaffected_by_flag() -> None: + """The flag only intercepts argument-shaped text; ordinary prompts + still route through the pre-existing dispatch.""" + rt = ChatRuntime( + config=RuntimeConfig(deduction_serving_enabled=True), no_load_state=True, + ) + resp = rt.chat("What is light?") + assert resp.grounding_source != "deduction" + + +# --------------------------------------------------------------------------- +# Live runtime — full propositional gold corpus, multi-turn session, wrong=0 +# --------------------------------------------------------------------------- + + +def test_runtime_decides_full_propositional_gold_corpus_wrong_zero() -> None: + """End-to-end regression: every Band v1 gold case, decided through the + real ``core chat`` serving path across one multi-turn session (not + just the isolated comprehend->project->oracle lane). wrong=0 is the + load-bearing assertion; declines are acceptable, a disagreement with + gold is not.""" + rt = ChatRuntime( + config=RuntimeConfig(deduction_serving_enabled=True), no_load_state=True, + ) + cases = _load_cases() + assert cases, "gold corpus must not be empty" + wrong: list[str] = [] + for case in cases: + resp = rt.chat(case["text"]) + assert resp.grounding_source == "deduction", ( + f"expected deduction routing for {case['text']!r}, " + f"got grounding_source={resp.grounding_source!r}" + ) + surface = resp.surface + gold = case["gold"] + if gold == "entailed" and "Your premises entail:" in surface: + continue + if gold == "refuted" and "entail the opposite" in surface: + continue + if gold == "unknown" and "don't settle" in surface: + continue + wrong.append(f"{case['text']!r} -> gold={gold} surface={surface!r}") + assert not wrong, "\n".join(wrong)