Shay 5f274b75b7 feat(deductive): binary relations + multi-variable grounding (finite propositional)

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.

2026-06-04 20:17:33 -07:00

4.3 KiB

Raw Permalink Blame History

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)

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.)
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.
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."

4.3 KiB Raw Permalink Blame History Unescape Escape