feat(deduction-serve): Phase 4 — Band v1b categorical/syllogism serving (ADR-0256)
core chat now decides Aristotelian syllogisms end-to-end -- the marquee
'basic logical work' widening. Closes Phase 0's fork: the ONLY categorical
decider was evals/syllogism/oracle.py (the sealed independence oracle serving
must not import; INV-25). This ships a production decider.
generate/proof_chain/categorical.py lowers a categorical argument to the
propositional regime (one Boolean atom per term-membership profile) and rides
the already-verified ROBDD engine -- no new decision procedure, soundness
inherits from the flagship. Sound AND complete for the modern/Boolean reading
(Darapti + existential-import-only forms correctly INVALID), with no reliance
on a lucky domain size. Independent of the eval oracle by mechanism (ROBDD-
over-profiles vs brute-force finite-model enumeration); proven by case-for-case
agreement with it across the whole syllogism gold lane.
New: generate/proof_chain/categorical.py, render_syllogism (deterministic
valid/invalid/inconsistent templates), CATEGORICAL shape-band, arena
categorical band (4 valid forms + 2 invalid, by-construction gold cross-checked
vs the independent syllogism oracle), tests/test_categorical_decider.py (8
tests incl. the independence-by-agreement proof).
Changed: chat/deduction_surface.py (categorical branch, license-gated via a
shared _license_gate helper; propositional path byte-identical), arena
DeductionSolver dual-path in lock-step with the composer, re-sealed ledger (5
bands, categorical earns SERVE at 0.99087 wrong=0), Phase-2 lane decide()
mirrors the dual path with the 3 categorical cases reclassified to their true
valid/invalid verdicts + 1 invalid case (n 27->28), report+SHA regenerated.
Honest wrinkles: irregular plurals ('fish') decline with unknown_morphology
(a reader limit, correctly not a wrong); surfaces read in singularized terms
('all whale are animal') -- the exact ids the engine reasoned over, no cosmetic
re-pluralization that could drift from the decision.
[Verification]: smoke 180 passed; cognition 122 passed/1 skipped; core test
--suite deductive 45 passed; test_categorical_decider 8 passed; practice
runner 5 bands all SERVE wrong=0; deduction_serve lane SHA regenerates to the
committed pin.
This commit is contained in:
Shay
parent
c98f1e07b2
commit
fdfb71f59b
16 changed files with 576 additions and 81 deletions
|
|
@ -7,6 +7,13 @@
|
|||
"t2_verified": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
"categorical": {
|
||||
"correct": 720,
|
||||
"refused": 0,
|
||||
"t2_agrees_gold": 0,
|
||||
"t2_verified": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
"conditional_chain": {
|
||||
"correct": 720,
|
||||
"refused": 0,
|
||||
|
|
@ -29,7 +36,7 @@
|
|||
"wrong": 0
|
||||
}
|
||||
},
|
||||
"content_sha256": "baf8d985deedc583ca52aa84296c270894598a31481dbff37f15287de339f9e6",
|
||||
"content_sha256": "08c31fbaec5dcf4981a5d23dd5df65da9625dcb23a4017450405e5ba517a1530",
|
||||
"note": "Sealed-practice committed ledger for deduction serving (ADR-0256). Engine reads, never writes. Ceilings stay at safe defaults (theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline reliability (reader+projector+engine) at volume >= 657 committed.",
|
||||
"provenance": "evals.deduction_serve.practice.runner.seal_ledger",
|
||||
"schema": "deduction_serve_ledger_v1"
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
"""chat/deduction_surface.py — Phase 1 DEDUCTION composer (deduction-serve arc).
|
||||
"""chat/deduction_surface.py — DEDUCTION composer (deduction-serve arc).
|
||||
|
||||
Wires the verified propositional-entailment engine (``generate.proof_chain``,
|
||||
716/716 wrong=0 on ``evals/deductive_logic``) into serving. When a prompt
|
||||
|
|
@ -8,18 +8,19 @@ strings, and decide with the sound+complete ROBDD entailment engine.
|
|||
Deterministic templates only (``generate.proof_chain.render``) — no LLM, no
|
||||
synthesis, matching every other composer in this package.
|
||||
|
||||
Band v1 scope (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md):
|
||||
propositional arguments with single-token atoms only. A categorical/syllogism
|
||||
"Therefore" argument is recognized as argument-shaped but declined as
|
||||
out-of-band — a production categorical decider is Band v1b, deferred.
|
||||
``evals.syllogism.oracle`` must never be imported here: it is the sealed
|
||||
independence oracle the comprehension lane scores against, not a serving
|
||||
decider — importing it would collapse INV-25 (independent gold).
|
||||
Bands (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md):
|
||||
- Band v1 — propositional arguments with single-token atoms.
|
||||
- Band v1b (Phase 4) — categorical/syllogism arguments ("All M are P. All S are
|
||||
M. Therefore all S are P."), projected by ``to_syllogism`` and decided by
|
||||
``generate.proof_chain.categorical`` (a propositional-lowering decider that
|
||||
rides the same verified ROBDD engine). ``evals.syllogism.oracle`` must never
|
||||
be imported here: it is the sealed independence oracle the comprehension lane
|
||||
scores against, not a serving decider — importing it would collapse INV-25
|
||||
(independent gold).
|
||||
|
||||
Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every
|
||||
path below returns a committed, honest surface — reader refusal, out-of-band
|
||||
shape, and all four ``EntailmentTrace`` outcomes (ENTAILED/REFUTED/UNKNOWN/
|
||||
REFUSED) — never a silent fall-through to a different composer.
|
||||
Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every path
|
||||
below returns a committed, honest surface — reader refusal, out-of-band shape,
|
||||
and every decision outcome — never a silent fall-through to a different composer.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
|
@ -30,11 +31,12 @@ from typing import Callable
|
|||
|
||||
from chat.deduction_serve_license import deduction_serve_license
|
||||
from core.reliability_gate import LicenseDecision
|
||||
from generate.meaning_graph.projectors import to_deductive_logic
|
||||
from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism
|
||||
from generate.meaning_graph.reader import Comprehension, comprehend
|
||||
from generate.proof_chain.categorical import CategoricalError, decide_syllogism
|
||||
from generate.proof_chain.entail import evaluate_entailment_with_trace
|
||||
from generate.proof_chain.render import render_entailment
|
||||
from generate.proof_chain.shape import classify_deduction_shape
|
||||
from generate.proof_chain.render import render_entailment, render_syllogism
|
||||
from generate.proof_chain.shape import CATEGORICAL, classify_deduction_shape
|
||||
|
||||
#: An argument's conclusion clause starts a sentence with "therefore" — the
|
||||
#: same shape ``generate.meaning_graph.reader`` recognizes per-clause
|
||||
|
|
@ -60,8 +62,8 @@ _READER_REFUSAL_SURFACE = (
|
|||
"decide it yet ({reason})."
|
||||
)
|
||||
_OUT_OF_BAND_SURFACE = (
|
||||
"That reads as an argument, but right now I can only decide plain "
|
||||
"propositional arguments (not categorical 'all/no/some' ones yet)."
|
||||
"That reads as an argument, but its form is outside what I can decide yet "
|
||||
"(I handle plain propositional and categorical 'all/no/some' arguments)."
|
||||
)
|
||||
|
||||
#: Disclosed hedge prepended when a decided argument's shape-band has NOT earned
|
||||
|
|
@ -104,13 +106,33 @@ def deduction_grounded_surface(
|
|||
comp = comprehend(text)
|
||||
if not isinstance(comp, Comprehension):
|
||||
return _READER_REFUSAL_SURFACE.format(reason=comp.reason)
|
||||
# Band v1 — propositional argument.
|
||||
projected = to_deductive_logic(comp)
|
||||
if projected is None:
|
||||
return _OUT_OF_BAND_SURFACE
|
||||
premises, query = projected
|
||||
trace = evaluate_entailment_with_trace(premises, query)
|
||||
surface = render_entailment(trace, premises, query)
|
||||
band = classify_deduction_shape(premises, query)
|
||||
if projected is not None:
|
||||
premises, query = projected
|
||||
trace = evaluate_entailment_with_trace(premises, query)
|
||||
surface = render_entailment(trace, premises, query)
|
||||
return _license_gate(surface, classify_deduction_shape(premises, query), license_lookup)
|
||||
# Band v1b — categorical / syllogism argument. Decided by the propositional-
|
||||
# lowering categorical decider (rides the same verified ROBDD engine); a
|
||||
# malformed categorical shape declines rather than guessing.
|
||||
syllogism = to_syllogism(comp)
|
||||
if syllogism is not None:
|
||||
structure, s_query = syllogism
|
||||
try:
|
||||
trace = decide_syllogism(structure, s_query)
|
||||
except CategoricalError:
|
||||
return _OUT_OF_BAND_SURFACE
|
||||
surface = render_syllogism(trace, structure, s_query)
|
||||
return _license_gate(surface, CATEGORICAL, license_lookup)
|
||||
return _OUT_OF_BAND_SURFACE
|
||||
|
||||
|
||||
def _license_gate(surface: str, band: str, license_lookup: _LicenseLookup) -> str:
|
||||
"""Serve *surface* authoritatively iff *band* holds a SERVE license; else
|
||||
serve the same sound answer DISCLOSED (hedged). The one place the earned-
|
||||
license posture is applied, shared by the propositional and categorical
|
||||
bands (ADR-0256)."""
|
||||
decision = license_lookup(band)
|
||||
if decision is not None and decision.licensed:
|
||||
return surface # earned SERVE — authoritative
|
||||
|
|
|
|||
|
|
@ -176,6 +176,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = {
|
|||
"tests/test_deductive_logic_entail.py",
|
||||
"tests/test_deduction_serve_lane.py",
|
||||
"tests/test_deduction_serve_license.py",
|
||||
"tests/test_categorical_decider.py",
|
||||
),
|
||||
"full": ("tests/",),
|
||||
}
|
||||
|
|
|
|||
|
|
@ -23,7 +23,8 @@ The ROBDD engine is sound **and** complete over the propositional regime — it
|
|||
|
||||
Make deduction serving an earned capability gated by a committed, SHA-sealed reliability ledger.
|
||||
|
||||
- **Shape-band capability axis** (`generate/proof_chain/shape.py::classify_deduction_shape`) — a deterministic, structural classification of a projected `(premises, query)` argument into one of four exhaustive bands: `disjunctive`, `conditional_chain`, `conditional_single`, `atomic`. Computed identically by the practice arena and the serving composer (no drift). Coarse on purpose: each band mixes entailed/refuted/unknown gold, so a band's reliability measures decision correctness across outcomes, not just how many entailments pass through.
|
||||
- **Shape-band capability axis** (`generate/proof_chain/shape.py`) — a deterministic, structural classification of an argument into one of five exhaustive bands: the four propositional bands `disjunctive` / `conditional_chain` / `conditional_single` / `atomic` (assigned by `classify_deduction_shape` over the projected `(premises, query)`), plus `categorical` (Band v1b, Phase 4 — assigned directly to any syllogism projected by `to_syllogism`). Computed identically by the practice arena and the serving composer (no drift). Coarse on purpose: each band mixes entailed/refuted/unknown (or valid/invalid) gold, so a band's reliability measures decision correctness across outcomes, not just how many entailments pass through.
|
||||
- **Band v1b — production categorical decider** (`generate/proof_chain/categorical.py`) — the piece Phase 0's fork identified as missing. Serving cannot import `evals/syllogism/oracle.py` (the sealed independence oracle; INV-25), so this is a fresh production decider that lowers a categorical argument to the propositional regime (one Boolean atom per term-membership *profile*) and rides the already-verified ROBDD engine. Sound AND complete for the modern/Boolean reading; independent of the eval oracle by mechanism (ROBDD over a profile encoding vs. brute-force subset enumeration), verified by case-for-case agreement with it across the syllogism gold lane. Serving projects a syllogism via `to_syllogism` and decides it here (ENTAILED ⇒ valid; UNKNOWN/REFUTED ⇒ invalid; REFUSED ⇒ inconsistent).
|
||||
- **Deduction practice arena** (`evals/deduction_serve/practice/`) — the **second** concrete instance of the ADR-0199 arena (GSM8K math is the first). A deterministic, synthetic, indexed corpus (`gold.py`, no clock/RNG) of propositional arguments per shape-band, each with **by-construction gold** (the generating template's logical form, independent of the reader — ADR-0199 L-2). `DeductionSolver` runs the exact serving pipeline; `ConstructionGoldTether` scores the committed outcome against the by-construction gold; a misread is caught as `wrong`. Sized to the SERVE volume floor (≥657 committed for a perfect record to clear θ_SERVE=0.99; `CASES_PER_BAND=720`).
|
||||
- **Construction-time soundness check** (`gold.py::assert_corpus_sound`) — every generated case's by-construction gold is cross-checked against the **independent truth-table oracle** (`evals.deductive_logic.oracle`, INV-25 — shares no code with the ROBDD engine) before the ledger can seal. A mis-stated template gold can never silently inflate the ledger.
|
||||
- **Sealed, SHA-verified committed ledger** (`chat/data/deduction_serve_ledger.json`, produced by `evals/deduction_serve/practice/runner.py::seal_ledger`) — the per-band `ClassTally`, self-sealed by `content_sha256`. The engine READS it; only the sealed-practice runner WRITES it. Mirrors the estimation ledger topology exactly (`generate/determine/data/estimation_ledger.json`).
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
@ -30,11 +30,13 @@ from dataclasses import dataclass, field
|
|||
from typing import Any
|
||||
|
||||
from core.learning_arena.protocols import Problem
|
||||
from generate.meaning_graph.projectors import to_deductive_logic
|
||||
from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism
|
||||
from generate.meaning_graph.reader import Comprehension, comprehend
|
||||
from generate.proof_chain.categorical import CategoricalError, decide_syllogism
|
||||
from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
|
||||
from generate.proof_chain.shape import (
|
||||
ATOMIC,
|
||||
CATEGORICAL,
|
||||
CONDITIONAL_CHAIN,
|
||||
CONDITIONAL_SINGLE,
|
||||
DISJUNCTIVE,
|
||||
|
|
@ -88,6 +90,25 @@ _TEMPLATES: dict[str, tuple[tuple[str, Any], ...]] = {
|
|||
# (a bare atom either restates or contradicts); the band is 2/3 the size
|
||||
# of the others, still well above the volume floor.
|
||||
),
|
||||
# Categorical (syllogism). Terms are synthetic PLURAL class nouns (``x3s`` →
|
||||
# the reader singularizes to ``x3``); ``a, b, c`` are the three distinct
|
||||
# middle/subject/predicate classes. Gold is the unconditional validity (modern
|
||||
# reading) of the standard form — cross-checked against the INDEPENDENT
|
||||
# syllogism oracle in ``assert_corpus_sound``.
|
||||
CATEGORICAL: (
|
||||
# Barbara (AAA) — valid.
|
||||
("valid", lambda a, b, c: f"All {a}s are {b}s. All {c}s are {a}s. Therefore all {c}s are {b}s."),
|
||||
# Celarent (EAE) — valid.
|
||||
("valid", lambda a, b, c: f"No {a}s are {b}s. All {c}s are {a}s. Therefore no {c}s are {b}s."),
|
||||
# Darii (AII) — valid.
|
||||
("valid", lambda a, b, c: f"All {a}s are {b}s. Some {c}s are {a}s. Therefore some {c}s are {b}s."),
|
||||
# Ferio (EIO) — valid.
|
||||
("valid", lambda a, b, c: f"No {a}s are {b}s. Some {c}s are {a}s. Therefore some {c}s are not {b}s."),
|
||||
# Undistributed middle (AAA-2) — INVALID.
|
||||
("invalid", lambda a, b, c: f"All {b}s are {a}s. All {c}s are {a}s. Therefore all {c}s are {b}s."),
|
||||
# Existential-import overreach — INVALID in the modern reading.
|
||||
("invalid", lambda a, b, c: f"All {a}s are {b}s. All {a}s are {c}s. Therefore some {c}s are {b}s."),
|
||||
),
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -117,7 +138,7 @@ def generate_problems(band: str, n: int) -> list[Problem]:
|
|||
def all_gold_problems() -> list[Problem]:
|
||||
"""The full deterministic corpus over every shape-band, in band order."""
|
||||
problems: list[Problem] = []
|
||||
for band in (CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC):
|
||||
for band in (CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC, CATEGORICAL):
|
||||
problems.extend(generate_problems(band, CASES_PER_BAND))
|
||||
return problems
|
||||
|
||||
|
|
@ -143,15 +164,26 @@ _OUTCOME_TO_CLASS = {
|
|||
Entailment.REFUSED: "declined",
|
||||
}
|
||||
|
||||
#: Categorical outcome mapping: a syllogism is VALID iff the conclusion is
|
||||
#: entailed; UNKNOWN/REFUTED ⇒ invalid; REFUSED ⇒ declined (inconsistent).
|
||||
_CATEGORICAL_TO_CLASS = {
|
||||
Entailment.ENTAILED: "valid",
|
||||
Entailment.REFUTED: "invalid",
|
||||
Entailment.UNKNOWN: "invalid",
|
||||
Entailment.REFUSED: "declined",
|
||||
}
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class DeductionSolver:
|
||||
"""The production serving pipeline as a ``DomainSolver``.
|
||||
|
||||
Runs exactly what ``chat/deduction_surface.py`` runs — ``comprehend`` →
|
||||
``to_deductive_logic`` → ``evaluate_entailment_with_trace`` — and commits
|
||||
the decided outcome class. A reader refusal / non-projectable comprehension
|
||||
is an uncommitted attempt (``refused``), never a guessed answer.
|
||||
Runs exactly what ``chat/deduction_surface.py`` runs — the propositional
|
||||
path (``to_deductive_logic`` → ``evaluate_entailment_with_trace``) then the
|
||||
categorical path (``to_syllogism`` → ``decide_syllogism``) — and commits the
|
||||
decided outcome class. A reader refusal / non-projectable comprehension /
|
||||
engine REFUSED is an uncommitted attempt, never a guessed answer. Kept in
|
||||
lock-step with the composer's dual path; the lane + license tests cover both.
|
||||
"""
|
||||
|
||||
domain_id: str = _DOMAIN_ID
|
||||
|
|
@ -164,21 +196,35 @@ class DeductionSolver:
|
|||
committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}",
|
||||
case_id=problem.problem_id, shape=problem.class_name,
|
||||
)
|
||||
# Band v1 — propositional.
|
||||
projected = to_deductive_logic(comp)
|
||||
if projected is None:
|
||||
if projected is not None:
|
||||
premises, query = projected
|
||||
outcome = evaluate_entailment_with_trace(premises, query).outcome
|
||||
return _DeductionAttempt(
|
||||
committed=False, answer=None, reason="unprojectable",
|
||||
case_id=problem.problem_id, shape=problem.class_name,
|
||||
committed=outcome is not Entailment.REFUSED,
|
||||
answer=_OUTCOME_TO_CLASS[outcome], reason="",
|
||||
case_id=problem.problem_id, shape=classify_deduction_shape(premises, query),
|
||||
)
|
||||
# Band v1b — categorical / syllogism.
|
||||
syllogism = to_syllogism(comp)
|
||||
if syllogism is not None:
|
||||
structure, s_query = syllogism
|
||||
try:
|
||||
outcome = decide_syllogism(structure, s_query).outcome
|
||||
except CategoricalError:
|
||||
return _DeductionAttempt(
|
||||
committed=False, answer=None, reason="categorical_malformed",
|
||||
case_id=problem.problem_id, shape=CATEGORICAL,
|
||||
)
|
||||
return _DeductionAttempt(
|
||||
committed=outcome is not Entailment.REFUSED,
|
||||
answer=_CATEGORICAL_TO_CLASS[outcome], reason="",
|
||||
case_id=problem.problem_id, shape=CATEGORICAL,
|
||||
)
|
||||
premises, query = projected
|
||||
outcome = evaluate_entailment_with_trace(premises, query).outcome
|
||||
answer = _OUTCOME_TO_CLASS[outcome]
|
||||
# An engine REFUSED (inconsistent premises / out-of-regime) is an honest
|
||||
# non-commitment, not a served verdict.
|
||||
committed = outcome is not Entailment.REFUSED
|
||||
return _DeductionAttempt(
|
||||
committed=committed, answer=answer, reason="",
|
||||
case_id=problem.problem_id, shape=classify_deduction_shape(premises, query),
|
||||
committed=False, answer=None, reason="unprojectable",
|
||||
case_id=problem.problem_id, shape=problem.class_name,
|
||||
)
|
||||
|
||||
|
||||
|
|
@ -202,24 +248,37 @@ class ConstructionGoldTether:
|
|||
|
||||
def assert_corpus_sound() -> None:
|
||||
"""Belt-and-suspenders: every generated case's by-construction gold must
|
||||
agree with the INDEPENDENT truth-table oracle over its projected form.
|
||||
agree with an INDEPENDENT oracle over its projected form.
|
||||
|
||||
Guards against a template authoring bug (a mis-stated gold) silently
|
||||
inflating the ledger. Raises ``AssertionError`` on any disagreement. Uses
|
||||
the oracle (``evals.deductive_logic.oracle``), which shares no code with the
|
||||
ROBDD serving engine (INV-25), as the construction-time check.
|
||||
oracles that share no code with the ROBDD serving engine (INV-25): the
|
||||
truth-table ``evals.deductive_logic.oracle`` for propositional bands, and
|
||||
the finite-model ``evals.syllogism.oracle`` for the categorical band.
|
||||
"""
|
||||
from evals.deductive_logic.oracle import oracle_entailment
|
||||
from evals.syllogism.oracle import oracle_answer
|
||||
|
||||
for problem in all_gold_problems():
|
||||
comp = comprehend(problem.payload["text"])
|
||||
assert isinstance(comp, Comprehension), problem.payload["text"]
|
||||
gold = problem.payload["gold"]
|
||||
projected = to_deductive_logic(comp)
|
||||
assert projected is not None, problem.payload["text"]
|
||||
premises, query = projected
|
||||
oracle = oracle_entailment(premises, query)
|
||||
assert oracle == problem.payload["gold"], (
|
||||
f"{problem.problem_id}: oracle={oracle} gold={problem.payload['gold']} "
|
||||
if projected is not None:
|
||||
premises, query = projected
|
||||
oracle = oracle_entailment(premises, query)
|
||||
assert oracle == gold, (
|
||||
f"{problem.problem_id}: oracle={oracle} gold={gold} "
|
||||
f"text={problem.payload['text']!r}"
|
||||
)
|
||||
continue
|
||||
syllogism = to_syllogism(comp)
|
||||
assert syllogism is not None, problem.payload["text"]
|
||||
structure, s_query = syllogism
|
||||
oracle_valid = oracle_answer(structure, s_query)["valid"]
|
||||
oracle_class = "valid" if oracle_valid else "invalid"
|
||||
assert oracle_class == gold, (
|
||||
f"{problem.problem_id}: syllogism_oracle={oracle_class} gold={gold} "
|
||||
f"text={problem.payload['text']!r}"
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
{
|
||||
"aggregate": {
|
||||
"correct": 27,
|
||||
"correct": 28,
|
||||
"declined": 0,
|
||||
"n": 27,
|
||||
"n": 28,
|
||||
"wrong": 0
|
||||
},
|
||||
"all_correct": true,
|
||||
|
|
@ -13,23 +13,27 @@
|
|||
"v1": {
|
||||
"all_cases_correct": true,
|
||||
"by_gold": {
|
||||
"declined": 9,
|
||||
"declined": 6,
|
||||
"entailed": 8,
|
||||
"invalid": 1,
|
||||
"refuted": 5,
|
||||
"unknown": 5
|
||||
"unknown": 5,
|
||||
"valid": 3
|
||||
},
|
||||
"correct_by_gold": {
|
||||
"declined": 9,
|
||||
"declined": 6,
|
||||
"entailed": 8,
|
||||
"invalid": 1,
|
||||
"refuted": 5,
|
||||
"unknown": 5
|
||||
"unknown": 5,
|
||||
"valid": 3
|
||||
},
|
||||
"counts": {
|
||||
"correct": 27,
|
||||
"correct": 28,
|
||||
"declined": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
"n": 27
|
||||
"n": 28
|
||||
}
|
||||
},
|
||||
"wrong_is_zero": true
|
||||
|
|
|
|||
|
|
@ -42,8 +42,9 @@ from collections import Counter
|
|||
from pathlib import Path
|
||||
|
||||
from chat.deduction_surface import looks_like_deductive_argument
|
||||
from generate.meaning_graph.projectors import to_deductive_logic
|
||||
from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism
|
||||
from generate.meaning_graph.reader import Comprehension, comprehend
|
||||
from generate.proof_chain.categorical import CategoricalError, decide_syllogism
|
||||
from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
|
||||
|
||||
_ROOT = Path(__file__).resolve().parent
|
||||
|
|
@ -59,6 +60,14 @@ _OUTCOME_TO_CLASS = {
|
|||
Entailment.REFUSED: "declined",
|
||||
}
|
||||
|
||||
#: Categorical outcome → verdict class (matches the composer / arena mapping).
|
||||
_CATEGORICAL_TO_CLASS = {
|
||||
Entailment.ENTAILED: "valid",
|
||||
Entailment.REFUTED: "invalid",
|
||||
Entailment.UNKNOWN: "invalid",
|
||||
Entailment.REFUSED: "declined",
|
||||
}
|
||||
|
||||
|
||||
def _load(path: Path) -> list[dict]:
|
||||
with path.open(encoding="utf-8") as fh:
|
||||
|
|
@ -66,13 +75,14 @@ def _load(path: Path) -> list[dict]:
|
|||
|
||||
|
||||
def decide(text: str) -> str:
|
||||
"""Run the exact pipeline ``chat/deduction_surface.py`` runs in
|
||||
serving and return the outcome class: entailed/refuted/unknown/declined.
|
||||
"""Run the exact decision pipeline ``chat/deduction_surface.py`` runs in
|
||||
serving and return the outcome class: entailed/refuted/unknown (propositional),
|
||||
valid/invalid (categorical), or declined.
|
||||
|
||||
Mirrors ``deduction_grounded_surface`` call-for-call up to (but not
|
||||
including) the prose render — the same production decision, typed
|
||||
instead of rendered, so this lane's assertions are robust to wording
|
||||
changes.
|
||||
including) the prose render and the license gate — the same production
|
||||
decision, typed instead of rendered, so this lane's assertions are robust
|
||||
to wording changes.
|
||||
"""
|
||||
if not looks_like_deductive_argument(text):
|
||||
return "declined"
|
||||
|
|
@ -80,11 +90,17 @@ def decide(text: str) -> str:
|
|||
if not isinstance(comp, Comprehension):
|
||||
return "declined"
|
||||
projected = to_deductive_logic(comp)
|
||||
if projected is None:
|
||||
return "declined"
|
||||
premises, query = projected
|
||||
trace = evaluate_entailment_with_trace(premises, query)
|
||||
return _OUTCOME_TO_CLASS[trace.outcome]
|
||||
if projected is not None:
|
||||
premises, query = projected
|
||||
return _OUTCOME_TO_CLASS[evaluate_entailment_with_trace(premises, query).outcome]
|
||||
syllogism = to_syllogism(comp)
|
||||
if syllogism is not None:
|
||||
structure, s_query = syllogism
|
||||
try:
|
||||
return _CATEGORICAL_TO_CLASS[decide_syllogism(structure, s_query).outcome]
|
||||
except CategoricalError:
|
||||
return "declined"
|
||||
return "declined"
|
||||
|
||||
|
||||
def build_report(cases: list[dict]) -> dict:
|
||||
|
|
|
|||
|
|
@ -20,8 +20,9 @@
|
|||
{"id": "ds-v1-0020", "text": "If p then q. p. Not q. Therefore r.", "gold": "declined", "class": "inconsistent_premises"}
|
||||
{"id": "ds-v1-0021", "text": "p. Not p. Therefore p.", "gold": "declined", "class": "inconsistent_premises"}
|
||||
{"id": "ds-v1-0022", "text": "p or q. Not p. Not q. Therefore p.", "gold": "declined", "class": "inconsistent_premises"}
|
||||
{"id": "ds-v1-0023", "text": "All mammals are animals. All whales are mammals. Therefore all whales are animals.", "gold": "declined", "class": "out_of_band_categorical"}
|
||||
{"id": "ds-v1-0024", "text": "No reptiles are mammals. All snakes are reptiles. Therefore no snakes are mammals.", "gold": "declined", "class": "out_of_band_categorical"}
|
||||
{"id": "ds-v1-0023", "text": "All mammals are animals. All whales are mammals. Therefore all whales are animals.", "gold": "valid", "class": "categorical_barbara"}
|
||||
{"id": "ds-v1-0024", "text": "No reptiles are mammals. All snakes are reptiles. Therefore no snakes are mammals.", "gold": "valid", "class": "categorical_celarent"}
|
||||
{"id": "ds-v1-0025", "text": "If it rains then the ground is wet. It rains. Therefore the ground is wet.", "gold": "declined", "class": "out_of_band_multiword_conditional"}
|
||||
{"id": "ds-v1-0026", "text": "Some students are poets. All poets are artists. Therefore some students are artists.", "gold": "declined", "class": "out_of_band_categorical"}
|
||||
{"id": "ds-v1-0026", "text": "Some students are poets. All poets are artists. Therefore some students are artists.", "gold": "valid", "class": "categorical_datisi"}
|
||||
{"id": "ds-v1-0028", "text": "All cats are animals. All dogs are animals. Therefore all dogs are cats.", "gold": "invalid", "class": "categorical_undistributed_middle"}
|
||||
{"id": "ds-v1-0027", "text": "If p then q. If q then r. If r then s. p. Therefore s.", "gold": "entailed", "class": "three_hop_chain"}
|
||||
|
|
|
|||
167
generate/proof_chain/categorical.py
Normal file
167
generate/proof_chain/categorical.py
Normal file
|
|
@ -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_<bits>``
|
||||
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",
|
||||
]
|
||||
|
|
@ -17,6 +17,14 @@ from generate.proof_chain.entail import (
|
|||
EntailmentTrace,
|
||||
)
|
||||
|
||||
#: A/E/I/O categorical form → an English sentence template over (subject, predicate).
|
||||
_CATEGORICAL_PHRASE = {
|
||||
"A": "all {s} are {p}",
|
||||
"E": "no {s} are {p}",
|
||||
"I": "some {s} are {p}",
|
||||
"O": "some {s} are not {p}",
|
||||
}
|
||||
|
||||
|
||||
def render_entailment(
|
||||
trace: EntailmentTrace, premises: tuple[str, ...], query: str
|
||||
|
|
@ -51,4 +59,37 @@ def render_entailment(
|
|||
return f"Given: {given}. I can't evaluate {query} from that as stated."
|
||||
|
||||
|
||||
__all__ = ["render_entailment"]
|
||||
def _categorical_clause(prop: dict) -> str:
|
||||
"""One categorical proposition dict → its English clause."""
|
||||
template = _CATEGORICAL_PHRASE.get(prop.get("form", ""), "{s} ~ {p}")
|
||||
return template.format(s=prop.get("subject", "?"), p=prop.get("predicate", "?"))
|
||||
|
||||
|
||||
def render_syllogism(trace: EntailmentTrace, structure: dict, query: dict) -> str:
|
||||
"""The user-facing surface for a categorical (syllogism) verdict.
|
||||
|
||||
Deterministic templates over the argument's own clauses — no synthesis. The
|
||||
``EntailmentTrace`` is the propositional-lowering decision (``ENTAILED`` ⇒
|
||||
valid; ``UNKNOWN``/``REFUTED`` ⇒ invalid; ``REFUSED`` ⇒ inconsistent).
|
||||
"""
|
||||
premises = "; ".join(
|
||||
_categorical_clause(p) for p in structure.get("premises", [])
|
||||
)
|
||||
conclusion = _categorical_clause(query.get("conclusion", {}))
|
||||
if trace.outcome is Entailment.ENTAILED:
|
||||
return f"Given: {premises}. That's valid — {conclusion} follows."
|
||||
if trace.outcome is Entailment.REFUSED and trace.reason == INCONSISTENT_PREMISES:
|
||||
return (
|
||||
f"Given: {premises}. Those premises are inconsistent — they can't all "
|
||||
f"be true, so I won't assert anything from them."
|
||||
)
|
||||
if trace.outcome is Entailment.REFUSED:
|
||||
return f"Given: {premises}. I can't evaluate {conclusion} from that as stated."
|
||||
# UNKNOWN or REFUTED — the conclusion is not forced by the premises.
|
||||
return (
|
||||
f"Given: {premises}. That doesn't follow — {conclusion} isn't guaranteed "
|
||||
f"by those premises."
|
||||
)
|
||||
|
||||
|
||||
__all__ = ["render_entailment", "render_syllogism"]
|
||||
|
|
|
|||
|
|
@ -27,12 +27,20 @@ DISJUNCTIVE = "disjunctive"
|
|||
CONDITIONAL_CHAIN = "conditional_chain"
|
||||
CONDITIONAL_SINGLE = "conditional_single"
|
||||
ATOMIC = "atomic"
|
||||
#: Band v1b (Phase 4) — categorical/syllogism arguments. Distinct from the four
|
||||
#: propositional bands: a categorical argument is projected by ``to_syllogism``
|
||||
#: (not ``to_deductive_logic``) and decided by ``generate.proof_chain.categorical``
|
||||
#: (the propositional-lowering decider), so the serving composer assigns this band
|
||||
#: directly rather than by ``classify_deduction_shape`` (which reads propositional
|
||||
#: formula strings).
|
||||
CATEGORICAL = "categorical"
|
||||
|
||||
SHAPE_BANDS: tuple[str, ...] = (
|
||||
DISJUNCTIVE,
|
||||
CONDITIONAL_CHAIN,
|
||||
CONDITIONAL_SINGLE,
|
||||
ATOMIC,
|
||||
CATEGORICAL,
|
||||
)
|
||||
|
||||
|
||||
|
|
@ -62,6 +70,7 @@ def classify_deduction_shape(premises: tuple[str, ...], query: str) -> str:
|
|||
|
||||
__all__ = [
|
||||
"ATOMIC",
|
||||
"CATEGORICAL",
|
||||
"CONDITIONAL_CHAIN",
|
||||
"CONDITIONAL_SINGLE",
|
||||
"DISJUNCTIVE",
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@ PINNED_SHAS: dict[str, str] = {
|
|||
"public_demo": "7d8ba0dbae9287cfe0bf15d231fa78a75abc627121c14900439293e01e1cc1d3",
|
||||
"math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4",
|
||||
"deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f",
|
||||
"deduction_serve_v1": "8fd86265b075be060b72f0d7b3677737de38268ee57b9bcfac30a7f6296d55eb",
|
||||
"deduction_serve_v1": "b23234b4b57d92e3df9daa3b5d4bbf7fdc505355e32c1440af321c2e1f86bdd2",
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
90
tests/test_categorical_decider.py
Normal file
90
tests/test_categorical_decider.py
Normal file
|
|
@ -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)
|
||||
|
|
@ -16,15 +16,18 @@ _V1 = _ROOT / "v1" / "cases.jsonl"
|
|||
|
||||
def test_v1_lane_wrong_is_zero() -> None:
|
||||
report = build_report(_load(_V1))
|
||||
assert report["n"] == 27
|
||||
assert report["n"] == 28
|
||||
assert report["counts"]["wrong"] == 0
|
||||
assert report["all_cases_correct"] is True
|
||||
# the sizeable, honest signal: non-trivial committed classes covered
|
||||
# the sizeable, honest signal: non-trivial committed classes covered,
|
||||
# including the categorical band (valid + invalid) added in Phase 4.
|
||||
cbg = report["correct_by_gold"]
|
||||
assert cbg.get("entailed", 0) >= 5
|
||||
assert cbg.get("refuted", 0) >= 5
|
||||
assert cbg.get("unknown", 0) >= 5
|
||||
assert cbg.get("declined", 0) >= 5
|
||||
assert cbg.get("valid", 0) >= 3
|
||||
assert cbg.get("invalid", 0) >= 1
|
||||
|
||||
|
||||
def test_runner_treats_wrong_verdict_as_the_only_real_failure() -> None:
|
||||
|
|
|
|||
|
|
@ -85,16 +85,27 @@ def test_inconsistent_premises_renders_typed_decline() -> None:
|
|||
assert "inconsistent" in surface
|
||||
|
||||
|
||||
def test_categorical_argument_declines_out_of_band() -> None:
|
||||
"""A syllogism-shaped "therefore" argument commits (argument-shaped)
|
||||
but is honestly declined — Band v1 is propositional-only; the
|
||||
production categorical decider is deferred (Band v1b)."""
|
||||
def test_categorical_argument_is_decided_band_v1b() -> None:
|
||||
"""A valid categorical syllogism is now DECIDED (Band v1b, Phase 4) — the
|
||||
production categorical decider serves a validity verdict, no longer a
|
||||
decline."""
|
||||
surface = deduction_grounded_surface(
|
||||
"All mammals are animals. All whales are mammals. "
|
||||
"Therefore all whales are animals."
|
||||
)
|
||||
assert surface is not None
|
||||
assert "categorical" in surface
|
||||
assert "valid" in surface
|
||||
assert "follows" in surface
|
||||
|
||||
|
||||
def test_invalid_categorical_argument_is_rejected() -> None:
|
||||
"""An invalid syllogism (undistributed middle) is decided INVALID, not
|
||||
declined and not falsely served as valid (wrong=0 on the categorical band)."""
|
||||
surface = deduction_grounded_surface(
|
||||
"All cats are animals. All dogs are animals. Therefore all dogs are cats."
|
||||
)
|
||||
assert surface is not None
|
||||
assert "doesn't follow" in surface
|
||||
|
||||
|
||||
def test_multiword_conditional_declines_reader_refusal() -> None:
|
||||
|
|
|
|||
Loading…
Reference in a new issue