diff --git a/evals/capability_index/adapters.py b/evals/capability_index/adapters.py index d65acaab..24951dac 100644 --- a/evals/capability_index/adapters.py +++ b/evals/capability_index/adapters.py @@ -63,8 +63,15 @@ def comprehension_total_ordering_result() -> DomainResult: return DomainResult("comprehension_total_ordering", c, w, r) +def comprehension_propositional_result() -> DomainResult: + from evals.comprehension.propositional_runner import run + + c, w, r = _counts(run()) + return DomainResult("comprehension_propositional", c, w, r) + + #: The reasoning domains currently composed into the index (self-loading lanes). -#: The three ``comprehension_*`` lanes score the GENERAL comprehension reader +#: The four ``comprehension_*`` lanes score the GENERAL comprehension reader #: (prose -> MeaningGraph -> projection -> independent oracle), so the index now #: measures comprehension breadth, not just structured-input reasoning. ADAPTERS = ( @@ -74,6 +81,7 @@ ADAPTERS = ( comprehension_set_membership_result, comprehension_syllogism_result, comprehension_total_ordering_result, + comprehension_propositional_result, ) diff --git a/evals/capability_index/baseline.json b/evals/capability_index/baseline.json index 551e6b34..34dad1bd 100644 --- a/evals/capability_index/baseline.json +++ b/evals/capability_index/baseline.json @@ -1,14 +1,22 @@ { - "capability_score": 0.917231, - "coverage_geomean": 0.917231, - "coverage_micro": 0.993481, + "capability_score": 0.928622, + "coverage_geomean": 0.928622, + "coverage_micro": 0.993582, "accuracy_micro": 1.0, - "breadth": 6, + "breadth": 7, "min_domain_coverage": 0.833333, "wrong_total": 0, "assert_mode_valid": true, - "deterministic_digest": "13d7db6c4fc8caed703164cd16c196ecb426a31fb5bcb9658fe630be760179ab", + "deterministic_digest": "51df7bba62a035c73bdaf289ea20cded05b66b2f7ca5fd8bbcb04f127d60cadf", "domains": [ + { + "domain": "comprehension_propositional", + "correct": 12, + "wrong": 0, + "refused": 0, + "coverage": 1.0, + "accuracy": 1.0 + }, { "domain": "comprehension_set_membership", "correct": 8, diff --git a/evals/comprehension/propositional_runner.py b/evals/comprehension/propositional_runner.py new file mode 100644 index 00000000..56aa7ac8 --- /dev/null +++ b/evals/comprehension/propositional_runner.py @@ -0,0 +1,71 @@ +"""Score the general comprehension reader on the propositional_logic gold lane. + +prose -> comprehend() -> to_deductive_logic() -> independent ROBDD oracle -> verdict +vs gold. A refusal (unreadable prose, unprojectable, or an oracle "refused" because +the projected formula could not be evaluated) is NOT a wrong; only a committed +verdict that disagrees with gold is wrong (must stay 0). +""" + +from __future__ import annotations + +import json +import sys +from typing import Any + +from evals.deductive_logic.oracle import REFUSED, oracle_entailment +from evals.propositional_logic.runner import _load_cases +from generate.meaning_graph.projectors import to_deductive_logic +from generate.meaning_graph.reader import Refusal, comprehend + + +def run() -> dict[str, Any]: + cases = _load_cases() + correct = wrong = refused = 0 + wrongs: list[dict[str, Any]] = [] + + for case in cases: + comp = comprehend(case["text"]) + if isinstance(comp, Refusal): + refused += 1 + continue + projected = to_deductive_logic(comp) + if projected is None: + refused += 1 + continue + premises, query = projected + got = oracle_entailment(premises, query) + if got == REFUSED: + # the projected formula could not be evaluated -> decline, not a wrong + refused += 1 + continue + if got == case.get("gold"): + correct += 1 + else: + wrong += 1 + wrongs.append( + {"id": case.get("id"), "got": got, "gold": case.get("gold"), "text": case["text"]} + ) + + return { + "domain": "comprehension_propositional", + "total": len(cases), + "correct": correct, + "wrong": wrong, + "refused": refused, + "wrongs": wrongs, + "counts": {"correct": correct, "wrong": wrong, "refused": refused}, + } + + +def main() -> int: + report = run() + print(json.dumps({k: v for k, v in report.items() if k != "wrongs"}, indent=2, sort_keys=True)) + if report["wrong"]: + print("WRONG > 0 — comprehension produced a wrong committed answer:", file=sys.stderr) + print(json.dumps(report["wrongs"], indent=2), file=sys.stderr) + return 1 + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/evals/propositional_logic/__init__.py b/evals/propositional_logic/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/evals/propositional_logic/runner.py b/evals/propositional_logic/runner.py new file mode 100644 index 00000000..126ad424 --- /dev/null +++ b/evals/propositional_logic/runner.py @@ -0,0 +1,59 @@ +"""Gold-only runner for the staged propositional-logic lane. + +The independent arbiter is ``evals.deductive_logic.oracle.oracle_entailment`` (the +ROBDD-matched brute-force entailment checker). This runner verifies the committed +gold is exactly that oracle's verdict on each case's ``premises``/``query`` formula +strings — so the gold cannot drift from the independent oracle. +""" + +from __future__ import annotations + +import json +import sys +from pathlib import Path +from typing import Any + +from evals.deductive_logic.oracle import oracle_entailment + +_CASES = Path(__file__).resolve().parent / "v1" / "cases.jsonl" + + +def _load_cases(path: Path = _CASES) -> list[dict[str, Any]]: + return [ + json.loads(line) + for line in path.read_text(encoding="utf-8").splitlines() + if line.strip() + ] + + +def run(path: Path = _CASES) -> dict[str, Any]: + cases = _load_cases(path) + failures: list[str] = [] + for case in cases: + got = oracle_entailment(tuple(case["premises"]), case["query"]) + if got != case.get("gold"): + failures.append(f"{case['id']}: oracle={got!r} != gold={case.get('gold')!r}") + + correct = len(cases) - len(failures) + return { + "domain": "propositional_logic", + "total": len(cases), + "correct": correct, + "wrong": 0, + "refused": 0, + "gold_integrity_failures": failures, + "counts": {"correct": correct, "wrong": 0, "refused": 0}, + } + + +def main() -> int: + report = run() + print(json.dumps(report, indent=2, sort_keys=True)) + if report["gold_integrity_failures"]: + print("GOLD INTEGRITY FAILURE", file=sys.stderr) + return 1 + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/evals/propositional_logic/v1/cases.jsonl b/evals/propositional_logic/v1/cases.jsonl new file mode 100644 index 00000000..45acf3c7 --- /dev/null +++ b/evals/propositional_logic/v1/cases.jsonl @@ -0,0 +1,12 @@ +{"id":"pl-v1-0001","seed":20260605,"text":"If p then q. p. Therefore q.","premises":["p implies q","p"],"query":"q","gold":"entailed","class":"modus_ponens"} +{"id":"pl-v1-0002","seed":20260605,"text":"If p then q. Not q. Therefore not p.","premises":["p implies q","not q"],"query":"not p","gold":"entailed","class":"modus_tollens"} +{"id":"pl-v1-0003","seed":20260605,"text":"If p then q. If q then r. Therefore if p then r.","premises":["p implies q","q implies r"],"query":"p implies r","gold":"entailed","class":"hypothetical_syllogism"} +{"id":"pl-v1-0004","seed":20260605,"text":"p or q. Not p. Therefore q.","premises":["p or q","not p"],"query":"q","gold":"entailed","class":"disjunctive_syllogism"} +{"id":"pl-v1-0005","seed":20260605,"text":"p or q. Not q. Therefore p.","premises":["p or q","not q"],"query":"p","gold":"entailed","class":"disjunctive_syllogism"} +{"id":"pl-v1-0006","seed":20260605,"text":"If p then q. q. Therefore p.","premises":["p implies q","q"],"query":"p","gold":"unknown","class":"affirming_consequent_invalid"} +{"id":"pl-v1-0007","seed":20260605,"text":"If p then q. Not p. Therefore not q.","premises":["p implies q","not p"],"query":"not q","gold":"unknown","class":"denying_antecedent_invalid"} +{"id":"pl-v1-0008","seed":20260605,"text":"If p then q. If q then r. p. Therefore r.","premises":["p implies q","q implies r","p"],"query":"r","gold":"entailed","class":"chained_modus_ponens"} +{"id":"pl-v1-0009","seed":20260605,"text":"If rain then wet. rain. Therefore wet.","premises":["rain implies wet","rain"],"query":"wet","gold":"entailed","class":"modus_ponens_words"} +{"id":"pl-v1-0010","seed":20260605,"text":"If fire then smoke. Not smoke. Therefore not fire.","premises":["fire implies smoke","not smoke"],"query":"not fire","gold":"entailed","class":"modus_tollens_words"} +{"id":"pl-v1-0011","seed":20260605,"text":"p or q. p. Therefore not q.","premises":["p or q","p"],"query":"not q","gold":"unknown","class":"inclusive_or_invalid"} +{"id":"pl-v1-0012","seed":20260605,"text":"sun or moon. Not sun. Therefore moon.","premises":["sun or moon","not sun"],"query":"moon","gold":"entailed","class":"disjunctive_syllogism_words"} diff --git a/generate/meaning_graph/projectors.py b/generate/meaning_graph/projectors.py index 36696c73..50b15aa1 100644 --- a/generate/meaning_graph/projectors.py +++ b/generate/meaning_graph/projectors.py @@ -132,3 +132,46 @@ def to_total_ordering(comp: Comprehension) -> tuple[dict[str, Any], dict[str, An else: query = {"kind": "compare", "left": q.arguments[0], "right": q.arguments[1]} return structure, query + + +#: Propositional predicates serialized into formula strings for the ROBDD oracle. +_PROP_PREDICATES = frozenset({"implies", "or", "asserted"}) + + +def _formula(predicate: str, args: tuple[str, ...], negated: bool) -> str | None: + """Serialize a propositional relation/query into a deductive_logic formula + string (keyword operators the oracle tokenizer accepts).""" + if predicate == "asserted": + return f"not {args[0]}" if negated else args[0] + if predicate == "implies": + return f"{args[0]} implies {args[1]}" + if predicate == "or": + return f"{args[0]} or {args[1]}" + return None + + +def to_deductive_logic(comp: Comprehension) -> tuple[tuple[str, ...], str] | None: + """Project into ``(premises, query)`` formula strings for + ``evals.deductive_logic.oracle.oracle_entailment``. + + Returns ``None`` (treated as a refusal) unless the comprehension is purely + propositional with >=1 premise and exactly one propositional query — so a + categorical/ordering comprehension never leaks into the entailment oracle. + """ + graph = comp.meaning_graph + premises: list[str] = [] + for r in graph.relations: + if r.predicate not in _PROP_PREDICATES: + return None # a non-propositional relation -> not this domain + formula = _formula(r.predicate, r.arguments, r.negated) + if formula is None: + return None + premises.append(formula) + + prop_queries = [q for q in comp.queries if q.predicate in _PROP_PREDICATES] + if not premises or len(comp.queries) != 1 or len(prop_queries) != 1: + return None + query = _formula(prop_queries[0].predicate, prop_queries[0].arguments, prop_queries[0].negated) + if query is None: + return None + return tuple(premises), query diff --git a/generate/meaning_graph/reader.py b/generate/meaning_graph/reader.py index 50bb96f1..ddf8b264 100644 --- a/generate/meaning_graph/reader.py +++ b/generate/meaning_graph/reader.py @@ -303,6 +303,30 @@ def _parse_sort(toks: list[str], detail: str) -> str | None: raise _Reject("ambiguous_sort_order", detail) +def _parse_propositional(toks: list[str], detail: str) -> tuple[str, tuple[str, ...], bool] | None: + """A propositional clause -> (predicate, atom_ids, negated); None if not it. + + Grammar (atoms are single tokens or reserved-free multi-word NPs): + ``if

