48827f281a
The first SIZEABLE, honestly-verified reasoning capability — built on CORE's
own terrain (exact, verifiable, deterministic), not GSM8K's stochastic terrain.
THE OPERATOR (generate/proof_chain/entail.py, ADR-0206):
- evaluate_entailment(premises, query) -> entailed | refuted | unknown | refused.
- The multi-hop inference operator evals/symbolic_logic/gaps.md said did not exist
("no operator that takes A->B, B->C and returns A->C") and ADR-0205 deferred.
- Built on the ADR-0201 ROBDD canonicalizer: premises |= Q iff (AND P) -> Q is a
tautology. SOUND AND COMPLETE for propositional logic, not single-step.
- wrong=0 is structural: an exact tautology check refuses (LogicError) on
malformed / out-of-decidable-regime (quantified/predicate) input, never guesses.
THE HONEST METRIC (evals/deductive_logic/):
- holdout v1 (500 cases): 500 correct / 0 WRONG, incl. 227 non-trivial deductions
(117 entailed + 110 refuted). dev (200): 200/0.
- Gold from an INDEPENDENT truth-table oracle (oracle.py) sharing zero code with
the engine. 8,000-case fuzz across two independent decision procedures:
0 disagreements. This is the soundness evidence the GSM8K composer could never
produce (it could not separate its 2 right from its 87 wrong answers).
- contract.md states the load-bearing honesty boundary: PROPOSITIONAL ONLY, and
given-formulas (NL->logic grounding is a separate later layer, kept out of scope
so we do not re-step on the GSM8K natural-language rake).
TESTS (17, all green): classic inference shapes (MP, multi-hop chain, modus
tollens, disjunctive/hypothetical syllogism, conjunctive rules, genuine unknown),
refusal boundary (inconsistent / quantified / predicate / malformed), and a
deterministic engine-vs-oracle fuzz cross-check.
Pure new module — does NOT touch serving. Smoke 73 passed; invariants 40 passed.
92 lines
3.4 KiB
Python
92 lines
3.4 KiB
Python
"""Deterministic generator for the deductive-logic lane.
|
|
|
|
Produces RuleTaker-style propositional problems — base **facts** plus implication
|
|
**rules** (conjunctive antecedent → literal consequent) plus a literal **query** —
|
|
with the gold answer computed by the *independent* truth-table oracle
|
|
(:mod:`evals.deductive_logic.oracle`), never by the engine under test.
|
|
|
|
Determinism: a fixed-seed ``random.Random`` per split, so the committed
|
|
``cases.jsonl`` is exactly reproducible. Splits use disjoint seeds. Inconsistent
|
|
premise sets (oracle → ``refused``) are discarded, so every emitted case has a
|
|
definite ``entailed`` / ``refuted`` / ``unknown`` gold — the engine is scored on
|
|
producing the right *deduction*, with ``wrong=0`` as the floor.
|
|
|
|
Atom counts are kept small (≤ 7) so the oracle's 2^k enumeration is cheap and the
|
|
ROBDD never approaches its node budget.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import json
|
|
import random
|
|
from pathlib import Path
|
|
from typing import Final
|
|
|
|
from evals.deductive_logic.oracle import REFUSED, oracle_entailment
|
|
|
|
_ATOMS: Final[tuple[str, ...]] = ("a", "b", "c", "d", "e", "f", "g")
|
|
|
|
|
|
def _literal(rng: random.Random, atom: str) -> str:
|
|
return atom if rng.random() < 0.5 else f"~{atom}"
|
|
|
|
|
|
def _make_case(rng: random.Random, case_id: str) -> dict | None:
|
|
k = rng.randint(4, len(_ATOMS))
|
|
atoms = rng.sample(_ATOMS, k)
|
|
|
|
premises: list[str] = []
|
|
|
|
# Base facts: assert a few literals (kept distinct atoms).
|
|
n_facts = rng.randint(1, max(1, k // 2))
|
|
fact_atoms = rng.sample(atoms, n_facts)
|
|
for at in fact_atoms:
|
|
premises.append(_literal(rng, at))
|
|
|
|
# Implication rules: (L1 & ... ) -> Lc. Bias antecedents toward earlier atoms
|
|
# and consequents toward later atoms so multi-hop chains form.
|
|
n_rules = rng.randint(2, 5)
|
|
for _ in range(n_rules):
|
|
body_size = rng.randint(1, 2)
|
|
body_atoms = rng.sample(atoms, min(body_size, k))
|
|
body = " & ".join(_literal(rng, at) for at in body_atoms)
|
|
head_atom = rng.choice(atoms)
|
|
head = _literal(rng, head_atom)
|
|
premises.append(f"({body}) -> {head}")
|
|
|
|
query = _literal(rng, rng.choice(atoms))
|
|
|
|
gold = oracle_entailment(tuple(premises), query)
|
|
if gold == REFUSED:
|
|
return None # inconsistent premises — discard; keep only definite golds
|
|
|
|
return {"id": case_id, "premises": premises, "query": query, "gold": gold}
|
|
|
|
|
|
def generate(seed: int, n: int, prefix: str) -> list[dict]:
|
|
"""Generate ``n`` consistent cases deterministically from ``seed``."""
|
|
rng = random.Random(seed)
|
|
cases: list[dict] = []
|
|
attempts = 0
|
|
while len(cases) < n:
|
|
attempts += 1
|
|
case = _make_case(rng, f"{prefix}-{len(cases):04d}")
|
|
if case is not None:
|
|
cases.append(case)
|
|
if attempts > n * 50: # pragma: no cover - safety valve
|
|
raise RuntimeError("generator could not reach target count")
|
|
return cases
|
|
|
|
|
|
def _write(path: Path, cases: list[dict]) -> None:
|
|
path.parent.mkdir(parents=True, exist_ok=True)
|
|
with path.open("w", encoding="utf-8") as fh:
|
|
for case in cases:
|
|
fh.write(json.dumps(case, ensure_ascii=False, sort_keys=True) + "\n")
|
|
|
|
|
|
if __name__ == "__main__":
|
|
root = Path(__file__).resolve().parent
|
|
_write(root / "dev" / "cases.jsonl", generate(20260604, 200, "dl-dev-v1"))
|
|
_write(root / "holdout" / "v1" / "cases.jsonl", generate(70260604, 500, "dl-holdout-v1"))
|
|
print("generated dev=200 holdout=500")
|