e84c0e8428
Completes the all/no/some square. `some` is read for the first time: "All mammals are vertebrates. Some whales are mammals. Therefore some whales are vertebrates." is decided entailed; "All unicorns are horned. Therefore some unicorns are horned." is decided unsettled, with the no-existential-import reading disclosed in the surface. Mechanism (generate/proof_chain/exist.py): v5-VP's per-individual lowering over a domain widened by one Skolem witness per existential premise and — the load-bearing part — one ARBITRARY element per existential conclusion, at which every universal still instantiates and about which no premise asserts anything. Refuting an existential means deriving a universal, and the arbitrary element is what makes that derivation genuine instead of an assumption of domain closure: without it "Rex is a wolf. Rex is not tame. Therefore some wolves are tame." reads as REFUTED from a domain of one wolf. With it, UNKNOWN. Four `en_exist_*` bands earned SERVE at 720x wrong=0 on the first arena seal (25-band ledger); the 32-case hand-authored v2_exist split passed 32/32 first run; full lane 166/166 wrong=0 across six splits. Also fixes a wrong-answer path this work uncovered in Band v1b (ADR-0261 §5.1): `to_syllogism` FILTERED premises it could not express out of the projection and answered from the remainder, so "Aristotle is a philosopher. All philosophers are scholars. Therefore some scholars are philosophers." lost its only witness and was served "that doesn't follow". It now refuses — matching its propositional sibling `to_deductive_logic`, which always has — and the argument falls through to the bands that can hold a singular fact. The categorical band re-earned SERVE 720/720 after the change; both examples are pinned as regression cases. Promotion: `ds-mem-0020` declined -> unknown (ADR-0258's existential scope-out, now read; an anonymous witness never transfers to a named individual, so UNKNOWN is its honest verdict, not entailed). [Verification]: core test --suite deductive 232 passed; reader tests 33/33; register+surface tests 52 passed; arena 25 bands x 720 wrong=0 (all SERVE); lane 166/166 wrong=0; lane SHAs 9/10 match (public_demo drift is pre-existing on the base commit and unrelated — evidence in the Tier-S brief).
1219 lines
61 KiB
Python
1219 lines
61 KiB
Python
"""Practice gold lane for the deduction-serve arc (Phase 3, ADR-0256).
|
||
|
||
The second concrete instance of the ADR-0199 cross-domain learning arena
|
||
(GSM8K math is the first). It measures the FULL serving pipeline
|
||
(reader → projector → ROBDD engine) per propositional shape-band, so the
|
||
reliability gate can earn a per-band SERVE license.
|
||
|
||
What is measured (and why it is not circular): the ROBDD engine is
|
||
sound+complete by construction — it is never wrong on the problem it is
|
||
given. The FALLIBLE part is the reader/projector: a template-based reader
|
||
can misparse a natural-language argument and hand the engine the *wrong*
|
||
problem, which it then soundly decides — a wrong served answer. This arena's
|
||
gold is authored **by construction** from the template that generated each
|
||
case (independent of the reader — ADR-0199 L-2), so a misread is caught as a
|
||
``wrong``. A band earns SERVE only when the whole pipeline reads AND decides
|
||
that shape correctly at volume.
|
||
|
||
Deterministic + synthetic: atoms are indexed (``no clock, no randomness``);
|
||
each band mixes entailed/refuted/unknown gold so reliability measures decision
|
||
correctness across outcomes, not just how many entailments pass through.
|
||
|
||
Sized to the SERVE volume floor: a perfect record clears θ_SERVE=0.99 only at
|
||
``n/(n+z²) ≥ 0.99`` (z=2.576) ⇒ ``n ≥ 657`` committed. ``CASES_PER_BAND``
|
||
exceeds that so each in-band shape earns the license honestly by volume.
|
||
"""
|
||
|
||
from __future__ import annotations
|
||
|
||
from dataclasses import dataclass, field
|
||
from typing import Any
|
||
|
||
from core.learning_arena.protocols import Problem
|
||
from generate.meaning_graph.projectors import to_deductive_logic, to_syllogism
|
||
from generate.meaning_graph.reader import Comprehension, comprehend
|
||
from generate.proof_chain.categorical import CategoricalError, decide_syllogism
|
||
from generate.proof_chain.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.exist import ExistArgument, read_exist_argument
|
||
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,
|
||
CONDITIONAL_CHAIN,
|
||
CONDITIONAL_SINGLE,
|
||
DISJUNCTIVE,
|
||
EN_ATOMIC,
|
||
EN_CONDITIONAL_CHAIN,
|
||
EN_CONDITIONAL_SINGLE,
|
||
EN_CONDMEM_CHAIN,
|
||
EN_CONDMEM_CONDITIONAL,
|
||
EN_CONDMEM_DISJUNCTIVE,
|
||
EN_CONDMEM_FUSED,
|
||
EN_DISJUNCTIVE,
|
||
EN_EXIST_CHAIN,
|
||
EN_EXIST_NEGATIVE,
|
||
EN_EXIST_UNIVERSAL,
|
||
EN_EXIST_WITNESS,
|
||
EN_MEMBER_ATOMIC,
|
||
EN_MEMBER_CHAIN,
|
||
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"
|
||
|
||
#: Cases per shape-band. ≥657 lets a perfect record clear the θ_SERVE=0.99
|
||
#: Wilson floor; a comfortable margin above it so the earned license is
|
||
#: unambiguous. Split across the band's gold-outcome templates.
|
||
CASES_PER_BAND = 720
|
||
|
||
#: A deterministic pool of single-token, non-reserved, identifier-safe atom
|
||
#: names. Indexed selection varies the argument per case (distinct problems),
|
||
#: with no clock/RNG. Three distinct atoms per case is always enough for the
|
||
#: templates below.
|
||
_ATOM_POOL: tuple[str, ...] = tuple(f"x{i}" for i in range(3, 300))
|
||
|
||
|
||
def _atoms(index: int, count: int) -> tuple[str, ...]:
|
||
"""``count`` distinct atoms for case ``index`` — deterministic, no overlap."""
|
||
base = (index * 3) % (len(_ATOM_POOL) - count)
|
||
return tuple(_ATOM_POOL[base + j] for j in range(count))
|
||
|
||
|
||
#: Each band's gold templates: (gold_outcome, text_builder). A builder takes the
|
||
#: distinct atoms and returns the natural-language argument text. Every template's
|
||
#: gold is TRUE BY CONSTRUCTION — the logical form guarantees it, verified against
|
||
#: the independent oracle at generation time (see ``_assert_sound`` below).
|
||
_TEMPLATES: dict[str, tuple[tuple[str, Any], ...]] = {
|
||
CONDITIONAL_SINGLE: (
|
||
("entailed", lambda a, b, c: f"If {a} then {b}. {a}. Therefore {b}."),
|
||
("refuted", lambda a, b, c: f"If {a} then {b}. {a}. Therefore not {b}."),
|
||
("unknown", lambda a, b, c: f"If {a} then {b}. Therefore {a}."),
|
||
),
|
||
CONDITIONAL_CHAIN: (
|
||
("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a}. Therefore {c}."),
|
||
("refuted", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a}. Therefore not {c}."),
|
||
("unknown", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. Therefore {c}."),
|
||
),
|
||
DISJUNCTIVE: (
|
||
("entailed", lambda a, b, c: f"{a} or {b}. Not {a}. Therefore {b}."),
|
||
("refuted", lambda a, b, c: f"{a} or {b}. Not {a}. Therefore {a}."),
|
||
("unknown", lambda a, b, c: f"{a} or {b}. Therefore {a}."),
|
||
),
|
||
ATOMIC: (
|
||
("entailed", lambda a, b, c: f"{a}. Therefore {a}."),
|
||
("refuted", lambda a, b, c: f"{a}. Therefore not {a}."),
|
||
# No genuine 'unknown' atomic argument exists over a single premise
|
||
# (a bare atom either restates or contradicts); the band is 2/3 the size
|
||
# of the others, still well above the volume floor.
|
||
),
|
||
# Categorical (syllogism). Terms are synthetic PLURAL class nouns (``x3s`` →
|
||
# the reader singularizes to ``x3``); ``a, b, c`` are the three distinct
|
||
# middle/subject/predicate classes. Gold is the unconditional validity (modern
|
||
# reading) of the standard form — cross-checked against the INDEPENDENT
|
||
# syllogism oracle in ``assert_corpus_sound``.
|
||
CATEGORICAL: (
|
||
# Barbara (AAA) — valid.
|
||
("valid", lambda a, b, c: f"All {a}s are {b}s. All {c}s are {a}s. Therefore all {c}s are {b}s."),
|
||
# Celarent (EAE) — valid.
|
||
("valid", lambda a, b, c: f"No {a}s are {b}s. All {c}s are {a}s. Therefore no {c}s are {b}s."),
|
||
# Darii (AII) — valid.
|
||
("valid", lambda a, b, c: f"All {a}s are {b}s. Some {c}s are {a}s. Therefore some {c}s are {b}s."),
|
||
# Ferio (EIO) — valid.
|
||
("valid", lambda a, b, c: f"No {a}s are {b}s. Some {c}s are {a}s. Therefore some {c}s are not {b}s."),
|
||
# Undistributed middle (AAA-2) — INVALID.
|
||
("invalid", lambda a, b, c: f"All {b}s are {a}s. All {c}s are {a}s. Therefore all {c}s are {b}s."),
|
||
# Existential-import overreach — INVALID in the modern reading.
|
||
("invalid", lambda a, b, c: f"All {a}s are {b}s. All {a}s are {c}s. Therefore some {c}s are {b}s."),
|
||
),
|
||
}
|
||
|
||
|
||
# --- Band v2-EN (ADR-0257): English-clause synthetic corpus -------------------
|
||
#
|
||
# Deterministic copular-clause lexicon: 20 subjects × 12 states = 240 distinct
|
||
# clauses ("the alarm is armed", …). Negation is the copular form the English
|
||
# reader normalizes ("the alarm is not armed" → ``~atom``), so the corpus
|
||
# exercises the negation machinery (modus tollens, disjunctive syllogism), not
|
||
# just affirmative flows. Content is synthetic ON PURPOSE — the reader is
|
||
# content-blind (opaque atoms), so the license certifies STRUCTURAL fidelity per
|
||
# shape; hand-authored real-English cases live in the eval lane
|
||
# (``evals/deduction_serve/v2_en``) to keep the synthetic corpus honest.
|
||
|
||
_EN_SUBJECTS: tuple[str, ...] = (
|
||
"the alarm", "the door", "the light", "the valve", "the engine",
|
||
"the fan", "the screen", "the sensor", "the pump", "the relay",
|
||
"the switch", "the heater", "the camera", "the router", "the beacon",
|
||
"the latch", "the motor", "the buzzer", "the gate", "the lamp",
|
||
)
|
||
_EN_STATES: tuple[str, ...] = (
|
||
"on", "off", "open", "closed", "armed", "active",
|
||
"locked", "ready", "hot", "cold", "live", "set",
|
||
)
|
||
_EN_CLAUSE_COUNT = len(_EN_SUBJECTS) * len(_EN_STATES)
|
||
|
||
|
||
def _en_clause(slot: int) -> str:
|
||
subject = _EN_SUBJECTS[slot % len(_EN_SUBJECTS)]
|
||
state = _EN_STATES[(slot // len(_EN_SUBJECTS)) % len(_EN_STATES)]
|
||
return f"{subject} is {state}"
|
||
|
||
|
||
def _en_clauses(index: int, count: int) -> tuple[str, ...]:
|
||
"""``count`` distinct clauses for case ``index`` — deterministic, no RNG."""
|
||
base = (index * 7) % (_EN_CLAUSE_COUNT - count)
|
||
return tuple(_en_clause(base + j) for j in range(count))
|
||
|
||
|
||
def _en_neg(clause: str) -> str:
|
||
"""The copular negation of a lexicon clause ("… is X" → "… is not X")."""
|
||
return clause.replace(" is ", " is not ", 1)
|
||
|
||
|
||
#: English-band templates: (gold, text_builder, intended_premises, intended_query).
|
||
#: The INTENDED formulas are the template's logical form over fixed placeholder
|
||
#: atoms — the reader-independent gold ``assert_corpus_sound`` cross-checks
|
||
#: against the truth-table oracle (INV-25: no reader, no ROBDD involvement).
|
||
_EN_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
|
||
EN_CONDITIONAL_SINGLE: (
|
||
# Modus ponens.
|
||
("entailed", lambda a, b, c: f"If {a} then {b}. {a.capitalize()}. Therefore {b}.",
|
||
("pa implies pb", "pa"), "pb"),
|
||
# Modus tollens (copular negation).
|
||
("entailed", lambda a, b, c: f"If {a} then {b}. {_en_neg(b).capitalize()}. Therefore {_en_neg(a)}.",
|
||
("pa implies pb", "not pb"), "not pa"),
|
||
# Direct contradiction of the consequent.
|
||
("refuted", lambda a, b, c: f"If {a} then {b}. {a.capitalize()}. Therefore {_en_neg(b)}.",
|
||
("pa implies pb", "pa"), "not pb"),
|
||
# Affirming the consequent — classic non-sequitur.
|
||
("unknown", lambda a, b, c: f"If {a} then {b}. {b.capitalize()}. Therefore {a}.",
|
||
("pa implies pb", "pb"), "pa"),
|
||
# Denying the antecedent — classic non-sequitur.
|
||
("unknown", lambda a, b, c: f"If {a} then {b}. {_en_neg(a).capitalize()}. Therefore {_en_neg(b)}.",
|
||
("pa implies pb", "not pa"), "not pb"),
|
||
# No anchor at all.
|
||
("unknown", lambda a, b, c: f"If {a} then {b}. Therefore {a}.",
|
||
("pa implies pb",), "pa"),
|
||
),
|
||
EN_CONDITIONAL_CHAIN: (
|
||
# Two-hop modus ponens.
|
||
("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a.capitalize()}. Therefore {c}.",
|
||
("pa implies pb", "pb implies pc", "pa"), "pc"),
|
||
# Two-hop modus tollens (contraposition through the chain).
|
||
("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {_en_neg(c).capitalize()}. Therefore {_en_neg(a)}.",
|
||
("pa implies pb", "pb implies pc", "not pc"), "not pa"),
|
||
# Hypothetical syllogism — a conditional CONCLUSION.
|
||
("entailed", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. Therefore if {a} then {c}.",
|
||
("pa implies pb", "pb implies pc"), "pa implies pc"),
|
||
# Chain contradiction.
|
||
("refuted", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. {a.capitalize()}. Therefore {_en_neg(c)}.",
|
||
("pa implies pb", "pb implies pc", "pa"), "not pc"),
|
||
# Chain with no anchor.
|
||
("unknown", lambda a, b, c: f"If {a} then {b}. If {b} then {c}. Therefore {c}.",
|
||
("pa implies pb", "pb implies pc"), "pc"),
|
||
),
|
||
EN_DISJUNCTIVE: (
|
||
# Disjunctive syllogism.
|
||
("entailed", lambda a, b, c: f"{a.capitalize()} or {b}. {_en_neg(a).capitalize()}. Therefore {b}.",
|
||
("pa or pb", "not pa"), "pb"),
|
||
# Disjunctive syllogism, "either" spelling, other disjunct.
|
||
("entailed", lambda a, b, c: f"Either {a} or {b}. {_en_neg(b).capitalize()}. Therefore {a}.",
|
||
("pa or pb", "not pb"), "pa"),
|
||
# Constructive dilemma.
|
||
("entailed", lambda a, b, c: f"If {a} then {c}. If {b} then {c}. {a.capitalize()} or {b}. Therefore {c}.",
|
||
("pa implies pc", "pb implies pc", "pa or pb"), "pc"),
|
||
# Eliminating one disjunct entails the other — its negation is refuted.
|
||
("refuted", lambda a, b, c: f"{a.capitalize()} or {b}. {_en_neg(a).capitalize()}. Therefore {_en_neg(b)}.",
|
||
("pa or pb", "not pa"), "not pb"),
|
||
# A bare disjunction settles neither disjunct.
|
||
("unknown", lambda a, b, c: f"{a.capitalize()} or {b}. Therefore {a}.",
|
||
("pa or pb",), "pa"),
|
||
),
|
||
EN_ATOMIC: (
|
||
# Restatement.
|
||
("entailed", lambda a, b, c: f"{a.capitalize()}. Therefore {a}.",
|
||
("pa",), "pa"),
|
||
# Conjunction elimination (top-level "and" premise splits).
|
||
("entailed", lambda a, b, c: f"{a.capitalize()} and {b}. Therefore {a}.",
|
||
("pa", "pb"), "pa"),
|
||
# Disjunction introduction.
|
||
("entailed", lambda a, b, c: f"{a.capitalize()}. Therefore {a} or {b}.",
|
||
("pa",), "pa or pb"),
|
||
# Conjunction introduction (an "and" CONCLUSION).
|
||
("entailed", lambda a, b, c: f"{a.capitalize()}. {b.capitalize()}. Therefore {a} and {b}.",
|
||
("pa", "pb"), "pa and pb"),
|
||
# Direct self-contradiction.
|
||
("refuted", lambda a, b, c: f"{a.capitalize()}. Therefore {_en_neg(a)}.",
|
||
("pa",), "not pa"),
|
||
# Unrelated conclusion.
|
||
("unknown", lambda a, b, c: f"{a.capitalize()}. Therefore {b}.",
|
||
("pa",), "pb"),
|
||
),
|
||
}
|
||
|
||
# --- Band v3-MEM (ADR-0258): member-argument synthetic corpus -----------------
|
||
#
|
||
# Names × class-noun (singular, plural) pairs × state adjectives. The class
|
||
# lexicon deliberately exercises EVERY row-type of the reader's closed number
|
||
# table — irregular (man/men, person/people, child/children, wolf/wolves,
|
||
# mouse/mice, goose/geese), invariant (sheep, fish), and each regular suffix
|
||
# rule (+s, +es, y↔ies) — so the earned license certifies the linking relation
|
||
# itself, not just the sentence grammar. Content is synthetic ON PURPOSE
|
||
# (same posture as the v2-EN corpus above); hand-authored real-English cases
|
||
# live in ``evals/deduction_serve/v2_member``.
|
||
|
||
_MEM_NAMES: tuple[str, ...] = (
|
||
"Rex", "Ada", "Kai", "Milo", "Nova", "Otis", "Pia", "Quinn", "Rio", "Sol",
|
||
"Tara", "Ugo", "Vera", "Wren", "Yara", "Zed", "Bo", "Cyra", "Dax", "Elio",
|
||
)
|
||
_MEM_CLASSES: tuple[tuple[str, str], ...] = (
|
||
("man", "men"), ("person", "people"), ("child", "children"),
|
||
("wolf", "wolves"), ("mouse", "mice"), ("goose", "geese"),
|
||
("sheep", "sheep"), ("fish", "fish"),
|
||
("cat", "cats"), ("dog", "dogs"), ("fox", "foxes"), ("pony", "ponies"),
|
||
)
|
||
_MEM_STATES: tuple[str, ...] = (
|
||
"mortal", "loyal", "wild", "tame", "swift", "calm",
|
||
"bold", "shy", "warm", "quiet", "brave", "free",
|
||
)
|
||
|
||
|
||
def _mem_case(index: int) -> tuple[str, str, tuple[str, str], tuple[str, str], tuple[str, str], str]:
|
||
"""Deterministic (name1, name2, class1, class2, class3, state) for case
|
||
``index`` — names and the three classes are always 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) - 2)
|
||
c1, c2, c3 = _MEM_CLASSES[base], _MEM_CLASSES[base + 1], _MEM_CLASSES[base + 2]
|
||
state = _MEM_STATES[(index * 7) % len(_MEM_STATES)]
|
||
return n1, n2, c1, c2, c3, state
|
||
|
||
|
||
#: Member-band templates: (gold, text_builder, intended_premises, intended_query).
|
||
#: Builders take ``(n1, n2, c1, c2, c3, st)`` from ``_mem_case``; the INTENDED
|
||
#: formulas are the template's per-individual lowering over fixed placeholder
|
||
#: atoms (``ma`` = first (individual, class) pair, …), cross-checked against
|
||
#: the truth-table oracle with no reader in the loop (INV-25).
|
||
_MEM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
|
||
EN_MEMBER_SINGLE: (
|
||
# Instantiated modus ponens onto a state predicate.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n1} is {st}.",
|
||
("ma", "ma implies mb"), "mb"),
|
||
# Instantiated modus ponens onto a membership conclusion ("every" spelling).
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Every {c1[0]} is a {c2[0]}. Therefore {n1} is a {c2[0]}.",
|
||
("ma", "ma implies mb"), "mb"),
|
||
# Universal stated FIRST ("each" spelling) — order independence.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"Each {c1[0]} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.",
|
||
("ma implies mb", "ma"), "mb"),
|
||
# Contradicting the instantiated consequent.
|
||
("refuted",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n1} is not {st}.",
|
||
("ma", "ma implies mb"), "not mb"),
|
||
# Converse instantiation — affirming the consequent.
|
||
("unknown",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. All {c1[1]} are {st}. Therefore {n1} is a {c1[0]}.",
|
||
("mb", "ma implies mb"), "ma"),
|
||
# The universal binds a DIFFERENT named individual than the conclusion's.
|
||
("unknown",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n2} is {st}.",
|
||
("ma", "ma implies mb", "mc implies md"), "md"),
|
||
),
|
||
EN_MEMBER_CHAIN: (
|
||
# Two-hop instantiated chain onto a state.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is {st}.",
|
||
("ma", "ma implies mb", "mb implies mc"), "mc"),
|
||
# Two-hop chain onto a MEMBERSHIP conclusion — the conclusion's singular
|
||
# article form links to the chain's plural class.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {c3[1]}. Therefore {n1} is a {c3[0]}.",
|
||
("ma", "ma implies mb", "mb implies mc"), "mc"),
|
||
# Chain contradiction.
|
||
("refuted",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is not {st}.",
|
||
("ma", "ma implies mb", "mb implies mc"), "not mc"),
|
||
# Broken chain — the individual's class never enters it.
|
||
("unknown",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c2[1]} are {c3[1]}. All {c3[1]} are {st}. Therefore {n1} is {st}.",
|
||
("ma", "mb implies mc", "mc implies md"), "md"),
|
||
# Reverse traversal — chains do not run backwards.
|
||
("unknown",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is a {c1[0]}.",
|
||
("mc", "ma implies mb", "mb implies mc"), "ma"),
|
||
),
|
||
EN_MEMBER_NEGATIVE: (
|
||
# Instantiated E-form onto a state.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is not {st}.",
|
||
("ma", "ma implies not mb"), "not mb"),
|
||
# Instantiated E-form onto a membership conclusion.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {c2[1]}. Therefore {n1} is not a {c2[0]}.",
|
||
("ma", "ma implies not mb"), "not mb"),
|
||
# A-chain into an E-form.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. No {c2[1]} are {st}. Therefore {n1} is not {st}.",
|
||
("ma", "ma implies mb", "mb implies not mc"), "not mc"),
|
||
# Contradicting the E-form's instantiation.
|
||
("refuted",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is {st}.",
|
||
("ma", "ma implies not mb"), "mb"),
|
||
# Denied antecedent under an E-form — nothing follows.
|
||
("unknown",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is not a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is not {st}.",
|
||
("not ma", "ma implies not mb"), "not mb"),
|
||
),
|
||
EN_MEMBER_ATOMIC: (
|
||
# Membership restatement (the promoted ds-en-0022 shape).
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is a {c1[0]}.",
|
||
("ma",), "ma"),
|
||
# State restatement.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. Therefore {n1} is {st}.",
|
||
("ma",), "ma"),
|
||
# Selection from two facts about one individual.
|
||
("entailed",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. {n1} is {st}. Therefore {n1} is {st}.",
|
||
("ma", "mb"), "mb"),
|
||
# Self-contradiction (membership).
|
||
("refuted",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is not a {c1[0]}.",
|
||
("ma",), "not ma"),
|
||
# Negated fact contradicted.
|
||
("refuted",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is not {st}. Therefore {n1} is {st}.",
|
||
("not ma",), "ma"),
|
||
# Unrelated conclusion.
|
||
("unknown",
|
||
lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is {st}.",
|
||
("ma",), "mb"),
|
||
),
|
||
}
|
||
|
||
# --- 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"),
|
||
),
|
||
}
|
||
|
||
|
||
# --- 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"),
|
||
),
|
||
}
|
||
|
||
|
||
# --- Band v6-EX (ADR-0261): existential synthetic corpus ----------------------
|
||
#
|
||
# Reuses the v3-MEM name/class/state pools and the v5-VP verb pool, and adds
|
||
# nothing new to the lexicon: this band's novelty is the LOWERING (a Skolem
|
||
# witness per existential premise, one arbitrary element per existential
|
||
# conclusion), not the vocabulary. The templates deliberately include both
|
||
# subaltern moods ("all C are P, therefore some C are P" ⇒ UNKNOWN, no
|
||
# existential import) and both contradictory pairs (A refutes O, E refutes I),
|
||
# so the earned license certifies the square of opposition as this band reads
|
||
# it. Content is synthetic ON PURPOSE (same posture as every earlier corpus);
|
||
# hand-authored real-English cases live in ``evals/deduction_serve/v2_exist``.
|
||
|
||
|
||
def _exist_case(
|
||
index: int,
|
||
) -> tuple[str, tuple[str, str], tuple[str, str], tuple[str, str], tuple[str, str], str]:
|
||
"""Deterministic (name, class1, class2, class3, verb, state) for case
|
||
``index`` — the three classes are pairwise distinct."""
|
||
n1 = _MEM_NAMES[(index * 3) % len(_MEM_NAMES)]
|
||
base = (index * 5) % (len(_MEM_CLASSES) - 2)
|
||
c1, c2, c3 = _MEM_CLASSES[base], _MEM_CLASSES[base + 1], _MEM_CLASSES[base + 2]
|
||
v1 = _VERB_FORMS[(index * 7) % len(_VERB_FORMS)]
|
||
st = _MEM_STATES[(index * 11) % len(_MEM_STATES)]
|
||
return n1, c1, c2, c3, v1, st
|
||
|
||
|
||
#: Existential-band templates: (gold, text_builder, intended_premises,
|
||
#: intended_query). Builders take ``(n1, c1, c2, c3, v1, st)`` from
|
||
#: ``_exist_case``; the INTENDED formulas are the template's lowering over
|
||
#: fixed placeholder atoms — ``m*`` at the named individual, ``w*``/``x*`` at
|
||
#: the first/second witness, ``k*`` at the arbitrary element — cross-checked
|
||
#: against the truth-table oracle with no reader in the loop (INV-25). A
|
||
#: universal contributes ONE implication per domain element, and an
|
||
#: existential conclusion one disjunct per domain element; the intended forms
|
||
#: mirror that exactly, so a lowering that drops (or invents) a domain element
|
||
#: shows up as a disagreement rather than passing silently.
|
||
_EXIST_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = {
|
||
EN_EXIST_WITNESS: (
|
||
# I-form conversion — "some C are S" ⇒ "some S are C". A state word
|
||
# (never in the shared reader's morphology) stands in for the second
|
||
# term here and in the two other otherwise-all-class templates below:
|
||
# a text whose every term IS in that lexicon is read by the CATEGORICAL
|
||
# band (v1b) long before this one, and the arena must exercise the
|
||
# fall-through path serving actually takes, not a shape v1b keeps.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {st}. Therefore some {st} are {c1[1]}.",
|
||
("wa and wb",), "(wb and wa) or (kb and ka)"),
|
||
# A named individual IS a witness.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. {n1} is {st}. Therefore some {c1[1]} are {st}.",
|
||
("ma", "mb"), "(ma and mb) or (ka and kb)"),
|
||
# O-form restatement.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are not {st}. Therefore some {c1[1]} are not {st}.",
|
||
("wa and (not wb)",), "(wa and (not wb)) or (ka and (not kb))"),
|
||
# The witness is anonymous — a stated singular fact still contradicts.
|
||
("refuted",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {st}. {n1} is not {st}. Therefore {n1} is {st}.",
|
||
("wa and wb", "not mb"), "mb"),
|
||
# The witness never transfers to a named individual (the anti-leak case).
|
||
("unknown",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.",
|
||
("wa and wb", "ma"), "mb"),
|
||
# Two existentials do not compose — distinct witnesses stay distinct.
|
||
("unknown",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. Some {c1[1]} are {c3[1]}. Therefore some {c2[1]} are {c3[1]}.",
|
||
("wa and wb", "xa and xc"), "(wb and wc) or (xb and xc) or (kb and kc)"),
|
||
),
|
||
EN_EXIST_UNIVERSAL: (
|
||
# Darii — the universal fires at the witness.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"All {c1[1]} are {st}. Some {c2[1]} are {c1[1]}. Therefore some {c2[1]} are {st}.",
|
||
("wa implies wb", "ka implies kb", "wc and wa"), "(wc and wb) or (kc and kb)"),
|
||
# "every" spelling, singular class forms — number linking at the witness.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"Every {c1[0]} is a {c2[0]}. Some {c1[1]} are {st}. Therefore some {c2[1]} are {st}.",
|
||
("wa implies wb", "ka implies kb", "wa and wc"), "(wb and wc) or (kb and kc)"),
|
||
# The named individual supplies the existential witness.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore some {c1[1]} are {st}.",
|
||
("ma", "ma implies mb", "ka implies kb"), "(ma and mb) or (ka and kb)"),
|
||
# Verb universal discharged at the witness.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"All {c1[1]} {v1[0]}. Some {c2[1]} are {c1[1]}. Therefore some {c2[1]} {v1[0]}.",
|
||
("wa implies wv", "ka implies kv", "wc and wa"), "(wc and wv) or (kc and kv)"),
|
||
# NO existential import — the subaltern does not follow.
|
||
("unknown",
|
||
lambda n1, c1, c2, c3, v1, st: f"All {c1[1]} are {st}. Therefore some {c1[1]} are {st}.",
|
||
("ka implies kb",), "ka and kb"),
|
||
# Undistributed middle with an existential premise.
|
||
("unknown",
|
||
lambda n1, c1, c2, c3, v1, st: f"All {c2[1]} are {c1[1]}. Some {c3[1]} are {c1[1]}. Therefore some {c3[1]} are {c2[1]}.",
|
||
("wa implies wb", "ka implies kb", "wc and wb"), "(wc and wa) or (kc and ka)"),
|
||
# A-form and O-form are contradictories — the A refutes the O.
|
||
("refuted",
|
||
lambda n1, c1, c2, c3, v1, st: f"All {c1[1]} are {st}. Therefore some {c1[1]} are not {st}.",
|
||
("ka implies kb",), "ka and (not kb)"),
|
||
# Universal instantiated at the named individual contradicts the query.
|
||
("refuted",
|
||
lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Some {c2[1]} are {c1[1]}. Therefore {n1} is not {st}.",
|
||
("ma", "ma implies mb", "wa implies wb", "wc and wa"), "not mb"),
|
||
),
|
||
EN_EXIST_CHAIN: (
|
||
# Two-hop chain carrying the witness to the conclusion.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. All {c2[1]} are {c3[1]}. All {c3[1]} are {st}. Therefore some {c1[1]} are {st}.",
|
||
("wa and wb", "wb implies wc", "kb implies kc", "wc implies wd", "kc implies kd"),
|
||
"(wa and wd) or (ka and kd)"),
|
||
# Chain from a named individual to an existential conclusion.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore some {c2[1]} are {st}.",
|
||
("ma", "ma implies mb", "ka implies kb", "mb implies mc", "kb implies kc"),
|
||
"(mb and mc) or (kb and kc)"),
|
||
# Membership chain into a verb universal.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. All {c2[1]} are {c3[1]}. All {c3[1]} {v1[0]}. Therefore some {c1[1]} {v1[0]}.",
|
||
("wa and wb", "wb implies wc", "kb implies kc", "wc implies wv", "kc implies kv"),
|
||
"(wa and wv) or (ka and kv)"),
|
||
# Broken chain — the subsumption points the wrong way.
|
||
("unknown",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. All {c3[1]} are {c2[1]}. All {c3[1]} are {st}. Therefore some {c1[1]} are {st}.",
|
||
("wa and wb", "wc implies wb", "kc implies kb", "wc implies wd", "kc implies kd"),
|
||
"(wa and wd) or (ka and kd)"),
|
||
# Reverse traversal — chains do not run backwards.
|
||
("unknown",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {st}. All {c2[1]} are {c1[1]}. All {c3[1]} are {c2[1]}. Therefore some {c3[1]} are {st}.",
|
||
("wa and wb", "wc implies wa", "kc implies ka", "wd implies wc", "kd implies kc"),
|
||
"(wd and wb) or (kd and kb)"),
|
||
# Chain into a contradicted singular conclusion.
|
||
("refuted",
|
||
lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Some {c3[1]} are {c1[1]}. Therefore {n1} is not {st}.",
|
||
("ma", "ma implies mb", "wa implies wb", "mb implies mc", "wb implies wc", "wd and wa"),
|
||
"not mc"),
|
||
),
|
||
EN_EXIST_NEGATIVE: (
|
||
# Ferio — E-form plus I-form yields the O-form.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"No {c1[1]} are {st}. Some {c2[1]} are {c1[1]}. Therefore some {c2[1]} are not {st}.",
|
||
("wa implies not wb", "ka implies not kb", "wc and wa"),
|
||
"(wc and (not wb)) or (kc and (not kb))"),
|
||
# E-form plus a named individual yields the O-form.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Therefore some {c1[1]} are not {st}.",
|
||
("ma", "ma implies not mb", "ka implies not kb"),
|
||
"(ma and (not mb)) or (ka and (not kb))"),
|
||
# Verb E-form with the plural "do not" conclusion.
|
||
("entailed",
|
||
lambda n1, c1, c2, c3, v1, st: f"No {c1[1]} {v1[0]}. Some {c2[1]} are {c1[1]}. Therefore some {c2[1]} do not {v1[0]}.",
|
||
("wa implies not wv", "ka implies not kv", "wc and wa"),
|
||
"(wc and (not wv)) or (kc and (not kv))"),
|
||
# E-form and I-form are contradictories — the E refutes the I.
|
||
("refuted",
|
||
lambda n1, c1, c2, c3, v1, st: f"No {c1[1]} are {st}. Therefore some {c1[1]} are {st}.",
|
||
("ka implies not kb",), "ka and kb"),
|
||
# E-form instantiated at the named individual contradicts the query.
|
||
("refuted",
|
||
lambda n1, c1, c2, c3, v1, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Some {c2[1]} are {c1[1]}. Therefore {n1} is {st}.",
|
||
("ma", "ma implies not mb", "wa implies not wb", "wc and wa"), "mb"),
|
||
# The E-form binds a class the witness never enters.
|
||
("unknown",
|
||
lambda n1, c1, c2, c3, v1, st: f"Some {c1[1]} are {c2[1]}. No {c3[1]} are {st}. Therefore some {c1[1]} are not {st}.",
|
||
("wa and wb", "wc implies not wd", "kc implies not kd"),
|
||
"(wa and (not wd)) or (ka and (not kd))"),
|
||
),
|
||
}
|
||
|
||
|
||
#: Ledger band order: the five v1 bands, the four v2-EN bands, the four
|
||
#: v3-MEM bands, the four v4-CM bands, the four v5-VP bands, then the four
|
||
#: v6-EX 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,
|
||
EN_EXIST_NEGATIVE, EN_EXIST_CHAIN, EN_EXIST_UNIVERSAL, EN_EXIST_WITNESS,
|
||
)
|
||
|
||
|
||
def generate_problems(band: str, n: int) -> list[Problem]:
|
||
"""``n`` synthetic problems for ``band``, cycling its gold templates.
|
||
|
||
Deterministic: problem ``i`` uses template ``i % len(templates)`` and
|
||
deterministic atom/clause selection. Each ``payload`` carries the raw
|
||
``text`` and the by-construction ``gold`` the tether scores against;
|
||
English-band payloads additionally carry the template's ``intended``
|
||
logical form for the reader-independent oracle cross-check.
|
||
"""
|
||
problems: list[Problem] = []
|
||
if band in _EXIST_TEMPLATES:
|
||
templates = _EXIST_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(*_exist_case(i)),
|
||
"gold": gold,
|
||
"intended": {
|
||
"premises": list(intended_premises),
|
||
"query": intended_query,
|
||
},
|
||
},
|
||
)
|
||
)
|
||
return problems
|
||
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):
|
||
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(*_mem_case(i)),
|
||
"gold": gold,
|
||
"intended": {
|
||
"premises": list(intended_premises),
|
||
"query": intended_query,
|
||
},
|
||
},
|
||
)
|
||
)
|
||
return problems
|
||
if band in _EN_TEMPLATES:
|
||
templates = _EN_TEMPLATES[band]
|
||
for i in range(n):
|
||
gold, builder, intended_premises, intended_query = templates[i % len(templates)]
|
||
a, b, c = _en_clauses(i, 3)
|
||
problems.append(
|
||
Problem(
|
||
problem_id=f"{band}-{i:04d}",
|
||
class_name=band,
|
||
payload={
|
||
"text": builder(a, b, c),
|
||
"gold": gold,
|
||
"intended": {
|
||
"premises": list(intended_premises),
|
||
"query": intended_query,
|
||
},
|
||
},
|
||
)
|
||
)
|
||
return problems
|
||
templates = _TEMPLATES[band]
|
||
for i in range(n):
|
||
gold, builder = templates[i % len(templates)]
|
||
a, b, c = _atoms(i, 3)
|
||
text = builder(a, b, c)
|
||
problems.append(
|
||
Problem(
|
||
problem_id=f"{band}-{i:04d}",
|
||
class_name=band,
|
||
payload={"text": text, "gold": gold},
|
||
)
|
||
)
|
||
return problems
|
||
|
||
|
||
def all_gold_problems() -> list[Problem]:
|
||
"""The full deterministic corpus over every shape-band, in band order."""
|
||
problems: list[Problem] = []
|
||
for band in _ALL_BANDS:
|
||
problems.extend(generate_problems(band, CASES_PER_BAND))
|
||
return problems
|
||
|
||
|
||
# --- the ADR-0199 DomainSolver / GoldTether for deduction serving -------------
|
||
|
||
|
||
@dataclass(frozen=True, slots=True)
|
||
class _DeductionAttempt:
|
||
committed: bool
|
||
answer: Any # the outcome class the pipeline decided, or None on decline
|
||
reason: str
|
||
case_id: str
|
||
shape: str
|
||
derivations: tuple[Any, ...] = field(default_factory=tuple)
|
||
trace_sha256: str = ""
|
||
|
||
|
||
_OUTCOME_TO_CLASS = {
|
||
Entailment.ENTAILED: "entailed",
|
||
Entailment.REFUTED: "refuted",
|
||
Entailment.UNKNOWN: "unknown",
|
||
Entailment.REFUSED: "declined",
|
||
}
|
||
|
||
#: Categorical outcome mapping: a syllogism is VALID iff the conclusion is
|
||
#: entailed; UNKNOWN/REFUTED ⇒ invalid; REFUSED ⇒ declined (inconsistent).
|
||
_CATEGORICAL_TO_CLASS = {
|
||
Entailment.ENTAILED: "valid",
|
||
Entailment.REFUTED: "invalid",
|
||
Entailment.UNKNOWN: "invalid",
|
||
Entailment.REFUSED: "declined",
|
||
}
|
||
|
||
|
||
@dataclass(frozen=True, slots=True)
|
||
class DeductionSolver:
|
||
"""The production serving pipeline as a ``DomainSolver``.
|
||
|
||
Runs exactly what ``chat/deduction_surface.py`` runs — the propositional
|
||
path (``to_deductive_logic`` → ``evaluate_entailment_with_trace``) then the
|
||
categorical path (``to_syllogism`` → ``decide_syllogism``) — and commits the
|
||
decided outcome class. A reader refusal / non-projectable comprehension /
|
||
engine REFUSED is an uncommitted attempt, never a guessed answer. Kept in
|
||
lock-step with the composer's dual path; the lane + license tests cover both.
|
||
"""
|
||
|
||
domain_id: str = _DOMAIN_ID
|
||
|
||
def attempt(self, problem: Problem) -> _DeductionAttempt:
|
||
text = problem.payload["text"]
|
||
comp = comprehend(text)
|
||
if not isinstance(comp, Comprehension):
|
||
# Band v2-EN / v3-MEM fallbacks — mirror the composer: the shared
|
||
# reader refused, but the English-clause or member-argument reader
|
||
# may read it.
|
||
english = self._attempt_english(problem)
|
||
if english is not None:
|
||
return english
|
||
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
|
||
verb = self._attempt_verb(problem)
|
||
if verb is not None:
|
||
return verb
|
||
exist = self._attempt_exist(problem)
|
||
if exist is not None:
|
||
return exist
|
||
return _DeductionAttempt(
|
||
committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}",
|
||
case_id=problem.problem_id, shape=problem.class_name,
|
||
)
|
||
# Band v1 — propositional.
|
||
projected = to_deductive_logic(comp)
|
||
if projected is not None:
|
||
premises, query = projected
|
||
outcome = evaluate_entailment_with_trace(premises, query).outcome
|
||
return _DeductionAttempt(
|
||
committed=outcome is not Entailment.REFUSED,
|
||
answer=_OUTCOME_TO_CLASS[outcome], reason="",
|
||
case_id=problem.problem_id, shape=classify_deduction_shape(premises, query),
|
||
)
|
||
# Band v1b — categorical / syllogism.
|
||
syllogism = to_syllogism(comp)
|
||
if syllogism is not None:
|
||
structure, s_query = syllogism
|
||
try:
|
||
outcome = decide_syllogism(structure, s_query).outcome
|
||
except CategoricalError:
|
||
return _DeductionAttempt(
|
||
committed=False, answer=None, reason="categorical_malformed",
|
||
case_id=problem.problem_id, shape=CATEGORICAL,
|
||
)
|
||
return _DeductionAttempt(
|
||
committed=outcome is not Entailment.REFUSED,
|
||
answer=_CATEGORICAL_TO_CLASS[outcome], reason="",
|
||
case_id=problem.problem_id, shape=CATEGORICAL,
|
||
)
|
||
english = self._attempt_english(problem)
|
||
if english is not None:
|
||
return english
|
||
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
|
||
verb = self._attempt_verb(problem)
|
||
if verb is not None:
|
||
return verb
|
||
exist = self._attempt_exist(problem)
|
||
if exist is not None:
|
||
return exist
|
||
return _DeductionAttempt(
|
||
committed=False, answer=None, reason="unprojectable",
|
||
case_id=problem.problem_id, shape=problem.class_name,
|
||
)
|
||
|
||
def _attempt_english(self, problem: Problem) -> _DeductionAttempt | None:
|
||
"""Band v2-EN: the English-clause argument path, or ``None`` when the
|
||
English reader refuses (the caller then records the honest decline)."""
|
||
arg = read_english_argument(problem.payload["text"])
|
||
if not isinstance(arg, EnglishArgument):
|
||
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,
|
||
)
|
||
|
||
def _attempt_member(self, problem: Problem) -> _DeductionAttempt | None:
|
||
"""Band v3-MEM: the member-argument path, or ``None`` when the member
|
||
reader refuses (the caller then records the honest decline)."""
|
||
arg = read_member_argument(problem.payload["text"])
|
||
if not isinstance(arg, MemberArgument):
|
||
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,
|
||
)
|
||
|
||
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,
|
||
)
|
||
|
||
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,
|
||
)
|
||
|
||
|
||
def _attempt_exist(self, problem: Problem) -> _DeductionAttempt | None:
|
||
"""Band v6-EX: the existential argument path, or ``None`` when the
|
||
reader refuses (the caller then records the honest decline)."""
|
||
arg = read_exist_argument(problem.payload["text"])
|
||
if not isinstance(arg, ExistArgument):
|
||
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:
|
||
"""Scores the pipeline's committed outcome against the by-construction gold.
|
||
|
||
The gold lives in ``problem.payload["gold"]`` — authored by the generating
|
||
template's logical form, independent of the reader (ADR-0199 L-2). A pipeline
|
||
that misreads the text and decides a different outcome is scored ``wrong``.
|
||
"""
|
||
|
||
domain_id: str = _DOMAIN_ID
|
||
|
||
def is_correct(self, attempt: _DeductionAttempt, problem: Problem) -> bool:
|
||
return bool(attempt.committed) and attempt.answer == problem.payload["gold"]
|
||
|
||
def gold_answer(self, problem: Problem) -> str:
|
||
return str(problem.payload["gold"])
|
||
|
||
|
||
def assert_corpus_sound() -> None:
|
||
"""Belt-and-suspenders: every generated case's by-construction gold must
|
||
agree with an INDEPENDENT oracle over its projected form.
|
||
|
||
Guards against a template authoring bug (a mis-stated gold) silently
|
||
inflating the ledger. Raises ``AssertionError`` on any disagreement. Uses
|
||
oracles that share no code with the ROBDD serving engine (INV-25): the
|
||
truth-table ``evals.deductive_logic.oracle`` for propositional bands, and
|
||
the finite-model ``evals.syllogism.oracle`` for the categorical band.
|
||
"""
|
||
from evals.deductive_logic.oracle import oracle_entailment
|
||
from evals.syllogism.oracle import oracle_answer
|
||
|
||
for problem in all_gold_problems():
|
||
gold = problem.payload["gold"]
|
||
# Band v2-EN: the payload carries the template's INTENDED logical form —
|
||
# the oracle checks it directly, with no reader in the loop at all
|
||
# (stronger independence than the v1 path below, which needs the reader
|
||
# to project before the oracle can pronounce).
|
||
intended = problem.payload.get("intended")
|
||
if intended is not None:
|
||
oracle = oracle_entailment(tuple(intended["premises"]), intended["query"])
|
||
assert oracle == gold, (
|
||
f"{problem.problem_id}: oracle={oracle} gold={gold} "
|
||
f"intended={intended!r} text={problem.payload['text']!r}"
|
||
)
|
||
continue
|
||
comp = comprehend(problem.payload["text"])
|
||
assert isinstance(comp, Comprehension), problem.payload["text"]
|
||
projected = to_deductive_logic(comp)
|
||
if projected is not None:
|
||
premises, query = projected
|
||
oracle = oracle_entailment(premises, query)
|
||
assert oracle == gold, (
|
||
f"{problem.problem_id}: oracle={oracle} gold={gold} "
|
||
f"text={problem.payload['text']!r}"
|
||
)
|
||
continue
|
||
syllogism = to_syllogism(comp)
|
||
assert syllogism is not None, problem.payload["text"]
|
||
structure, s_query = syllogism
|
||
oracle_valid = oracle_answer(structure, s_query)["valid"]
|
||
oracle_class = "valid" if oracle_valid else "invalid"
|
||
assert oracle_class == gold, (
|
||
f"{problem.problem_id}: syllogism_oracle={oracle_class} gold={gold} "
|
||
f"text={problem.payload['text']!r}"
|
||
)
|
||
|
||
|
||
__all__ = [
|
||
"CASES_PER_BAND",
|
||
"ConstructionGoldTether",
|
||
"DeductionSolver",
|
||
"all_gold_problems",
|
||
"assert_corpus_sound",
|
||
"generate_problems",
|
||
]
|