then `` -> ("implies", (P, Q), False) + ``not

`` -> ("asserted", (P,), True) + ``

or `` -> ("or", (P, Q), False) + ``

`` (one token) -> ("asserted", (P,), False) + Anything else is None (let other templates / refusal handle it).""" + if not toks: + return None + if toks[0] == "if" and "then" in toks: + then_idx = toks.index("then") + return "implies", (_chunk(toks[1:then_idx], detail), _chunk(toks[then_idx + 1:], detail)), False + if toks[0] == "not": + return "asserted", (_chunk(toks[1:], detail),), True + if "or" in toks: + i = toks.index("or") + return "or", (_chunk(toks[:i], detail), _chunk(toks[i + 1:], detail)), False + if len(toks) == 1: # bare atomic assertion (single token only — keep the floor) + return "asserted", (_chunk(toks, detail),), False + return None + + def comprehend(text: str, source_id: str = "input") -> Comprehension | Refusal: """Comprehend *text* into a MeaningGraph + queries, or a typed Refusal.""" if not text or not text.strip(): @@ -314,7 +338,7 @@ def comprehend(text: str, source_id: str = "input") -> Comprehension | Refusal: role_kind: dict[str, str] = {} span_for: dict[str, MeaningSpan] = {} - relations: list[tuple[str, tuple[str, ...], MeaningSpan]] = [] + relations: list[tuple[str, tuple[str, ...], MeaningSpan, bool]] = [] queries: list[Query] = [] def claim(entity_id: str, kind: str, span: MeaningSpan) -> None: @@ -343,7 +367,7 @@ def comprehend(text: str, source_id: str = "input") -> Comprehension | Refusal: graph = MeaningGraph( entities=entities, relations=tuple( - Relation(pred, args, sp) for pred, args, sp in relations + Relation(pred, args, sp, negated) for pred, args, sp, negated in relations ), ) except MeaningGraphError as exc: # defensive — construction invariants @@ -357,7 +381,7 @@ def _read_clause( question: bool, span: MeaningSpan, claim, - relations: list[tuple[str, tuple[str, ...], MeaningSpan]], + relations: list[tuple[str, tuple[str, ...], MeaningSpan, bool]], queries: list[Query], ) -> None: """Match one clause against the templates; mutate accumulators or REFUSE.""" @@ -382,16 +406,24 @@ def _read_clause( queries.append(Query("sort", (order,), span)) return - # --- syllogism conclusion: "therefore " ------------------- # + # --- conclusion: "therefore " ------------- # if toks[0] == "therefore": - parsed = _parse_categorical(toks[1:], clause) - if parsed is None: - raise _Reject("unreadable_conclusion", clause) - predicate, sub, sup = parsed - claim(sub, "class", span) - claim(sup, "class", span) - queries.append(Query(predicate, (sub, sup), span)) - return + rest = toks[1:] + categorical = _parse_categorical(rest, clause) + if categorical is not None: + predicate, sub, sup = categorical + claim(sub, "class", span) + claim(sup, "class", span) + queries.append(Query(predicate, (sub, sup), span)) + return + propositional = _parse_propositional(rest, clause) + if propositional is not None: + predicate, atoms, negated = propositional + for atom in atoms: + claim(atom, "proposition", span) + queries.append(Query(predicate, atoms, span, negated)) + return + raise _Reject("unreadable_conclusion", clause) # --- membership query: "is [the] a|an ?" ------------------------ # if question and toks[0] == "is": @@ -429,7 +461,7 @@ def _read_clause( predicate, sub, sup = categorical claim(sub, "class", span) claim(sup, "class", span) - relations.append((predicate, (sub, sup), span)) + relations.append((predicate, (sub, sup), span, False)) return # --- membership fact: "[the] is a|an " -------------------------- # @@ -442,7 +474,7 @@ def _read_clause( cls = _chunk(after[1:], clause) claim(name, "individual", span) claim(cls, "class", span) - relations.append(("member", (name, cls), span)) + relations.append(("member", (name, cls), span, False)) return # --- ordering fact: " [is] [than] " ----------------------- # @@ -451,7 +483,16 @@ def _read_clause( lo, hi = comparative claim(lo, "item", span) claim(hi, "item", span) - relations.append(("less", (lo, hi), span)) + relations.append(("less", (lo, hi), span, False)) + return + + # --- propositional fact (fallback): if/then, or, not, bare atom -------- # + propositional = _parse_propositional(toks, clause) + if propositional is not None: + predicate, atoms, negated = propositional + for atom in atoms: + claim(atom, "proposition", span) + relations.append((predicate, atoms, span, negated)) return raise _Reject("no_template_match", clause) diff --git a/tests/test_capability_index.py b/tests/test_capability_index.py index edc80c32..71195357 100644 --- a/tests/test_capability_index.py +++ b/tests/test_capability_index.py @@ -87,7 +87,7 @@ def test_empty_index_is_well_defined() -> None: def test_real_lanes_compose_into_the_index_with_wrong_zero() -> None: - # The baseline: three structured-input reasoning lanes PLUS the three + # The baseline: three structured-input reasoning lanes PLUS the four # comprehension lanes (prose -> MeaningGraph -> projection -> independent # oracle) compose into the cross-domain index with zero wrong commits. from evals.capability_index.adapters import collect_domain_results @@ -97,7 +97,7 @@ def test_real_lanes_compose_into_the_index_with_wrong_zero() -> None: idx = aggregate(list(collection.results)) assert idx.wrong_total == 0 assert idx.assert_mode_valid - assert idx.breadth == 6 + assert idx.breadth == 7 assert {d.domain for d in idx.domains} == { "deductive_logic", "dimensional", @@ -105,6 +105,7 @@ def test_real_lanes_compose_into_the_index_with_wrong_zero() -> None: "comprehension_set_membership", "comprehension_syllogism", "comprehension_total_ordering", + "comprehension_propositional", } assert idx.capability_score > 0.5 # real, non-trivial cross-domain capability diff --git a/tests/test_comprehension_propositional.py b/tests/test_comprehension_propositional.py new file mode 100644 index 00000000..bfd16071 --- /dev/null +++ b/tests/test_comprehension_propositional.py @@ -0,0 +1,32 @@ +"""Phase 2b — end-to-end: the comprehension reader scored on propositional_logic. + +prose -> comprehend -> to_deductive_logic -> INDEPENDENT ROBDD oracle -> verdict vs +gold. The load-bearing invariant: wrong == 0 (the reader refuses rather than emit a +formula that yields a wrong verdict). This lane reads the classic propositional +argument forms (modus ponens/tollens, hypothetical & disjunctive syllogism) and the +classic fallacies (affirming the consequent, denying the antecedent), which the +oracle correctly marks ``unknown``. +""" + +from __future__ import annotations + +from evals.comprehension.propositional_runner import run + + +def test_comprehension_propositional_wrong_is_zero() -> None: + report = run() + assert report["wrong"] == 0, report["wrongs"] + + +def test_comprehension_propositional_has_real_coverage() -> None: + report = run() + assert report["correct"] > 0 + assert report["correct"] + report["refused"] == report["total"] + + +def test_comprehension_propositional_full_coverage() -> None: + # Every staged case is read end-to-end with zero wrong commits — atoms are + # single tokens / reserved-free multi-word NPs, so chunking is unambiguous. + report = run() + assert report["refused"] == 0 + assert report["correct"] == report["total"] diff --git a/tests/test_comprehension_reader.py b/tests/test_comprehension_reader.py index 9146e916..4fb9507c 100644 --- a/tests/test_comprehension_reader.py +++ b/tests/test_comprehension_reader.py @@ -357,3 +357,62 @@ def test_ambiguous_two_np_subset_query_refuses() -> None: comp = comprehend("Are all metal objects soft objects?") assert isinstance(comp, Refusal) assert comp.reason == "ambiguous_subset_query" + + +# --------------------------------------------------------------------------- # +# Propositional logic — if/then, not, or, bare atom, therefore (deductive_logic) +# --------------------------------------------------------------------------- # + + +def _qry(comp: Comprehension) -> tuple: + return tuple((q.predicate, q.arguments, q.negated) for q in comp.queries) + + +def test_conditional_is_implies() -> None: + comp = comprehend("If p then q.") + assert isinstance(comp, Comprehension) + assert _rel(comp, "implies") == (("implies", ("p", "q")),) + assert _entity_kind(comp, "p") == "proposition" + + +def test_bare_atom_is_asserted() -> None: + comp = comprehend("p.") + assert isinstance(comp, Comprehension) + assert _rel(comp, "asserted") == (("asserted", ("p",)),) + + +def test_not_atom_is_negated_assertion() -> None: + comp = comprehend("Not p.") + assert isinstance(comp, Comprehension) + rel = comp.meaning_graph.relations[0] + assert (rel.predicate, rel.arguments, rel.negated) == ("asserted", ("p",), True) + + +def test_disjunction_is_or() -> None: + comp = comprehend("p or q.") + assert isinstance(comp, Comprehension) + assert _rel(comp, "or") == (("or", ("p", "q")),) + + +def test_therefore_atom_is_asserted_query() -> None: + comp = comprehend("If p then q. p. Therefore q.") + assert isinstance(comp, Comprehension) + assert _qry(comp) == (("asserted", ("q",), False),) + + +def test_therefore_not_atom_is_negated_query() -> None: + comp = comprehend("If p then q. Not q. Therefore not p.") + assert isinstance(comp, Comprehension) + assert _qry(comp) == (("asserted", ("p",), True),) + + +def test_therefore_conditional_is_implies_query() -> None: + comp = comprehend("If p then q. If q then r. Therefore if p then r.") + assert isinstance(comp, Comprehension) + assert _qry(comp) == (("implies", ("p", "r"), False),) + + +def test_multiword_proposition_chunks_without_reserved_words() -> None: + comp = comprehend("If heavy rain then big flood.") + assert isinstance(comp, Comprehension) + assert _rel(comp, "implies") == (("implies", ("heavy_rain", "big_flood")),) diff --git a/tests/test_comprehension_wrong_zero_property.py b/tests/test_comprehension_wrong_zero_property.py index 0a6da290..0cb26539 100644 --- a/tests/test_comprehension_wrong_zero_property.py +++ b/tests/test_comprehension_wrong_zero_property.py @@ -23,6 +23,7 @@ from __future__ import annotations import random +from evals.deductive_logic.oracle import REFUSED, oracle_entailment from evals.set_membership.oracle import OracleError as SetError from evals.set_membership.oracle import oracle_answer as set_oracle from evals.syllogism.oracle import OracleError as SylError @@ -30,6 +31,7 @@ from evals.syllogism.oracle import oracle_answer as syl_oracle from evals.total_ordering.oracle import OracleError as OrdError from evals.total_ordering.oracle import oracle_answer as ord_oracle from generate.meaning_graph.projectors import ( + to_deductive_logic, to_set_membership, to_syllogism, to_total_ordering, @@ -304,3 +306,67 @@ def test_multiword_total_ordering_is_faithful_or_refuses() -> None: committed += 1 assert got == expected, (prose, got, expected) assert committed > 50 + + +# --------------------------------------------------------------------------- # +# Propositional logic — faithful entailment verdict or refuse (ROBDD oracle) +# --------------------------------------------------------------------------- # + +_ATOMS = [f"p{i}" for i in range(5)] + + +def _prop_fact(rng): + """Return (prose_clause, formula) for a random propositional premise.""" + kind = rng.choice(["implies", "or", "atom", "not_atom"]) + if kind == "implies": + a, b = rng.sample(_ATOMS, 2) + return f"If {a} then {b}.", f"{a} implies {b}" + if kind == "or": + a, b = rng.sample(_ATOMS, 2) + return f"{a} or {b}.", f"{a} or {b}" + if kind == "not_atom": + a = rng.choice(_ATOMS) + return f"Not {a}.", f"not {a}" + a = rng.choice(_ATOMS) + return f"{a}.", a + + +def _prop_query(rng): + """Return (conclusion_prose, formula) for a random propositional query.""" + kind = rng.choice(["atom", "not_atom", "implies"]) + if kind == "implies": + a, b = rng.sample(_ATOMS, 2) + return f"Therefore if {a} then {b}.", f"{a} implies {b}" + if kind == "not_atom": + a = rng.choice(_ATOMS) + return f"Therefore not {a}.", f"not {a}" + a = rng.choice(_ATOMS) + return f"Therefore {a}.", a + + +def test_propositional_reader_is_faithful_or_refuses() -> None: + rng = random.Random(161803) + committed = 0 + for _ in range(400): + n = rng.randint(1, 3) + facts = [_prop_fact(rng) for _ in range(n)] + concl_prose, query_formula = _prop_query(rng) + prose = " ".join(p for p, _ in facts) + " " + concl_prose + premises = tuple(f for _, f in facts) + expected = oracle_entailment(premises, query_formula) + + comp = comprehend(prose) + if isinstance(comp, Refusal): + continue + projected = to_deductive_logic(comp) + if projected is None: + continue + got = oracle_entailment(*projected) + if got == REFUSED: + continue # oracle could not evaluate -> decline, not a wrong + committed += 1 + # When the reader commits it must agree with the oracle's verdict on the + # ground-truth formulas (unless the ground truth itself was inconsistent). + if expected != REFUSED: + assert got == expected, (prose, got, expected, premises, query_formula) + assert committed > 50 diff --git a/tests/test_meaning_graph_projectors.py b/tests/test_meaning_graph_projectors.py index 73f2d4e8..8fe22459 100644 --- a/tests/test_meaning_graph_projectors.py +++ b/tests/test_meaning_graph_projectors.py @@ -8,7 +8,11 @@ silent wrong). from __future__ import annotations -from generate.meaning_graph.projectors import to_syllogism, to_total_ordering +from generate.meaning_graph.projectors import ( + to_deductive_logic, + to_syllogism, + to_total_ordering, +) from generate.meaning_graph.reader import Comprehension, comprehend @@ -108,3 +112,32 @@ def test_one_graph_projects_only_to_its_domain() -> None: comp = _comp("All mammals are animals. Therefore all mammals are animals.") assert to_syllogism(comp) is not None assert to_total_ordering(comp) is None + assert to_deductive_logic(comp) is None # categorical relations -> not propositional + + +# --------------------------------------------------------------------------- # +# to_deductive_logic +# --------------------------------------------------------------------------- # + + +def test_to_deductive_logic_serializes_formulas() -> None: + comp = _comp("If p then q. p. Therefore q.") + projected = to_deductive_logic(comp) + assert projected is not None + premises, query = projected + assert set(premises) == {"p implies q", "p"} + assert query == "q" + + +def test_to_deductive_logic_serializes_negation_and_disjunction() -> None: + comp = _comp("p or q. Not q. Therefore p.") + projected = to_deductive_logic(comp) + assert projected is not None + premises, query = projected + assert set(premises) == {"p or q", "not q"} + assert query == "p" + + +def test_to_deductive_logic_none_for_categorical_comprehension() -> None: + # No propositional relations / query -> nothing askable of the entailment oracle. + assert to_deductive_logic(_comp("All mammals are animals.")) is None