core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions

feat(comprehend): propositional-logic comprehension (4th domain, flagship oracle)

Browse source 
Adds comprehension_propositional — the comprehension organ now reads the classic
propositional ARGUMENT FORMS end-to-end into the flagship deductive_logic ROBDD
oracle (the most robustly independent gold in the repo). The neutral MeaningGraph
now feeds FOUR independent oracles (set-membership, syllogism-validity,
total-ordering, propositional-entailment) from one interlingua — the Option-B
interlingua thesis validated.

reader.py: propositional templates (atoms are chunked NP ids; fits the existing
entities + n-ary relations + negation model — NO interlingua change, propositional
is not arithmetic-quantities):
  - "if <P> then <Q>"        -> implies(P, Q)
  - "not <P>"                -> asserted(P, negated=True)
  - "<P> or <Q>"             -> or(P, Q)
  - "<P>" (single token)     -> asserted(P)   (bare-atom, single-token only to
                                                keep the parse-or-refuse floor)
  - "therefore <prop>"       -> query of the same predicate
Relations now carry a negated flag end-to-end (asserted negation).

projectors.py: to_deductive_logic serializes propositional relations/query into
formula strings (keyword operators the oracle tokenizer accepts); returns None
(refusal) unless the comprehension is purely propositional, so categorical/ordering
comprehensions never leak into the entailment oracle.

evals: new evals/propositional_logic/v1 (12 cases — modus ponens/tollens,
hypothetical & disjunctive syllogism, the affirming-consequent / denying-antecedent
fallacies which the oracle marks "unknown"; gold = oracle verdict) + gold-only
runner + evals/comprehension/propositional_runner.py. Oracle "refused" (formula
unevaluable) is treated as a decline, never a wrong.

Scores: comprehension_propositional 12/12 wrong=0 (full coverage); no regression on
the 3 existing lanes (8/8, 7/8, 7/8). Capability index breadth 6->7, score
0.917231 -> 0.928622, wrong_total 0, digest 51df7bba…

Tests: reader propositional templates; to_deductive_logic projector tests;
end-to-end full-coverage wrong=0; propositional generative round-trip added to the
wrong=0 property suite (verified to BITE under a reversed-implies mutation);
capability breadth 6->7. 115 targeted + 87 smoke green. Lane SHAs 8/9 (sole miss =
public_demo env wall-clock flake; deductive_logic_v1 unchanged).
This commit is contained in:
Shay 2026-06-05 23:24:54 -07:00
parent 07f1c235a9
commit f66f2ee47f
13 changed files with 457 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
evals/capability_index/adapters.py
View file

@ -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,
)

18
evals/capability_index/baseline.json
View file

@ -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,

71
evals/comprehension/propositional_runner.py Normal file
View file

@ -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())

0
evals/propositional_logic/__init__.py Normal file
View file

59
evals/propositional_logic/runner.py Normal file
View file

@ -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())

12
evals/propositional_logic/v1/cases.jsonl Normal file
View file

@ -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"}

43
generate/meaning_graph/projectors.py
View file

@ -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

71
generate/meaning_graph/reader.py
View file

@ -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 <P> then <Q>`` -> ("implies", (P, Q), False)
``not <P>`` -> ("asserted", (P,), True)
``<P> or <Q>`` -> ("or", (P, Q), False)
``<P>`` (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 <categorical>" ------------------- #
# --- conclusion: "therefore <categorical | propositional>" ------------- #
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] <X> a|an <Y>?" ------------------------ #
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] <X> is a|an <Y>" -------------------------- #
@ -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: "<X> [is] <comp> [than] <Y>" ----------------------- #
@ -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)

5
tests/test_capability_index.py
View file

@ -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

32
tests/test_comprehension_propositional.py Normal file
View file

@ -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"]

59
tests/test_comprehension_reader.py
View file

@ -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")),)

66
tests/test_comprehension_wrong_zero_property.py
View file

@ -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

35
tests/test_meaning_graph_projectors.py
View file

@ -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