diff --git a/evals/proofwriter_owa/fixtures.jsonl b/evals/proofwriter_owa/fixtures.jsonl new file mode 100644 index 00000000..63db8438 --- /dev/null +++ b/evals/proofwriter_owa/fixtures.jsonl @@ -0,0 +1,19 @@ +{"id": "owa-001", "facts": ["Rex is a dog.", "All dogs are mammals."], "query": "Is Rex a mammal?", "expected": "True", "serving_support": true, "note": "member then subset (member o subset)"} +{"id": "owa-002", "facts": ["Rex is a dog.", "All dogs are mammals.", "All mammals are animals."], "query": "Is Rex an animal?", "expected": "True", "serving_support": true, "note": "member o subset o subset"} +{"id": "owa-003", "facts": ["All dogs are mammals."], "query": "Are all dogs mammals?", "expected": "True", "serving_support": true, "note": "direct subset"} +{"id": "owa-004", "facts": ["All dogs are mammals.", "All mammals are animals."], "query": "Are all dogs animals?", "expected": "True", "serving_support": true, "note": "subset o subset"} +{"id": "owa-005", "facts": ["Truth is a concept."], "query": "Is truth a concept?", "expected": "True", "serving_support": true, "note": "direct member"} +{"id": "owa-006", "facts": ["Alice is the parent of Bob."], "query": "Is Alice the parent of Bob?", "expected": "True", "serving_support": true, "note": "relational direct"} +{"id": "owa-007", "facts": ["Bob is the child of Alice."], "query": "Is Alice the parent of Bob?", "expected": "True", "serving_support": true, "note": "relational inverse one-hop (#775)"} +{"id": "owa-008", "facts": ["Alice is the sibling of Bob."], "query": "Is Bob the sibling of Alice?", "expected": "True", "serving_support": true, "note": "relational symmetric one-hop (#775)"} +{"id": "owa-009", "facts": ["Bob is less than Alice."], "query": "Is Alice greater than Bob?", "expected": "True", "serving_support": true, "note": "relational inverse order one-hop (#775)"} +{"id": "owa-010", "facts": ["All dogs are mammals."], "query": "Are all mammals dogs?", "expected": "Unknown", "serving_support": false, "note": "reverse subset is not entailed"} +{"id": "owa-011", "facts": ["Rex is a dog.", "All cats are mammals."], "query": "Is Rex a mammal?", "expected": "Unknown", "serving_support": false, "note": "no chain: dog has no superclass given"} +{"id": "owa-012", "facts": ["Alice is the sibling of Bob."], "query": "Is Alice the parent of Bob?", "expected": "Unknown", "serving_support": false, "note": "cross-predicate: sibling does not imply parent"} +{"id": "owa-013", "facts": ["Alice is less than Bob."], "query": "Is Bob less than Alice?", "expected": "Unknown", "serving_support": false, "note": "asymmetric: a is a[n] ." -> member(x, y) + "All are ." -> subset(x, y) (regular plurals) + "No is a[n] ." -> disjoint(x, y) + " is [the] ." -> rel(lemma, a, b) + query: "Is a[n] ?" -> member?(x, y) + "Are all ?" -> subset?(x, y) + "Is [the] ?" -> rel?(lemma, a, b) + +OWA semantics: + member?(x, y): True if y is in the is-a closure of x's classes; False if some class + in that closure is declared disjoint from y; else Unknown. + subset?(x, y): True if y is in x's superclass closure; False if some class in that + closure is disjoint from y; else Unknown. + rel?(lemma, a, b): True on a direct edge, a declared INVERSE edge (b,a), or a declared + SYMMETRIC edge (b,a) — ONE hop only. Else Unknown. (No transitive relational + chains in B1; no relational negation in this grammar.) +""" + +from __future__ import annotations + +import re + +# The oracle's OWN relational ontology — declared here, NOT imported from +# generate.meaning_graph.relational, so the gold producer stays disjoint from the +# solver. (It mirrors the pack's algebra for the predicates this fixture uses.) +_INVERSE: dict[str, str] = { + "less_than": "greater_than", "greater_than": "less_than", + "parent_of": "child_of", "child_of": "parent_of", + "left_of": "right_of", "right_of": "left_of", + "before_event": "after_event", "after_event": "before_event", +} +_SYMMETRIC: frozenset[str] = frozenset({ + "sibling_of", "spouse_of", "equal_to", "distinct_from", "adjacent_to", +}) +_CONNECTIVE: dict[str, str] = { + "parent of": "parent_of", "child of": "child_of", "sibling of": "sibling_of", + "spouse of": "spouse_of", "less than": "less_than", "greater than": "greater_than", + "equal to": "equal_to", "distinct from": "distinct_from", + "left of": "left_of", "right of": "right_of", "inside of": "inside_of", + "adjacent to": "adjacent_to", +} +# longest connective first so "parent of" wins before any single-token prefix +_CONN_ALT = "|".join(re.escape(k) for k in sorted(_CONNECTIVE, key=len, reverse=True)) + +_MEMBER = re.compile(r"^(\w+) is an? (\w+)\.$") +_SUBSET = re.compile(r"^All (\w+) are (\w+)\.$") +_DISJOINT = re.compile(r"^No (\w+) is an? (\w+)\.$") +_REL = re.compile(rf"^(\w+) is (?:the )?({_CONN_ALT}) (\w+)\.$") + +_Q_MEMBER = re.compile(r"^Is (\w+) an? (\w+)\?$") +_Q_SUBSET = re.compile(r"^Are all (\w+) (\w+)\?$") +_Q_REL = re.compile(rf"^Is (\w+) (?:the )?({_CONN_ALT}) (\w+)\?$") + + +class OracleParseError(ValueError): + """A fixture string is outside the closed B1 grammar — fail loudly, never guess.""" + + +def _sing(word: str) -> str: + """Singularize a regular plural class noun ('dogs' -> 'dog'). Used ONLY in the + explicitly-plural slots of the subset patterns, so 'species'/'Socrates' (which only + appear in singular `is a` slots) are never mangled.""" + w = word.lower() + return w[:-1] if w.endswith("s") and not w.endswith("ss") else w + + +def parse_fact(text: str) -> tuple: + t = text.strip() + if (m := _DISJOINT.match(t)): + return ("disjoint", m.group(1).lower(), m.group(2).lower()) + if (m := _SUBSET.match(t)): + return ("subset", _sing(m.group(1)), _sing(m.group(2))) + if (m := _REL.match(t)): + return ("rel", _CONNECTIVE[m.group(2)], m.group(1).lower(), m.group(3).lower()) + if (m := _MEMBER.match(t)): + return ("member", m.group(1).lower(), m.group(2).lower()) + raise OracleParseError(f"unparseable fact: {text!r}") + + +def parse_query(text: str) -> tuple: + t = text.strip() + if (m := _Q_REL.match(t)): + return ("rel?", _CONNECTIVE[m.group(2)], m.group(1).lower(), m.group(3).lower()) + if (m := _Q_SUBSET.match(t)): + return ("subset?", _sing(m.group(1)), _sing(m.group(2))) + if (m := _Q_MEMBER.match(t)): + return ("member?", m.group(1).lower(), m.group(2).lower()) + raise OracleParseError(f"unparseable query: {text!r}") + + +def _closure(start: str, supers: dict[str, set[str]]) -> set[str]: + """`start` plus every superclass reachable over subset edges (BFS, deterministic).""" + seen = {start} + stack = [start] + while stack: + node = stack.pop() + for sup in sorted(supers.get(node, ())): + if sup not in seen: + seen.add(sup) + stack.append(sup) + return seen + + +def label(facts: list[str], query: str) -> str: + """The OWA gold label for `query` given `facts`: 'True' | 'Unknown' | 'False'.""" + members: dict[str, set[str]] = {} + supers: dict[str, set[str]] = {} + disjoint: set[frozenset[str]] = set() + rels: set[tuple[str, str, str]] = set() + for text in facts: + f = parse_fact(text) + if f[0] == "member": + members.setdefault(f[1], set()).add(f[2]) + elif f[0] == "subset": + supers.setdefault(f[1], set()).add(f[2]) + elif f[0] == "disjoint": + disjoint.add(frozenset((f[1], f[2]))) + else: # rel + rels.add((f[1], f[2], f[3])) + + q = parse_query(query) + if q[0] == "member?": + _, subj, cls = q + reach: set[str] = set() + for c0 in members.get(subj, ()): + reach |= _closure(c0, supers) + if cls in reach: + return "True" + if any(frozenset((d, cls)) in disjoint for d in reach): + return "False" + return "Unknown" + if q[0] == "subset?": + _, x, y = q + clo = _closure(x, supers) + if y in clo: + return "True" + if any(frozenset((d, y)) in disjoint for d in clo): + return "False" + return "Unknown" + # rel? + _, lemma, a, b = q + if (lemma, a, b) in rels: + return "True" + inv = _INVERSE.get(lemma) + if inv is not None and (inv, b, a) in rels: + return "True" + if lemma in _SYMMETRIC and (lemma, b, a) in rels: + return "True" + return "Unknown" diff --git a/evals/proofwriter_owa/provenance.md b/evals/proofwriter_owa/provenance.md new file mode 100644 index 00000000..745e7f40 --- /dev/null +++ b/evals/proofwriter_owa/provenance.md @@ -0,0 +1,46 @@ +# evals/proofwriter_owa — provenance (B1: OWA refusal floor) + +The ProofWriter-OWA refusal-floor lane (mastery-v2 Step 3, Brief 1). It proves the +open-world soundness floor: the engine's `determine()` never asserts a query `True` when +the open-world truth is `Unknown` or `False`. It hardens "unknown ≠ false" before the +transitive-chain (B2) and closed-world (B4) work can stress it. + +## Independent gold (oracle), not a dataset slice + +This environment has no live ProofWriter dataset access, so the items are **hand-authored +in ProofWriter-OWA style** — small is-a / relational theories + one yes/no query — rather +than verbatim dataset rows. Critically, the gold label is **not** hand-asserted: it is +computed by a **separate minimal oracle** (`oracle.py`) with its own parser and its own +OWA reasoner, importing **none** of `determine`, `comprehend` / MeaningGraph realization, +or the production predicate-entailment helpers (INV-25 / INV-27 — the gold producer is +disjoint from the solver). The fixture's hand-authored `expected` field pins the oracle's +output, so the oracle is itself verified (`test_oracle_matches_authored_expected`). + +Source / semantics reference: AllenAI **ProofWriter** (V2020.12.3, arXiv:2012.13048) — the +open-world `{True, Unknown, False}` label semantics. Attribution only; no dataset +redistribution. + +## What the lane checks + +- **`wrong == 0`** — `determine()` asserts `True` only on a gold-`True` item. A `True` + assertion on a gold `Unknown` OR `False` is a soundness breach. (`determine()` is sound, + so this is a hard floor; the lane makes any regression *findable* against the + independent oracle.) +- gold-`True` items marked `serving_support` (member/subset subsumption, plus #775 + inverse/symmetric one-hop) **must** determine `True` — no silent coverage loss. +- no `answer=False` is ever constructed (INV-30 holds, behaviorally re-checked here). + +## Scope (oracle grammar) + +member / subset / is-a closure; explicit negation (`No X is a Y` → disjointness, the +source of every gold-`False`); and #775 inverse/symmetric **one-hop** relational rules. +**No transitive relational chains** — that is Brief 2; an "oracle-only gold side" hook is +left for when it lands. + +This lane is **measure-only**: it touches no engine code and is deliberately **not a +capability-index domain** (a refusal floor has low coverage and would drag the index's +`coverage_geomean`). It runs as its own standalone wrong=0 gate. + +## Current result + +`19 items → 9 correct (all serving_support True), 10 refused (Unknown/False), 0 wrong`. diff --git a/evals/proofwriter_owa/score.py b/evals/proofwriter_owa/score.py new file mode 100644 index 00000000..d5128601 --- /dev/null +++ b/evals/proofwriter_owa/score.py @@ -0,0 +1,117 @@ +"""Score the ProofWriter-OWA refusal floor: `determine()` vs the independent oracle. + +For each fixture item: compute the OWA gold with the disjoint `oracle.label(...)`, then run +the production path (`comprehend`/`comprehend_relational` -> `realize` -> `determine`) and +compare. The invariant is **wrong=0**: `determine()` may assert True only on a gold-`True` +item; asserting True on a gold `Unknown` or `False` is a soundness breach (it would mean +the engine claimed entailment where the open world does not entail it). + +Measure-only — imports no `generate.derivation` / `core.reliability_gate`; NOT a +capability-index domain. A refusal on a gold-`True` item is a coverage miss (recorded), +never a wrong — UNLESS the item is marked `serving_support` (within the engine's claimed +support), in which case it must determine True. +""" + +from __future__ import annotations + +import json +import sys +from pathlib import Path +from typing import Any + +from chat.runtime import ChatRuntime +from evals.proofwriter_owa.oracle import label as owa_label +from generate.determine import Determined, determine +from generate.meaning_graph.reader import Refusal, comprehend +from generate.meaning_graph.relational import ( + comprehend_relational, + load_relational_pack_lemmas, +) +from generate.realize import realize_comprehension +from session.context import SessionContext + +_FIXTURES = Path(__file__).resolve().parent / "fixtures.jsonl" +_HIGH = 10**9 + + +def _load(path: Path = _FIXTURES) -> list[dict[str, Any]]: + return [ + json.loads(line) + for line in path.read_text(encoding="utf-8").splitlines() + if line.strip() + ] + + +def _comprehend_any(text: str, pack): + """Relational reader first (specific), else the general comprehension reader.""" + c = comprehend_relational(text, pack) + if isinstance(c, Refusal): + return comprehend(text) + return c + + +def run(path: Path = _FIXTURES) -> dict[str, Any]: + items = _load(path) + pack = load_relational_pack_lemmas() + rt = ChatRuntime(no_load_state=True) + vocab, persona = rt._context.vocab, rt._context.persona + + correct = refused = wrong = 0 + wrongs: list[dict[str, Any]] = [] + coverage_gaps: list[dict[str, Any]] = [] # serving_support gold-True that refused + + for it in items: + gold = owa_label(it["facts"], it["query"]) + ctx = SessionContext( + vocab=vocab, persona=persona, vault_reproject_interval=_HIGH + ) + for fact in it["facts"]: + realize_comprehension(_comprehend_any(fact, pack), ctx) + res = determine(_comprehend_any(it["query"], pack), ctx) + asserted_true = isinstance(res, Determined) and res.answer is True + + if asserted_true and gold == "True": + correct += 1 + elif asserted_true: # gold Unknown/False but engine asserted True -> BREACH + wrong += 1 + wrongs.append({"id": it["id"], "gold": gold, "query": it["query"]}) + else: + refused += 1 + if it.get("serving_support") and gold == "True": + coverage_gaps.append({"id": it["id"], "query": it["query"]}) + + return { + "domain": "proofwriter_owa", + "total": len(items), + "correct": correct, + "refused": refused, + "wrong": wrong, + "wrongs": wrongs, + "coverage_gaps": coverage_gaps, + "counts": {"correct": correct, "wrong": wrong, "refused": refused}, + } + + +def main() -> int: + r = run() + print(json.dumps({k: v for k, v in r.items() if k != "wrongs"}, indent=2, sort_keys=True)) + failed = False + if r["wrong"]: + print( + "WRONG > 0 — determine asserted True on a non-True OWA gold (soundness breach):", + file=sys.stderr, + ) + print(json.dumps(r["wrongs"], indent=2), file=sys.stderr) + failed = True + if r["coverage_gaps"]: + print( + "COVERAGE GAPS — serving-supported gold-True items refused (acceptance breach):", + file=sys.stderr, + ) + print(json.dumps(r["coverage_gaps"], indent=2), file=sys.stderr) + failed = True + return 1 if failed else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/test_proofwriter_owa_lane.py b/tests/test_proofwriter_owa_lane.py new file mode 100644 index 00000000..320705ce --- /dev/null +++ b/tests/test_proofwriter_owa_lane.py @@ -0,0 +1,76 @@ +"""Lane test — ProofWriter-OWA refusal floor (B1, measure-only). + +The independent oracle computes the OWA gold; the production `determine()` path must never +assert True on a non-`True` gold (wrong=0 — the soundness floor). The oracle is itself +pinned to the fixture's hand-authored `expected`. This is NOT a capability-index domain. +""" + +from __future__ import annotations + +import hashlib +from pathlib import Path + +import pytest + +from chat.runtime import ChatRuntime +from evals.proofwriter_owa.oracle import label as owa_label +from evals.proofwriter_owa.score import _comprehend_any, _load, run +from generate.determine import Determined, determine +from generate.meaning_graph.relational import load_relational_pack_lemmas +from generate.realize import realize_comprehension +from session.context import SessionContext + +_FIXTURES = ( + Path(__file__).resolve().parent.parent + / "evals" + / "proofwriter_owa" + / "fixtures.jsonl" +) +_FIXTURES_SHA = "7b340849a945d27306793a109fd65532803be40281b6da15809f9d33ea7f6580" +_HIGH = 10**9 + + +def test_fixtures_sha_pinned() -> None: + got = hashlib.sha256(_FIXTURES.read_bytes()).hexdigest() + assert got == _FIXTURES_SHA, f"fixtures.jsonl drifted: {got}" + + +def test_oracle_matches_authored_expected() -> None: + """Pin the independent oracle to the hand-authored intent — the oracle is verified, + so its gold can be trusted as the disjoint reference for `determine()`.""" + for it in _load(): + assert owa_label(it["facts"], it["query"]) == it["expected"], it["id"] + + +@pytest.fixture(scope="module") +def report(): + return run() + + +def test_refusal_floor_wrong_zero(report) -> None: + """THE floor: `determine()` never asserts True on a gold `Unknown`/`False`.""" + assert report["wrong"] == 0, report["wrongs"] + + +def test_serving_support_truths_are_determined(report) -> None: + """Every gold-`True` item inside the engine's claimed support determines True — + no silent coverage loss — and the lane actually exercises a positive path.""" + assert report["coverage_gaps"] == [], report["coverage_gaps"] + assert report["correct"] > 0 + + +def test_no_answer_false_constructed() -> None: + """Behavioral echo of INV-30: across every item, `determine()` never yields + `answer=False` (the open-world gear is True-or-refuse).""" + pack = load_relational_pack_lemmas() + rt = ChatRuntime(no_load_state=True) + vocab, persona = rt._context.vocab, rt._context.persona + for it in _load(): + ctx = SessionContext( + vocab=vocab, persona=persona, vault_reproject_interval=_HIGH + ) + for fact in it["facts"]: + realize_comprehension(_comprehend_any(fact, pack), ctx) + res = determine(_comprehend_any(it["query"], pack), ctx) + if isinstance(res, Determined): + assert res.answer is True, it["id"]