diff --git a/CLAIMS.md b/CLAIMS.md index 4b8315c5..42354c01 100644 --- a/CLAIMS.md +++ b/CLAIMS.md @@ -43,7 +43,7 @@ is a CI failure (`.github/workflows/lane-shas.yml`). | ADR-0104 | `curriculum_loop_closure` | Curriculum-sourced proposals route through single reviewed teaching path | `evals/curriculum_loop_closure/results/v1_dev.json` | `cb94ca0042d78ec2624129ff6493d52e767b69feea32d2997b85d88f1c0883af` | | ADR-0131 | `math_teaching_corpus_v1` | Math teaching corpus replays deterministically; all chains pass exit criterion (correct_rate=1.0, wrong=0) | `evals/math_teaching_corpus/v1/report.json` | `eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4` | | ADR-0206 | `deductive_logic_v1` | Propositional entailment scored against an independent truth-table oracle; dev+holdout+external 716/716 correct, wrong=0, refused=0 | `evals/deductive_logic/report.json` | `97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f` | -| ADR-0256 | `deduction_serve_v1` | Flag-gated deduction serving decides real English/member/fused arguments end-to-end under earned SERVE licenses; wrong=0 across all splits | `evals/deduction_serve/report.json` | `b530ed99c414a6d1bdd239752b0e1c6c8c03893f402198def29122b9c2a8a8be` | +| ADR-0256 | `deduction_serve_v1` | Flag-gated deduction serving decides real English/member/fused arguments end-to-end under earned SERVE licenses; wrong=0 across all splits | `evals/deduction_serve/report.json` | `f4fa7331bbee40c898be9ea2a8cabf36f28c8a19a7500433e0fa966c05905a8a` | ## Verification diff --git a/chat/data/deduction_serve_ledger.json b/chat/data/deduction_serve_ledger.json index a946cb12..017d644e 100644 --- a/chat/data/deduction_serve_ledger.json +++ b/chat/data/deduction_serve_ledger.json @@ -118,9 +118,37 @@ "t2_agrees_gold": 0, "t2_verified": 0, "wrong": 0 + }, + "en_verb_chain": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_verb_fact": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_verb_negative": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_verb_universal": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 } }, - "content_sha256": "6285a423957bc9a3a6a562515a338dfd6f36188ac00f45c1a6ea979c4e3cc710", + "content_sha256": "b5dd8db3ac4770f229269c16d388325a0763237ff84c21618309468eabf46a77", "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 f23c0df2..1e1e7304 100644 --- a/chat/deduction_surface.py +++ b/chat/deduction_surface.py @@ -34,6 +34,13 @@ Bands (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md): 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. +- Band v5-VP (ADR-0260) — verb-predicate arguments ("All philosophers teach. + Socrates is a philosopher. Therefore Socrates teaches."), read by + ``generate.proof_chain.verb`` via per-individual lowering with a second + (individual, verb-group, object) atom family alongside v3-MEM's membership + atoms, decided by the same engine. Tried strictly AFTER v4-CM (the earlier + bands refuse quantifier-led verb universals, is-a + verb mixes, and + ``does not`` negation) — 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, @@ -59,8 +66,10 @@ from generate.proof_chain.render import ( render_entailment, render_entailment_english, render_entailment_member, + render_entailment_verb, render_syllogism, ) +from generate.proof_chain.verb import VerbArgument, read_verb_argument from generate.proof_chain.shape import CATEGORICAL, classify_deduction_shape #: An argument's conclusion clause starts a sentence with "therefore" — the @@ -143,6 +152,9 @@ def deduction_grounded_surface( cond_member = _cond_member_band_surface(text, license_lookup) if cond_member is not None: return cond_member + verb = _verb_band_surface(text, license_lookup) + if verb is not None: + return verb return _READER_REFUSAL_SURFACE.format(reason=comp.reason) # Band v1 — propositional argument. projected = to_deductive_logic(comp) @@ -175,6 +187,10 @@ def deduction_grounded_surface( cond_member = _cond_member_band_surface(text, license_lookup) if cond_member is not None: return cond_member + # Band v5-VP fallback — the verb-predicate shapes every earlier band guards out. + verb = _verb_band_surface(text, license_lookup) + if verb is not None: + return verb return _OUT_OF_BAND_SURFACE @@ -220,6 +236,21 @@ def _cond_member_band_surface(text: str, license_lookup: _LicenseLookup) -> str return _license_gate(surface, arg.band, license_lookup) +def _verb_band_surface(text: str, license_lookup: _LicenseLookup) -> str | None: + """Band v5-VP (ADR-0260): read *text* as a verb-predicate argument + (membership atoms + verb atoms over one per-individual space), 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). Rendered by ``render_entailment_verb``, whose UNKNOWN + scoping extends the member phrasing to the verb reading.""" + arg = read_verb_argument(text) + if not isinstance(arg, VerbArgument): + return None + trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula) + surface = render_entailment_verb(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 d094bea5..0f94f2bf 100644 --- a/core/cli_test.py +++ b/core/cli_test.py @@ -180,6 +180,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = { "tests/test_english_argument_reader.py", "tests/test_member_argument_reader.py", "tests/test_cond_member_argument_reader.py", + "tests/test_verb_argument_reader.py", "tests/test_deduction_serve_e2e.py", ), "full": ("tests/",), diff --git a/docs/adr/ADR-0260-verb-predicate-band.md b/docs/adr/ADR-0260-verb-predicate-band.md new file mode 100644 index 00000000..fcbe04e1 --- /dev/null +++ b/docs/adr/ADR-0260-verb-predicate-band.md @@ -0,0 +1,131 @@ +# ADR-0260 — Band v5-VP: verb-predicate arguments, decided + +- **Status:** Proposed +- **Date:** 2026-07-24 +- **Arc:** deduction-serve (ADR-0256 → 0257 → 0258 → 0259 → this) +- **Governs:** `generate/proof_chain/verb.py`, the `en_verb_*` shape-bands, + their arena templates, the `v2_verb` lane split, and the + `_verb_band_surface` serving tier. + +## 1. Context + +ADR-0258 §6.3 scoped verb predicates out of the member band: v3-MEM reads +only copula sentences, so "All philosophers teach. Socrates is a +philosopher. Therefore Socrates teaches." refused — despite being the plain +English shape in which most non-logic subject matter states its rules +(physics, biology, and every other domain speak in verb sentences, not is-a +chains). The generalization arc (docs/plans/generalization-arc-2026-07-24.md +Phase 1.1) makes this the single highest-leverage reading unlock: Phase 2's +curriculum-entailment serving is gated on it. + +The earlier bands each guard this territory out rather than misreading it: +v2-EN refuses quantifier-led sentences (`categorical_shape_out_of_band`), +is-a clauses (`membership_shape_out_of_band`), and unnormalized negation +(`internal_negation_unread`); v3-MEM/v4-CM refuse copula-free sentences +(`sentence_shape_out_of_band`). Pure verb-fact restatements with none of +those triggers are ALREADY decided soundly by v2-EN as opaque clause-atoms — +so this band's genuine territory is exactly the fall-through: arguments +mixing verb sentences with quantified rules, membership facts, or `does not` +negation. + +## 2. Decision + +Add `generate.proof_chain.verb.read_verb_argument` as the next fallback tier +(after v1 / v1b / v2-EN / v3-MEM / v4-CM), extending v3-MEM's +per-individual propositional lowering with a SECOND atom family in one +shared space: + +- **Membership atoms** *(individual, class-group)* — minted by v3-MEM's own + `_parse_singular` / `_parse_universal`, reused verbatim (copula sentences + keep their exact v3-MEM reading, refusals included). +- **Verb atoms** *(individual, verb-lemma-group, object-term)* — minted from + verb facts (` []`, `does not` negation, the + sentential-not prefix) and verb universals + (`all|every|each|no [the] []`). + +A verb universal instantiates at every named individual as +`mem(i, C) -> [~]verb(i)` — so a membership fact minted by a copula sentence +discharges a verb rule. The same verified ROBDD engine decides. + +Bands (priority order): `en_verb_negative` (any negative universal, either +kind) > `en_verb_chain` (≥2 universals) > `en_verb_universal` (exactly 1) > +`en_verb_fact` (facts only). Rendered by `render_entailment_verb` — the +member surface with the UNKNOWN scoping extended to the verb reading. Rides +`deduction_serving_enabled` (default off); no new flag. + +## 3. Why this is sound + +1. **Instantiation** — identical to ADR-0258 §3: universal instantiation at + named individuals is truth-preserving in every first-order model, and + each *(verb-group, object-term)* pair is one opaque unary predicate over + the same named-individual domain. ENTAILED / REFUTED / inconsistent + verdicts over the lowered premises hold in every model of the original + argument; completeness within the fragment lifts the same way (a + propositional countermodel's domain is exactly the named individuals). +2. **Agreement is the ONE new identification** — a universal's base form + ("teach") and a singular fact's 3sg form ("teaches") are identified iff + related by a CLOSED relation: a verb-specific irregular table (has/have, + goes/go, does/do; consulted first, sole authority for its tokens) else + the three regular suffix rules (+s, +es after sibilants, y↔ies). The noun + table is deliberately NOT reused — it would misroute verb forms like + "lives" (noun: life; verb: live). Under-linking costs coverage, never + soundness. Object terms link by exact token identity only. +3. **Scope-tight segmentation** — without a lexicon, an arbitrary + copula-free token run cannot be soundly split into subject/verb/object; + the band reads single-token name/class/verb/object shapes ONLY, and + refuses everything longer, typed. A three-token sentence read as + (subject, verb, object) is a disclosed reading, restated verbatim in the + surface's "Given:" line. +4. **Cascade honesty** — every text this band decides was verified to be + REFUSED by all four earlier bands (the arena templates and lane cases + are constructed on the fall-through path serving actually uses), so this + tier is pure widening: every previously-served argument is served + byte-identically. + +## 4. License and render + +The four `en_verb_*` bands earned SERVE through the ADR-0199 arena +(720/band committed, wrong=0, θ_SERVE=0.99; ledger resealed at 21 bands). +The arena's by-construction gold is cross-checked template-by-template +against the independent truth-table oracle over each template's INTENDED +per-individual lowering, with no reader in the loop (INV-25). Unearned or +ledger-stripped deployments serve the same sound answer hedged +(`_UNVERIFIED_SHAPE_DISCLOSURE`), exactly as every earlier band. + +## 5. Scope-outs (typed refusals today, future bands' territory) + +1. **Connective × verb composition** — "If Socrates teaches then …" + refuses `mixed_structure_out_of_band`; fusing v4-CM's connective grammar + over verb leaves is the natural next composition. +2. **Multi-token subjects/objects, PPs, adverbs, ditransitives** — + `sentence_shape_out_of_band`. Note one disclosed misreading inside the + 3-token shape: an adverb in object position ("Lena runs quickly") is + read as an object TERM — never unsound (worst case an over-scoped + UNKNOWN), documented here rather than guessed at. +3. **Tense** — `did not` refuses `tense_out_of_band`; bare past forms + ("taught") are indistinguishable from lemmas without a lexicon and read + as distinct opaque lemmas (under-linking, sound). +4. **Arity/subsumption** — "teaches" does not entail "teaches logic" (nor + vice versa) under the face-value reading; both directions stay UNKNOWN, + scoped. Same posture v2-EN already takes for opaque clauses. +5. **Plural/bare subjects in verb facts** ("dogs bark") — read as an + individual named "dogs" (disclosed in the UNKNOWN scoping); the copula + analogue is refused by v3-MEM's bare-plural guard, but no copula means no + plural signal in the closed grammar. +6. Existential (`some`) witnesses, identity/co-reference — unchanged + scope-outs inherited from ADR-0258 §6 (existentials are the + generalization arc's Phase 1.2, assigned to the Opus tier). + +## 6. Verification + +- `tests/test_verb_argument_reader.py` — 34 tests: gap-is-real cross-check, + flagship lowering, every agreement rule, object-in-atom-key, chain + discharge, cross-individual non-leakage, family separation + (teacher/teaches), 14 typed refusals incl. delegated v3-MEM reasons, + honesty caps, determinism. +- Surface/e2e/lane: `tests/test_deduction_surface.py` (+5), + `tests/test_deduction_serve_e2e.py` (+1), + `tests/test_deduction_serve_lane.py` (+1 over the 28-case `v2_verb` + split) — full lane 134/134, wrong=0, all five splits. +- Arena: 4 × 720 committed, wrong=0, first seal run; corpus soundness + asserted against the independent oracle before sealing (15,120 cases). diff --git a/docs/research/verb-predicate-band-2026-07-24.md b/docs/research/verb-predicate-band-2026-07-24.md new file mode 100644 index 00000000..ba7582d5 --- /dev/null +++ b/docs/research/verb-predicate-band-2026-07-24.md @@ -0,0 +1,87 @@ +# Band v5-VP — verb-predicate arguments, decided (ADR-0260) + +**Date:** 2026-07-24 · **Branch:** `feat/verb-predicate-band` (stacked on +`feat/generalization-phase0`) · **Arc:** generalization +(docs/plans/generalization-arc-2026-07-24.md, Phase 1.1 — Tier F) + +## What CORE can now do + +``` +> All philosophers teach. Socrates is a philosopher. Therefore Socrates teaches. +Given: all philosophers teach; socrates is a philosopher. +Your premises entail: socrates teaches. +``` + +Verb sentences — the shape in which every non-logic subject states its +rules — now read and decide. The cascade's earlier bands each guard this +territory out (v2-EN refuses quantifier leads / is-a clauses / `does not`; +v3-MEM and v4-CM refuse copula-free sentences), so the tier is pure +widening on the fall-through path. + +## Mechanism (ADR-0260 §2) + +v3-MEM's per-individual lowering, extended with a second atom family in ONE +shared space: membership atoms *(individual, class-group)* — minted by +v3-MEM's own parsers reused verbatim — plus verb atoms *(individual, +verb-lemma-group, object-term)*. A verb universal instantiates at every +named individual as `mem(i,C) -> [~]verb(i)`, so a copula-minted membership +fact discharges a verb rule. The ONE new semantic identification is 3sg +agreement: a closed verb relation (irregular table has/goes/does first, then ++s / +es-after-sibilant / y↔ies) links "teach"↔"teaches". The noun table is +deliberately NOT reused — it would misroute "lives" (noun: life; verb: +live). Everything the relation cannot relate stays distinct: under-linking +costs coverage, never soundness. + +Segmentation is scope-tight: single-token name/class/verb/object shapes +only (` []`, `does not`, sentential-not, `all|every|each| +no [the] []`); anything longer refuses typed — without a +lexicon there is no sound split of an arbitrary copula-free run. + +## Earned licenses + +Four new bands — `en_verb_universal`, `en_verb_chain`, `en_verb_negative`, +`en_verb_fact` — each 720/720 committed, wrong=0, first seal run; ledger +resealed at **21 bands** (12,240 + 2,880 committed). The synthetic verb pool +exercises every rule of the closed agreement relation, so the license +certifies the linking itself. Corpus soundness asserted case-by-case against +the independent truth-table oracle over each template's INTENDED lowering +(no reader in the loop, INV-25) before sealing. + +Lane: `evals/deduction_serve/v2_verb` — 28 hand-authored real-English cases +(11 entailed / 4 refuted / 5 unknown / 8 declined), 28/28 first run; full +lane now 134/134 wrong=0 across five splits. Gates: verb reader tests 34, +deduction battery 86, smoke + warmed_session via pre-push. + +## Wrinkles worth surfacing + +1. **Adverb-as-object misreading (disclosed, not fixed):** "Lena runs + quickly" parses as verb+object ("quickly" an opaque term). Never unsound + — worst case an over-scoped UNKNOWN — but it is a real misreading the + 3-token shape cannot detect without a lexicon. ADR-0260 §5.2 documents + it; the vocab-boundary instrument (plan Phase 3.1) is where a principled + fix would come from. +2. **Arity subsumption stays UNKNOWN:** "teaches" ⊬ "teaches logic" and + conversely — the face-value posture v2-EN already takes, now visible on + verbs. A human reads the intransitive as subsuming; the scoped UNKNOWN + phrasing carries the honesty. +3. **Plural verb-fact subjects read as individuals:** "dogs bark" is an + individual named "dogs" in this fragment (no copula ⇒ no plural signal in + the closed grammar). The membership analogue stays refused by v3-MEM's + bare-plural guard. +4. **`doesn't` is not expanded** by the shared tokenizer's contraction + table (only isn't/aren't/wasn't/weren't are) — so "The engine doesn't + start" still refuses via the `n't` guard, preserving the e2e + out-of-regime test byte-for-byte. Adding verb contractions is a + deliberate non-goal until the tense scope-out is faced whole. + +## Stacking note + +This branch stacks on `feat/generalization-phase0` (merge that PR first): +both touch `scripts/verify_lane_shas.py` / `CLAIMS.md`, and the claims +generator's `_LANE_ADR` fix lands there. + +## Next (per the plan's tier assignment) + +Tier O (Opus): Band v6-EX existential witnesses (Phase 1.2), then the +Phase-2 physics lane against the §4 curriculum-entailment contract — for +which this band was the gate. diff --git a/evals/deduction_serve/contract.md b/evals/deduction_serve/contract.md index ed1dbfc9..90fd07d0 100644 --- a/evals/deduction_serve/contract.md +++ b/evals/deduction_serve/contract.md @@ -9,7 +9,8 @@ The **production serving decider** — the exact pipeline → `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) → `read_cond_member_argument` (Band v4-CM, -ADR-0259) — with `evaluate_entailment_with_trace` (the ROBDD engine, +ADR-0259) → `read_verb_argument` (Band v5-VP, ADR-0260) — 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 @@ -29,6 +30,10 @@ against wording-only changes. membership sentence reading, incl. genuine universal+connective fusion cases (a bare universal's instantiated atom unifying with a connective leaf's atom). +- `v2_verb/` — hand-authored verb-predicate arguments (ADR-0260): verb + universals discharged by membership facts across every closed agreement + rule (+s, +es, y↔ies, irregular go/goes), transitive objects at face + value, and eight typed decline shapes. This is **distinct** from two existing lanes that sound similar: @@ -91,12 +96,21 @@ decides for that exact text. — 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 +- **Verb predicates** — refused by every band until Band v5-VP (ADR-0260) + decided them (`v2_verb/`). NO existing case promoted: every remaining + decline in the older splits uses contraction negation ("doesn't" — not + in the shared tokenizer's expansion table, so v5's `n't` guard refuses + identically) or structure v5 also guards out; the full lane's prior + splits stayed byte-stable. +- **Still-open declines** (honest, typed): verb-phrase contraction + 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…0023/0025/0026`), a universal clause nested inside a - connective, compound conclusions (`ds-cm-0020…0026`). + connective, compound conclusions (`ds-cm-0020…0026`), and the verb + band's own scope-outs — `did not` tense, multi-token subjects, + prepositional/ditransitive shapes, connective×verb composition + (`ds-vb-0021…0028`). ## Reproduce diff --git a/evals/deduction_serve/practice/gold.py b/evals/deduction_serve/practice/gold.py index 5d882eef..89869035 100644 --- a/evals/deduction_serve/practice/gold.py +++ b/evals/deduction_serve/practice/gold.py @@ -37,6 +37,7 @@ from generate.proof_chain.cond_member import CondMemberArgument, read_cond_membe 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 +from generate.proof_chain.verb import VerbArgument, read_verb_argument from generate.proof_chain.shape import ( ATOMIC, CATEGORICAL, @@ -56,6 +57,10 @@ from generate.proof_chain.shape import ( EN_MEMBER_NEGATIVE, EN_MEMBER_SINGLE, classify_deduction_shape, + EN_VERB_CHAIN, + EN_VERB_FACT, + EN_VERB_NEGATIVE, + EN_VERB_UNIVERSAL, ) _DOMAIN_ID = "deductive_logic_serve" @@ -501,13 +506,161 @@ _CM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = { } +# --- Band v5-VP (ADR-0260): verb-predicate synthetic corpus ------------------- +# +# Reuses the v3-MEM name/class pools and adds a verb-forms pool that exercises +# EVERY rule of the reader's closed verb-agreement relation — +s (bark/barks, +# run/runs, live/lives), +es after sibilants (teach/teaches, push/pushes, +# watch/watches, mix/mixes), y↔ies (study/studies, carry/carries, fly/flies), +# and the irregular table (go/goes, have/has) — so the earned license +# certifies the agreement linking itself, not just the sentence grammar. +# Content is synthetic ON PURPOSE (same posture as the v2-EN / v3-MEM corpora); +# hand-authored real-English cases live in ``evals/deduction_serve/v2_verb``. + +_VERB_FORMS: tuple[tuple[str, str], ...] = ( + ("teach", "teaches"), ("bark", "barks"), ("study", "studies"), + ("go", "goes"), ("run", "runs"), ("push", "pushes"), + ("carry", "carries"), ("watch", "watches"), ("live", "lives"), + ("fly", "flies"), ("mix", "mixes"), ("have", "has"), +) +_VERB_OBJECTS: tuple[str, ...] = ( + "logic", "music", "bread", "stones", "rivers", "wool", + "grain", "tools", "maps", "songs", "boats", "lamps", +) + + +def _verb_case( + index: int, +) -> tuple[str, str, tuple[str, str], tuple[str, str], tuple[str, str], tuple[str, str], str]: + """Deterministic (name1, name2, class1, class2, verb1, verb2, object) for + case ``index`` — names, classes, and verbs are pairwise distinct.""" + n1 = _MEM_NAMES[(index * 3) % len(_MEM_NAMES)] + n2 = _MEM_NAMES[(index * 3 + 1) % len(_MEM_NAMES)] + base = (index * 5) % (len(_MEM_CLASSES) - 1) + c1, c2 = _MEM_CLASSES[base], _MEM_CLASSES[base + 1] + vbase = (index * 7) % (len(_VERB_FORMS) - 1) + v1, v2 = _VERB_FORMS[vbase], _VERB_FORMS[vbase + 1] + ob = _VERB_OBJECTS[(index * 11) % len(_VERB_OBJECTS)] + return n1, n2, c1, c2, v1, v2, ob + + +#: Verb-band templates: (gold, text_builder, intended_premises, intended_query). +#: Builders take ``(n1, n2, c1, c2, v1, v2, ob)`` from ``_verb_case``; the +#: INTENDED formulas are the template's per-individual lowering over fixed +#: placeholder atoms (``ma``… membership, ``va``… verb), cross-checked against +#: the truth-table oracle with no reader in the loop (INV-25). Every template's +#: text is a shape the earlier bands REFUSE (quantifier-led verb universal, +#: is-a + verb mix, or ``does not`` negation), so the arena exercises exactly +#: the fall-through path serving uses. +_VERB_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = { + EN_VERB_UNIVERSAL: ( + # Instantiated modus ponens onto an intransitive verb. + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} {v1[0]}. Therefore {n1} {v1[1]}.", + ("ma", "ma implies vb"), "vb"), + # "every" spelling, singular class + 3sg verb, transitive. + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"Every {c1[0]} {v1[1]} {ob}. {n1} is a {c1[0]}. Therefore {n1} {v1[1]} {ob}.", + ("ma implies vb", "ma"), "vb"), + # "each" spelling, universal first — order independence. + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"Each {c1[0]} {v1[1]}. {n1} is a {c1[0]}. Therefore {n1} {v1[1]}.", + ("ma implies vb", "ma"), "vb"), + # Contradicting the instantiated verb. + ("refuted", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.", + ("ma", "ma implies vb"), "not vb"), + # The universal binds a DIFFERENT named individual than the conclusion's. + ("unknown", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} {v1[0]}. Therefore {n2} {v1[1]}.", + ("ma", "ma implies vb", "mc implies vd"), "vd"), + # Affirming the consequent — the verb fact does not yield membership. + ("unknown", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} {v1[1]}. All {c1[1]} {v1[0]}. Therefore {n1} is a {c1[0]}.", + ("vb", "ma implies vb"), "ma"), + ), + EN_VERB_CHAIN: ( + # Membership chain discharging a verb universal. + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} {v1[0]}. Therefore {n1} {v1[1]}.", + ("ma", "ma implies mb", "mb implies vc"), "vc"), + # Transitive, sentence order shuffled. + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"All {c1[1]} are {c2[1]}. {n1} is a {c1[0]}. All {c2[1]} {v1[0]} {ob}. Therefore {n1} {v1[1]} {ob}.", + ("ma implies mb", "ma", "mb implies vc"), "vc"), + # Chain contradiction. + ("refuted", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.", + ("ma", "ma implies mb", "mb implies vc"), "not vc"), + # Broken chain — the subsumption points the wrong way. + ("unknown", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c2[1]} are {c1[1]}. All {c2[1]} {v1[0]}. Therefore {n1} {v1[1]}.", + ("ma", "mb implies ma", "mb implies vc"), "vc"), + # Two verb universals — the wrong verb's rule cannot fire. + ("unknown", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} {v1[0]}. All {c2[1]} {v2[0]}. Therefore {n1} {v2[1]}.", + ("ma", "ma implies vb", "mc implies vd"), "vd"), + ), + EN_VERB_NEGATIVE: ( + # Instantiated E-form onto an intransitive verb. + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. No {c1[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.", + ("ma", "ma implies not vb"), "not vb"), + # A-chain into an E-form verb universal. + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. No {c2[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.", + ("ma", "ma implies mb", "mb implies not vc"), "not vc"), + # Transitive E-form. + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. No {c1[1]} {v1[0]} {ob}. Therefore {n1} does not {v1[0]} {ob}.", + ("ma", "ma implies not vb"), "not vb"), + # Contradicting the E-form's instantiation. + ("refuted", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is a {c1[0]}. No {c1[1]} {v1[0]}. Therefore {n1} {v1[1]}.", + ("ma", "ma implies not vb"), "vb"), + # Denied antecedent under an E-form — nothing follows. + ("unknown", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} is not a {c1[0]}. No {c1[1]} {v1[0]}. Therefore {n1} does not {v1[0]}.", + ("not ma", "ma implies not vb"), "not vb"), + ), + EN_VERB_FACT: ( + # Negated fact restated through the sentential-not spelling (the + # ``does not`` form is what makes the earlier bands refuse). + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} does not {v1[0]}. Therefore it is not the case that {n1} {v1[1]}.", + ("not va",), "not va"), + # Selection beside an is-a anchor (the anchor forces the fall-through). + ("entailed", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} {v1[1]} {ob}. {n1} is a {c1[0]}. Therefore {n1} {v1[1]} {ob}.", + ("va", "mb"), "va"), + # Contradicting a stated verb fact. + ("refuted", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} {v1[1]}. {n1} is a {c1[0]}. Therefore {n1} does not {v1[0]}.", + ("va", "mb"), "not va"), + # Negated transitive fact contradicted. + ("refuted", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} does not {v1[0]} {ob}. Therefore {n1} {v1[1]} {ob}.", + ("not va",), "va"), + # Arity is read at face value — intransitive does not yield transitive. + ("unknown", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} {v1[1]}. {n1} is a {c1[0]}. Therefore {n1} {v1[1]} {ob}.", + ("va", "mb"), "vc"), + # Distinct verbs stay distinct. + ("unknown", + lambda n1, n2, c1, c2, v1, v2, ob: f"{n1} does not {v1[0]}. Therefore {n1} does not {v2[0]}.", + ("not va",), "not vb"), + ), +} + + #: Ledger band order: the five v1 bands, the four v2-EN bands, the four -#: v3-MEM bands, then the four v4-CM bands. +#: v3-MEM bands, the four v4-CM bands, then the four v5-VP 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, + EN_VERB_NEGATIVE, EN_VERB_CHAIN, EN_VERB_UNIVERSAL, EN_VERB_FACT, ) @@ -521,6 +674,25 @@ def generate_problems(band: str, n: int) -> list[Problem]: logical form for the reader-independent oracle cross-check. """ problems: list[Problem] = [] + if band in _VERB_TEMPLATES: + templates = _VERB_TEMPLATES[band] + for i in range(n): + gold, builder, intended_premises, intended_query = templates[i % len(templates)] + problems.append( + Problem( + problem_id=f"{band}-{i:04d}", + class_name=band, + payload={ + "text": builder(*_verb_case(i)), + "gold": gold, + "intended": { + "premises": list(intended_premises), + "query": intended_query, + }, + }, + ) + ) + return problems 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): @@ -644,6 +816,9 @@ class DeductionSolver: cond_member = self._attempt_cond_member(problem) if cond_member is not None: return cond_member + verb = self._attempt_verb(problem) + if verb is not None: + return verb return _DeductionAttempt( committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}", case_id=problem.problem_id, shape=problem.class_name, @@ -683,6 +858,9 @@ class DeductionSolver: cond_member = self._attempt_cond_member(problem) if cond_member is not None: return cond_member + verb = self._attempt_verb(problem) + if verb is not None: + return verb return _DeductionAttempt( committed=False, answer=None, reason="unprojectable", case_id=problem.problem_id, shape=problem.class_name, @@ -733,6 +911,21 @@ class DeductionSolver: case_id=problem.problem_id, shape=arg.band, ) + def _attempt_verb(self, problem: Problem) -> _DeductionAttempt | None: + """Band v5-VP: the verb-predicate argument path, or ``None`` when the + reader refuses (the caller then records the honest decline).""" + arg = read_verb_argument(problem.payload["text"]) + if not isinstance(arg, VerbArgument): + 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 a65a5fba..18b06f99 100644 --- a/evals/deduction_serve/report.json +++ b/evals/deduction_serve/report.json @@ -1,8 +1,8 @@ { "aggregate": { - "correct": 106, + "correct": 134, "declined": 0, - "n": 106, + "n": 134, "wrong": 0 }, "all_correct": true, @@ -97,6 +97,27 @@ "wrong": 0 }, "n": 26 + }, + "v2_verb": { + "all_cases_correct": true, + "by_gold": { + "declined": 8, + "entailed": 11, + "refuted": 4, + "unknown": 5 + }, + "correct_by_gold": { + "declined": 8, + "entailed": 11, + "refuted": 4, + "unknown": 5 + }, + "counts": { + "correct": 28, + "declined": 0, + "wrong": 0 + }, + "n": 28 } }, "wrong_is_zero": true diff --git a/evals/deduction_serve/runner.py b/evals/deduction_serve/runner.py index 8bd05bb3..9b259965 100644 --- a/evals/deduction_serve/runner.py +++ b/evals/deduction_serve/runner.py @@ -49,6 +49,7 @@ from generate.proof_chain.cond_member import CondMemberArgument, read_cond_membe 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 +from generate.proof_chain.verb import VerbArgument, read_verb_argument _ROOT = Path(__file__).resolve().parent @@ -66,6 +67,10 @@ _SPLITS: tuple[tuple[str, Path], ...] = ( # same content-disjoint discipline (connectives composed over singular- # membership clauses, incl. universal+connective fusion cases). ("v2_condmem", _ROOT / "v2_condmem" / "cases.jsonl"), + # Band v5-VP (ADR-0260) — hand-authored verb-predicate arguments, same + # content-disjoint discipline (verb agreement across +s/+es/y↔ies and the + # irregular table on real verbs: writes, debates, cries, goes). + ("v2_verb", _ROOT / "v2_verb" / "cases.jsonl"), ) _OUTCOME_TO_CLASS = { @@ -142,6 +147,15 @@ 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 _decide_verb(text) + outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome + return _OUTCOME_TO_CLASS[outcome] + + +def _decide_verb(text: str) -> str: + """Band v5-VP fallback (ADR-0260) — mirrors ``_verb_band_surface``.""" + arg = read_verb_argument(text) + if not isinstance(arg, VerbArgument): 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_verb/cases.jsonl b/evals/deduction_serve/v2_verb/cases.jsonl new file mode 100644 index 00000000..cb120b9e --- /dev/null +++ b/evals/deduction_serve/v2_verb/cases.jsonl @@ -0,0 +1,28 @@ +{"id": "ds-vb-0001", "text": "All poets write. Homer is a poet. Therefore Homer writes.", "gold": "entailed", "class": "verb_universal_modus_ponens"} +{"id": "ds-vb-0002", "text": "Every senator debates policy. Cicero is a senator. Therefore Cicero debates policy.", "gold": "entailed", "class": "verb_universal_transitive"} +{"id": "ds-vb-0003", "text": "Anselm is a monk. Each monk prays. Therefore Anselm prays.", "gold": "entailed", "class": "verb_universal_each_spelling"} +{"id": "ds-vb-0004", "text": "Aristotle is a philosopher. All philosophers are scholars. All scholars read. Therefore Aristotle reads.", "gold": "entailed", "class": "verb_chain_membership"} +{"id": "ds-vb-0005", "text": "All sparrows are birds. Jack is a sparrow. All birds build nests. Therefore Jack builds nests.", "gold": "entailed", "class": "verb_chain_transitive"} +{"id": "ds-vb-0006", "text": "Miriam is a nun. No nuns marry. Therefore Miriam does not marry.", "gold": "entailed", "class": "verb_negative_e_form"} +{"id": "ds-vb-0007", "text": "Felix is a tortoise. All tortoises are reptiles. No reptiles purr. Therefore Felix does not purr.", "gold": "entailed", "class": "verb_negative_chain"} +{"id": "ds-vb-0008", "text": "Clara paints portraits. Clara is an artist. Therefore Clara paints portraits.", "gold": "entailed", "class": "verb_fact_selection"} +{"id": "ds-vb-0009", "text": "Boris does not smoke. Therefore it is not the case that Boris smokes.", "gold": "entailed", "class": "verb_fact_negation_restated"} +{"id": "ds-vb-0010", "text": "Every baby cries. Moses is a baby. Therefore Moses cries.", "gold": "entailed", "class": "verb_universal_ies_agreement"} +{"id": "ds-vb-0011", "text": "All pilgrims go. Dante is a pilgrim. Therefore Dante goes.", "gold": "entailed", "class": "verb_universal_irregular_agreement"} +{"id": "ds-vb-0012", "text": "All owls hunt. Hedwig is an owl. Therefore Hedwig does not hunt.", "gold": "refuted", "class": "verb_universal_contradiction"} +{"id": "ds-vb-0013", "text": "Petra is a judge. No judges gossip. Therefore Petra gossips.", "gold": "refuted", "class": "verb_negative_contradiction"} +{"id": "ds-vb-0014", "text": "Omar swims. Omar is an athlete. Therefore Omar does not swim.", "gold": "refuted", "class": "verb_fact_contradiction"} +{"id": "ds-vb-0015", "text": "Ida is a farmer. All farmers are workers. All workers vote. Therefore Ida does not vote.", "gold": "refuted", "class": "verb_chain_contradiction"} +{"id": "ds-vb-0016", "text": "All monks chant. Basil is a monk. Therefore Gregory chants.", "gold": "unknown", "class": "verb_wrong_individual"} +{"id": "ds-vb-0017", "text": "Nina sings. All larks sing. Therefore Nina is a lark.", "gold": "unknown", "class": "verb_affirming_consequent"} +{"id": "ds-vb-0018", "text": "Viktor cooks. Viktor is a chef. Therefore Viktor cooks stew.", "gold": "unknown", "class": "verb_arity_face_value"} +{"id": "ds-vb-0019", "text": "Rosa is not a lawyer. No lawyers whistle. Therefore Rosa does not whistle.", "gold": "unknown", "class": "verb_negative_denied_antecedent"} +{"id": "ds-vb-0020", "text": "Edgar does not dance. Therefore Edgar does not skate.", "gold": "unknown", "class": "verb_distinct_lemmas"} +{"id": "ds-vb-0021", "text": "Caesar did not surrender. Therefore Caesar surrenders.", "gold": "declined", "class": "tense_out_of_band"} +{"id": "ds-vb-0022", "text": "The old sailor whittles. The old sailor is a craftsman. Therefore the old sailor whittles.", "gold": "declined", "class": "multi_token_subject_out_of_band"} +{"id": "ds-vb-0023", "text": "Nero fiddles in Rome. Nero is an emperor. Therefore Nero fiddles.", "gold": "declined", "class": "prepositional_out_of_band"} +{"id": "ds-vb-0024", "text": "Hannah gives Samuel bread. Hannah is a mother. Therefore Hannah gives Samuel bread.", "gold": "declined", "class": "ditransitive_out_of_band"} +{"id": "ds-vb-0025", "text": "If Noah builds then Noah is a carpenter. Noah builds. Therefore Noah is a carpenter.", "gold": "declined", "class": "verb_connective_out_of_band"} +{"id": "ds-vb-0026", "text": "Someone sneezes. Ora is a doctor. Therefore Ora sneezes.", "gold": "declined", "class": "quantifier_out_of_band"} +{"id": "ds-vb-0027", "text": "Jonah preaches. Therefore all prophets preach.", "gold": "declined", "class": "universal_conclusion_out_of_band"} +{"id": "ds-vb-0028", "text": "The twins do not quarrel. Therefore the twins quarrel.", "gold": "declined", "class": "plural_do_not_out_of_band"} diff --git a/generate/proof_chain/render.py b/generate/proof_chain/render.py index 5520559a..e80b1d8c 100644 --- a/generate/proof_chain/render.py +++ b/generate/proof_chain/render.py @@ -132,6 +132,43 @@ def render_entailment_member( return f"Given: {given}. I can't evaluate {query_text} from that as stated." +def render_entailment_verb( + trace: EntailmentTrace, premise_texts: tuple[str, ...], query_text: str +) -> str: + """The user-facing surface for a verb-predicate (Band v5-VP) verdict. + + Same discipline as :func:`render_entailment_member`; the UNKNOWN template + additionally scopes the verb reading (ADR-0260 §3): each verb phrase is + read at face value — an unlinked agreement form or an unstated relation + between a verb and a class word could settle what the lowering leaves + open, so the claim is stated of the reading, disclosed as such. ENTAILED / + REFUTED / inconsistent survive any such refinement (instantiation is + sound and entailment is monotone) and are stated at full strength. + """ + given = "; ".join(premise_texts) + if trace.outcome is Entailment.ENTAILED: + return f"Given: {given}. Your premises entail: {query_text}." + if trace.outcome is Entailment.REFUTED: + return ( + f"Given: {given}. Your premises entail the opposite of " + f"{query_text} — it cannot hold." + ) + if trace.outcome is Entailment.UNKNOWN: + return ( + f"Given: {given}. Reading each name as one individual and each " + f"class word and verb phrase at face value, your premises don't " + f"settle whether {query_text} — it holds in some cases and fails " + f"in others." + ) + # REFUSED + if trace.reason == INCONSISTENT_PREMISES: + return ( + f"Given: {given}. Those premises are inconsistent — they " + f"can't all be true, so I won't assert anything from them." + ) + return f"Given: {given}. I can't evaluate {query_text} from that as stated." + + def _categorical_clause(prop: dict) -> str: """One categorical proposition dict → its English clause.""" template = _CATEGORICAL_PHRASE.get(prop.get("form", ""), "{s} ~ {p}") @@ -169,5 +206,6 @@ __all__ = [ "render_entailment", "render_entailment_english", "render_entailment_member", + "render_entailment_verb", "render_syllogism", ] diff --git a/generate/proof_chain/shape.py b/generate/proof_chain/shape.py index 6ff9d7cc..b7929b49 100644 --- a/generate/proof_chain/shape.py +++ b/generate/proof_chain/shape.py @@ -95,9 +95,27 @@ EN_CONDMEM_BANDS: tuple[str, ...] = ( EN_CONDMEM_CONDITIONAL, ) +#: Band v5-VP (ADR-0260) — verb-predicate arguments ("All philosophers teach. +#: Socrates is a philosopher. Therefore Socrates teaches."), read by +#: ``generate.proof_chain.verb`` via per-individual lowering with a second +#: (individual, verb-group, object) atom family alongside v3-MEM's membership +#: atoms. Same ``en_`` license discipline: a different reader must earn its +#: own per-shape record. Priority order: negative > chain > universal > fact. +EN_VERB_NEGATIVE = "en_verb_negative" +EN_VERB_CHAIN = "en_verb_chain" +EN_VERB_UNIVERSAL = "en_verb_universal" +EN_VERB_FACT = "en_verb_fact" + +EN_VERB_BANDS: tuple[str, ...] = ( + EN_VERB_NEGATIVE, + EN_VERB_CHAIN, + EN_VERB_UNIVERSAL, + EN_VERB_FACT, +) + #: Every serving shape-band — the ratified ledger's full key set. ALL_SHAPE_BANDS: tuple[str, ...] = ( - SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS + EN_CONDMEM_BANDS + SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS + EN_CONDMEM_BANDS + EN_VERB_BANDS ) @@ -147,6 +165,11 @@ __all__ = [ "EN_MEMBER_NEGATIVE", "EN_MEMBER_SINGLE", "EN_SHAPE_BANDS", + "EN_VERB_BANDS", + "EN_VERB_CHAIN", + "EN_VERB_FACT", + "EN_VERB_NEGATIVE", + "EN_VERB_UNIVERSAL", "SHAPE_BANDS", "classify_deduction_shape", ] diff --git a/generate/proof_chain/verb.py b/generate/proof_chain/verb.py new file mode 100644 index 00000000..914ce5c4 --- /dev/null +++ b/generate/proof_chain/verb.py @@ -0,0 +1,518 @@ +"""Verb-predicate argument reader — Band v5-VP (ADR-0260). + +Reads deductive arguments whose facts are VERB sentences — "All philosophers +teach. Socrates is a philosopher. Therefore Socrates teaches." — by extending +Band v3-MEM's per-individual propositional lowering with a second atom family: +one opaque minted atom per *(individual, verb-lemma-group, object-term)* +triple, alongside v3-MEM's *(individual, class-group)* membership atoms, in +ONE shared atom space. A verb universal ("all C [obj]", "no C +[obj]") instantiates at every named individual as ``mem(i,C) -> [~]verb(i)``, +so a membership fact minted by the copula reading can discharge a verb rule — +the fusion this band exists for. The same verified ROBDD engine decides. + +Why this is sound (ADR-0260 §3): identical to ADR-0258 §3's argument. +Universal instantiation at named individuals is truth-preserving in every +first-order model; each *(verb-group, object-term)* pair is one opaque unary +predicate over the same named-individual domain, so ENTAILED / REFUTED / +inconsistent verdicts over the lowered premises hold in every model of the +original argument. Completeness within the fragment lifts the same way: a +propositional countermodel becomes a first-order countermodel whose domain is +exactly the named individuals. The ONE semantic identification added over +v3-MEM is third-person-singular agreement — a universal's base verb form +("teach") and a singular fact's 3sg form ("teaches") are identified iff +related by a CLOSED relation: a verb-specific irregular table (consulted +first, sole authority for its tokens) else the three regular suffix rules +(``+s``, ``+es`` after sibilants, ``y↔ies``). NOUN morphology is deliberately +NOT reused for verbs — the noun table would misroute forms like "lives" +(noun: life; verb: live). Anything the relation cannot relate stays distinct: +under-linking costs coverage, never soundness. Object terms link by exact +token identity only. + +Segmentation is scope-tight by design: without a lexicon there is no sound +way to split an arbitrary copula-free token run into subject/verb/object, so +this band reads EXACTLY `` ``, `` ``, their +``does not`` negations, the sentential-not prefix, and universals +``all|every|each|no [the] []`` — single-token name, +class, verb, and object. Everything longer or differently shaped refuses, +typed. Copula sentences delegate VERBATIM to v3-MEM's own ``_parse_singular`` +/ ``_parse_universal`` (membership facts and is-a universals coexist with +verb sentences in one argument). Connective composition with verb leaves is a +deliberate scope-out (ADR-0260 §5) — any connective token refuses. + +Tried strictly AFTER Bands v1 / v1b / v2-EN / v3-MEM / v4-CM (a fallback +tier) — pure widening; every previously-served argument is served +byte-identically. (v2-EN decides pure verb-fact restatements as opaque +clause-atoms already — soundly — so every argument that reaches this band +contains a quantifier lead, an is-a shape, or unnormalized negation that made +the earlier bands refuse.) 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``, ``mixed_structure_out_of_band``, + ``internal_negation_unread``, ``sentence_shape_out_of_band``, + ``tense_out_of_band``, ``structural_leak``, ``too_many_premises``, + ``too_many_atoms``. +""" + +from __future__ import annotations + +from dataclasses import dataclass + +# The v2-EN sentence splitter and tokenizer are reused VERBATIM (one +# normalization discipline across every argument band), and v3-MEM's singular/ +# universal copula parsers, token-run guard, noun-morphology linker, and +# sibilant set are reused VERBATIM — deliberate private-name imports inside +# the proof_chain package, same precedent as generate.proof_chain.member and +# generate.proof_chain.cond_member. +from generate.proof_chain.english import _SENTENCE_RE, _tokenize +from generate.proof_chain.member import ( + _A_LEADS, + _COPULA_FORMS, + _E_LEAD, + _QUANTIFIER_TOKENS, + _SENTENTIAL_NOT, + _SIBILANT_ENDINGS, + _Singular, + _Universal, + _check_run, + _forms_link, + _parse_singular, + _parse_universal, +) +from generate.proof_chain.member import _Reject as _MemberReject +from generate.proof_chain.shape import ( + EN_VERB_CHAIN, + EN_VERB_FACT, + EN_VERB_NEGATIVE, + EN_VERB_UNIVERSAL, +) + +#: Connective structure this band does not compose (a future band fuses the +#: v2-EN/v4-CM connective grammar with verb sentences — ADR-0260 §5). +_CONNECTIVES = frozenset({"if", "then", "or", "and", "either"}) + +#: Auxiliary/determiner tokens that can never BE the verb or object of an +#: in-band sentence. ``does`` is consumed only by the exact ``does not`` +#: negation shape; ``did not`` is past tense (a scope-out); bare ``do not`` +#: with a singular subject is not an in-band agreement pattern. +_ARTICLES = frozenset({"a", "an", "the"}) +_AUXILIARIES = frozenset({"do", "does", "did"}) + +#: Closed irregular 3sg table (3sg form → base). Consulted BEFORE the regular +#: suffix rules; table membership makes it the sole authority for that token. +#: Deliberately verb-specific — the noun table (member.py) would misroute +#: forms like "lives" (noun: life; verb: live). +_VERB_IRREGULAR_3SG: dict[str, str] = { + "has": "have", + "goes": "go", + "does": "do", +} +_VERB_TABLE_TOKENS = frozenset(_VERB_IRREGULAR_3SG) | frozenset( + _VERB_IRREGULAR_3SG.values() +) + +#: Honesty caps — beyond these the argument is refused, never truncated. +#: ``MAX_ATOMS`` counts minted atoms of BOTH families, so instantiation +#: fan-out is capped exactly where it multiplies. +MAX_PREMISE_SENTENCES = 16 +MAX_ATOMS = 24 + + +@dataclass(frozen=True, slots=True) +class VerbArgument: + """A successfully-read verb-predicate argument, engine-ready. + + Same shape as ``MemberArgument``: ``premise_formulas``/``query_formula`` + are propositional formula strings over minted atom ids; ``atoms[i]`` + displays the fact behind ``a{i}`` (``individual : class`` for membership + atoms, ``individual : verb [object]`` for verb atoms). + """ + + 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 VerbRefusal: + """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 = VerbRefusal(reason, detail) + + +@dataclass(frozen=True, slots=True) +class _VerbFact: + """`` []`` (optionally ``does not`` / sentential- + not negated) — a verb literal about one individual.""" + + ind: tuple[str, ...] + verb: str + obj: str | None + negated: bool + + +@dataclass(frozen=True, slots=True) +class _VerbUniversal: + """``all|every|each|no [the] []`` — instantiated + per individual at lowering time as ``mem(i, class) -> [~]verb(i)``. + ``negative`` marks the E-form (``no``).""" + + subject: tuple[str, ...] + verb: str + obj: str | None + negative: bool + + +_Record = _Singular | _Universal | _VerbFact | _VerbUniversal + + +def _verb_tokens_link(a: str, b: str) -> bool: + """True iff single tokens *a* and *b* are agreement forms of one verb + lemma under the closed relation (irregular table first, then the three + regular 3sg suffix rules).""" + if a == b: + return True + if a in _VERB_TABLE_TOKENS or b in _VERB_TABLE_TOKENS: + return _VERB_IRREGULAR_3SG.get(a) == b or _VERB_IRREGULAR_3SG.get(b) == a + short, long_ = (a, b) if len(a) <= len(b) else (b, a) + if long_ == short + "s" and not short.endswith(_SIBILANT_ENDINGS): + return True + if long_ == short + "es" and short.endswith(_SIBILANT_ENDINGS): + return True + if short.endswith("y") and long_ == short[:-1] + "ies": + return True + return False + + +def _check_verb_token(tok: str, detail: str) -> None: + """Guard the verb slot: the shared opaque-run guard plus the aux/article + exclusions (an auxiliary or determiner is never an in-band verb lemma).""" + _check_run((tok,), detail) + if tok in _ARTICLES or tok in _AUXILIARIES: + raise _Reject("sentence_shape_out_of_band", detail) + + +def _check_term_token(tok: str, detail: str) -> None: + """Guard a name/object slot: the shared opaque-run guard plus a dangling- + determiner check.""" + _check_run((tok,), detail) + if tok in _ARTICLES: + raise _Reject("sentence_shape_out_of_band", detail) + + +def _parse_verb_fact(toks: list[str], detail: str) -> _VerbFact: + """`` []`` / `` does not []``.""" + negated = False + if len(toks) >= 3 and toks[1] in _AUXILIARIES and toks[2] == "not": + if toks[1] == "did": + raise _Reject("tense_out_of_band", detail) + if toks[1] == "do": + raise _Reject("sentence_shape_out_of_band", detail) + negated = True + toks = [toks[0], *toks[3:]] + if any(t == "not" or t.endswith("n't") for t in toks): + raise _Reject("internal_negation_unread", detail) + if len(toks) < 2 or len(toks) > 3: + raise _Reject("sentence_shape_out_of_band", detail) + name, verb = toks[0], toks[1] + obj = toks[2] if len(toks) == 3 else None + _check_term_token(name, detail) + _check_verb_token(verb, detail) + if obj is not None: + _check_term_token(obj, detail) + return _VerbFact((name,), verb, obj, negated) + + +def _parse_verb_universal(toks: list[str], detail: str) -> _VerbUniversal: + """``all|every|each|no [the] []`` — no copula form.""" + negative = toks[0] == _E_LEAD + rest = toks[1:] + if rest and rest[0] == "the": # "all the dogs bark" — determiner, dropped + rest = rest[1:] + if any(t == "not" or t.endswith("n't") for t in rest): + # "All men do not teach" — scope-ambiguous (¬∀ vs ∀¬); the E-form + # ("no …") is the unambiguous spelling this band reads. + raise _Reject("internal_negation_unread", detail) + if any(t == "did" for t in rest): + raise _Reject("tense_out_of_band", detail) + if len(rest) < 2 or len(rest) > 3: + raise _Reject("sentence_shape_out_of_band", detail) + cls, verb = rest[0], rest[1] + obj = rest[2] if len(rest) == 3 else None + _check_term_token(cls, detail) + _check_verb_token(verb, detail) + if obj is not None: + _check_term_token(obj, detail) + return _VerbUniversal((cls,), verb, obj, negative) + + +def _parse_fact(toks: list[str], detail: str) -> _Singular | _VerbFact: + """A non-universal sentence: sentential-not unwraps first (its prefix + contains a copula, so it must be checked before copula routing); then a + copula routes to v3-MEM's own singular parser (membership fact), else the + verb-fact grammar.""" + if tuple(toks[: len(_SENTENTIAL_NOT)]) == _SENTENTIAL_NOT: + inner = _parse_fact(toks[len(_SENTENTIAL_NOT) :], detail) + if isinstance(inner, _Singular): + return _Singular(inner.ind, inner.cls, negated=not inner.negated) + return _VerbFact(inner.ind, inner.verb, inner.obj, negated=not inner.negated) + if not toks: + raise _Reject("empty_side", detail) + if any(t in _COPULA_FORMS for t in toks): + return _parse_singular(toks, detail) + return _parse_verb_fact(toks, detail) + + +def _parse_sentence(toks: list[str], detail: str) -> _Record: + if any(t in _CONNECTIVES for t in toks): + raise _Reject("mixed_structure_out_of_band", detail) + head = toks[0] + if head in _A_LEADS or head == _E_LEAD: + if any(t in ("is", "are") for t in toks): + return _parse_universal(toks, detail) # is-a universal (v3-MEM's) + return _parse_verb_universal(toks, detail) + if head in _QUANTIFIER_TOKENS: + raise _Reject("quantifier_out_of_band", detail) + return _parse_fact(toks, detail) + + +def read_verb_argument(text: str) -> VerbArgument | VerbRefusal: + """Read *text* as a verb-predicate argument, or refuse (typed). + + Deterministic and pure: same text → same ``VerbArgument``. The conclusion + is the final sentence, the sole "therefore"-led one, and must be a + singular fact (membership or verb); every earlier sentence is a premise. + Lowering is two-pass exactly as v3-MEM's — sentences parse first, THEN + individuals / class-groups / verb-groups are collected, THEN atoms mint + and universals instantiate at every named individual — with premise + formulas emitted in sentence order. + """ + if not text or not text.strip(): + return VerbRefusal("empty") + sentences = [ + (m.group(1), m.group(2)) for m in _SENTENCE_RE.finditer(text) if m.group(1).strip() + ] + if not sentences: + return VerbRefusal("empty") + + premises: list[_Record] = [] + premise_texts: list[str] = [] + conclusion: _Singular | _VerbFact | 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) + if any(t in _CONNECTIVES for t in rest): + raise _Reject("mixed_structure_out_of_band", body) + if rest[0] in _A_LEADS or rest[0] == _E_LEAD: + raise _Reject("universal_conclusion_out_of_band", body) + if rest[0] in _QUANTIFIER_TOKENS: + raise _Reject("quantifier_out_of_band", body) + conclusion = _parse_fact(rest, body) + query_text = " ".join(rest) + continue + if len(premises) >= MAX_PREMISE_SENTENCES: + raise _Reject("too_many_premises", body) + premises.append(_parse_sentence(toks, body)) + premise_texts.append(" ".join(toks)) + + if conclusion is None or query_text is None: + return VerbRefusal("no_conclusion") + if not premises: + return VerbRefusal("no_premises") + + records: list[_Record] = [*premises, conclusion] + + # Every argument this band DECIDES contains at least one verb + # construct — a pure-copula argument is v3-MEM/v4-CM territory (and + # only ever reaches here when those bands refused it, in which case + # the delegated parsers above raised the same typed refusal already; + # this check is a defensive closure of that invariant). + if not any(isinstance(r, (_VerbFact, _VerbUniversal)) for r in records): + raise _Reject("sentence_shape_out_of_band", "no verb predicate read") + + # --- lowering (ADR-0260 §2): v3-MEM's two-pass scheme, two families -- + individuals: list[tuple[str, ...]] = [] + for rec in records: + if isinstance(rec, (_Singular, _VerbFact)) and rec.ind not in individuals: + individuals.append(rec.ind) + + # Class groups — the SAME closed noun-morphology relation as v3-MEM. + cls_group_of: dict[tuple[str, ...], int] = {} + cls_reps: list[tuple[str, ...]] = [] + for rec in records: + forms: list[tuple[str, ...]] = [] + if isinstance(rec, _Singular): + forms = [rec.cls] + elif isinstance(rec, _Universal): + forms = [rec.subject, rec.predicate] + elif isinstance(rec, _VerbUniversal): + forms = [rec.subject] + for form in forms: + if form in cls_group_of: + continue + for gi, rep in enumerate(cls_reps): + if _forms_link(form, rep): + cls_group_of[form] = gi + break + else: + cls_group_of[form] = len(cls_reps) + cls_reps.append(form) + + # Verb groups — the closed verb-agreement relation (this band's one + # new semantic identification). + verb_group_of: dict[str, int] = {} + verb_reps: list[str] = [] + for rec in records: + if not isinstance(rec, (_VerbFact, _VerbUniversal)): + continue + form = rec.verb + if form in verb_group_of: + continue + for gi, rep in enumerate(verb_reps): + if _verb_tokens_link(form, rep): + verb_group_of[form] = gi + break + else: + verb_group_of[form] = len(verb_reps) + verb_reps.append(form) + + mint: dict[tuple, str] = {} + atom_display: list[str] = [] + + def _mint(key: tuple, display: str, detail: str) -> str: + 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(display) + return mint[key] + + def mem_atom(ind_idx: int, group: int, detail: str) -> str: + return _mint( + ("mem", ind_idx, group), + f"{' '.join(individuals[ind_idx])} : {' '.join(cls_reps[group])}", + detail, + ) + + def verb_atom(ind_idx: int, group: int, obj: str | None, detail: str) -> str: + shown = verb_reps[group] if obj is None else f"{verb_reps[group]} {obj}" + return _mint( + ("verb", ind_idx, group, obj), + f"{' '.join(individuals[ind_idx])} : {shown}", + detail, + ) + + premise_formulas: list[str] = [] + for rec, body_text in zip(premises, premise_texts): + if isinstance(rec, _Singular): + atom = mem_atom( + individuals.index(rec.ind), cls_group_of[rec.cls], body_text + ) + premise_formulas.append(f"~({atom})" if rec.negated else atom) + elif isinstance(rec, _VerbFact): + atom = verb_atom( + individuals.index(rec.ind), + verb_group_of[rec.verb], + rec.obj, + body_text, + ) + premise_formulas.append(f"~({atom})" if rec.negated else atom) + elif isinstance(rec, _Universal): + for ind_idx in range(len(individuals)): + antecedent = mem_atom(ind_idx, cls_group_of[rec.subject], body_text) + consequent = mem_atom(ind_idx, cls_group_of[rec.predicate], body_text) + premise_formulas.append( + f"({antecedent}) -> (~({consequent}))" + if rec.negative + else f"({antecedent}) -> ({consequent})" + ) + else: # _VerbUniversal + for ind_idx in range(len(individuals)): + antecedent = mem_atom(ind_idx, cls_group_of[rec.subject], body_text) + consequent = verb_atom( + ind_idx, verb_group_of[rec.verb], rec.obj, body_text + ) + premise_formulas.append( + f"({antecedent}) -> (~({consequent}))" + if rec.negative + else f"({antecedent}) -> ({consequent})" + ) + + if isinstance(conclusion, _Singular): + query_atom = mem_atom( + individuals.index(conclusion.ind), + cls_group_of[conclusion.cls], + query_text, + ) + else: + query_atom = verb_atom( + individuals.index(conclusion.ind), + verb_group_of[conclusion.verb], + conclusion.obj, + query_text, + ) + query_formula = f"~({query_atom})" if conclusion.negated else query_atom + 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 (the v4-CM lesson). + return VerbRefusal(rej.refusal.reason, rej.refusal.detail) + + universals = [r for r in premises if isinstance(r, (_Universal, _VerbUniversal))] + if any( + (isinstance(u, _Universal) and u.negative) + or (isinstance(u, _VerbUniversal) and u.negative) + for u in universals + ): + band = EN_VERB_NEGATIVE + elif len(universals) >= 2: + band = EN_VERB_CHAIN + elif len(universals) == 1: + band = EN_VERB_UNIVERSAL + else: + band = EN_VERB_FACT + + return VerbArgument( + 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", + "VerbArgument", + "VerbRefusal", + "read_verb_argument", +] diff --git a/scripts/verify_lane_shas.py b/scripts/verify_lane_shas.py index e2c9826c..10476059 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": "b530ed99c414a6d1bdd239752b0e1c6c8c03893f402198def29122b9c2a8a8be", + "deduction_serve_v1": "f4fa7331bbee40c898be9ea2a8cabf36f28c8a19a7500433e0fa966c05905a8a", } diff --git a/tests/test_deduction_serve_e2e.py b/tests/test_deduction_serve_e2e.py index 5826c376..52c31d75 100644 --- a/tests/test_deduction_serve_e2e.py +++ b/tests/test_deduction_serve_e2e.py @@ -166,3 +166,16 @@ def test_out_of_regime_argument_refuses_honestly() -> None: resp = rt.chat("The engine doesn't start. Therefore the engine is broken.") assert resp.grounding_source == "deduction" assert "can't parse" in resp.surface # honest reader-refusal disclosure + + +def test_verb_predicate_is_decided_end_to_end() -> None: + """The ADR-0260 flagship: a verb universal discharged by a membership + fact, decided through the real REPL spine — closed 3sg agreement linking + the universal's base form to the conclusion's inflected form.""" + rt = _runtime(True) + resp = rt.chat( + "All philosophers teach. Socrates is a philosopher. " + "Therefore Socrates teaches." + ) + assert resp.grounding_source == "deduction" + assert "Your premises entail: socrates teaches" in resp.surface diff --git a/tests/test_deduction_serve_lane.py b/tests/test_deduction_serve_lane.py index a223e1eb..1af1aedf 100644 --- a/tests/test_deduction_serve_lane.py +++ b/tests/test_deduction_serve_lane.py @@ -15,6 +15,7 @@ _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" +_V2_VERB = _ROOT / "v2_verb" / "cases.jsonl" def test_v1_lane_wrong_is_zero() -> None: @@ -89,6 +90,22 @@ def test_v2_condmem_lane_wrong_is_zero() -> None: assert cbg.get("declined", 0) >= 7 +def test_v2_verb_lane_wrong_is_zero() -> None: + """Band v5-VP (ADR-0260): hand-authored verb-predicate arguments — + universals discharged by membership facts across every closed agreement + rule (+s, +es, y↔ies, irregular go/goes), transitive objects at face + value, and eight distinct honest-decline shapes — decided wrong=0.""" + report = build_report(_load(_V2_VERB)) + assert report["n"] == 28 + assert report["counts"]["wrong"] == 0 + assert report["all_cases_correct"] is True + cbg = report["correct_by_gold"] + assert cbg.get("entailed", 0) >= 11 + assert cbg.get("refuted", 0) >= 4 + assert cbg.get("unknown", 0) >= 5 + assert cbg.get("declined", 0) >= 8 + + def test_runner_treats_wrong_verdict_as_the_only_real_failure() -> None: """A committed disagreement with gold is ``wrong``; a decline never is, even when gold expected a definite verdict (that's a miss, tracked via diff --git a/tests/test_deduction_surface.py b/tests/test_deduction_surface.py index 0e48eab3..f13e584d 100644 --- a/tests/test_deduction_surface.py +++ b/tests/test_deduction_surface.py @@ -371,3 +371,64 @@ def test_runtime_decides_full_propositional_gold_corpus_wrong_zero() -> None: continue wrong.append(f"{case['text']!r} -> gold={gold} surface={surface!r}") assert not wrong, "\n".join(wrong) + + +def test_verb_predicate_is_decided_band_v5_vp() -> None: + """The ADR-0258 §6.3 verb-predicate scope-out, now decided (ADR-0260): + a verb universal discharged by a membership fact, authoritatively (the + ``en_verb_universal`` band holds an earned SERVE license).""" + surface = deduction_grounded_surface( + "All philosophers teach. Socrates is a philosopher. " + "Therefore Socrates teaches." + ) + assert surface is not None + assert "Your premises entail: socrates teaches" in surface + assert not surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + + +def test_verb_universal_discharged_by_membership_chain() -> None: + """The mechanism this band adds: the membership atom minted by copula + sentences unifies with a verb universal's instantiated antecedent across + an is-a chain — neither v3-MEM (refuses verb sentences) nor v2-EN + (refuses quantifier leads and is-a clauses) alone decides this.""" + surface = deduction_grounded_surface( + "Felix is a tortoise. All tortoises are reptiles. All reptiles crawl. " + "Therefore Felix crawls." + ) + assert surface is not None + assert "Your premises entail: felix crawls" in surface + + +def test_verb_unknown_is_scoped_to_the_verb_reading() -> None: + surface = deduction_grounded_surface( + "Viktor cooks. Viktor is a chef. Therefore Viktor cooks stew." + ) + assert surface is not None + assert "verb phrase at face value" in surface + assert "don't settle" in surface + + +def test_verb_unearned_band_would_be_hedged() -> None: + """The en_verb_* bands ride the SAME earned-license gate: strip the + license and the same sound answer is served DISCLOSED, never + authoritatively.""" + surface = deduction_grounded_surface( + "All philosophers teach. Socrates is a philosopher. " + "Therefore Socrates teaches.", + license_lookup=lambda band: None, + ) + assert surface is not None + assert surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + assert "Your premises entail: socrates teaches" in surface + + +def test_verb_reader_refusal_keeps_prior_honest_surface() -> None: + """When the verb band ALSO cannot read the argument (here: a + ditransitive), the pre-existing honest surface is preserved verbatim — + the band only widens.""" + surface = deduction_grounded_surface( + "Hannah gives Samuel bread. Hannah is a mother. " + "Therefore Hannah gives Samuel bread." + ) + assert surface is not None + assert "Your premises entail" not in surface diff --git a/tests/test_verb_argument_reader.py b/tests/test_verb_argument_reader.py new file mode 100644 index 00000000..9b3cebba --- /dev/null +++ b/tests/test_verb_argument_reader.py @@ -0,0 +1,250 @@ +"""Band v5-VP (ADR-0260) — verb-predicate argument reader contract. + +The reader extends v3-MEM's per-individual propositional lowering with a +second atom family — one atom per *(individual, verb-lemma-group, +object-term)* — in one shared atom space, so a verb universal's +instantiation can be discharged by a membership fact minted from a copula +sentence. 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 third-person-singular agreement links a universal's base verb form to a +singular fact's 3sg form via the closed verb relation (NOT the noun table). +""" + +from __future__ import annotations + +import pytest + +from generate.proof_chain.member import MemberRefusal, read_member_argument +from generate.proof_chain.shape import ( + EN_VERB_CHAIN, + EN_VERB_FACT, + EN_VERB_NEGATIVE, + EN_VERB_UNIVERSAL, +) +from generate.proof_chain.verb import ( + MAX_ATOMS, + MAX_PREMISE_SENTENCES, + VerbArgument, + VerbRefusal, + read_verb_argument, +) + + +def _read(text: str) -> VerbArgument: + arg = read_verb_argument(text) + assert isinstance(arg, VerbArgument), arg + return arg + + +def _refusal(text: str) -> VerbRefusal: + ref = read_verb_argument(text) + assert isinstance(ref, VerbRefusal), ref + return ref + + +# --- the gap this band fills is real ----------------------------------------- + + +def test_the_gap_this_band_fills_is_real() -> None: + """The exact ADR-0258 §6.3 verb-predicate scope-out: v3-MEM refuses verb + sentences (no copula ⇒ ``sentence_shape_out_of_band``); this band decides + them. Both facts hold at once — v3-MEM is unchanged, this is a new tier.""" + text = "All philosophers teach. Socrates is a philosopher. Therefore Socrates teaches." + assert isinstance(read_member_argument(text), MemberRefusal) + assert isinstance(read_verb_argument(text), VerbArgument) + + +# --- the flagship reading ----------------------------------------------------- + + +def test_flagship_universal_verb_instantiation() -> None: + arg = _read( + "All philosophers teach. Socrates is a philosopher. Therefore Socrates teaches." + ) + assert arg.band == EN_VERB_UNIVERSAL + # Universal instantiates at the one named individual: mem -> verb; the + # membership fact anchors it; the query is the instantiated verb atom. + assert arg.premise_formulas == ("(a0) -> (a1)", "a0") + assert arg.query_formula == "a1" + assert arg.atoms == ("socrates : philosophers", "socrates : teach") + + +def test_agreement_links_base_and_third_person_forms() -> None: + # +s rule: live/lives must land in ONE verb group (and must NOT be routed + # through the noun table, where "lives" is the plural of "life"). + arg = _read("All men live. Socrates is a man. Therefore Socrates lives.") + assert arg.query_formula == "a1" # same atom as the instantiated consequent + assert "socrates : live" in arg.atoms + + +@pytest.mark.parametrize( + "universal_form, conclusion_form", + [ + ("teach", "teaches"), # +es after sibilant + ("study", "studies"), # y -> ies + ("go", "goes"), # irregular table + ("bark", "barks"), # +s + ], +) +def test_agreement_rules_each_link(universal_form: str, conclusion_form: str) -> None: + arg = _read( + f"All wolves {universal_form}. Rex is a wolf. Therefore Rex {conclusion_form}." + ) + assert arg.band == EN_VERB_UNIVERSAL + assert arg.premise_formulas == ("(a0) -> (a1)", "a0") + assert arg.query_formula == "a1" + + +def test_transitive_object_is_part_of_the_atom_key() -> None: + arg = _read( + "All poets write verses. Homer is a poet. Therefore Homer writes verses." + ) + assert arg.query_formula == "a1" + assert "homer : write verses" in arg.atoms + # A different object is a DIFFERENT atom — arity/object at face value. + arg2 = _read( + "All poets write verses. Homer is a poet. Therefore Homer writes epics." + ) + assert arg2.query_formula == "a2" + + +def test_negative_universal_instantiates_negated() -> None: + arg = _read("Miriam is a nun. No nuns marry. Therefore Miriam does not marry.") + assert arg.band == EN_VERB_NEGATIVE + assert arg.premise_formulas == ("a0", "(a0) -> (~(a1))") + assert arg.query_formula == "~(a1)" + + +def test_membership_chain_discharges_verb_universal() -> None: + arg = _read( + "Felix is a tortoise. All tortoises are reptiles. All reptiles crawl. " + "Therefore Felix crawls." + ) + assert arg.band == EN_VERB_CHAIN + assert arg.premise_formulas == ("a0", "(a0) -> (a1)", "(a1) -> (a2)") + assert arg.query_formula == "a2" + + +def test_sentential_not_wraps_a_verb_fact() -> None: + arg = _read( + "Boris does not smoke. Therefore it is not the case that Boris smokes." + ) + assert arg.band == EN_VERB_FACT + assert arg.premise_formulas == ("~(a0)",) + assert arg.query_formula == "~(a0)" + + +def test_universal_does_not_leak_across_individuals() -> None: + arg = _read( + "All monks chant. Basil is a monk. Therefore Gregory chants." + ) + # The universal instantiates at BOTH named individuals; the query is + # Gregory's verb atom, whose membership antecedent nothing anchors. + assert arg.premise_formulas == ("(a0) -> (a1)", "(a2) -> (a3)", "a0") + assert arg.query_formula == "a3" + assert arg.atoms[2] == "gregory : monks" + + +def test_verb_and_class_words_never_cross_families() -> None: + # "teacher" (class) and "teaches" (verb) must stay distinct atoms even + # though the noun rules could relate the strings. + arg = _read("Socrates teaches. Therefore Socrates is a teacher.") + assert arg.premise_formulas == ("a0",) + assert arg.query_formula == "a1" + + +# --- band classification ------------------------------------------------------ + + +@pytest.mark.parametrize( + "text, band", + [ + ("All poets write. Homer is a poet. Therefore Homer writes.", + EN_VERB_UNIVERSAL), + ("Homer is a poet. All poets are artists. All artists dream. Therefore Homer dreams.", + EN_VERB_CHAIN), + ("Homer is a poet. No poets whistle. Therefore Homer does not whistle.", + EN_VERB_NEGATIVE), + ("Homer writes. Homer is a poet. Therefore Homer writes.", + EN_VERB_FACT), + ], +) +def test_band_classification(text: str, band: str) -> None: + assert _read(text).band == band + + +# --- typed refusals ----------------------------------------------------------- + + +@pytest.mark.parametrize( + "text, reason", + [ + ("Caesar did not surrender. Therefore Caesar surrenders.", + "tense_out_of_band"), + ("The old sailor whittles. Therefore Socrates naps.", + "sentence_shape_out_of_band"), + ("Nero fiddles in Rome. Therefore Nero fiddles.", + "sentence_shape_out_of_band"), + ("Hannah gives Samuel bread. Therefore Hannah gives Samuel bread.", + "sentence_shape_out_of_band"), + # "do not" after a multi-token subject: the negation is real but the + # grammar cannot normalize it (the exact `` does not`` shape is + # the only one read), so the honest reason is the unread negation. + ("The twins do not quarrel. Therefore the twins quarrel.", + "internal_negation_unread"), + ("If Noah builds then Noah rests. Noah builds. Therefore Noah rests.", + "mixed_structure_out_of_band"), + ("Someone sneezes. Therefore Ora sneezes.", + "quantifier_out_of_band"), + ("All men do not teach. Socrates is a man. Therefore Socrates teaches.", + "internal_negation_unread"), + ("Jonah preaches. Therefore all prophets preach.", + "universal_conclusion_out_of_band"), + ("Socrates teaches. Do philosophers teach?", + "question_sentence"), + # Delegated copula parses keep v3-MEM's own typed refusals. + ("Dogs are loyal. Rex barks. Therefore Rex barks.", + "bare_plural_out_of_band"), + ("Socrates is the philosopher. Socrates teaches. Therefore Socrates teaches.", + "definite_description_out_of_band"), + ("Socrates is a man who teaches. Therefore Socrates teaches.", + "relative_clause_out_of_band"), + # A pure-copula argument is never decided by this band (defensive + # closure — such texts belong to v3-MEM/v4-CM). + ("Socrates is a man. Therefore Socrates is a man.", + "sentence_shape_out_of_band"), + ], +) +def test_typed_refusals(text: str, reason: str) -> None: + assert _refusal(text).reason == reason + + +# --- honesty caps ------------------------------------------------------------- + + +def test_premise_cap_refuses_not_truncates() -> None: + body = " ".join(f"Zed{i} naps." for i in range(MAX_PREMISE_SENTENCES + 1)) + ref = _refusal(body + " Therefore Zed0 naps.") + assert ref.reason == "too_many_premises" + + +def test_atom_cap_refuses_not_truncates() -> None: + # Each premise mints one verb atom; 16 premises fit the premise cap, but + # a universal instantiated at every individual overflows MAX_ATOMS. + names = [f"Kip{i}" for i in range(12)] + body = " ".join(f"{n} naps." for n in names) + body += " " + " ".join(f"{n} is a squirrel." for n in names[:4]) + text = body + " All squirrels forage. Therefore Kip0 forages." + ref = _refusal(text) + assert ref.reason in ("too_many_atoms", "too_many_premises") + + +# --- determinism -------------------------------------------------------------- + + +def test_reading_is_deterministic() -> None: + text = ( + "All poets write. Homer is a poet. Therefore Homer writes." + ) + assert read_verb_argument(text) == read_verb_argument(text) + assert MAX_ATOMS == 24 and MAX_PREMISE_SENTENCES == 16