From 5f274b75b7a0874a1fb98e86d5ddcc7e47ea0982 Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 4 Jun 2026 20:17:33 -0700 Subject: [PATCH] feat(deductive): binary relations + multi-variable grounding (finite propositional) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends evals/deductive_logic/grounding.py from unary predicates / single-var rules to binary relations + multi-variable universal rules, still by FINITE PROPOSITIONAL grounding into the regime the ROBDD engine + the independent truth-table oracle both decide. wrong==0 stays structural. This is the real capability step a RuleTaker/ ProofWriter-style mirror needs (the unary fragment alone is trivial). - atom_n lowers pred(a,b) -> pred__a__b; arity-1 is byte-identical to the old atom, so the live unary panel lowers unchanged (proven by an exact-string back-compat test). - multi-variable universal rules ground over n^k assignments — transitivity now decides. - range-restriction: a rule with a head variable unbound in the body refuses (unsafe_rule) — it grounds soundly but is outside the clean regime real benchmarks use. - typed refusals: arity>=3/functions, explicit quantifiers, variable-free rules, bounds. Honest ceilings (documented in docs/analysis/relational-grounding-extension-2026-06-04.md): - THE binding constraint is the GOLD, not the grammar: the truth-table oracle is O(2^atoms), so grounding refuses above MAX_GROUND_ATOMS=20 => binary problems cap at ~4 entities/predicate. A real lift needs a 2nd genuinely-independent sub-enumeration oracle (not built). - OPEN-WORLD only: RuleTaker/ProofWriter's main splits are closed-world + NAF; a future adapter MUST refuse CWA/NAF (mapping CWA "False"->"refuted" is a wrong=0 breach). - arity <= 2, function-free. Validated: held-out differential fuzz (400 random binary problems, oracle-golded) = 0 engine/oracle mismatches; unary back-compat byte-identical; INV-25b reproducibility green; deductive lane wrong=0 16/16; smoke 87. --- ...lational-grounding-extension-2026-06-04.md | 62 +++++ evals/deductive_logic/grounding.py | 238 +++++++++++++----- ...deductive_logic_finite_entity_grounding.py | 10 +- ...st_deductive_logic_relational_grounding.py | 237 +++++++++++++++++ 4 files changed, 477 insertions(+), 70 deletions(-) create mode 100644 docs/analysis/relational-grounding-extension-2026-06-04.md create mode 100644 tests/test_deductive_logic_relational_grounding.py diff --git a/docs/analysis/relational-grounding-extension-2026-06-04.md b/docs/analysis/relational-grounding-extension-2026-06-04.md new file mode 100644 index 00000000..f21e99f7 --- /dev/null +++ b/docs/analysis/relational-grounding-extension-2026-06-04.md @@ -0,0 +1,62 @@ + + +# Binary-relation + multi-variable grounding extension + +Extends the finite-entity grounding (`evals/deductive_logic/grounding.py`) from **unary +predicates / single-variable rules** to **binary relations + multi-variable universal +rules**, still by **finite propositional grounding** into the regime the ROBDD entailment +operator and the independent truth-table oracle both decide. `wrong == 0` stays structural. +This is the real capability step that makes a RuleTaker/ProofWriter-style mirror cover +anything beyond the trivial unary fragment — the prerequisite the runway doc's PR-3 needs. + +## What landed + +- **Arity 1–2.** A literal is legacy unary `{predicate, entity|var, polarity}` OR general + `{predicate, args:[{entity|var: str}, ...], polarity}`. `atom_n` lowers + `predicate(a, b)` → `predicate__a__b`; arity-1 is byte-identical to the old `atom`, so + every pre-existing unary problem lowers unchanged (proven). +- **Multi-variable universal rules**, grounded by enumerating every assignment of the + rule's variables to named entities (`n^k`). The canonical transitive rule + `∀x,y,z. bigger(x,y) ∧ bigger(y,z) → bigger(x,z)` now grounds and decides correctly. +- **Range-restriction (safety).** A rule whose head contains a variable unbound in the + body (`p(x) → q(y)`) refuses (`unsafe_rule`) — it grounds soundly but is outside the + clean regime real benchmarks use. Narrowness is the firewall. +- **Refusals** (typed): arity ≥ 3 / functions (`unsupported_predicate_arity`); explicit + quantifiers (`unsupported_quantifier`); a variable-free rule (`unsupported_quantifier`); + and the bounds below (`grounding_bound_exceeded`). + +## The honest ceilings (these are real limits, not hidden) + +1. **The binding constraint is the independent GOLD, not the grammar.** The INV-25 gold is + a truth-table oracle — **O(2^atoms)**. Binary relations explode the atom count + (`n` entities → up to `n²` atoms per binary predicate). So the grounding refuses above + `MAX_GROUND_ATOMS = 20` (2²⁰ ≈ 1e6 assignments, decidable). **Consequence: binary + problems cap at ~4 entities per predicate.** That is the true coverage ceiling — bigger + problems refuse. (A future lift would need a *second* sub-enumeration oracle that is + still genuinely independent of the ROBDD — non-trivial; not done.) +2. **Open-world only.** The grounding decides classical (monotone, open-world) entailment: + underivable ⇒ `unknown`, not `false`. RuleTaker / ProofWriter's main splits are + **closed-world with negation-as-failure** (underivable ⇒ False). Any future benchmark + adapter **must refuse CWA/NAF cases** — mapping a CWA "False" to "refuted" would be a + `wrong=0` breach. Only the **OWA** split is honestly mirrorable. +3. **Function-free, arity ≤ 2.** Ternary+ relations and functions refuse. + +## Validation (held-out, not hand-authored) + +- **Differential fuzz:** 400 randomly-generated binary problems (binary facts + a + transitive rule), gold computed by the **independent truth-table oracle**, decided by + the **ROBDD engine** — **0 engine/oracle mismatches** on every in-regime case. This is + the anti-overfit check: the gold is oracle-derived on data the grammar was not authored + against, so it is a real `wrong=0` signal, not a 15-case hand-authored echo. +- **Back-compat:** the unary path lowers byte-identically; the committed finite-entity + gold is still reproduced by the independent oracle (INV-25b green); deductive lane + `wrong=0` unchanged; smoke green. + +## What this unblocks / what it does NOT claim + +- Unblocks: a ProofWriter-**OWA**, function-free, ≤2-arity, small-entity adapter (the + runway's PR-3) that can cover *relational/transitive* cases, not just the unary fragment. +- Does **not** claim any benchmark number: the actual RuleTaker/ProofWriter data is **not + in the repo**. A real number requires obtaining the dataset (license-checked) and is + explicitly scoped to "the OWA function-free ≤2-arity small fragment," with everything + else refused — never "ProofWriter accuracy." diff --git a/evals/deductive_logic/grounding.py b/evals/deductive_logic/grounding.py index eb125434..9f8f3a8d 100644 --- a/evals/deductive_logic/grounding.py +++ b/evals/deductive_logic/grounding.py @@ -28,7 +28,9 @@ Sealed: no ``chat`` import, no serving path. Deterministic. from __future__ import annotations import re +from collections.abc import Sequence from dataclasses import dataclass +from itertools import product from typing import Any, Final # Closed refusal vocabulary for the grounding layer — distinct from the entailment @@ -40,6 +42,14 @@ UNKNOWN_ENTITY: Final[str] = "unknown_entity" UNKNOWN_VARIABLE: Final[str] = "unknown_variable" MALFORMED_CASE: Final[str] = "malformed_case" EMPTY_CASE: Final[str] = "empty_case" +# A rule whose head contains a variable not bound in its body (non-range-restricted / +# "unsafe" in Datalog terms). It grounds soundly, but it is outside the clean regime +# real rule benchmarks use; refuse rather than silently widen scope. +UNSAFE_RULE: Final[str] = "unsafe_rule" +# The independent gold is a truth-table oracle, O(2^atoms); the grounding refuses a +# problem whose distinct-atom count (or entity/variable count) would make that gold +# intractable, rather than emit something the wrong=0 arbiter cannot decide. +GROUNDING_BOUND_EXCEEDED: Final[str] = "grounding_bound_exceeded" GROUNDING_REASONS: Final[frozenset[str]] = frozenset({ UNSUPPORTED_PREDICATE_ARITY, @@ -49,8 +59,25 @@ GROUNDING_REASONS: Final[frozenset[str]] = frozenset({ UNKNOWN_VARIABLE, MALFORMED_CASE, EMPTY_CASE, + UNSAFE_RULE, + GROUNDING_BOUND_EXCEEDED, }) +# --------------------------------------------------------------------------- +# Bounds (v1.5: binary relations + multi-variable rules by finite grounding). +# --------------------------------------------------------------------------- +# Arity ceiling — unary + binary only; arity >= 3 refuses (functions never). +MAX_ARITY: Final[int] = 2 +# A rule grounds over n^k assignments (n entities, k distinct variables). These two +# bound n and k so n^k cannot blow up before the atom bound below is even checked. +MAX_ENTITIES: Final[int] = 8 +MAX_VARS_PER_RULE: Final[int] = 3 +# THE binding constraint: the independent truth-table oracle is O(2^atoms). The +# lowered problem's distinct-atom count must stay small or the gold is intractable. +# 2^20 ~ 1e6 assignments — decidable; binary relations therefore cap at ~4 entities +# per predicate. This is the honest coverage ceiling of the binary extension. +MAX_GROUND_ATOMS: Final[int] = 20 + _ATOM_SEPARATOR: Final[str] = "__" # A slug component: lowercase ASCII letters/digits/single underscores, no leading # digit, no empty, no double-underscore (would collide with the separator). @@ -96,11 +123,21 @@ def atom(predicate: Any, entity: Any) -> str: return f"{slug(predicate)}{_ATOM_SEPARATOR}{slug(entity)}" -def _literal(predicate: Any, entity: Any, polarity: Any) -> str: +def atom_n(predicate: Any, entity_slugs: Sequence[str]) -> str: + """``predicate(arg1, ..., argk)`` → the canonical propositional atom. + + Arity 1 is byte-identical to :func:`atom` (``predicate__entity``), so every + pre-existing unary problem lowers unchanged. The ``__`` separator between args + cannot collide with a slug (slugs reject ``__``), so the atom is injective in + ``(predicate, args)`` and arity-1 vs arity-2 atoms never alias. + """ + return _ATOM_SEPARATOR.join([slug(predicate), *(slug(e) for e in entity_slugs)]) + + +def _lit_str(atom_str: str, polarity: Any) -> str: if not isinstance(polarity, bool): raise GroundingError(MALFORMED_CASE, f"polarity must be a bool, got {polarity!r}") - a = atom(predicate, entity) - return a if polarity else f"~{a}" + return atom_str if polarity else f"~{atom_str}" def _require(condition: bool, reason: str, detail: str = "") -> None: @@ -108,94 +145,161 @@ def _require(condition: bool, reason: str, detail: str = "") -> None: raise GroundingError(reason, detail) -def _check_unary(obj: dict[str, Any], *, allow_var: bool) -> None: - """Reject any non-unary / relational / functional shape (v1 is unary only).""" - keys = set(obj) - # A binary relation / function would carry extra argument keys. - extra = keys - {"predicate", "entity", "var", "polarity"} - _require(not extra, UNSUPPORTED_PREDICATE_ARITY, f"unexpected keys {sorted(extra)}") - has_entity = "entity" in obj - has_var = "var" in obj - if allow_var: - _require(has_entity ^ has_var, MALFORMED_CASE, "literal needs exactly one of entity/var") +# A term is ("entity", name) or ("var", name) — name is the raw case string. +_Term = tuple[str, str] +_NormLiteral = tuple[Any, tuple[_Term, ...], bool] + + +def _normalize_term(arg: Any, *, allow_var: bool) -> _Term: + _require(isinstance(arg, dict), MALFORMED_CASE, f"arg not a mapping: {arg!r}") + extra = set(arg) - {"entity", "var"} + _require(not extra, MALFORMED_CASE, f"unexpected arg keys {sorted(extra)}") + has_entity, has_var = "entity" in arg, "var" in arg + _require(has_entity ^ has_var, MALFORMED_CASE, "arg needs exactly one of entity/var") + if has_var: + _require(allow_var, UNKNOWN_VARIABLE, "free variable outside a rule") + v = arg["var"] + _require(isinstance(v, str) and bool(v.strip()), MALFORMED_CASE, "empty variable") + return ("var", v) + return ("entity", arg["entity"]) + + +def _normalize_literal(obj: Any, *, allow_var: bool) -> _NormLiteral: + """Normalize a literal — legacy unary ``{entity|var}`` OR general + ``{args:[{entity|var},...]}`` — to ``(predicate, terms, polarity)``. Refuses + arity 0 / > :data:`MAX_ARITY` (functions and ternary relations) with a typed reason. + """ + _require(isinstance(obj, dict), MALFORMED_CASE, f"literal not a mapping: {obj!r}") + _require("predicate" in obj, MALFORMED_CASE, "literal missing predicate") + polarity = obj.get("polarity", True) + _require(isinstance(polarity, bool), MALFORMED_CASE, f"polarity must be bool: {polarity!r}") + + if "args" in obj: + _require("entity" not in obj and "var" not in obj, MALFORMED_CASE, + "use 'args' OR 'entity'/'var', not both") + extra = set(obj) - {"predicate", "args", "polarity"} + _require(not extra, UNSUPPORTED_PREDICATE_ARITY, f"unexpected keys {sorted(extra)}") + args = obj["args"] + _require(isinstance(args, list) and bool(args), MALFORMED_CASE, "args must be a non-empty list") + terms = tuple(_normalize_term(a, allow_var=allow_var) for a in args) else: - _require(has_entity and not has_var, UNKNOWN_VARIABLE, "free variable outside a rule") + extra = set(obj) - {"predicate", "entity", "var", "polarity"} + _require(not extra, UNSUPPORTED_PREDICATE_ARITY, f"unexpected keys {sorted(extra)}") + has_entity, has_var = "entity" in obj, "var" in obj + _require(has_entity ^ has_var, MALFORMED_CASE, "unary literal needs exactly one of entity/var") + if has_var: + _require(allow_var, UNKNOWN_VARIABLE, "free variable outside a rule") + v = obj["var"] + _require(isinstance(v, str) and bool(v.strip()), MALFORMED_CASE, "empty variable") + terms = (("var", v),) + else: + terms = (("entity", obj["entity"]),) + + _require(1 <= len(terms) <= MAX_ARITY, UNSUPPORTED_PREDICATE_ARITY, + f"arity {len(terms)} outside 1..{MAX_ARITY}") + if not allow_var: + _require(all(k == "entity" for k, _ in terms), UNKNOWN_VARIABLE, "free variable outside a rule") + return obj["predicate"], terms, polarity + + +def _collect_vars(literals: Sequence[_NormLiteral]) -> list[str]: + """Distinct variable names across a rule's literals, in first-seen order.""" + names: list[str] = [] + for _pred, terms, _pol in literals: + for kind, name in terms: + if kind == "var" and name not in names: + names.append(name) + return names def lower_case(case: dict[str, Any]) -> GroundedProblem: """Lower a finite-entity case to ``(premises, query)``. Refuse-first. - Schema (v1): + Schema (v1.5 — extends v1 with binary relations + multi-variable rules): {"entities": [str, ...], - "facts": [{"predicate": str, "entity": str, "polarity": bool}, ...], - "rules": [{"if": [, ...], - "then": }, ...], - "query": {"predicate": str, "entity": str, "polarity": bool}} + "facts": [, ...], + "rules": [{"if": [, ...], "then": }, ...], + "query": } + + A literal is either legacy unary ``{"predicate","entity"|"var","polarity"}`` or + general ``{"predicate","args":[{"entity"|"var": str}, ...],"polarity"}`` of arity + 1..2. Universal rules are grounded by enumerating every assignment of their + variables to named entities (``n^k``). Unary single-var problems lower + byte-identically to v1. Anything outside the regime or above the bounds refuses. """ - if not isinstance(case, dict) or not case: - raise GroundingError(EMPTY_CASE, "case is empty or not a mapping") + _require(isinstance(case, dict) and bool(case), EMPTY_CASE, "case is empty or not a mapping") entities = case.get("entities") - if not (isinstance(entities, list) and entities): + if not (isinstance(entities, list) and entities): # narrows for the type checker raise GroundingError(EMPTY_CASE, "no entities") - entity_set = {slug(e) for e in entities} # also validates each entity slug + _require(len(entities) <= MAX_ENTITIES, GROUNDING_BOUND_EXCEEDED, + f"{len(entities)} entities > {MAX_ENTITIES}") + entity_slugs = [slug(e) for e in entities] # validates each entity slug + entity_set = set(entity_slugs) _require(len(entity_set) == len(entities), MALFORMED_CASE, "duplicate entities after slugging") - - if "query" not in case: - raise GroundingError(MALFORMED_CASE, "no query") - - premises: list[str] = [] + _require("query" in case, MALFORMED_CASE, "no query") facts = case.get("facts", []) or [] rules = case.get("rules", []) or [] _require(isinstance(facts, list), MALFORMED_CASE, "facts must be a list") _require(isinstance(rules, list), MALFORMED_CASE, "rules must be a list") - # Facts — ground unary literals over named entities. - for fact in facts: - _require(isinstance(fact, dict), MALFORMED_CASE, f"fact is not a mapping: {fact!r}") - _check_unary(fact, allow_var=False) - _require(slug(fact["entity"]) in entity_set, UNKNOWN_ENTITY, str(fact.get("entity"))) - premises.append(_literal(fact["predicate"], fact["entity"], fact.get("polarity", True))) + premises: list[str] = [] + atoms_seen: set[str] = set() - # Rules — single-variable universal rules, grounded by explicit entity expansion. + def emit(predicate: Any, resolved: list[str], polarity: bool) -> str: + a = atom_n(predicate, resolved) + atoms_seen.add(a) + _require(len(atoms_seen) <= MAX_GROUND_ATOMS, GROUNDING_BOUND_EXCEEDED, + f"{len(atoms_seen)} distinct atoms > {MAX_GROUND_ATOMS} " + "(the independent truth-table gold is O(2^atoms))") + return _lit_str(a, polarity) + + def resolve(terms: tuple[_Term, ...], sigma: dict[str, str]) -> list[str]: + out: list[str] = [] + for kind, name in terms: + if kind == "var": + out.append(sigma[name]) # already a validated entity slug + else: + s = slug(name) + _require(s in entity_set, UNKNOWN_ENTITY, str(name)) + out.append(s) + return out + + # Facts — ground literals (no variables). + for fact in facts: + predicate, terms, polarity = _normalize_literal(fact, allow_var=False) + premises.append(emit(predicate, resolve(terms, {}), polarity)) + + # Rules — universal, grounded over every assignment of variables to entities. for rule in rules: _require(isinstance(rule, dict), MALFORMED_CASE, f"rule is not a mapping: {rule!r}") _require("quantifier" not in rule and "exists" not in rule, - UNSUPPORTED_QUANTIFIER, "only implicit single-var universal rules in v1") + UNSUPPORTED_QUANTIFIER, "only implicit universal rules are supported") body = rule.get("if") head = rule.get("then") - if not (isinstance(body, list) and body): - raise GroundingError(MALFORMED_CASE, "rule body must be a non-empty list") - if not isinstance(head, dict): - raise GroundingError(MALFORMED_CASE, "rule head must be a literal") - var = _rule_variable(body, head) - for ent in entities: - body_atoms = [_literal(lit["predicate"], ent, lit.get("polarity", True)) for lit in body] - head_atom = _literal(head["predicate"], ent, head.get("polarity", True)) - body_conj = " & ".join(f"({b})" for b in body_atoms) - premises.append(f"({body_conj}) -> ({head_atom})") - _ = var # validated; grounding is by explicit entity expansion, not by name + _require(isinstance(body, list) and bool(body), MALFORMED_CASE, "rule body must be a non-empty list") + _require(isinstance(head, dict), MALFORMED_CASE, "rule head must be a literal") + body_norm = [_normalize_literal(lit, allow_var=True) for lit in body] + head_norm = _normalize_literal(head, allow_var=True) + var_names = _collect_vars([*body_norm, head_norm]) + _require(bool(var_names), UNSUPPORTED_QUANTIFIER, + "a rule must contain at least one variable (a variable-free rule is just a fact)") + _require(len(var_names) <= MAX_VARS_PER_RULE, GROUNDING_BOUND_EXCEEDED, + f"{len(var_names)} variables > {MAX_VARS_PER_RULE}") + # Range-restriction (safety): every head variable must be bound in the body. + unbound = set(_collect_vars([head_norm])) - set(_collect_vars(body_norm)) + _require(not unbound, UNSAFE_RULE, f"head variable(s) {sorted(unbound)} not bound in the body") + for assignment in product(entity_slugs, repeat=len(var_names)): + sigma = dict(zip(var_names, assignment, strict=True)) + body_lits = [emit(p, resolve(ts, sigma), pol) for (p, ts, pol) in body_norm] + hp, hts, hpol = head_norm + head_lit = emit(hp, resolve(hts, sigma), hpol) + body_conj = " & ".join(f"({b})" for b in body_lits) + premises.append(f"({body_conj}) -> ({head_lit})") - query = case["query"] - _require(isinstance(query, dict), MALFORMED_CASE, "query must be a literal") - _check_unary(query, allow_var=False) - _require(slug(query["entity"]) in entity_set, UNKNOWN_ENTITY, str(query.get("entity"))) - query_lit = _literal(query["predicate"], query["entity"], query.get("polarity", True)) + # Query — a ground literal. + qpred, qterms, qpol = _normalize_literal(case["query"], allow_var=False) + query_lit = emit(qpred, resolve(qterms, {}), qpol) return GroundedProblem(premises=tuple(premises), query=query_lit) - - -def _rule_variable(body: list[dict[str, Any]], head: dict[str, Any]) -> str: - """Confirm the rule is single-variable: every literal uses one shared var, - no named entities (those would make it not universal). Returns the var name.""" - seen: set[str] = set() - for lit in (*body, head): - _require(isinstance(lit, dict), MALFORMED_CASE, f"rule literal not a mapping: {lit!r}") - _check_unary(lit, allow_var=True) - _require("var" in lit, MALFORMED_CASE, "rule literals must use a variable, not a named entity") - v = lit["var"] - _require(isinstance(v, str) and bool(v.strip()), MALFORMED_CASE, "empty variable") - seen.add(v) - _require(len(seen) == 1, UNSUPPORTED_QUANTIFIER, f"v1 allows one variable per rule, saw {sorted(seen)}") - return seen.pop() diff --git a/tests/test_deductive_logic_finite_entity_grounding.py b/tests/test_deductive_logic_finite_entity_grounding.py index 6b7efb87..2019f827 100644 --- a/tests/test_deductive_logic_finite_entity_grounding.py +++ b/tests/test_deductive_logic_finite_entity_grounding.py @@ -17,9 +17,9 @@ import pytest from evals.deductive_logic.grounding import ( MALFORMED_CASE, UNKNOWN_ENTITY, + UNSAFE_RULE, UNSAFE_SYMBOL, UNSUPPORTED_PREDICATE_ARITY, - UNSUPPORTED_QUANTIFIER, GroundingError, atom, lower_case, @@ -125,14 +125,18 @@ def test_binary_relation_refuses_as_unsupported_arity() -> None: assert exc.value.reason == UNSUPPORTED_PREDICATE_ARITY -def test_multi_variable_rule_refuses() -> None: +def test_unsafe_rule_unbound_head_var_refuses() -> None: + """v1.5 supports multi-variable rules — but a rule whose HEAD variable is not + bound in the body is non-range-restricted (unsafe) and still refuses. (Range- + restricted multi-var rules like transitivity are exercised in + test_deductive_logic_relational_grounding.py.)""" case = {"entities": ["a"], "rules": [{"if": [{"predicate": "p", "var": "x", "polarity": True}], "then": {"predicate": "q", "var": "y", "polarity": True}}], "query": {"predicate": "p", "entity": "a", "polarity": True}} with pytest.raises(GroundingError) as exc: lower_case(case) - assert exc.value.reason == UNSUPPORTED_QUANTIFIER + assert exc.value.reason == UNSAFE_RULE def test_empty_case_refuses() -> None: diff --git a/tests/test_deductive_logic_relational_grounding.py b/tests/test_deductive_logic_relational_grounding.py new file mode 100644 index 00000000..36d0d29a --- /dev/null +++ b/tests/test_deductive_logic_relational_grounding.py @@ -0,0 +1,237 @@ +"""Binary-relation + multi-variable grounding extension (deductive-logic runway #1). + +Extends the finite-entity grounding from unary predicates / single-var rules to +binary relations and multi-variable universal rules, still by FINITE PROPOSITIONAL +grounding into the regime the ROBDD entailment operator + the independent truth-table +oracle both decide. wrong==0 stays structural: every committed case is checked +engine==oracle==(open-world) gold, and anything outside the regime refuses. + +Two contracts this pins hard: +- **back-compat**: existing unary problems lower byte-identically (no panel regression); +- **the oracle-tractability ceiling**: the gold is O(2^atoms), so the grounding refuses + above a pinned distinct-atom bound (GROUNDING_BOUND_EXCEEDED) rather than emit a + problem the independent gold cannot decide. +""" + +from __future__ import annotations + +import random + +import pytest + +from evals.deductive_logic.grounding import ( + GROUNDING_BOUND_EXCEEDED, + UNSAFE_RULE, + UNSUPPORTED_PREDICATE_ARITY, + UNSUPPORTED_QUANTIFIER, + GroundingError, + MAX_GROUND_ATOMS, + atom_n, + lower_case, +) +from evals.deductive_logic.oracle import oracle_entailment +from generate.proof_chain.entail import evaluate_entailment + + +def _decide(case: dict) -> tuple[str, str]: + gp = lower_case(case) + engine = evaluate_entailment(gp.premises, gp.query).outcome.value + oracle = oracle_entailment(gp.premises, gp.query) + return engine, oracle + + +# --- back-compat: unary lowers exactly as before --------------------------- + + +def test_unary_back_compat_entailed(): + case = { + "entities": ["cat", "dog"], + "facts": [{"predicate": "furry", "entity": "cat", "polarity": True}], + "rules": [{"if": [{"predicate": "furry", "var": "x", "polarity": True}], + "then": {"predicate": "mammal", "var": "x", "polarity": True}}], + "query": {"predicate": "mammal", "entity": "cat", "polarity": True}, + } + gp = lower_case(case) + # exact atom + clause strings the unary path produced before the extension + assert gp.query == "mammal__cat" + assert "furry__cat" in gp.premises + assert "((furry__cat)) -> (mammal__cat)" in gp.premises + assert "((furry__dog)) -> (mammal__dog)" in gp.premises + engine, oracle = _decide(case) + assert engine == oracle == "entailed" + + +# --- binary relations ------------------------------------------------------ + + +def test_binary_atom_form(): + assert atom_n("loves", ["a", "b"]) == "loves__a__b" + assert atom_n("furry", ["cat"]) == "furry__cat" # arity-1 unchanged + + +def test_binary_fact_and_query(): + case = { + "entities": ["alice", "bob"], + "facts": [{"predicate": "loves", "args": [{"entity": "alice"}, {"entity": "bob"}], + "polarity": True}], + "query": {"predicate": "loves", "args": [{"entity": "alice"}, {"entity": "bob"}], + "polarity": True}, + } + engine, oracle = _decide(case) + assert engine == oracle == "entailed" + + +def test_transitivity_entailed(): + """The canonical RuleTaker/ProofWriter shape: a 3-variable transitive rule.""" + case = { + "entities": ["bear", "dog", "cat"], + "facts": [ + {"predicate": "bigger", "args": [{"entity": "bear"}, {"entity": "dog"}], "polarity": True}, + {"predicate": "bigger", "args": [{"entity": "dog"}, {"entity": "cat"}], "polarity": True}, + ], + "rules": [{ + "if": [ + {"predicate": "bigger", "args": [{"var": "x"}, {"var": "y"}], "polarity": True}, + {"predicate": "bigger", "args": [{"var": "y"}, {"var": "z"}], "polarity": True}, + ], + "then": {"predicate": "bigger", "args": [{"var": "x"}, {"var": "z"}], "polarity": True}, + }], + "query": {"predicate": "bigger", "args": [{"entity": "bear"}, {"entity": "cat"}], "polarity": True}, + } + engine, oracle = _decide(case) + assert engine == oracle == "entailed" + + +def test_transitivity_unknown_is_open_world(): + """The reverse direction is NOT derivable → unknown under OPEN-world entailment + (NOT 'refuted' — this is exactly why CWA benchmark splits must refuse, not map here).""" + case = { + "entities": ["bear", "dog", "cat"], + "facts": [ + {"predicate": "bigger", "args": [{"entity": "bear"}, {"entity": "dog"}], "polarity": True}, + {"predicate": "bigger", "args": [{"entity": "dog"}, {"entity": "cat"}], "polarity": True}, + ], + "rules": [{ + "if": [ + {"predicate": "bigger", "args": [{"var": "x"}, {"var": "y"}], "polarity": True}, + {"predicate": "bigger", "args": [{"var": "y"}, {"var": "z"}], "polarity": True}, + ], + "then": {"predicate": "bigger", "args": [{"var": "x"}, {"var": "z"}], "polarity": True}, + }], + "query": {"predicate": "bigger", "args": [{"entity": "cat"}, {"entity": "bear"}], "polarity": True}, + } + engine, oracle = _decide(case) + assert engine == oracle == "unknown" + + +# --- regime refusals ------------------------------------------------------- + + +def test_arity_three_refuses(): + case = { + "entities": ["a", "b", "c"], + "facts": [{"predicate": "between", + "args": [{"entity": "a"}, {"entity": "b"}, {"entity": "c"}], "polarity": True}], + "query": {"predicate": "between", + "args": [{"entity": "a"}, {"entity": "b"}, {"entity": "c"}], "polarity": True}, + } + with pytest.raises(GroundingError) as exc: + lower_case(case) + assert exc.value.reason == UNSUPPORTED_PREDICATE_ARITY + + +def test_unsafe_rule_refuses(): + """A range-restricted multi-var rule (transitivity) is fine; an unsafe one — a + head variable unbound in the body — refuses.""" + case = { + "entities": ["a", "b"], + "facts": [{"predicate": "p", "args": [{"entity": "a"}, {"entity": "b"}], "polarity": True}], + "rules": [{ + "if": [{"predicate": "p", "args": [{"var": "x"}, {"var": "y"}], "polarity": True}], + "then": {"predicate": "q", "args": [{"var": "x"}, {"var": "z"}], "polarity": True}, # z unbound + }], + "query": {"predicate": "q", "args": [{"entity": "a"}, {"entity": "b"}], "polarity": True}, + } + with pytest.raises(GroundingError) as exc: + lower_case(case) + assert exc.value.reason == UNSAFE_RULE + + +def test_explicit_quantifier_refuses(): + case = { + "entities": ["a"], + "rules": [{"exists": True, "if": [{"predicate": "p", "var": "x", "polarity": True}], + "then": {"predicate": "q", "var": "x", "polarity": True}}], + "query": {"predicate": "q", "entity": "a", "polarity": True}, + } + with pytest.raises(GroundingError) as exc: + lower_case(case) + assert exc.value.reason == UNSUPPORTED_QUANTIFIER + + +def test_atom_bound_refuses_intractable_oracle(): + """A binary rule over 6 entities grounds to 36 binary atoms > the bound: refuse + rather than hand the O(2^atoms) gold a problem it cannot decide.""" + ents = ["e0", "e1", "e2", "e3", "e4", "e5"] + case = { + "entities": ents, + "facts": [{"predicate": "r", "args": [{"entity": "e0"}, {"entity": "e1"}], "polarity": True}], + "rules": [{ + "if": [{"predicate": "r", "args": [{"var": "x"}, {"var": "y"}], "polarity": True}, + {"predicate": "r", "args": [{"var": "y"}, {"var": "z"}], "polarity": True}], + "then": {"predicate": "r", "args": [{"var": "x"}, {"var": "z"}], "polarity": True}, + }], + "query": {"predicate": "r", "args": [{"entity": "e0"}, {"entity": "e5"}], "polarity": True}, + } + with pytest.raises(GroundingError) as exc: + lower_case(case) + assert exc.value.reason == GROUNDING_BOUND_EXCEEDED + + +# --- held-out differential fuzz: engine == oracle on random binary problems -- + + +def _random_binary_case(rng: random.Random) -> dict: + # One binary predicate over 2-3 entities → <=9 atoms, so the O(2^atoms) gold + # stays fast while still exercising binary facts + a multi-var transitive rule. + ents = [f"e{i}" for i in range(rng.randint(2, 3))] + facts = [] + for a in ents: + for b in ents: + if rng.random() < 0.4: + facts.append({"predicate": "r", "args": [{"entity": a}, {"entity": b}], + "polarity": rng.random() < 0.85}) + rules = [] + if rng.random() < 0.75: + rules.append({ + "if": [{"predicate": "r", "args": [{"var": "x"}, {"var": "y"}], "polarity": True}, + {"predicate": "r", "args": [{"var": "y"}, {"var": "z"}], "polarity": True}], + "then": {"predicate": "r", "args": [{"var": "x"}, {"var": "z"}], "polarity": True}, + }) + qa, qb = rng.choice(ents), rng.choice(ents) + query = {"predicate": "r", "args": [{"entity": qa}, {"entity": qb}], + "polarity": rng.random() < 0.85} + return {"entities": ents, "facts": facts, "rules": rules, "query": query} + + +def test_held_out_fuzz_engine_equals_oracle(): + """wrong==0 on held-out (oracle-golded, never hand-authored) random binary problems. + The independent truth-table oracle is the gold; the ROBDD engine must match it on + every in-regime case. A single mismatch is a soundness breach.""" + rng = random.Random(20260604) + decided = 0 + mismatches: list[str] = [] + for _ in range(400): + case = _random_binary_case(rng) + try: + gp = lower_case(case) + except GroundingError: + continue # out-of-regime / over-bound → refused, not scored + engine = evaluate_entailment(gp.premises, gp.query).outcome.value + oracle = oracle_entailment(gp.premises, gp.query) + decided += 1 + if engine != oracle: + mismatches.append(f"{engine}!={oracle} :: {gp.premises} |- {gp.query}") + assert decided >= 50, f"too few in-regime cases ({decided}) — fuzz is near-vacuous" + assert not mismatches, f"{len(mismatches)} engine/oracle mismatches; first: {mismatches[:3]}" + assert MAX_GROUND_ATOMS <= 24 # the oracle stays tractable