diff --git a/chat/data/deduction_serve_ledger.json b/chat/data/deduction_serve_ledger.json index 2d0eb3c7..a946cb12 100644 --- a/chat/data/deduction_serve_ledger.json +++ b/chat/data/deduction_serve_ledger.json @@ -56,6 +56,34 @@ "t2_verified": 0, "wrong": 0 }, + "en_condmem_chain": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_condmem_conditional": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_condmem_disjunctive": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_condmem_fused": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, "en_disjunctive": { "correct": 720, "refused": 0, @@ -92,7 +120,7 @@ "wrong": 0 } }, - "content_sha256": "3fa864444de56e9e316e8509d3b84648215af73e86540b10199d51182cb7d5ca", + "content_sha256": "6285a423957bc9a3a6a562515a338dfd6f36188ac00f45c1a6ea979c4e3cc710", "note": "Sealed-practice committed ledger for deduction serving (ADR-0256). Engine reads, never writes. Ceilings stay at safe defaults (theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline reliability (reader+projector+engine) at volume >= 657 committed.", "provenance": "evals.deduction_serve.practice.runner.seal_ledger", "schema": "deduction_serve_ledger_v1" diff --git a/chat/deduction_surface.py b/chat/deduction_surface.py index 02e8fb5d..f23c0df2 100644 --- a/chat/deduction_surface.py +++ b/chat/deduction_surface.py @@ -27,6 +27,13 @@ Bands (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md): mortal."), read by ``generate.proof_chain.member`` via per-individual propositional lowering and decided by the same engine. Tried strictly AFTER v2-EN (which guards these shapes out) — again a pure widening tier. +- Band v4-CM (ADR-0259) — conditional-membership fusion arguments ("If + Socrates is a man then Socrates is mortal. Socrates is a man. Therefore + Socrates is mortal."), composing v2-EN's connective grammar with v3-MEM's + singular-membership sentence reading over one shared per-individual atom + space, read by ``generate.proof_chain.cond_member``. Tried strictly AFTER + v3-MEM (which guards these shapes out via ``mixed_structure_out_of_band``) + — again a pure widening tier. Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every path below returns a committed, honest surface — reader refusal, out-of-band shape, @@ -44,6 +51,7 @@ 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.cond_member import CondMemberArgument, read_cond_member_argument from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import evaluate_entailment_with_trace from generate.proof_chain.member import MemberArgument, read_member_argument @@ -132,6 +140,9 @@ def deduction_grounded_surface( member = _member_band_surface(text, license_lookup) if member is not None: return member + cond_member = _cond_member_band_surface(text, license_lookup) + if cond_member is not None: + return cond_member return _READER_REFUSAL_SURFACE.format(reason=comp.reason) # Band v1 — propositional argument. projected = to_deductive_logic(comp) @@ -160,6 +171,10 @@ def deduction_grounded_surface( member = _member_band_surface(text, license_lookup) if member is not None: return member + # Band v4-CM fallback — the conditional-membership shapes v3-MEM guards out. + cond_member = _cond_member_band_surface(text, license_lookup) + if cond_member is not None: + return cond_member return _OUT_OF_BAND_SURFACE @@ -189,6 +204,22 @@ def _member_band_surface(text: str, license_lookup: _LicenseLookup) -> str | Non return _license_gate(surface, arg.band, license_lookup) +def _cond_member_band_surface(text: str, license_lookup: _LicenseLookup) -> str | None: + """Band v4-CM (ADR-0259): read *text* as a conditional-membership argument + (v2-EN connectives over v3-MEM singular-membership leaves), and decide + with the same verified ROBDD engine; ``None`` when the reader refuses (the + caller keeps its pre-existing honest surface — this band only ever widens + what is decided). Reuses ``render_entailment_member`` unchanged: its + UNKNOWN scoping is exactly as accurate here (every clause is read all the + way to individual+class; connectives add no new hidden structure).""" + arg = read_cond_member_argument(text) + if not isinstance(arg, CondMemberArgument): + return None + trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula) + surface = render_entailment_member(trace, arg.premise_texts, arg.query_text) + return _license_gate(surface, arg.band, license_lookup) + + 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- diff --git a/core/cli_test.py b/core/cli_test.py index a82d7305..d094bea5 100644 --- a/core/cli_test.py +++ b/core/cli_test.py @@ -179,6 +179,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = { "tests/test_categorical_decider.py", "tests/test_english_argument_reader.py", "tests/test_member_argument_reader.py", + "tests/test_cond_member_argument_reader.py", "tests/test_deduction_serve_e2e.py", ), "full": ("tests/",), diff --git a/docs/adr/ADR-0259-conditional-membership-fusion-band.md b/docs/adr/ADR-0259-conditional-membership-fusion-band.md new file mode 100644 index 00000000..fffee6b9 --- /dev/null +++ b/docs/adr/ADR-0259-conditional-membership-fusion-band.md @@ -0,0 +1,163 @@ +# ADR-0259 — Conditional-membership fusion band (Band v4-CM) + +- **Status:** Proposed +- **Date:** 2026-07-23 +- **Relates to:** ADR-0258 (Band v3-MEM — this is its scope-out #1), ADR-0257 + (Band v2-EN — the connective grammar this band reuses), ADR-0256 (earned + license), ADR-0201 (ROBDD keystone), ADR-0175/0199 (calibrated learning / + arena) + +## 1. Context + +ADR-0258 §6.1 reserved conditional–membership fusion as a future band: + +> "If Socrates is a man then Socrates is mortal. Socrates is a man. +> Therefore Socrates is mortal." + +Band v3-MEM refuses this — `mixed_structure_out_of_band` — because its +per-sentence grammar treats a connective token (`if`/`then`/`or`/`and`/ +`either`) anywhere in a sentence as announcing structure that band does not +compose. Band v2-EN refuses the same text for the complementary reason: +its opaque-atom minter explicitly rejects `is [a|an]` clauses +(`membership_shape_out_of_band`) rather than flattening membership +structure it cannot read. Each band is individually sound and, by design, +refuses exactly what the other reads — the gap is the composition, not +either reader's engine. + +## 2. Decision + +Add `generate/proof_chain/cond_member.py` — a third reader, tried strictly +AFTER Bands v1 / v1b / v2-EN / v3-MEM (a fallback tier; every previously +served argument stays byte-identical) — that composes v2-EN's connective +grammar (`if/then`, `or`, `and`, `either` sugar, top-level `and`-splitting) +with v3-MEM's singular membership sentence reading, over the SAME +per-individual atom space: + +- **Sentence dispatch** (closed, ordered): a bare top-level `X and Y` + premise (no `if`/`or` anywhere) splits into independent singular + records, exactly as v2-EN does — semantically conjoining, keeping the + connective inventory the shape-bands classify over uncluttered. Any + OTHER sentence containing a connective token is parsed by the ported + junction/conditional grammar below. A universal-lead (`all|every|each| + no`) sentence with NO connective token is a bare universal, read + UNCHANGED by v3-MEM's own `_parse_universal`. Everything else is a bare + singular fact, read UNCHANGED by v3-MEM's own `_parse_singular` (which + already normalizes every negation form this band needs — leading `not`, + the sentential `it is not the case that` prefix, and copular `is not`). + Checking for a connective token BEFORE the universal-lead dispatch (not + after) is load-bearing: it is what stops a connective token from ever + silently leaking into an opaque name/class run. +- **Connective grammar over membership leaves:** `if then ` and + ` or ` / ` and ` (with `either` as sugar, mixed `and`+`or` at + one level refused as `ambiguous_and_or`, a conditional nested inside + another refused as `nested_conditional` — identical restrictions to + v2-EN, ported verbatim) build a small formula tree (`_Lit` / `_And` / + `_Or` / `_Implies`) whose LEAVES are v3-MEM singular facts, not opaque + atoms. Because `_parse_singular` is negation-aware on its own, this + band's grammar needs no separate negation layer — v2-EN needs one only + because ITS leaf-miller (`_AtomTable.mint`) is negation-blind. +- **A conclusion stays a single singular fact** (optionally negated), + matching v3-MEM's existing discipline exactly: a universal or + connective-shaped conclusion refuses + (`universal_conclusion_out_of_band` / new `compound_conclusion_out_of_band`) + rather than attempting a compound render. +- **One shared per-individual atom space:** every singular fact — whether + a bare sentence, an and-split part, or a leaf nested inside a connective + tree — contributes to the SAME two-pass lowering v3-MEM already performs + (collect named individuals and closed-morphology class-groups first, + THEN mint one opaque atom per attested `(individual, class)` pair, THEN + instantiate every bare universal at every named individual). A bare + universal may now instantiate at an individual named ONLY inside a + connective's leaf, and a connective's leaf atom may now UNIFY with an + atom a bare universal's instantiation also produced — this atom-sharing + across the two mechanisms is the fusion the band is named for, and nothing + about it is a new soundness claim: it is the same per-individual + instantiation ADR-0258 §3 already proved sound, applied to a strictly + larger set of premise formulas. +- **Four new shape-bands**, priority order first-match: `en_condmem_fused` + (a bare universal coexists with a connective sentence — the mechanism + above genuinely fires), `en_condmem_disjunctive` (an `or` appears + anywhere in any connective sentence), `en_condmem_chain` (two or more + connective sentences, no universal, no `or`), `en_condmem_conditional` + (the base case — exactly one `if/then`, no universal, no `or`). A + successfully-decided argument in this band always contains at least one + connective sentence — every other reason v3-MEM would refuse also makes + THIS reader refuse identically (it reuses v3-MEM's own + `_parse_universal`/`_parse_singular`, guards included), so there is no + connective-free case this band could newly decide; no fifth "atomic" + band is needed. + +## 3. Why the composition is sound (the load-bearing argument) + +1. **Nothing here is a new inference rule.** Every connective (`&`, `|`, + `->`) is standard propositional structure the ROBDD engine already + decides; every leaf is a v3-MEM singular-membership atom, minted and + linked by the IDENTICAL closed morphology relation ADR-0258 §3 already + proved sound and (for this fragment) complete. Composing them is + substitution of one sound reading's atoms into another sound reading's + connective positions — the propositional engine's soundness does not + care which reader supplied which formula string. +2. **Universal instantiation stays sound when the instantiated individual + is named only inside a connective.** ADR-0258 §3's argument — every + first-order model of `∀x(C1(x)→C2(x))` satisfies the instantiation at + every domain element, so at every NAMED individual in particular — does + not depend on WHERE in the argument that individual's name appears. An + individual introduced solely as the subject of an `if`-clause leaf is + still a named individual; instantiating a bare universal at it is still + a sound consequence of the universal, exactly as if it had appeared in + its own bare sentence. +3. **Completeness is preserved for the same closed fragment.** The + fragment is unchanged from ADR-0258 (singular literals + A/E + universals, Boolean reading, no existential import) with one syntactic + widening: singular literals may now be combined by `&`/`|`/`->` before + appearing as a premise or antecedent/consequent. A propositional + countermodel still lifts to a first-order countermodel over exactly + the named individuals, by the identical argument — connectives among + already-Boolean atoms do not change what "every element is a named + individual" needs to guarantee. UNKNOWN therefore still means genuinely + not forced within the disclosed reading, and the surface still scopes + itself exactly as v3-MEM's does (reused verbatim — see §4). +4. **The refusal vocabulary stays a strict superset of v3-MEM's, plus + v2-EN's connective-shape guards.** `nested_conditional` and + `ambiguous_and_or` are v2-EN's own restrictions, ported unchanged + (English `and`/`or` scope genuinely is ambiguous when mixed; a + conditional nested inside another is refused rather than guessed at, + in both bands identically). `compound_conclusion_out_of_band` is new + and narrow: it exists only to keep the conclusion a single renderable + fact, not to hide any inference. + +## 4. What the earned licenses certify; rendering + +Same posture as ADR-0258 §4: the license certifies reader fidelity, not +engine soundness. `render_entailment_member` (ADR-0258) is reused +UNCHANGED for this band's surface — its UNKNOWN scoping ("reading each +name as one individual and each class word at face value…") is exactly as +accurate here, since every clause in this band's arguments is read all the +way down to individual+class; connectives introduce no additional hidden +structure the surface would need to disclose. No new render function is +added. + +## 5. Scope-outs (deliberate) + +1. **A universal clause cannot be nested inside a connective** — only a + bare top-level universal sentence instantiates; `if all men are + mortal then …` refuses (typed, via the same connective-shape-first + dispatch that protects bare universals from silent corruption). + Composing a QUANTIFIED antecedent/consequent is a larger, separate + question (it would need bound-variable tracking across clauses, not + just shared individuals) and is left for a future band if a real case + ever needs it. +2. **Existential premises, tense, verb predicates, identity/definite + descriptions** — unchanged scope-outs, inherited from ADR-0258 §6 + via the reused `_parse_singular`/`_parse_universal`. +3. **Flag posture unchanged:** rides `deduction_serving_enabled` (default + off); no new flag. + +## 6. Verification + +- `uv run core test --suite deductive -q` — reader contract, surfaces, + license, all four lane splits, e2e through `ChatRuntime`. +- Practice arena: 17 bands × 720 = 12,240 cases, wrong=0 required for every + band; ledger re-sealed (`chat/data/deduction_serve_ledger.json`). +- Eval lane: v1 28/28, v2_en 26/26, v2_member 26/26, v2_condmem new — + wrong=0; report re-pinned (`scripts/verify_lane_shas.py`). diff --git a/docs/research/conditional-membership-fusion-band-2026-07-23.md b/docs/research/conditional-membership-fusion-band-2026-07-23.md new file mode 100644 index 00000000..aa89ff77 --- /dev/null +++ b/docs/research/conditional-membership-fusion-band-2026-07-23.md @@ -0,0 +1,124 @@ +# Band v4-CM: conditional-membership fusion, decided (ADR-0259) + +**Date:** 2026-07-23 · **Arc:** deduction-serve, band 5 of the cascade +**ADR:** ADR-0259 (Proposed) · **Flag:** `deduction_serving_enabled` (default off, unchanged) + +## What CORE serves now (flag-on transcripts) + +Decided, from the real `core chat` spine, over the user's own sentences — +the exact gap ADR-0258 §6.1 reserved: + +> **If Socrates is a man then Socrates is mortal. Socrates is a man. +> Therefore Socrates is mortal.** +> → Given: if socrates is a man then socrates is mortal; socrates is a man. +> Your premises entail: socrates is mortal. + +The genuine fusion case — a bare universal's instantiated atom UNIFYING +with a connective leaf's atom, something neither v2-EN nor v3-MEM alone can +decide: + +> **All men are mortal. If Socrates is a philosopher then Socrates is a +> man. Socrates is a philosopher. Therefore Socrates is mortal.** +> → …Your premises entail: socrates is mortal. + +> **If Socrates is a man then Socrates is mortal. Therefore Socrates is +> mortal.** *(the antecedent is never asserted)* +> → …Reading each name as one individual and each class word at face +> value, your premises don't settle whether socrates is mortal — it holds +> in some cases and fails in others. + +That last one is `ds-mem-0024` — the eval-lane case pinned `declined` +purely for want of a reading band, now promoted. It is the **first +promotion in this corpus that does not land on `entailed`**: the band now +reads the text, and the honest answer for THAT specific text is UNKNOWN +(no premise ever asserts the antecedent). Promotion means "now decided +correctly," not "now decided favorably." + +## Mechanism (one new module, everything else reused) + +`generate/proof_chain/cond_member.py` composes v2-EN's connective grammar +(`if/then`, `or`, `and`, `either`) with v3-MEM's singular-membership +sentence reading, over ONE shared per-individual atom space. Concretely: +a sentence is checked for a connective token BEFORE the universal-lead +check (so a stray connective can never leak into an opaque universal/ +singular name run); a bare top-level `and` premise still splits into +independent facts (v2-EN's own discipline); everything else containing +`if`/`then`/`or`/`either` builds a small formula tree (`Lit`/`And`/`Or`/ +`Implies`) whose LEAVES are v3-MEM singular facts — parsed by v3-MEM's own +`_parse_singular`, reused verbatim, which is already negation-aware (unlike +v2-EN's opaque-atom minter, so this band needs no separate negation layer). +The SAME two-pass lowering v3-MEM already performs — collect named +individuals and closed-morphology class-groups, THEN mint atoms, THEN +instantiate every bare universal at every named individual — now also +scans leaves nested inside connective trees, which is what lets a +universal instantiate at an individual named only inside an `if`-clause, +and lets a connective leaf's atom unify with one a universal's +instantiation also produced. + +**Soundness (ADR-0259 §3):** nothing here is a new inference rule — every +connective is standard propositional structure the ROBDD engine already +decides; every leaf is minted and linked by the IDENTICAL closed +morphology relation ADR-0258 §3 already proved sound and, for this +fragment, complete. Universal instantiation stays sound regardless of +WHERE a named individual's name appears in the argument; composing +connectives over already-Boolean membership atoms does not change what +"every element is a named individual" needs to guarantee for completeness. +UNKNOWN is rendered by `render_entailment_member` UNCHANGED — no new +render function; its scoping is exactly as accurate here. + +## Earned, not flagged (ADR-0256 discipline) + +- Four new shape-bands — `en_condmem_fused/disjunctive/chain/conditional` + — each earned SERVE at the arena: **17 bands × 720 = 12,240 cases, + wrong=0**, reliability 0.99087 ≥ θ_SERVE=0.99; ledger re-sealed + (`chat/data/deduction_serve_ledger.json`, 17 bands, sha `6285a423…`). + Priority order fused > disjunctive > chain > conditional; a successfully- + decided argument in this band always contains ≥1 connective sentence (any + other refusal reason v3-MEM would hit, this band hits identically, via + the SAME reused guards), so no fifth "atomic" band is needed. +- Arena gold is by-construction and cross-checked against the truth-table + oracle over each template's INTENDED formulas — no reader in the loop + (INV-25). The FUSED templates specifically encode the cross-mechanism + unification (verified by hand-trace against the real reader before + writing gold, then confirmed by the independent oracle). +- New hand-authored real-English lane `evals/deduction_serve/v2_condmem/` + (26 cases, content-disjoint): **26/26**, alongside v1 **28/28**, v2_en + **26/26**, and v2_member **26/26** (wrong=0 everywhere; the promoted + `ds-mem-0024` now scores against its corrected `unknown` gold). + +## Verification + +- `uv run core test --suite deductive -q`: **160 passed** (31-test reader + contract new: flagship, modus tollens, both disjunctive spellings, the + and-split-is-not-a-connective case, two-hop chains, the fusion mechanism + itself — including a no-leak-across-individuals check — band + classification, the full refusal vocabulary, both honesty caps, + determinism). +- Practice arena: `all_bands_serve_licensed=True wrong_is_zero=True` (17 + bands). +- Lane splits: v1 28/28 · v2_en 26/26 · v2_member 26/26 (post-promotion) · + v2_condmem 26/26. +- Smoke suite: **180 passed**. Warmed-session lane: **10 passed**. + +## A wrinkle worth surfacing + +`scripts/verify_lane_shas.py --update` was run once to re-pin +`deduction_serve_v1` and, because the flag updates every lane in one pass, +it also silently rewrote `miner_loop_closure`, `curriculum_loop_closure`, +and `demo_composition`'s pins and DROPPED `public_demo`'s pin entirely +(that lane errored — `all_claims_supported=False` — a known flake). Those +three rewrites were reverted; **only** the `deduction_serve_v1` line was +hand-edited to the freshly-computed SHA. The three lanes' drift is +real, pre-existing, and unrelated to this arc (this worktree branched +directly off the just-merged main) — it is reported here, not fixed, since +diagnosing it is outside this band's scope and blind re-pinning is exactly +what the tool's own remediation text warns against. + +## Scope-outs (deliberate, ADR-0259 §5) + +A universal clause cannot be nested inside a connective (only a bare +top-level universal instantiates) — composing a quantified antecedent/ +consequent would need bound-variable tracking across clauses, a larger +question left for a future band if a real case needs it. Existential +premises, tense, verb predicates, identity/definite descriptions remain +out of band, inherited unchanged from ADR-0258. diff --git a/evals/deduction_serve/contract.md b/evals/deduction_serve/contract.md index 6b60bd10..ed1dbfc9 100644 --- a/evals/deduction_serve/contract.md +++ b/evals/deduction_serve/contract.md @@ -8,8 +8,9 @@ The **production serving decider** — the exact pipeline `comprehend` (reader) → the band cascade — `to_deductive_logic` (Band v1) → `to_syllogism` + the categorical decider (Band v1b, ADR-0256) → `read_english_argument` (Band v2-EN, ADR-0257) → `read_member_argument` -(Band v3-MEM, ADR-0258) — with `evaluate_entailment_with_trace` (the -ROBDD engine, ADR-0201/ADR-0218) deciding every band. +(Band v3-MEM, ADR-0258) → `read_cond_member_argument` (Band v4-CM, +ADR-0259) — with `evaluate_entailment_with_trace` (the ROBDD engine, +ADR-0201/ADR-0218) deciding every band. `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 @@ -23,6 +24,11 @@ against wording-only changes. content disjoint from the synthetic practice lexicon. - `v2_member/` — hand-authored membership/universal arguments (ADR-0258), incl. real nouns across every number-link row-type. +- `v2_condmem/` — hand-authored conditional-membership arguments + (ADR-0259): v2-EN's connective grammar composed over v3-MEM's singular- + membership sentence reading, incl. genuine universal+connective fusion + cases (a bare universal's instantiated atom unifying with a connective + leaf's atom). This is **distinct** from two existing lanes that sound similar: @@ -63,7 +69,9 @@ corpus, since every committed case reads as an argument by design). Boundaries are DISCOVERED as declines, then PROMOTED to decided gold when a later band earns the shape (the corpus keeps the case, renamed -`…_formerly_out_of_band`): +`…_formerly_out_of_band`). Promotion does not always mean "→ entailed": +the promoted gold is whatever the newly-earned band actually, honestly +decides for that exact text. - **Nested negation inside `if/then`** — a shared-reader grammar limit (`not` is reserved inside if/then slots); `ds-v1-0006` declined until @@ -74,10 +82,21 @@ a later band earns the shape (the corpus keeps the case, renamed Band v1b since ADR-0256. - **`is a` membership** — `ds-en-0022` declined until Band v3-MEM decided it (promoted, ADR-0258). +- **A bare conditional over membership clauses** — `ds-mem-0024` + (`"If Socrates is a man then Socrates is mortal. Therefore Socrates is + mortal."`) declined (`mixed_structure_out_of_band`) until Band v4-CM + landed (ADR-0259), which reads it — but the antecedent is never + asserted, so its honest verdict is **UNKNOWN**, not entailed. Promoted + declined → unknown, renamed `conditional_no_anchor_formerly_out_of_band` + — the first promotion in this corpus that does not land on `entailed`, + because the promoted band's own correct answer for THIS text is a + non-commitment, not a new capability to showcase. - **Still-open declines** (honest, typed): verb-phrase negation (`ds-en-0023/0024`), ambiguous `and`/`or` scope (`ds-en-0025`), nested conditionals (`ds-en-0026`), existential quantifiers / bare plurals / - definite descriptions / relative clauses / tense (`ds-mem-0020…0026`). + definite descriptions / relative clauses / tense + (`ds-mem-0020…0023/0025/0026`), a universal clause nested inside a + connective, compound conclusions (`ds-cm-0020…0026`). ## Reproduce diff --git a/evals/deduction_serve/practice/gold.py b/evals/deduction_serve/practice/gold.py index 7afd5c33..5d882eef 100644 --- a/evals/deduction_serve/practice/gold.py +++ b/evals/deduction_serve/practice/gold.py @@ -33,6 +33,7 @@ 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.cond_member import CondMemberArgument, read_cond_member_argument from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace from generate.proof_chain.member import MemberArgument, read_member_argument @@ -45,6 +46,10 @@ from generate.proof_chain.shape import ( EN_ATOMIC, EN_CONDITIONAL_CHAIN, EN_CONDITIONAL_SINGLE, + EN_CONDMEM_CHAIN, + EN_CONDMEM_CONDITIONAL, + EN_CONDMEM_DISJUNCTIVE, + EN_CONDMEM_FUSED, EN_DISJUNCTIVE, EN_MEMBER_ATOMIC, EN_MEMBER_CHAIN, @@ -387,12 +392,122 @@ _MEM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = { ), } -#: Ledger band order: the five v1 bands, the four v2-EN bands, then the four -#: v3-MEM bands. +# --- Band v4-CM (ADR-0259): conditional-membership synthetic corpus ---------- +# +# Reuses the v3-MEM case generator (``_mem_case``) directly — same names/ +# classes/states pool, no new lexicon needed. Composes v2-EN's connective +# grammar with v3-MEM's singular-membership sentence reading over the SAME +# per-individual atom space; the FUSED templates specifically exercise a bare +# universal instantiation UNIFYING (via the closed morphology relation) with +# an atom a connective's leaf also produced — the mechanism this band adds. + +_CM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = { + EN_CONDMEM_CONDITIONAL: ( + # Modus ponens over membership atoms. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.", + ("ca implies cb", "ca"), "cb"), + # Modus tollens. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is not {st}. Therefore {n1} is not a {c1[0]}.", + ("ca implies cb", "not cb"), "not ca"), + # Direct contradiction of the consequent. + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is not {st}.", + ("ca implies cb", "ca"), "not cb"), + # Affirming the consequent — classic non-sequitur. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is {st}. Therefore {n1} is a {c1[0]}.", + ("ca implies cb", "cb"), "ca"), + # Denying the antecedent — classic non-sequitur. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. {n1} is not a {c1[0]}. Therefore {n1} is not {st}.", + ("ca implies cb", "not ca"), "not cb"), + # No anchor at all. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. Therefore {n1} is a {c1[0]}.", + ("ca implies cb",), "ca"), + ), + EN_CONDMEM_DISJUNCTIVE: ( + # Disjunctive syllogism over membership atoms. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]} or {n1} is a {c2[0]}. {n1} is not a {c1[0]}. Therefore {n1} is a {c2[0]}.", + ("ca or cb", "not ca"), "cb"), + # "either" spelling, other disjunct. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"Either {n1} is a {c1[0]} or {n1} is a {c2[0]}. {n1} is not a {c2[0]}. Therefore {n1} is a {c1[0]}.", + ("ca or cb", "not cb"), "ca"), + # Constructive dilemma. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]} or {n1} is a {c2[0]}. Therefore {n1} is {st}.", + ("ca implies cc", "cb implies cc", "ca or cb"), "cc"), + # Eliminating one disjunct entails the other's negation is refuted. + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]} or {n1} is a {c2[0]}. {n1} is not a {c1[0]}. Therefore {n1} is not a {c2[0]}.", + ("ca or cb", "not ca"), "not cb"), + # A bare disjunction settles neither disjunct. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]} or {n1} is a {c2[0]}. Therefore {n1} is a {c1[0]}.", + ("ca or cb",), "ca"), + ), + EN_CONDMEM_CHAIN: ( + # Two-hop modus ponens across two connective sentences. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.", + ("ca implies cb", "cb implies cc", "ca"), "cc"), + # Two-hop modus tollens. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is not {st}. Therefore {n1} is not a {c1[0]}.", + ("ca implies cb", "cb implies cc", "not cc"), "not ca"), + # Two-hop chain onto a MEMBERSHIP conclusion (not a state). + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is a {c3[0]}. {n1} is a {c1[0]}. Therefore {n1} is a {c3[0]}.", + ("ca implies cb", "cb implies cc", "ca"), "cc"), + # Chain contradiction. + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is not {st}.", + ("ca implies cb", "cb implies cc", "ca"), "not cc"), + # Chain with no anchor. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is a {c2[0]}. If {n1} is a {c2[0]} then {n1} is {st}. Therefore {n1} is {st}.", + ("ca implies cb", "cb implies cc"), "cc"), + ), + EN_CONDMEM_FUSED: ( + # The mechanism: a bare universal's instantiated atom UNIFIES (via + # the closed morphology relation) with a connective leaf's atom — + # neither mechanism alone would decide this. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"All {c1[1]} are {c2[1]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.", + ("ca implies cb", "cb implies cc", "ca"), "cc"), + # Reversed sentence order — connective first, universal second. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"If {n1} is a {c1[0]} then {n1} is {st}. All {c2[1]} are {c1[1]}. {n1} is a {c2[0]}. Therefore {n1} is {st}.", + ("ca implies cb", "cc implies ca", "cc"), "cb"), + # Universal first, singular second, connective third. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"All {c1[1]} are {c2[1]}. {n1} is a {c1[0]}. If {n1} is a {c2[0]} then {n1} is {st}. Therefore {n1} is {st}.", + ("ca implies cb", "ca", "cb implies cc"), "cc"), + # Fused chain contradiction. + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"All {c1[1]} are {c2[1]}. If {n1} is a {c2[0]} then {n1} is {st}. {n1} is a {c1[0]}. Therefore {n1} is not {st}.", + ("ca implies cb", "cb implies cc", "ca"), "not cc"), + # The universal binds a DIFFERENT individual than the connective and + # query concern — instantiating it for one individual must not leak + # into another's conclusion. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"All {c1[1]} are {st}. If {n2} is a {c2[0]} then {n2} is a {c1[0]}. {n1} is a {c1[0]}. Therefore {n2} is {st}.", + ("ca implies cb", "cc implies cd", "ce implies ca", "cc"), "cb"), + ), +} + + +#: Ledger band order: the five v1 bands, the four v2-EN bands, the four +#: v3-MEM bands, then the four v4-CM bands. _ALL_BANDS: tuple[str, ...] = ( CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC, CATEGORICAL, EN_CONDITIONAL_SINGLE, EN_CONDITIONAL_CHAIN, EN_DISJUNCTIVE, EN_ATOMIC, EN_MEMBER_SINGLE, EN_MEMBER_CHAIN, EN_MEMBER_NEGATIVE, EN_MEMBER_ATOMIC, + EN_CONDMEM_FUSED, EN_CONDMEM_DISJUNCTIVE, EN_CONDMEM_CHAIN, EN_CONDMEM_CONDITIONAL, ) @@ -406,8 +521,8 @@ def generate_problems(band: str, n: int) -> list[Problem]: logical form for the reader-independent oracle cross-check. """ problems: list[Problem] = [] - if band in _MEM_TEMPLATES: - templates = _MEM_TEMPLATES[band] + if band in _MEM_TEMPLATES or band in _CM_TEMPLATES: + templates = _MEM_TEMPLATES[band] if band in _MEM_TEMPLATES else _CM_TEMPLATES[band] for i in range(n): gold, builder, intended_premises, intended_query = templates[i % len(templates)] problems.append( @@ -526,6 +641,9 @@ class DeductionSolver: member = self._attempt_member(problem) if member is not None: return member + cond_member = self._attempt_cond_member(problem) + if cond_member is not None: + return cond_member return _DeductionAttempt( committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}", case_id=problem.problem_id, shape=problem.class_name, @@ -562,6 +680,9 @@ class DeductionSolver: member = self._attempt_member(problem) if member is not None: return member + cond_member = self._attempt_cond_member(problem) + if cond_member is not None: + return cond_member return _DeductionAttempt( committed=False, answer=None, reason="unprojectable", case_id=problem.problem_id, shape=problem.class_name, @@ -597,6 +718,21 @@ class DeductionSolver: case_id=problem.problem_id, shape=arg.band, ) + def _attempt_cond_member(self, problem: Problem) -> _DeductionAttempt | None: + """Band v4-CM: the conditional-membership argument path, or ``None`` + when the reader refuses (the caller then records the honest decline).""" + arg = read_cond_member_argument(problem.payload["text"]) + if not isinstance(arg, CondMemberArgument): + return None + outcome = evaluate_entailment_with_trace( + arg.premise_formulas, arg.query_formula + ).outcome + return _DeductionAttempt( + committed=outcome is not Entailment.REFUSED, + answer=_OUTCOME_TO_CLASS[outcome], reason="", + case_id=problem.problem_id, shape=arg.band, + ) + @dataclass(frozen=True, slots=True) class ConstructionGoldTether: diff --git a/evals/deduction_serve/report.json b/evals/deduction_serve/report.json index 22114fe7..a65a5fba 100644 --- a/evals/deduction_serve/report.json +++ b/evals/deduction_serve/report.json @@ -1,8 +1,8 @@ { "aggregate": { - "correct": 80, + "correct": 106, "declined": 0, - "n": 80, + "n": 106, "wrong": 0 }, "all_correct": true, @@ -35,6 +35,27 @@ }, "n": 28 }, + "v2_condmem": { + "all_cases_correct": true, + "by_gold": { + "declined": 7, + "entailed": 10, + "refuted": 4, + "unknown": 5 + }, + "correct_by_gold": { + "declined": 7, + "entailed": 10, + "refuted": 4, + "unknown": 5 + }, + "counts": { + "correct": 26, + "declined": 0, + "wrong": 0 + }, + "n": 26 + }, "v2_en": { "all_cases_correct": true, "by_gold": { @@ -59,16 +80,16 @@ "v2_member": { "all_cases_correct": true, "by_gold": { - "declined": 7, + "declined": 6, "entailed": 12, "refuted": 3, - "unknown": 4 + "unknown": 5 }, "correct_by_gold": { - "declined": 7, + "declined": 6, "entailed": 12, "refuted": 3, - "unknown": 4 + "unknown": 5 }, "counts": { "correct": 26, diff --git a/evals/deduction_serve/runner.py b/evals/deduction_serve/runner.py index bb6a6127..8bd05bb3 100644 --- a/evals/deduction_serve/runner.py +++ b/evals/deduction_serve/runner.py @@ -45,6 +45,7 @@ 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.cond_member import CondMemberArgument, read_cond_member_argument from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace from generate.proof_chain.member import MemberArgument, read_member_argument @@ -61,6 +62,10 @@ _SPLITS: tuple[tuple[str, Path], ...] = ( # same content-disjoint discipline (incl. the number-link table on real # nouns: men, people, children, canaries, sheep). ("v2_member", _ROOT / "v2_member" / "cases.jsonl"), + # Band v4-CM (ADR-0259) — hand-authored conditional-membership arguments, + # same content-disjoint discipline (connectives composed over singular- + # membership clauses, incl. universal+connective fusion cases). + ("v2_condmem", _ROOT / "v2_condmem" / "cases.jsonl"), ) _OUTCOME_TO_CLASS = { @@ -124,9 +129,19 @@ def _decide_english(text: str) -> str: def _decide_member(text: str) -> str: - """Band v3-MEM fallback (ADR-0258) — mirrors ``_member_band_surface``.""" + """Band v3-MEM fallback (ADR-0258) — mirrors ``_member_band_surface``; + chains into the Band v4-CM fallback exactly as the composer does.""" arg = read_member_argument(text) if not isinstance(arg, MemberArgument): + return _decide_cond_member(text) + outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome + return _OUTCOME_TO_CLASS[outcome] + + +def _decide_cond_member(text: str) -> str: + """Band v4-CM fallback (ADR-0259) — mirrors ``_cond_member_band_surface``.""" + arg = read_cond_member_argument(text) + if not isinstance(arg, CondMemberArgument): return "declined" outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome return _OUTCOME_TO_CLASS[outcome] diff --git a/evals/deduction_serve/v2_condmem/cases.jsonl b/evals/deduction_serve/v2_condmem/cases.jsonl new file mode 100644 index 00000000..7cfca296 --- /dev/null +++ b/evals/deduction_serve/v2_condmem/cases.jsonl @@ -0,0 +1,26 @@ +{"id": "ds-cm-0001", "text": "If Socrates is a man then Socrates is mortal. Socrates is a man. Therefore Socrates is mortal.", "gold": "entailed", "class": "conditional_modus_ponens"} +{"id": "ds-cm-0002", "text": "If the museum is open then the ticket booth is staffed. The ticket booth is not staffed. Therefore the museum is not open.", "gold": "entailed", "class": "conditional_modus_tollens"} +{"id": "ds-cm-0003", "text": "Either the witness is lying or the suspect is guilty. The witness is not lying. Therefore the suspect is guilty.", "gold": "entailed", "class": "either_disjunctive_syllogism"} +{"id": "ds-cm-0004", "text": "The key is in the drawer or the key is on the hook. The key is not in the drawer. Therefore the key is on the hook.", "gold": "entailed", "class": "plain_or_disjunctive_syllogism"} +{"id": "ds-cm-0005", "text": "If the alarm is triggered then the guard is alerted. If the sensor is triggered then the guard is alerted. The alarm is triggered or the sensor is triggered. Therefore the guard is alerted.", "gold": "entailed", "class": "constructive_dilemma"} +{"id": "ds-cm-0006", "text": "If the pressure is high then the valve is open. If the valve is open then the tank is draining. The pressure is high. Therefore the tank is draining.", "gold": "entailed", "class": "two_hop_chain"} +{"id": "ds-cm-0007", "text": "If Nova is a suspect then Nova is a person of interest. If Nova is a person of interest then Nova is a flight risk. Nova is a suspect. Therefore Nova is a flight risk.", "gold": "entailed", "class": "two_hop_chain_membership"} +{"id": "ds-cm-0008", "text": "All engineers are employees. If Dax is an employee then Dax is insured. Dax is an engineer. Therefore Dax is insured.", "gold": "entailed", "class": "universal_connective_fusion"} +{"id": "ds-cm-0009", "text": "If Dax is an employee then Dax is insured. All contractors are employees. Dax is a contractor. Therefore Dax is insured.", "gold": "entailed", "class": "fusion_reversed_order"} +{"id": "ds-cm-0010", "text": "All students are learners. Priya is a student. If Priya is a learner then Priya is curious. Therefore Priya is curious.", "gold": "entailed", "class": "fusion_universal_first_order"} +{"id": "ds-cm-0011", "text": "If the reactor is critical then the reactor is unstable. The reactor is critical. Therefore the reactor is not unstable.", "gold": "refuted", "class": "conditional_direct_contradiction"} +{"id": "ds-cm-0012", "text": "If the code compiles then the code is buildable. If the code is buildable then the code is deployable. The code compiles. Therefore the code is not deployable.", "gold": "refuted", "class": "chain_contradiction"} +{"id": "ds-cm-0013", "text": "All interns are trainees. If Kai is a trainee then Kai is supervised. Kai is an intern. Therefore Kai is not supervised.", "gold": "refuted", "class": "fusion_chain_contradiction"} +{"id": "ds-cm-0014", "text": "The switch is on or the switch is off. The switch is not on. Therefore the switch is not off.", "gold": "refuted", "class": "disjunct_elimination_denial"} +{"id": "ds-cm-0015", "text": "If it is raining then the ground is wet. The ground is wet. Therefore it is raining.", "gold": "unknown", "class": "affirming_the_consequent"} +{"id": "ds-cm-0016", "text": "If the server is overloaded then the response is slow. The server is not overloaded. Therefore the response is not slow.", "gold": "unknown", "class": "denying_the_antecedent"} +{"id": "ds-cm-0017", "text": "If the bridge is closed then the traffic is rerouted. Therefore the bridge is closed.", "gold": "unknown", "class": "no_anchor"} +{"id": "ds-cm-0018", "text": "The door is locked or the door is unlocked. Therefore the door is locked.", "gold": "unknown", "class": "bare_disjunction"} +{"id": "ds-cm-0019", "text": "All senators are legislators. If Elio is a legislator then Elio is a committee member. Priya is a senator. Therefore Elio is a committee member.", "gold": "unknown", "class": "fusion_wrong_individual"} +{"id": "ds-cm-0020", "text": "If the door is open then if the window is open then the room is cold. Therefore the room is cold.", "gold": "declined", "class": "nested_conditional"} +{"id": "ds-cm-0021", "text": "The car is red and the car is fast or the car is loud. Therefore the car is fast.", "gold": "declined", "class": "ambiguous_and_or"} +{"id": "ds-cm-0022", "text": "If Nora is a pilot then Nora is licensed. Nora is a pilot. Therefore Nora is licensed and Nora is trained.", "gold": "declined", "class": "compound_conclusion_out_of_band"} +{"id": "ds-cm-0023", "text": "If someone is a suspect then someone is questioned. Therefore someone is questioned.", "gold": "declined", "class": "quantifier_out_of_band"} +{"id": "ds-cm-0024", "text": "If Elio is a manager then dogs are loyal. Elio is a manager. Therefore dogs are loyal.", "gold": "declined", "class": "bare_plural_out_of_band"} +{"id": "ds-cm-0025", "text": "If Elio is a manager then Elio is the boss. Elio is a manager. Therefore Elio is the boss.", "gold": "declined", "class": "definite_description_out_of_band"} +{"id": "ds-cm-0026", "text": "If Elio is a manager then the car that speeds is dangerous. Elio is a manager. Therefore the car that speeds is dangerous.", "gold": "declined", "class": "relative_clause_out_of_band"} diff --git a/evals/deduction_serve/v2_member/cases.jsonl b/evals/deduction_serve/v2_member/cases.jsonl index 9a6b4810..eb7401d9 100644 --- a/evals/deduction_serve/v2_member/cases.jsonl +++ b/evals/deduction_serve/v2_member/cases.jsonl @@ -21,6 +21,6 @@ {"id": "ds-mem-0021", "text": "Dogs are loyal. Rex is a dog. Therefore Rex is loyal.", "gold": "declined", "class": "bare_plural_out_of_band"} {"id": "ds-mem-0022", "text": "Socrates is the philosopher. All philosophers are wise. Therefore Socrates is wise.", "gold": "declined", "class": "definite_description_out_of_band"} {"id": "ds-mem-0023", "text": "Socrates is a man. All men are mortal. Therefore all men are mortal.", "gold": "declined", "class": "universal_conclusion_out_of_band"} -{"id": "ds-mem-0024", "text": "If Socrates is a man then Socrates is mortal. Therefore Socrates is mortal.", "gold": "declined", "class": "mixed_structure_out_of_band"} +{"id": "ds-mem-0024", "text": "If Socrates is a man then Socrates is mortal. Therefore Socrates is mortal.", "gold": "unknown", "class": "conditional_no_anchor_formerly_out_of_band"} {"id": "ds-mem-0025", "text": "Rex is a dog that barks. All dogs are loyal. Therefore Rex is loyal.", "gold": "declined", "class": "relative_clause_out_of_band"} {"id": "ds-mem-0026", "text": "Socrates was a man. All men are mortal. Therefore Socrates is mortal.", "gold": "declined", "class": "tense_out_of_band"} diff --git a/generate/proof_chain/cond_member.py b/generate/proof_chain/cond_member.py new file mode 100644 index 00000000..1e2ebb1a --- /dev/null +++ b/generate/proof_chain/cond_member.py @@ -0,0 +1,447 @@ +"""Conditional-membership argument reader — Band v4-CM (ADR-0259). + +Composes Band v2-EN's connective grammar (``if/then``, ``or``, ``and``, +``either`` sugar) with Band v3-MEM's singular-membership sentence reading, so +"If Socrates is a man then Socrates is mortal. Socrates is a man. Therefore +Socrates is mortal." decides — the ``mixed_structure_out_of_band`` gap +ADR-0258 §6.1 reserved as a future band. + +Why this needs no new negation layer (unlike v2-EN): v2-EN's leaf minter +(``_AtomTable.mint``) is negation-BLIND, so its grammar must strip "not" +before minting. This band's leaf is ``generate.proof_chain.member``'s own +``_parse_singular`` — already negation-aware (leading "not", the sentential +"it is not the case that" prefix, and copular "is not") — so a leaf is parsed +directly, no separate negation-extraction step. + +Why composing is sound (ADR-0259 §3, the load-bearing argument): every +connective built here (``&``, ``|``, ``->``) is standard propositional +structure the ROBDD engine already decides; every leaf is a v3-MEM singular +fact minted and linked by the SAME closed morphology relation ADR-0258 §3 +proved sound and (for this fragment) complete. A bare universal may now +instantiate at an individual named only inside a connective's leaf — still +sound, since ADR-0258 §3's argument does not depend on WHERE a named +individual appears — and a connective's leaf atom may unify with an atom a +universal's instantiation also produced (the fusion this band is named for). +UNKNOWN is rendered by the UNCHANGED ``render_entailment_member`` (ADR-0258): +its scoping ("reading each name as one individual and each class word at +face value…") is exactly as accurate here, since every clause is read all +the way to individual+class — connectives add no new hidden structure. + +Dispatch order is load-bearing: a sentence is checked for a connective token +BEFORE the universal-lead check (not after), so a connective token can never +silently leak into an opaque universal/singular name or class run. + +Tried strictly AFTER Bands v1 / v1b / v2-EN / v3-MEM (a fallback tier) — pure +widening; every previously-served argument is served byte-identically. +Refusal-first, closed reason vocabulary: + + ``empty``, ``question_sentence``, ``no_conclusion``, + ``multiple_conclusions``, ``conclusion_not_last``, ``no_premises``, + ``empty_side``, ``quantifier_out_of_band``, ``bare_plural_out_of_band``, + ``definite_description_out_of_band``, ``relative_clause_out_of_band``, + ``universal_conclusion_out_of_band``, ``compound_conclusion_out_of_band``, + ``internal_negation_unread``, ``sentence_shape_out_of_band``, + ``structural_leak``, ``nested_conditional``, ``ambiguous_and_or``, + ``too_many_premises``, ``too_many_atoms``. +""" + +from __future__ import annotations + +from dataclasses import dataclass + +# The v2-EN sentence splitter, tokenizer, and generic token-run splitter are +# reused VERBATIM (one normalization discipline across every argument band — +# deliberate private-name imports inside the proof_chain package, same +# precedent as generate.proof_chain.member). +from generate.proof_chain.english import _SENTENCE_RE, _split_on, _tokenize +from generate.proof_chain.member import ( + _A_LEADS, + _E_LEAD, + _QUANTIFIER_TOKENS, + _Singular, + _Universal, + _forms_link, + _parse_singular, + _parse_universal, +) +from generate.proof_chain.member import _Reject as _MemberReject +from generate.proof_chain.shape import ( + EN_CONDMEM_CHAIN, + EN_CONDMEM_CONDITIONAL, + EN_CONDMEM_DISJUNCTIVE, + EN_CONDMEM_FUSED, +) + +#: Connective structure this band's grammar composes (v2-EN's inventory, +#: minus "therefore" — that token is the commit-gate handled by the +#: outer sentence loop, never part of a clause's own structure). +_CONNECTIVE_TOKENS = frozenset({"if", "then", "or", "and", "either"}) + +#: Honesty caps — beyond these the argument is refused, never truncated. +#: ``MAX_ATOMS`` counts minted (individual, class) pairs. +MAX_PREMISE_SENTENCES = 16 +MAX_ATOMS = 24 + + +@dataclass(frozen=True, slots=True) +class CondMemberArgument: + """A successfully-read conditional-membership argument, engine-ready. + + Same shape as ``MemberArgument``/``EnglishArgument``: ``premise_formulas``/ + ``query_formula`` are propositional formula strings over minted atom ids; + ``atoms[i]`` displays the *(individual, class)* pair behind ``a{i}``. + ``premise_texts``/``query_text`` are the normalized original sentences. + """ + + premise_formulas: tuple[str, ...] + query_formula: str + premise_texts: tuple[str, ...] + query_text: str + band: str + atoms: tuple[str, ...] + + +@dataclass(frozen=True, slots=True) +class CondMemberRefusal: + """A typed refusal — the argument is not honestly readable by this band.""" + + reason: str + detail: str = "" + + +class _Reject(Exception): + def __init__(self, reason: str, detail: str = "") -> None: + super().__init__(reason) + self.refusal = CondMemberRefusal(reason, detail) + + +# --- the formula tree: leaves are v3-MEM singular facts, not opaque atoms ---- + + +@dataclass(frozen=True, slots=True) +class _Lit: + leaf: int + + +@dataclass(frozen=True, slots=True) +class _And: + left: "_Formula" + right: "_Formula" + + +@dataclass(frozen=True, slots=True) +class _Or: + left: "_Formula" + right: "_Formula" + + +@dataclass(frozen=True, slots=True) +class _Implies: + left: "_Formula" + right: "_Formula" + + +_Formula = _Lit | _And | _Or | _Implies + + +@dataclass(frozen=True, slots=True) +class _Connective: + """A parsed connective sentence: its formula tree over LOCAL leaf indices, + plus the singular facts those indices reference (leaf-parse order).""" + + formula: _Formula + leaves: tuple[_Singular, ...] + + +def _is_connective(toks: list[str]) -> bool: + return any(t in _CONNECTIVE_TOKENS for t in toks) + + +def _leaf(toks: list[str], leaves: list[_Singular], detail: str) -> _Lit: + """One membership leaf — reuses v3-MEM's own singular parser verbatim, + which is already negation-aware and already guards every name/class run + (quantifiers, relative clauses, definite descriptions, tense, bare + plurals) via ``_check_run``.""" + leaves.append(_parse_singular(toks, detail)) + return _Lit(len(leaves) - 1) + + +def _parse_junction(toks: list[str], leaves: list[_Singular], detail: str) -> _Formula: + """Or/and over membership leaves. "either" is consumed before a + disjunction; mixed top-level and+or refuses (English scope is genuinely + ambiguous); a conditional may not nest inside a junction.""" + if "if" in toks or "then" in toks: + raise _Reject("nested_conditional", detail) + if toks and toks[0] == "either" and "or" in toks: + toks = toks[1:] + has_or = "or" in toks + has_and = "and" in toks + if has_or and has_and: + raise _Reject("ambiguous_and_or", detail) + if has_or or has_and: + sep = "or" if has_or else "and" + parts = _split_on(toks, sep) + if any(not p for p in parts): + raise _Reject("empty_side", detail) + combine = _Or if has_or else _And + node = _leaf(parts[0], leaves, detail) + for part in parts[1:]: + node = combine(node, _leaf(part, leaves, detail)) + return node + return _leaf(toks, leaves, detail) + + +def _parse_node(toks: list[str], leaves: list[_Singular], detail: str) -> _Formula: + """One full connective sentence: ``if then `` (junctions allowed on + both sides, no nested conditionals) or a bare junction.""" + if toks and toks[0] == "if": + if "then" not in toks: + raise _Reject("nested_conditional", detail) + then_idx = toks.index("then") + antecedent = toks[1:then_idx] + consequent = toks[then_idx + 1 :] + if not antecedent or not consequent: + raise _Reject("empty_side", detail) + left = _parse_junction(antecedent, leaves, detail) + right = _parse_junction(consequent, leaves, detail) + return _Implies(left, right) + return _parse_junction(toks, leaves, detail) + + +def _parse_premise_records( + toks: list[str], detail: str +) -> list[_Singular | _Universal | _Connective]: + """A premise sentence -> one or more records. A top-level conjunction + (" and .", no "if"/"or" anywhere) splits into separate singular + records — identical to conjoining (v2-EN's exact discipline, ported). + Any OTHER connective-bearing sentence builds a ``_Connective``. A + connective-token check happens BEFORE the universal-lead check so a + stray connective token can never leak into a bare universal's name/class + run undetected.""" + if toks[0] != "if" and "and" in toks and "or" not in toks and "if" not in toks: + parts = _split_on(toks, "and") + if any(not p for p in parts): + raise _Reject("empty_side", detail) + return [_parse_singular(p, detail) for p in parts] + if _is_connective(toks): + leaves: list[_Singular] = [] + formula = _parse_node(toks, leaves, detail) + return [_Connective(formula, tuple(leaves))] + if toks[0] in _A_LEADS or toks[0] == _E_LEAD: + return [_parse_universal(toks, detail)] + if toks[0] in _QUANTIFIER_TOKENS: + raise _Reject("quantifier_out_of_band", detail) + return [_parse_singular(toks, detail)] + + +def _parse_conclusion(toks: list[str], detail: str) -> _Singular: + """The conclusion stays a single singular fact (optionally negated) — + matching v3-MEM's own discipline; a universal or connective-shaped + conclusion refuses rather than attempting a compound render.""" + if _is_connective(toks): + raise _Reject("compound_conclusion_out_of_band", detail) + if toks[0] in _A_LEADS or toks[0] == _E_LEAD: + raise _Reject("universal_conclusion_out_of_band", detail) + if toks[0] in _QUANTIFIER_TOKENS: + raise _Reject("quantifier_out_of_band", detail) + return _parse_singular(toks, detail) + + +def _contains_or(node: _Formula) -> bool: + if isinstance(node, _Lit): + return False + if isinstance(node, _Or): + return True + return _contains_or(node.left) or _contains_or(node.right) + + +def _count_implies(node: _Formula) -> int: + if isinstance(node, _Lit): + return 0 + n = 1 if isinstance(node, _Implies) else 0 + return n + _count_implies(node.left) + _count_implies(node.right) + + +def read_cond_member_argument(text: str) -> CondMemberArgument | CondMemberRefusal: + """Read *text* as a conditional-membership argument, or refuse (typed). + + Deterministic and pure: same text -> same ``CondMemberArgument``. The + conclusion is the final sentence, the sole "therefore"-led one, and must + be a single singular fact; every earlier sentence is a premise. Lowering + is two-pass exactly as v3-MEM's — sentences (and connective leaves) parse + first, THEN individuals/class-groups are collected from every singular + fact wherever it appears (bare, and-split, or nested inside a connective + tree), THEN atoms are minted and universals instantiate at every named + individual — with premise formulas emitted in sentence order. + """ + if not text or not text.strip(): + return CondMemberRefusal("empty") + sentences = [ + (m.group(1), m.group(2)) for m in _SENTENCE_RE.finditer(text) if m.group(1).strip() + ] + if not sentences: + return CondMemberRefusal("empty") + + premise_records: list[_Singular | _Universal | _Connective] = [] + record_details: list[str] = [] + premise_texts: list[str] = [] + conclusion: _Singular | None = None + query_text: str | None = None + + try: + for idx, (body, terminator) in enumerate(sentences): + if terminator == "?": + raise _Reject("question_sentence", body) + toks = _tokenize(body) + if not toks: + continue + if toks[0] == "therefore": + if conclusion is not None: + raise _Reject("multiple_conclusions", body) + if idx != len(sentences) - 1: + raise _Reject("conclusion_not_last", body) + rest = toks[1:] + if not rest: + raise _Reject("empty_side", body) + conclusion = _parse_conclusion(rest, body) + query_text = " ".join(rest) + continue + if len(premise_texts) >= MAX_PREMISE_SENTENCES: + raise _Reject("too_many_premises", body) + records = _parse_premise_records(toks, body) + premise_records.extend(records) + record_details.extend([body] * len(records)) + premise_texts.append(" ".join(toks)) + + if conclusion is None or query_text is None: + return CondMemberRefusal("no_conclusion") + if not premise_records: + return CondMemberRefusal("no_premises") + + # --- lowering (ADR-0259 §2): shared with v3-MEM's two-pass scheme -- + all_records: list[_Singular | _Universal | _Connective] = [ + *premise_records, conclusion, + ] + + # Named individuals, first-appearance order — scanning bare + # singulars AND every leaf nested inside a connective. + individuals: list[tuple[str, ...]] = [] + + def _visit_individual(ind: tuple[str, ...]) -> None: + if ind not in individuals: + individuals.append(ind) + + for rec in all_records: + if isinstance(rec, _Singular): + _visit_individual(rec.ind) + elif isinstance(rec, _Connective): + for leaf in rec.leaves: + _visit_individual(leaf.ind) + + # Class groups: each attested form joins the FIRST group whose + # representative it links to — greedy, deterministic, closed (the + # SAME morphology relation as v3-MEM). + group_of: dict[tuple[str, ...], int] = {} + reps: list[tuple[str, ...]] = [] + + def _register_form(form: tuple[str, ...]) -> None: + if form in group_of: + return + for gi, rep in enumerate(reps): + if _forms_link(form, rep): + group_of[form] = gi + return + group_of[form] = len(reps) + reps.append(form) + + for rec in all_records: + if isinstance(rec, _Singular): + _register_form(rec.cls) + elif isinstance(rec, _Universal): + _register_form(rec.subject) + _register_form(rec.predicate) + elif isinstance(rec, _Connective): + for leaf in rec.leaves: + _register_form(leaf.cls) + + mint: dict[tuple[int, int], str] = {} + atom_display: list[str] = [] + + def atom_for(ind_idx: int, group: int, detail: str) -> str: + key = (ind_idx, group) + if key not in mint: + if len(atom_display) >= MAX_ATOMS: + raise _Reject("too_many_atoms", detail) + mint[key] = f"a{len(atom_display)}" + atom_display.append( + f"{' '.join(individuals[ind_idx])} : {' '.join(reps[group])}" + ) + return mint[key] + + def atom_of_singular(fact: _Singular, detail: str) -> str: + atom = atom_for(individuals.index(fact.ind), group_of[fact.cls], detail) + return f"~({atom})" if fact.negated else atom + + def render_formula(node: _Formula, leaves: tuple[_Singular, ...], detail: str) -> str: + if isinstance(node, _Lit): + return atom_of_singular(leaves[node.leaf], detail) + left = render_formula(node.left, leaves, detail) + right = render_formula(node.right, leaves, detail) + if isinstance(node, _And): + return f"({left}) & ({right})" + if isinstance(node, _Or): + return f"({left}) | ({right})" + return f"({left}) -> ({right})" # _Implies + + premise_formulas: list[str] = [] + for rec, detail in zip(premise_records, record_details): + if isinstance(rec, _Singular): + premise_formulas.append(atom_of_singular(rec, detail)) + elif isinstance(rec, _Connective): + premise_formulas.append(render_formula(rec.formula, rec.leaves, detail)) + else: # _Universal — instantiate at every named individual + for ind_idx in range(len(individuals)): + antecedent = atom_for(ind_idx, group_of[rec.subject], detail) + consequent = atom_for(ind_idx, group_of[rec.predicate], detail) + premise_formulas.append( + f"({antecedent}) -> (~({consequent}))" + if rec.negative + else f"({antecedent}) -> ({consequent})" + ) + + query_formula = atom_of_singular(conclusion, query_text) + except (_Reject, _MemberReject) as rej: + # ``_parse_singular``/``_parse_universal`` are v3-MEM's own functions, + # reused verbatim — their failures raise v3-MEM's OWN ``_Reject`` + # class (same shape, different identity), so both are caught here and + # normalized to THIS band's refusal type. + return CondMemberRefusal(rej.refusal.reason, rej.refusal.detail) + + connectives = [r for r in premise_records if isinstance(r, _Connective)] + has_universal = any(isinstance(r, _Universal) for r in premise_records) + if has_universal and connectives: + band = EN_CONDMEM_FUSED + elif any(_contains_or(c.formula) for c in connectives): + band = EN_CONDMEM_DISJUNCTIVE + elif sum(_count_implies(c.formula) for c in connectives) >= 2: + band = EN_CONDMEM_CHAIN + else: + band = EN_CONDMEM_CONDITIONAL + + return CondMemberArgument( + premise_formulas=tuple(premise_formulas), + query_formula=query_formula, + premise_texts=tuple(premise_texts), + query_text=query_text, + band=band, + atoms=tuple(atom_display), + ) + + +__all__ = [ + "MAX_ATOMS", + "MAX_PREMISE_SENTENCES", + "CondMemberArgument", + "CondMemberRefusal", + "read_cond_member_argument", +] diff --git a/generate/proof_chain/shape.py b/generate/proof_chain/shape.py index 993b8ea2..6ff9d7cc 100644 --- a/generate/proof_chain/shape.py +++ b/generate/proof_chain/shape.py @@ -77,8 +77,28 @@ EN_MEMBER_BANDS: tuple[str, ...] = ( EN_MEMBER_ATOMIC, ) +#: Band v4-CM (ADR-0259) — conditional-membership fusion arguments, composing +#: v2-EN's connective grammar with v3-MEM's singular-membership sentence +#: reading ("If Socrates is a man then Socrates is mortal. …"), read by +#: ``generate.proof_chain.cond_member``. Same ``en_`` license discipline: a +#: different reader must earn its own per-shape record. Priority order: +#: fused > disjunctive > chain > conditional. +EN_CONDMEM_FUSED = "en_condmem_fused" +EN_CONDMEM_DISJUNCTIVE = "en_condmem_disjunctive" +EN_CONDMEM_CHAIN = "en_condmem_chain" +EN_CONDMEM_CONDITIONAL = "en_condmem_conditional" + +EN_CONDMEM_BANDS: tuple[str, ...] = ( + EN_CONDMEM_FUSED, + EN_CONDMEM_DISJUNCTIVE, + EN_CONDMEM_CHAIN, + EN_CONDMEM_CONDITIONAL, +) + #: Every serving shape-band — the ratified ledger's full key set. -ALL_SHAPE_BANDS: tuple[str, ...] = SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS +ALL_SHAPE_BANDS: tuple[str, ...] = ( + SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS + EN_CONDMEM_BANDS +) def classify_deduction_shape(premises: tuple[str, ...], query: str) -> str: @@ -115,6 +135,11 @@ __all__ = [ "EN_ATOMIC", "EN_CONDITIONAL_CHAIN", "EN_CONDITIONAL_SINGLE", + "EN_CONDMEM_BANDS", + "EN_CONDMEM_CHAIN", + "EN_CONDMEM_CONDITIONAL", + "EN_CONDMEM_DISJUNCTIVE", + "EN_CONDMEM_FUSED", "EN_DISJUNCTIVE", "EN_MEMBER_ATOMIC", "EN_MEMBER_BANDS", diff --git a/scripts/verify_lane_shas.py b/scripts/verify_lane_shas.py index 0e38dccf..735f1ad9 100644 --- a/scripts/verify_lane_shas.py +++ b/scripts/verify_lane_shas.py @@ -51,7 +51,7 @@ PINNED_SHAS: dict[str, str] = { "public_demo": "7d8ba0dbae9287cfe0bf15d231fa78a75abc627121c14900439293e01e1cc1d3", "math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4", "deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", - "deduction_serve_v1": "ec446d70a6ba2eaaf04671800924754a3cfaacfc46f3225ca73e961169cd625d", + "deduction_serve_v1": "b530ed99c414a6d1bdd239752b0e1c6c8c03893f402198def29122b9c2a8a8be", } diff --git a/tests/test_cond_member_argument_reader.py b/tests/test_cond_member_argument_reader.py new file mode 100644 index 00000000..b86a4a94 --- /dev/null +++ b/tests/test_cond_member_argument_reader.py @@ -0,0 +1,301 @@ +"""Band v4-CM (ADR-0259) — conditional-membership argument reader contract. + +The reader composes v2-EN's connective grammar (if/then, or, and, either) +with v3-MEM's singular-membership sentence reading over ONE shared +per-individual atom space. It is pure and deterministic. Soundness rides on +the ROBDD engine; these tests pin that the reader hands it the RIGHT problem +— in particular that a bare universal's instantiated atom correctly UNIFIES +with a connective leaf's atom when the two mechanisms share a class (the +"fusion" this band is named for). +""" + +from __future__ import annotations + +import pytest + +from generate.proof_chain.cond_member import ( + MAX_ATOMS, + MAX_PREMISE_SENTENCES, + CondMemberArgument, + CondMemberRefusal, + read_cond_member_argument, +) +from generate.proof_chain.member import MemberRefusal, read_member_argument +from generate.proof_chain.shape import ( + EN_CONDMEM_CHAIN, + EN_CONDMEM_CONDITIONAL, + EN_CONDMEM_DISJUNCTIVE, + EN_CONDMEM_FUSED, +) + + +def _read(text: str) -> CondMemberArgument: + arg = read_cond_member_argument(text) + assert isinstance(arg, CondMemberArgument), arg + return arg + + +def _refusal(text: str) -> CondMemberRefusal: + ref = read_cond_member_argument(text) + assert isinstance(ref, CondMemberRefusal), ref + return ref + + +# --- the composition itself: what v3-MEM refuses, this band decides ---------- + + +def test_the_gap_this_band_fills_is_real() -> None: + """The exact ADR-0258 §6.1 scope-out: v3-MEM refuses this shape in + isolation (pinned in test_member_argument_reader.py); this band decides + it. Both facts hold at once — v3-MEM is unchanged, this is a new tier.""" + text = "If Socrates is a man then Socrates is mortal. Socrates is a man. Therefore Socrates is mortal." + assert isinstance(read_member_argument(text), MemberRefusal) + assert isinstance(read_cond_member_argument(text), CondMemberArgument) + + +# --- the flagship reading ----------------------------------------------------- + + +def test_flagship_socrates_reads_as_conditional_modus_ponens() -> None: + arg = _read( + "If Socrates is a man then Socrates is mortal. Socrates is a man. " + "Therefore Socrates is mortal." + ) + assert arg.premise_formulas == ("(a0) -> (a1)", "a0") + assert arg.query_formula == "a1" + assert arg.premise_texts == ( + "if socrates is a man then socrates is mortal", "socrates is a man", + ) + assert arg.query_text == "socrates is mortal" + assert arg.band == EN_CONDMEM_CONDITIONAL + assert len(arg.atoms) == 2 + + +def test_modus_tollens_over_membership_atoms() -> None: + arg = _read( + "If Socrates is a man then Socrates is mortal. Socrates is not mortal. " + "Therefore Socrates is not a man." + ) + assert arg.premise_formulas == ("(a0) -> (a1)", "~(a1)") + assert arg.query_formula == "~(a0)" + + +def test_or_disjunctive_syllogism() -> None: + arg = _read( + "Socrates is a man or Socrates is a god. Socrates is not a god. " + "Therefore Socrates is a man." + ) + assert arg.premise_formulas == ("(a0) | (a1)", "~(a1)") + assert arg.query_formula == "a0" + assert arg.band == EN_CONDMEM_DISJUNCTIVE + + +def test_either_spelling_disjunctive_syllogism() -> None: + arg = _read( + "Either Socrates is a man or Socrates is a god. Socrates is not a man. " + "Therefore Socrates is a god." + ) + assert arg.premise_formulas == ("(a0) | (a1)", "~(a0)") + assert arg.query_formula == "a1" + + +def test_and_split_premise_is_two_bare_records_not_a_connective() -> None: + """A top-level "X and Y" PREMISE (no if/or) splits into independent + singular records — identical to conjoining, mirroring v2-EN exactly — + rather than building an ``&`` formula.""" + arg = _read( + "Socrates is a man and Plato is a man. All men are mortal. " + "Therefore Socrates is mortal." + ) + # The universal instantiates at EVERY named individual (Socrates AND + # Plato), each producing its own freshly-minted consequent atom. + assert arg.premise_formulas == ("a0", "a1", "(a0) -> (a2)", "(a1) -> (a3)") + assert arg.query_formula == "a2" + assert arg.premise_texts == ( + "socrates is a man and plato is a man", "all men are mortal", + ) + + +def test_two_hop_chain() -> None: + arg = _read( + "If Socrates is a man then Socrates is a philosopher. " + "If Socrates is a philosopher then Socrates is wise. " + "Socrates is a man. Therefore Socrates is wise." + ) + assert arg.premise_formulas == ("(a0) -> (a1)", "(a1) -> (a2)", "a0") + assert arg.query_formula == "a2" + assert arg.band == EN_CONDMEM_CHAIN + + +# --- the fusion mechanism: universal instantiation UNIFIES with a connective +# leaf's atom via the SAME closed morphology relation ------------------------ + + +def test_universal_instantiation_unifies_with_connective_leaf() -> None: + """The mechanism this band is named for: "all MEN are mortal" instantiates + Socrates : men -> Socrates : mortal via the SAME atom the connective's + consequent leaf mints for "Socrates is a man" (linked man<->men).""" + arg = _read( + "All men are mortal. If Socrates is a philosopher then Socrates is a man. " + "Socrates is a philosopher. Therefore Socrates is mortal." + ) + assert arg.premise_formulas == ("(a0) -> (a1)", "(a2) -> (a0)", "a2") + assert arg.query_formula == "a1" + assert arg.band == EN_CONDMEM_FUSED + assert len(arg.atoms) == 3 + + +def test_fusion_reversed_sentence_order_reads_identically() -> None: + arg = _read( + "If Socrates is a philosopher then Socrates is a man. All men are mortal. " + "Socrates is a philosopher. Therefore Socrates is mortal." + ) + # The connective mints philosopher/man first (a0/a1); the universal's + # antecedent REUSES a1 (men links to man), minting only mortal fresh (a2). + assert arg.premise_formulas == ("(a0) -> (a1)", "(a1) -> (a2)", "a0") + assert arg.query_formula == "a2" + assert arg.band == EN_CONDMEM_FUSED + + +def test_fusion_does_not_leak_across_individuals() -> None: + """Instantiating a bare universal for MULTIPLE named individuals must not + let one individual's fact force another's conclusion.""" + arg = _read( + "All men are mortal. If Plato is a philosopher then Plato is a man. " + "Socrates is a man. Therefore Plato is mortal." + ) + # mortal(plato) needs man(plato), which needs philosopher(plato) — never + # asserted; socrates's fact is irrelevant to the query. + from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace + + outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome + assert outcome is Entailment.UNKNOWN + + +# --- band classification ------------------------------------------------------ + + +@pytest.mark.parametrize( + ("text", "band"), + [ + ( + "If Bo is a cat then Bo is quick. Bo is a cat. Therefore Bo is quick.", + EN_CONDMEM_CONDITIONAL, + ), + ( + "Bo is a cat or Bo is a dog. Bo is not a cat. Therefore Bo is a dog.", + EN_CONDMEM_DISJUNCTIVE, + ), + ( + "If Bo is a cat then Bo is a hunter. If Bo is a hunter then Bo is quick. " + "Bo is a cat. Therefore Bo is quick.", + EN_CONDMEM_CHAIN, + ), + ( + "All cats are hunters. If Bo is a stray then Bo is a cat. Bo is a stray. " + "Therefore Bo is a hunter.", + EN_CONDMEM_FUSED, + ), + ], +) +def test_band_classification(text: str, band: str) -> None: + assert _read(text).band == band + + +# --- typed refusals ----------------------------------------------------------- + + +@pytest.mark.parametrize( + ("text", "reason"), + [ + ( + "If the door is open then if the window is open then the room is cold. " + "Therefore the room is cold.", + "nested_conditional", + ), + ( + "The car is red and the car is fast or the car is loud. " + "Therefore the car is fast.", + "ambiguous_and_or", + ), + ( + "If Socrates is a man then Socrates is mortal. Socrates is a man. " + "Therefore Socrates is mortal and Socrates is wise.", + "compound_conclusion_out_of_band", + ), + ( + "Socrates is a man. Therefore all men are mortal.", + "universal_conclusion_out_of_band", + ), + ( + "If someone is a suspect then someone is questioned. " + "Therefore someone is questioned.", + "quantifier_out_of_band", + ), + ( + "If Socrates is a man then dogs are loyal. Socrates is a man. " + "Therefore dogs are loyal.", + "bare_plural_out_of_band", + ), + ( + "If Socrates is a man then Socrates is the philosopher. Socrates is a man. " + "Therefore Socrates is the philosopher.", + "definite_description_out_of_band", + ), + ( + "If Socrates is a man then the dog that barks is loud. Socrates is a man. " + "Therefore the dog that barks is loud.", + "relative_clause_out_of_band", + ), + ( + "If Socrates was a man then Socrates was mortal. Socrates is a man. " + "Therefore Socrates is mortal.", + "sentence_shape_out_of_band", + ), + ("Is Socrates a man? Therefore Socrates is mortal.", "question_sentence"), + ( + "If Socrates is a man then Socrates is mortal. Socrates is a man.", + "no_conclusion", + ), + ("Therefore Socrates is mortal.", "no_premises"), + ( + "If Socrates is a man then Socrates is mortal. " + "Therefore Socrates is mortal. Plato is a man.", + "conclusion_not_last", + ), + ("", "empty"), + ], +) +def test_typed_refusals(text: str, reason: str) -> None: + assert _refusal(text).reason == reason + + +# --- honesty caps ------------------------------------------------------------- + + +def test_premise_cap_refuses_not_truncates() -> None: + facts = " ".join(f"N{i} is a cat." for i in range(MAX_PREMISE_SENTENCES)) + text = f"If Bo is a cat then Bo is quick. {facts} Therefore N0 is a cat." + ref = _refusal(text) + assert ref.reason == "too_many_premises" + + +def test_atom_cap_refuses_not_truncates() -> None: + n = MAX_ATOMS // 2 + 1 + facts = " ".join(f"N{i} is a dog." for i in range(n)) + ref = _refusal( + f"If Bo is a dog then Bo is loyal. {facts} All dogs are cats. " + f"Therefore N0 is a cat." + ) + assert ref.reason == "too_many_atoms" + + +# --- determinism -------------------------------------------------------------- + + +def test_reading_is_deterministic() -> None: + text = ( + "All men are mortal. If Socrates is a philosopher then Socrates is a man. " + "Socrates is a philosopher. Therefore Socrates is mortal." + ) + assert read_cond_member_argument(text) == read_cond_member_argument(text) diff --git a/tests/test_deduction_serve_e2e.py b/tests/test_deduction_serve_e2e.py index ed1c009a..5826c376 100644 --- a/tests/test_deduction_serve_e2e.py +++ b/tests/test_deduction_serve_e2e.py @@ -136,6 +136,27 @@ def test_member_argument_is_decided_end_to_end() -> None: assert "Your premises entail: tweety is not a reptile" in negative.surface +def test_conditional_membership_fusion_is_decided_end_to_end() -> None: + """The ADR-0259 flagship: a conditional whose clauses are membership + facts, decided through the real REPL spine — including the genuine + fusion case where a bare universal's instantiated atom unifies with a + connective leaf's atom.""" + rt = _runtime(True) + resp = rt.chat( + "If Socrates is a man then Socrates is mortal. Socrates is a man. " + "Therefore Socrates is mortal." + ) + assert resp.grounding_source == "deduction" + assert "Your premises entail: socrates is mortal" in resp.surface + + fused = rt.chat( + "All men are mortal. If Socrates is a philosopher then Socrates is a man. " + "Socrates is a philosopher. Therefore Socrates is mortal." + ) + assert fused.grounding_source == "deduction" + assert "Your premises entail: socrates is mortal" in fused.surface + + def test_out_of_regime_argument_refuses_honestly() -> None: """A 'therefore' argument NO band can read (verb-phrase negation — ADR-0257 scope-out #2, morphology work reserved for a future band) gets an diff --git a/tests/test_deduction_serve_lane.py b/tests/test_deduction_serve_lane.py index 2a1c2c2c..a223e1eb 100644 --- a/tests/test_deduction_serve_lane.py +++ b/tests/test_deduction_serve_lane.py @@ -14,6 +14,7 @@ from evals.deduction_serve.runner import _ROOT, _load, build_report _V1 = _ROOT / "v1" / "cases.jsonl" _V2_EN = _ROOT / "v2_en" / "cases.jsonl" _V2_MEMBER = _ROOT / "v2_member" / "cases.jsonl" +_V2_CONDMEM = _ROOT / "v2_condmem" / "cases.jsonl" def test_v1_lane_wrong_is_zero() -> None: @@ -56,7 +57,10 @@ def test_v2_member_lane_wrong_is_zero() -> None: """Band v3-MEM (ADR-0258): hand-authored membership/universal arguments — real nouns exercising every number-link row-type (irregular, invariant, each regular suffix rule) — decided with wrong=0 across all four verdicts - and seven distinct honest-decline shapes.""" + and six distinct honest-decline shapes. (``ds-mem-0024``, a bare + conditional with no anchor, was promoted declined->unknown when Band + v4-CM landed — ADR-0259; it is genuinely UNKNOWN, not entailed, since the + antecedent is never asserted.)""" report = build_report(_load(_V2_MEMBER)) assert report["n"] == 26 assert report["counts"]["wrong"] == 0 @@ -64,7 +68,24 @@ def test_v2_member_lane_wrong_is_zero() -> None: cbg = report["correct_by_gold"] assert cbg.get("entailed", 0) >= 12 assert cbg.get("refuted", 0) >= 3 - assert cbg.get("unknown", 0) >= 4 + assert cbg.get("unknown", 0) >= 5 + assert cbg.get("declined", 0) >= 6 + + +def test_v2_condmem_lane_wrong_is_zero() -> None: + """Band v4-CM (ADR-0259): hand-authored conditional-membership arguments + — v2-EN's connective grammar composed over v3-MEM's singular-membership + sentence reading, including genuine universal+connective fusion cases — + decided with wrong=0 across all four verdicts and seven distinct honest- + decline shapes.""" + report = build_report(_load(_V2_CONDMEM)) + assert report["n"] == 26 + assert report["counts"]["wrong"] == 0 + assert report["all_cases_correct"] is True + cbg = report["correct_by_gold"] + assert cbg.get("entailed", 0) >= 10 + assert cbg.get("refuted", 0) >= 4 + assert cbg.get("unknown", 0) >= 5 assert cbg.get("declined", 0) >= 7 diff --git a/tests/test_deduction_surface.py b/tests/test_deduction_surface.py index f33a319e..0e48eab3 100644 --- a/tests/test_deduction_surface.py +++ b/tests/test_deduction_surface.py @@ -231,6 +231,66 @@ def test_member_reader_refusal_keeps_prior_honest_surface() -> None: assert "can't parse" in surface +def test_conditional_membership_fusion_is_decided_band_v4_cm() -> None: + """The ADR-0258 §6.1 scope-out, now decided (ADR-0259): a conditional + whose clauses are membership facts, authoritatively (the + ``en_condmem_conditional`` band holds an earned SERVE license).""" + surface = deduction_grounded_surface( + "If Socrates is a man then Socrates is mortal. Socrates is a man. " + "Therefore Socrates is mortal." + ) + assert surface is not None + assert "Your premises entail: socrates is mortal" in surface + assert not surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + + +def test_conditional_membership_fusion_genuinely_fuses() -> None: + """The mechanism this band adds: a bare universal's instantiated atom + unifies with a connective leaf's atom — neither mechanism alone decides + this argument.""" + surface = deduction_grounded_surface( + "All men are mortal. If Socrates is a philosopher then Socrates is a man. " + "Socrates is a philosopher. Therefore Socrates is mortal." + ) + assert surface is not None + assert "Your premises entail: socrates is mortal" in surface + + +def test_cond_member_unknown_is_scoped_to_the_instantiated_reading() -> None: + surface = deduction_grounded_surface( + "If Socrates is a man then Socrates is mortal. Therefore Socrates is mortal." + ) + assert surface is not None + assert "Reading each name as one individual" in surface + assert "don't settle" in surface + + +def test_cond_member_unearned_band_would_be_hedged() -> None: + """The en_condmem_* bands ride the SAME earned-license gate: strip the + license and the same sound answer is served DISCLOSED, never + authoritatively.""" + surface = deduction_grounded_surface( + "If Socrates is a man then Socrates is mortal. Socrates is a man. " + "Therefore Socrates is mortal.", + license_lookup=lambda band: None, + ) + assert surface is not None + assert surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + assert "Your premises entail: socrates is mortal" in surface + + +def test_cond_member_reader_refusal_keeps_prior_honest_surface() -> None: + """When the conditional-membership band ALSO cannot read the argument + (here: a conditional nested inside another), the pre-existing honest + surface is preserved verbatim — the band only widens.""" + surface = deduction_grounded_surface( + "If the door is open then if the window is open then the room is cold. " + "Therefore the room is cold." + ) + assert surface is not None + assert "can't parse" 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)