merge: bring in the polarity unit (#125) — resolve the suite-list conflict
Both units append to `deductive` at the same anchor, immediately after `tests/test_curriculum_practice.py`. Resolution keeps BOTH entries; nothing else in either hunk overlapped, and `core/cli_proposal_queue.py` auto-merged (polarity adds `--polarity` to the ratify parser, this branch adds the reseal subparser and ratify's "next:" line). Resolved here rather than at merge time so the resolution is visible on the PR that caused it.
This commit is contained in:
Shay
commit
bd996fa9a4
8 changed files with 656 additions and 21 deletions
|
|
@ -119,6 +119,7 @@ def cmd_proposal_queue_ratify(args: argparse.Namespace) -> int:
|
|||
reviewer=args.reviewer,
|
||||
rationale=args.rationale,
|
||||
intent=args.intent,
|
||||
polarity=args.polarity,
|
||||
)
|
||||
receipt = ratify_chain(record, dry_run=args.dry_run)
|
||||
except RatificationError as exc:
|
||||
|
|
@ -220,6 +221,8 @@ def cmd_proposal_queue_reseal(args: argparse.Namespace) -> int:
|
|||
|
||||
|
||||
def register(subparsers: argparse._SubParsersAction) -> None:
|
||||
from teaching.curriculum_premises import AFFIRMATIVE, POLARITIES
|
||||
|
||||
"""Attach the ``core proposal-queue`` subcommand tree to a top-level parser."""
|
||||
queue = subparsers.add_parser(
|
||||
"proposal-queue",
|
||||
|
|
@ -283,6 +286,18 @@ def register(subparsers: argparse._SubParsersAction) -> None:
|
|||
ratify.add_argument("--reviewer", required=True, help="who ratified this")
|
||||
ratify.add_argument("--rationale", required=True, help="why it is ratified")
|
||||
ratify.add_argument("--intent", default="cause")
|
||||
ratify.add_argument(
|
||||
"--polarity", choices=list(POLARITIES), default=AFFIRMATIVE,
|
||||
help=(
|
||||
"ADR-0264 R1. `negative` ratifies an explicitly TAUGHT refutation: "
|
||||
"the atom compiles under the sentential-negation prefix and the "
|
||||
"question answers `refuted`, which is different from an absent edge "
|
||||
"(UNKNOWN, the open-world reading). Must reuse the AFFIRMATIVE "
|
||||
"connective (R3) — `causes`, never `does not cause` — or it mints a "
|
||||
"different atom and silently fails to refute. Refused if the atom is "
|
||||
"already taught with the other polarity (R4)."
|
||||
),
|
||||
)
|
||||
ratify.add_argument("--dry-run", action="store_true",
|
||||
help="report the band delta without writing")
|
||||
ratify.add_argument("--json", action="store_true")
|
||||
|
|
|
|||
|
|
@ -85,6 +85,12 @@ TEST_SUITES: dict[str, tuple[str, ...]] = {
|
|||
# an audit source. It gates a live, flag-ON serving path, so it belongs
|
||||
# on the pre-push gate. ~1.5s.
|
||||
"tests/test_volume_honesty.py",
|
||||
# ADR-0264 R1-R4/R8 — taught curriculum NEGATIVES. Before this, a row
|
||||
# authored to refute compiled to a premise ASSERTING the atom, and the
|
||||
# independent oracle ignored polarity too, so gold agreed and wrong=0
|
||||
# stayed green. Corpus-level epistemology is unfalsifiable by every
|
||||
# other gate here, so this one belongs on the pre-push gate. ~0.4s.
|
||||
"tests/test_curriculum_polarity.py",
|
||||
),
|
||||
"runtime": (
|
||||
"tests/test_chat_runtime.py",
|
||||
|
|
@ -230,6 +236,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = {
|
|||
"tests/test_deduction_serve_e2e.py",
|
||||
"tests/test_curriculum_serve.py",
|
||||
"tests/test_curriculum_practice.py",
|
||||
"tests/test_curriculum_polarity.py",
|
||||
"tests/test_ledger_reseal.py",
|
||||
"tests/test_ratified_ledger_bridge.py",
|
||||
"tests/test_vocab_trigger_instrument.py",
|
||||
|
|
|
|||
|
|
@ -79,13 +79,34 @@ def _lemmas(pack_id: str) -> set[str]:
|
|||
return out
|
||||
|
||||
|
||||
def _edges(domain: str) -> list[tuple[str, str, str, str]]:
|
||||
"""``(subject, connective, object, chain_id)`` for every ratified row."""
|
||||
#: ADR-0264 R1/R8, restated independently — the serving path has its own copy of
|
||||
#: this vocabulary and the two must not share a polarity helper. Code-level
|
||||
#: independence is the whole evidentiary value of this oracle: if it imported the
|
||||
#: compiler's notion of polarity, agreement would only prove the compiler agrees
|
||||
#: with itself, and a polarity bug would be invisible on both sides at once.
|
||||
_AFFIRMATIVE = "affirmative"
|
||||
_NEGATIVE = "negative"
|
||||
_POLARITIES = (_AFFIRMATIVE, _NEGATIVE)
|
||||
|
||||
|
||||
def _row_polarity(row: dict) -> str | None:
|
||||
"""This oracle's own reading of a row's polarity.
|
||||
|
||||
Absent ⇒ affirmative. An unrecognized token ⇒ ``None``, and the caller drops
|
||||
the row: reading an unknown value as affirmative would let a row someone
|
||||
wrote to refute be scored as an assertion.
|
||||
"""
|
||||
value = str(row.get("polarity") or _AFFIRMATIVE).strip().lower()
|
||||
return value if value in _POLARITIES else None
|
||||
|
||||
|
||||
def _edges(domain: str) -> list[tuple[str, str, str, str, str]]:
|
||||
"""``(subject, connective, object, chain_id, polarity)`` per ratified row."""
|
||||
corpora, packs = _DOMAIN_SOURCES[domain]
|
||||
vocabulary = set()
|
||||
for pack in packs:
|
||||
vocabulary |= _lemmas(pack)
|
||||
out: list[tuple[str, str, str, str]] = []
|
||||
out: list[tuple[str, str, str, str, str]] = []
|
||||
for corpus in corpora:
|
||||
path = _CHAIN_DIR / f"{corpus}.jsonl"
|
||||
if not path.exists():
|
||||
|
|
@ -105,7 +126,12 @@ def _edges(domain: str) -> list[tuple[str, str, str, str]]:
|
|||
continue
|
||||
if connective not in _FAMILY_OF_CONNECTIVE:
|
||||
continue
|
||||
out.append((subject, connective, obj, row.get("chain_id", "")))
|
||||
polarity = _row_polarity(row)
|
||||
if polarity is None:
|
||||
continue
|
||||
out.append(
|
||||
(subject, connective, obj, row.get("chain_id", ""), polarity)
|
||||
)
|
||||
return out
|
||||
|
||||
|
||||
|
|
@ -159,12 +185,28 @@ def oracle_answer(domain: str, subject: str, relation: str, obj: str) -> OracleV
|
|||
# curriculum teaching "entropy reveals energy" has not thereby taught
|
||||
# "entropy causes energy". Family scoping decides which premises are in
|
||||
# play; the connective decides what was actually said.
|
||||
if any(s == subject and c == connective and o == obj for s, c, o, _id in edges):
|
||||
return OracleVerdict("entailed", "", family, 1)
|
||||
#
|
||||
# ADR-0264 R1/R8 — and the POLARITY decides which way. A taught negative row
|
||||
# is a taught refutation: the curriculum has said something about this atom,
|
||||
# and what it said is "no". That is categorically different from an absent
|
||||
# edge, which stays UNKNOWN under the open-world reading. Both are checked at
|
||||
# depth 1, against the same atom, so the two cannot be confused.
|
||||
for s, c, o, _id, polarity in edges:
|
||||
if s == subject and c == connective and o == obj:
|
||||
if polarity == _NEGATIVE:
|
||||
return OracleVerdict("refuted", "", family, 1)
|
||||
return OracleVerdict("entailed", "", family, 1)
|
||||
# No taught edge. Report the shortest path so the lane can prove the
|
||||
# serving path does NOT compose a chain into a claim.
|
||||
#
|
||||
# NEGATIVE rows are EXCLUDED from the adjacency (ADR-0264 R8). Reachability
|
||||
# here exists to measure whether an untaught pair is *composable* from taught
|
||||
# edges, and "a does not X b" supplies no step from a to b — treating it as
|
||||
# one would report a path built out of a denial.
|
||||
adjacency: dict[str, list[str]] = {}
|
||||
for s, _c, o, _id in edges:
|
||||
for s, _c, o, _id, polarity in edges:
|
||||
if polarity == _NEGATIVE:
|
||||
continue
|
||||
adjacency.setdefault(s, []).append(o)
|
||||
seen = {subject}
|
||||
queue: deque[tuple[str, int]] = deque([(subject, 0)])
|
||||
|
|
@ -181,8 +223,11 @@ def oracle_answer(domain: str, subject: str, relation: str, obj: str) -> OracleV
|
|||
return OracleVerdict("unknown", "", family, 0)
|
||||
|
||||
|
||||
def taught_edges(domain: str) -> list[tuple[str, str, str, str]]:
|
||||
"""Public view for the lane's provenance assertions."""
|
||||
def taught_edges(domain: str) -> list[tuple[str, str, str, str, str]]:
|
||||
"""Public view for the lane's provenance assertions.
|
||||
|
||||
Each row carries its polarity as the fifth element (ADR-0264 R1).
|
||||
"""
|
||||
return _edges(domain)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -124,11 +124,17 @@ def routable_atoms(domain: str, family: str) -> tuple[QueryAtom, ...]:
|
|||
|
||||
@lru_cache(maxsize=None)
|
||||
def taught_atoms(domain: str, family: str) -> frozenset[tuple[str, str, str, str]]:
|
||||
"""The atom keys a ratified chain states directly — the ``entailed`` class.
|
||||
"""The atom keys a ratified chain states directly — the COMMITTED classes.
|
||||
|
||||
Scarce by nature: a band has as many taught edges as the curriculum states,
|
||||
which is why ADR-0262 §5.1 makes authored volume the binding constraint on
|
||||
what a band can demonstrate beyond non-commitment.
|
||||
|
||||
Polarity-independent on purpose (ADR-0264 R1). A negative row states its atom
|
||||
just as directly as an affirmative one — it says "no" about it — so both are
|
||||
scarce committed evidence and both are force-included in a capped sample. The
|
||||
verdict they earn (``entailed`` vs ``refuted``) is the oracle's call, not this
|
||||
function's; classifying here would duplicate the gold rule inside the corpus.
|
||||
"""
|
||||
return frozenset(
|
||||
QueryAtom(domain, family, c.subject, c.connective, c.obj).key
|
||||
|
|
|
|||
|
|
@ -73,6 +73,21 @@ CONNECTIVE_FAMILY: dict[str, str] = {
|
|||
#: Relation families, in a stable order (the band-key axis — ADR-0262 §4).
|
||||
FAMILIES: tuple[str, ...] = ("causal", "modal", "sequence", "contrast", "evidential")
|
||||
|
||||
#: The two row polarities (ADR-0264 R1). ``polarity`` is a ROW-LEVEL field, not
|
||||
#: an ``intent`` value and not a new ``operator_family``: bands key on
|
||||
#: *(domain, connective-derived family)*, so a ``modal_negative`` family would
|
||||
#: create a fresh band at n=0 instead of adding refuted volume to the band it
|
||||
#: belongs to. An ABSENT field reads as affirmative, which is what makes the
|
||||
#: existing corpora valid unchanged.
|
||||
AFFIRMATIVE = "affirmative"
|
||||
NEGATIVE = "negative"
|
||||
POLARITIES: tuple[str, str] = (AFFIRMATIVE, NEGATIVE)
|
||||
|
||||
#: ADR-0264 R2 — the sentential-negation prefix the argument reader already
|
||||
#: parses (``generate/proof_chain/english.py``). Stated once here so the
|
||||
#: compiled form cannot drift from the form the reader accepts.
|
||||
NEGATION_PREFIX = "it is not the case that "
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class CurriculumChain:
|
||||
|
|
@ -83,13 +98,42 @@ class CurriculumChain:
|
|||
connective: str
|
||||
obj: str
|
||||
family: str
|
||||
#: ADR-0264 R1. Defaulted, so every existing construction site stays valid
|
||||
#: and an un-migrated corpus row reads as the affirmative it always was.
|
||||
polarity: str = AFFIRMATIVE
|
||||
|
||||
@property
|
||||
def negated(self) -> bool:
|
||||
return self.polarity == NEGATIVE
|
||||
|
||||
@property
|
||||
def atom_sentence(self) -> str:
|
||||
"""The affirmative core, independent of polarity — the ATOM this chain
|
||||
is about.
|
||||
|
||||
ADR-0264 R3 in one property: a negative row must mint the *same*
|
||||
propositional atom as its affirmative counterpart, or it cannot refute
|
||||
anything. A negative row that reworded the relation would produce a
|
||||
second, unrelated atom and the query would come back UNKNOWN instead of
|
||||
REFUTED — a taught refutation silently failing to refute, which is the
|
||||
worst available outcome here because nothing goes red.
|
||||
"""
|
||||
return f"{self.subject} {self.connective} {self.obj}"
|
||||
|
||||
@property
|
||||
def sentence(self) -> str:
|
||||
"""The English premise this chain compiles to. The connective is
|
||||
already a third-person-singular verb form, so the sentence lands in
|
||||
the verb-predicate grammar (ADR-0260) exactly as written."""
|
||||
return f"{self.subject} {self.connective} {self.obj}"
|
||||
"""The English premise this chain compiles to.
|
||||
|
||||
The connective is already a third-person-singular verb form, so the
|
||||
affirmative sentence lands in the verb-predicate grammar (ADR-0260)
|
||||
exactly as written. A negative row is the same sentence under the
|
||||
sentential-negation prefix (ADR-0264 R2), which the verb band reads as
|
||||
a negation OF THAT ATOM — so `(¬p, therefore p)` is a tautological
|
||||
refutation and the query decides REFUTED.
|
||||
"""
|
||||
if self.negated:
|
||||
return f"{NEGATION_PREFIX}{self.atom_sentence}"
|
||||
return self.atom_sentence
|
||||
|
||||
|
||||
@dataclass(frozen=True, slots=True)
|
||||
|
|
@ -189,6 +233,14 @@ def load_curriculum(domain: str) -> Curriculum:
|
|||
family = CONNECTIVE_FAMILY.get(connective)
|
||||
if family is None:
|
||||
continue
|
||||
# ADR-0264 R1 — absent polarity IS affirmative. An UNRECOGNIZED
|
||||
# polarity is dropped here rather than guessed: reading an
|
||||
# unknown token as affirmative would turn a row someone wrote to
|
||||
# refute into a row that asserts, which is the one direction of
|
||||
# error this whole rule exists to prevent.
|
||||
polarity = str(row.get("polarity") or AFFIRMATIVE).strip().lower()
|
||||
if polarity not in POLARITIES:
|
||||
continue
|
||||
chains.append(
|
||||
CurriculumChain(
|
||||
chain_id=str(row.get("chain_id") or ""),
|
||||
|
|
@ -196,6 +248,7 @@ def load_curriculum(domain: str) -> Curriculum:
|
|||
connective=connective,
|
||||
obj=str(row.get("object") or "").strip(),
|
||||
family=family,
|
||||
polarity=polarity,
|
||||
)
|
||||
)
|
||||
return Curriculum(
|
||||
|
|
@ -275,9 +328,13 @@ def resolve_pinned(curriculum: Curriculum, chain_ids: tuple[str, ...]) -> tuple[
|
|||
|
||||
|
||||
__all__ = [
|
||||
"AFFIRMATIVE",
|
||||
"CONNECTIVE_FAMILY",
|
||||
"FAMILIES",
|
||||
"MAX_PREMISE_SENTENCES",
|
||||
"NEGATION_PREFIX",
|
||||
"NEGATIVE",
|
||||
"POLARITIES",
|
||||
"Curriculum",
|
||||
"CurriculumChain",
|
||||
"UnratifiedChain",
|
||||
|
|
|
|||
|
|
@ -57,7 +57,13 @@ from core.capability.domains import (
|
|||
DOMAIN_CORPORA,
|
||||
DOMAIN_PACKS,
|
||||
)
|
||||
from teaching.curriculum_premises import CONNECTIVE_FAMILY, load_curriculum
|
||||
from teaching.curriculum_premises import (
|
||||
AFFIRMATIVE,
|
||||
CONNECTIVE_FAMILY,
|
||||
NEGATIVE,
|
||||
POLARITIES,
|
||||
load_curriculum,
|
||||
)
|
||||
|
||||
_REPO_ROOT = Path(__file__).resolve().parents[1]
|
||||
|
||||
|
|
@ -74,6 +80,10 @@ _ROW_FIELDS: tuple[str, ...] = (
|
|||
"intent",
|
||||
"connective",
|
||||
"object",
|
||||
# ADR-0264 R1 — row-level polarity, emitted only for NEGATIVE rows (see
|
||||
# ``ChainRecord.as_row``). An affirmative row omits it, so every committed
|
||||
# corpus stays byte-identical and no existing lane hash moves.
|
||||
"polarity",
|
||||
"subject_pack_id",
|
||||
"object_pack_id",
|
||||
"review_status",
|
||||
|
|
@ -100,9 +110,34 @@ class ChainRecord:
|
|||
object_pack_id: str
|
||||
review_status: str
|
||||
provenance: str
|
||||
#: ADR-0264 R1. Defaulted so existing construction sites are unchanged.
|
||||
polarity: str = AFFIRMATIVE
|
||||
|
||||
def as_row(self) -> dict[str, Any]:
|
||||
return {name: getattr(self, name) for name in _ROW_FIELDS}
|
||||
"""The committed row.
|
||||
|
||||
``polarity`` is OMITTED when affirmative. An absent field already reads
|
||||
as affirmative (ADR-0264 R1), so emitting it would add a redundant key
|
||||
to every future row while the committed corpora lack it — two spellings
|
||||
of the same fact, and a diff that looks like a schema change on rows
|
||||
whose meaning did not move.
|
||||
"""
|
||||
row = {
|
||||
name: getattr(self, name)
|
||||
for name in _ROW_FIELDS
|
||||
if name != "polarity"
|
||||
}
|
||||
if self.polarity != AFFIRMATIVE:
|
||||
# Re-insert in _ROW_FIELDS order — chain corpora are reviewed as
|
||||
# diffs, so key order is part of the artifact.
|
||||
ordered = {}
|
||||
for name in _ROW_FIELDS:
|
||||
if name == "polarity":
|
||||
ordered["polarity"] = self.polarity
|
||||
else:
|
||||
ordered[name] = row[name]
|
||||
return ordered
|
||||
return row
|
||||
|
||||
def as_jsonl_line(self) -> str:
|
||||
"""Byte-compatible with the committed corpora: compact separators,
|
||||
|
|
@ -221,6 +256,7 @@ def build_chain_record(
|
|||
reviewer: str,
|
||||
rationale: str,
|
||||
intent: str = "cause",
|
||||
polarity: str = AFFIRMATIVE,
|
||||
chain_id: str | None = None,
|
||||
) -> ChainRecord:
|
||||
"""Construct the record a reviewed decision implies.
|
||||
|
|
@ -236,11 +272,20 @@ def build_chain_record(
|
|||
if not rationale:
|
||||
raise RatificationError("ratification requires a stated rationale")
|
||||
|
||||
polarity = polarity.strip().lower()
|
||||
if polarity not in POLARITIES:
|
||||
raise RatificationError(
|
||||
f"polarity {polarity!r} is not one of {list(POLARITIES)} — the "
|
||||
"curriculum loader would drop this row (ADR-0264 R1)"
|
||||
)
|
||||
|
||||
family = CONNECTIVE_FAMILY.get(connective.strip())
|
||||
if family is None:
|
||||
raise RatificationError(
|
||||
f"connective {connective!r} is outside CONNECTIVE_FAMILY "
|
||||
f"{sorted(CONNECTIVE_FAMILY)} — the loader would drop this row"
|
||||
f"{sorted(CONNECTIVE_FAMILY)} — the loader would drop this row. "
|
||||
"A NEGATIVE row must reuse the affirmative connective (ADR-0264 R3), "
|
||||
"never a negated paraphrase of it."
|
||||
)
|
||||
|
||||
packs = DOMAIN_PACKS.get(domain, ())
|
||||
|
|
@ -273,6 +318,7 @@ def build_chain_record(
|
|||
object_pack_id=object_pack,
|
||||
review_status="reviewed",
|
||||
provenance=f"ratification-ceremony:{reviewer}:{rationale}",
|
||||
polarity=polarity,
|
||||
)
|
||||
|
||||
|
||||
|
|
@ -298,6 +344,10 @@ def validate_admissible(record: ChainRecord) -> None:
|
|||
raise RatificationError(
|
||||
f"object {record.object!r} absent from pack {record.object_pack_id}"
|
||||
)
|
||||
if record.polarity not in POLARITIES:
|
||||
raise RatificationError(
|
||||
f"polarity {record.polarity!r} has no meaning (ADR-0264 R1)"
|
||||
)
|
||||
for row in existing_rows(record.domain):
|
||||
if str(row.get("chain_id")) == record.chain_id:
|
||||
raise RatificationError(f"chain_id {record.chain_id} already committed")
|
||||
|
|
@ -306,6 +356,25 @@ def validate_admissible(record: ChainRecord) -> None:
|
|||
and str(row.get("connective")) == record.connective
|
||||
and str(row.get("object")) == record.object
|
||||
):
|
||||
# ADR-0264 R4 — a corpus stating both polarities of ONE atom is
|
||||
# contradictory, and the contradiction is rejected HERE rather than
|
||||
# discovered at serve time. `evaluate_entailment_with_trace` would
|
||||
# meet `p ∧ ¬p` and refuse INCONSISTENT_PREMISES, which is honest
|
||||
# but arrives as a band that has stopped answering anything in that
|
||||
# family — the curriculum silently going dark instead of the
|
||||
# authoring mistake being named.
|
||||
existing_polarity = (
|
||||
str(row.get("polarity") or AFFIRMATIVE).strip().lower()
|
||||
)
|
||||
if existing_polarity != record.polarity:
|
||||
raise RatificationError(
|
||||
f"contradiction: {row.get('chain_id')} already teaches "
|
||||
f"{existing_polarity} '{record.subject} {record.connective} "
|
||||
f"{record.object}'; this row would teach {record.polarity}. "
|
||||
"One atom cannot hold both polarities (ADR-0264 R4) — the "
|
||||
"compiled premises would be inconsistent and the band would "
|
||||
"refuse every question in the family."
|
||||
)
|
||||
raise RatificationError(
|
||||
f"duplicate edge: {row.get('chain_id')} already teaches "
|
||||
f"{record.subject} {record.connective} {record.object}"
|
||||
|
|
|
|||
427
tests/test_curriculum_polarity.py
Normal file
427
tests/test_curriculum_polarity.py
Normal file
|
|
@ -0,0 +1,427 @@
|
|||
"""ADR-0264 R1-R4 + R8 — explicitly-taught curriculum negatives.
|
||||
|
||||
Before this, `polarity` was read by NOTHING. `CurriculumChain.sentence` was
|
||||
unconditionally affirmative, so a row authored to REFUTE an atom compiled to a
|
||||
premise asserting it, and the question came back `entailed`. The independent
|
||||
oracle ignored the field too — so **gold agreed and `wrong=0` stayed green.**
|
||||
That is the shape of defect no gate in this repository can catch, which is why
|
||||
the epistemology was settled in an ADR before any code moved.
|
||||
|
||||
The five rules, and what each one is defending against:
|
||||
|
||||
- **R1** polarity is a ROW-LEVEL field; absent ⇒ affirmative. Not an `intent`
|
||||
value, not a new `operator_family`: bands key on the connective-derived family,
|
||||
so `modal_negative` would open a fresh band at n=0 instead of adding refuted
|
||||
volume to the band it belongs to.
|
||||
- **R2** a negative row compiles under the sentential-negation prefix the argument
|
||||
reader already parses.
|
||||
- **R3** a negative row MUST reuse the affirmative connective, so it mints the
|
||||
SAME propositional atom. A negated paraphrase mints a different atom and the
|
||||
query returns UNKNOWN — a taught refutation that silently fails to refute.
|
||||
- **R4** one atom cannot hold both polarities; the contradiction is rejected at
|
||||
ratification, not discovered at serve time as a band that stopped answering.
|
||||
- **R8** the oracle learns polarity INDEPENDENTLY (its own constants, its own
|
||||
reader) and excludes negatives from the reachability adjacency.
|
||||
|
||||
The end-to-end tests write a temporary row into the committed corpus and restore
|
||||
it, asserting **byte-identity** on the way out. No negative row is committed:
|
||||
authoring curriculum is Phase F and Shay's.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import json
|
||||
from pathlib import Path
|
||||
from typing import Iterator
|
||||
|
||||
import pytest
|
||||
|
||||
from chat.curriculum_surface import decide_curriculum_question
|
||||
from evals.curriculum_serve.oracle import oracle_answer, taught_edges
|
||||
from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace
|
||||
from generate.proof_chain.verb import VerbArgument, read_verb_argument
|
||||
from teaching.curriculum_premises import (
|
||||
AFFIRMATIVE,
|
||||
NEGATION_PREFIX,
|
||||
NEGATIVE,
|
||||
POLARITIES,
|
||||
CurriculumChain,
|
||||
compile_premises,
|
||||
load_curriculum,
|
||||
)
|
||||
from teaching.ratification import (
|
||||
ChainRecord,
|
||||
RatificationError,
|
||||
build_chain_record,
|
||||
validate_admissible,
|
||||
)
|
||||
|
||||
REPO_ROOT = Path(__file__).resolve().parents[1]
|
||||
_PHYSICS_CORPUS = REPO_ROOT / "teaching" / "domain_chains" / "physics_chains_v1.jsonl"
|
||||
|
||||
#: An atom physics does NOT teach, in taught vocabulary, so it routes and is
|
||||
#: UNKNOWN today — the clean slot to plant a negative in.
|
||||
_UNTAUGHT_ATOM = ("mass", "causes", "charge")
|
||||
|
||||
|
||||
def _chain(polarity: str = AFFIRMATIVE) -> CurriculumChain:
|
||||
return CurriculumChain(
|
||||
chain_id="x-causal-001",
|
||||
subject="force",
|
||||
connective="causes",
|
||||
obj="acceleration",
|
||||
family="causal",
|
||||
polarity=polarity,
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# R1 — the field, and its default.
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_r1_polarity_defaults_to_affirmative() -> None:
|
||||
"""An absent field must read as affirmative, or every committed row changes
|
||||
meaning the moment the field exists."""
|
||||
bare = CurriculumChain("i", "force", "causes", "acceleration", "causal")
|
||||
assert bare.polarity == AFFIRMATIVE
|
||||
assert bare.negated is False
|
||||
assert bare.sentence == "force causes acceleration"
|
||||
|
||||
|
||||
def test_r1_committed_corpora_carry_no_polarity_field_and_still_load() -> None:
|
||||
"""The migration is a no-op on disk: nothing was rewritten."""
|
||||
rows = [
|
||||
json.loads(line)
|
||||
for line in _PHYSICS_CORPUS.read_text(encoding="utf-8").splitlines()
|
||||
if line.strip()
|
||||
]
|
||||
assert rows
|
||||
assert not any("polarity" in row for row in rows), (
|
||||
"no committed row should carry polarity yet — Phase F authors those"
|
||||
)
|
||||
for chain in load_curriculum("physics").chains:
|
||||
assert chain.polarity == AFFIRMATIVE
|
||||
|
||||
|
||||
def test_r1_unrecognized_polarity_is_dropped_not_guessed() -> None:
|
||||
"""Reading an unknown token as affirmative would turn a row someone wrote to
|
||||
refute into a row that asserts — the one direction of error that matters."""
|
||||
assert set(POLARITIES) == {AFFIRMATIVE, NEGATIVE}
|
||||
with pytest.raises(RatificationError, match="polarity"):
|
||||
build_chain_record(
|
||||
domain="physics", subject="mass", connective="causes", obj="charge",
|
||||
reviewer="t", rationale="t", polarity="maybe",
|
||||
)
|
||||
|
||||
|
||||
def test_r1_polarity_is_not_a_new_operator_family() -> None:
|
||||
"""Bands key on the connective-derived family; a negative row keeps its band."""
|
||||
from chat.curriculum_surface import band_for
|
||||
|
||||
neg = _chain(NEGATIVE)
|
||||
assert neg.family == "causal"
|
||||
assert band_for("physics", neg.family) == "curriculum_physics_causal"
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# R2 — the compiled form, and that the reader accepts it.
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_r2_negative_row_compiles_under_the_negation_prefix() -> None:
|
||||
neg = _chain(NEGATIVE)
|
||||
assert neg.sentence == f"{NEGATION_PREFIX}force causes acceleration"
|
||||
assert neg.negated is True
|
||||
|
||||
|
||||
def test_r2_the_reader_actually_parses_that_form() -> None:
|
||||
"""The prefix is not decorative — the verb band must read it as a negation
|
||||
of the atom, or R2 compiles premises nothing can decide."""
|
||||
argument = f"{_chain(NEGATIVE).sentence}. Therefore force causes acceleration."
|
||||
arg = read_verb_argument(argument)
|
||||
assert isinstance(arg, VerbArgument), f"reader refused: {arg}"
|
||||
trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula)
|
||||
assert trace.outcome is Entailment.REFUTED
|
||||
assert trace.reason == "tautological_refutation"
|
||||
|
||||
|
||||
def test_r2_affirmative_control_still_entails() -> None:
|
||||
argument = f"{_chain().sentence}. Therefore force causes acceleration."
|
||||
arg = read_verb_argument(argument)
|
||||
assert isinstance(arg, VerbArgument)
|
||||
trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula)
|
||||
assert trace.outcome is Entailment.ENTAILED
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# R3 — the same atom. This is the silent-failure rule.
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_r3_negative_reuses_the_affirmative_atom() -> None:
|
||||
"""`atom_sentence` is polarity-independent — that IS R3."""
|
||||
assert _chain().atom_sentence == _chain(NEGATIVE).atom_sentence
|
||||
assert _chain(NEGATIVE).sentence.endswith(_chain(NEGATIVE).atom_sentence)
|
||||
|
||||
|
||||
def test_r3_a_different_connective_would_silently_fail_to_refute() -> None:
|
||||
"""Why R3 is a rule and not a style note.
|
||||
|
||||
A negative row spelled with a DIFFERENT relation word mints a different
|
||||
propositional atom, so it cannot contradict the query. The result is UNKNOWN
|
||||
— the curriculum was taught a refutation and answers "I don't know". Nothing
|
||||
goes red. This is the mechanism, demonstrated.
|
||||
"""
|
||||
same_atom = f"{NEGATION_PREFIX}force causes acceleration. Therefore force causes acceleration."
|
||||
other_atom = f"{NEGATION_PREFIX}force enables acceleration. Therefore force causes acceleration."
|
||||
|
||||
a = read_verb_argument(same_atom)
|
||||
b = read_verb_argument(other_atom)
|
||||
assert isinstance(a, VerbArgument) and isinstance(b, VerbArgument)
|
||||
assert evaluate_entailment_with_trace(a.premise_formulas, a.query_formula).outcome is Entailment.REFUTED
|
||||
assert evaluate_entailment_with_trace(b.premise_formulas, b.query_formula).outcome is Entailment.UNKNOWN, (
|
||||
"a negated paraphrase must be shown NOT to refute — that is the hazard R3 forbids"
|
||||
)
|
||||
|
||||
|
||||
def test_r3_ratification_refuses_a_connective_outside_the_closed_set() -> None:
|
||||
with pytest.raises(RatificationError, match="ADR-0264 R3"):
|
||||
build_chain_record(
|
||||
domain="physics", subject="mass", connective="does not cause",
|
||||
obj="charge", reviewer="t", rationale="t", polarity=NEGATIVE,
|
||||
)
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# R4 — contradiction rejected at ratification.
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def _record(polarity: str, subject: str = "force", obj: str = "acceleration") -> ChainRecord:
|
||||
return ChainRecord(
|
||||
chain_id="physics-causal-900", domain="physics", operator_family="causal",
|
||||
subject=subject, intent="cause", connective="causes", object=obj,
|
||||
subject_pack_id="en_physics_v1", object_pack_id="en_physics_v1",
|
||||
review_status="reviewed", provenance="test", polarity=polarity,
|
||||
)
|
||||
|
||||
|
||||
def test_r4_negating_an_already_taught_atom_is_rejected() -> None:
|
||||
"""physics-causal-001 teaches `force causes acceleration` affirmatively."""
|
||||
with pytest.raises(RatificationError, match="contradiction"):
|
||||
validate_admissible(_record(NEGATIVE))
|
||||
|
||||
|
||||
def test_r4_the_refusal_names_both_polarities_and_the_consequence() -> None:
|
||||
with pytest.raises(RatificationError) as exc:
|
||||
validate_admissible(_record(NEGATIVE))
|
||||
message = str(exc.value)
|
||||
assert AFFIRMATIVE in message and NEGATIVE in message
|
||||
assert "ADR-0264 R4" in message
|
||||
assert "inconsistent" in message
|
||||
|
||||
|
||||
def test_r4_same_polarity_duplicate_is_still_a_duplicate_not_a_contradiction() -> None:
|
||||
"""The two failures are different and must stay distinguishable."""
|
||||
with pytest.raises(RatificationError, match="duplicate edge"):
|
||||
validate_admissible(_record(AFFIRMATIVE))
|
||||
|
||||
|
||||
def test_r4_an_untaught_atom_admits_either_polarity() -> None:
|
||||
"""R4 forbids contradiction, not negatives."""
|
||||
subject, _connective, obj = _UNTAUGHT_ATOM
|
||||
validate_admissible(_record(NEGATIVE, subject=subject, obj=obj))
|
||||
validate_admissible(_record(AFFIRMATIVE, subject=subject, obj=obj))
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# R8 — the oracle, independently.
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def test_r8_oracle_does_not_import_the_compiler_s_polarity_vocabulary() -> None:
|
||||
"""Code-level independence is the whole evidentiary value.
|
||||
|
||||
If the oracle imported the compiler's polarity constants or helper, agreement
|
||||
would only prove the compiler agrees with itself and a polarity bug would be
|
||||
invisible on both sides at once.
|
||||
"""
|
||||
import inspect
|
||||
|
||||
import evals.curriculum_serve.oracle as oracle
|
||||
|
||||
source = inspect.getsource(oracle)
|
||||
assert "from teaching.curriculum_premises import" not in source
|
||||
assert "teaching.curriculum_premises" not in source
|
||||
# It has its own constants.
|
||||
assert oracle._AFFIRMATIVE == "affirmative"
|
||||
assert oracle._NEGATIVE == "negative"
|
||||
|
||||
|
||||
def test_r8_taught_edges_exposes_polarity() -> None:
|
||||
edges = taught_edges("physics")
|
||||
assert edges
|
||||
for _s, _c, _o, _id, polarity in edges:
|
||||
assert polarity == AFFIRMATIVE
|
||||
|
||||
|
||||
# ---------------------------------------------------------------------------
|
||||
# End to end, against a temporary corpus row. Restored byte-identically.
|
||||
# ---------------------------------------------------------------------------
|
||||
|
||||
def _plant(
|
||||
monkeypatch: pytest.MonkeyPatch, tmp_path: Path, *, polarity: str, chain_id: str
|
||||
) -> tuple[str, str, str]:
|
||||
"""Repoint BOTH loaders at a temp corpus carrying one extra row.
|
||||
|
||||
The committed corpus is never written. An earlier version of this fixture
|
||||
appended to `teaching/domain_chains/physics_chains_v1.jsonl` and restored it;
|
||||
that is safe under `smoke`/`deductive` (serial) but NOT under `full`, which
|
||||
injects `-n auto` — a parallel worker reading the corpus mid-mutation would
|
||||
see a row that is not committed, and the failure would look like a corpus
|
||||
problem rather than a test-isolation one.
|
||||
|
||||
Each loader is still redirected SEPARATELY, at its own module constant, and
|
||||
each still parses with its own code. Only the corpus LOCATION is shared; the
|
||||
ADR-0264 R8 independence being tested is untouched.
|
||||
"""
|
||||
import evals.curriculum_serve.oracle as oracle
|
||||
import teaching.curriculum_premises as premises
|
||||
|
||||
subject, connective, obj = _UNTAUGHT_ATOM
|
||||
row = {
|
||||
"chain_id": chain_id,
|
||||
"domain": "physics",
|
||||
"operator_family": "causal",
|
||||
"subject": subject,
|
||||
"intent": "cause",
|
||||
"connective": connective,
|
||||
"object": obj,
|
||||
"subject_pack_id": "en_physics_v1",
|
||||
"object_pack_id": "en_physics_v1",
|
||||
"review_status": "reviewed",
|
||||
"provenance": "test:polarity",
|
||||
}
|
||||
if polarity != AFFIRMATIVE:
|
||||
row["polarity"] = polarity
|
||||
|
||||
chain_dir = tmp_path / "teaching" / "domain_chains"
|
||||
chain_dir.mkdir(parents=True)
|
||||
for src in (REPO_ROOT / "teaching" / "domain_chains").glob("*.jsonl"):
|
||||
text = src.read_text(encoding="utf-8")
|
||||
if not text.endswith("\n"):
|
||||
text += "\n"
|
||||
if src.name == _PHYSICS_CORPUS.name:
|
||||
text += json.dumps(row, separators=(",", ":")) + "\n"
|
||||
(chain_dir / src.name).write_text(text, encoding="utf-8")
|
||||
# The compiler resolves corpora AND packs from its repo root, so the temp
|
||||
# tree needs the real packs visible under the same name.
|
||||
(tmp_path / "packs").symlink_to(REPO_ROOT / "packs")
|
||||
|
||||
monkeypatch.setattr(premises, "_REPO_ROOT", tmp_path)
|
||||
monkeypatch.setattr(oracle, "_CHAIN_DIR", chain_dir)
|
||||
premises.load_curriculum.cache_clear()
|
||||
premises._pack_lemmas.cache_clear()
|
||||
monkeypatch.setattr(
|
||||
premises.load_curriculum, "cache_clear", premises.load_curriculum.cache_clear
|
||||
)
|
||||
return subject, connective, obj
|
||||
|
||||
|
||||
@pytest.fixture
|
||||
def negative_row(
|
||||
monkeypatch: pytest.MonkeyPatch, tmp_path: Path
|
||||
) -> Iterator[tuple[str, str, str]]:
|
||||
"""A TAUGHT NEGATIVE for an atom physics does not otherwise teach."""
|
||||
atom = _plant(monkeypatch, tmp_path, polarity=NEGATIVE, chain_id="physics-causal-999")
|
||||
yield atom
|
||||
load_curriculum.cache_clear()
|
||||
|
||||
|
||||
def test_e2e_a_taught_negative_serves_refuted(negative_row: tuple[str, str, str]) -> None:
|
||||
"""The whole point: `polarity` now changes the answer.
|
||||
|
||||
Before this unit the same row served a confident `entailed` — a taught
|
||||
refutation answering "yes".
|
||||
"""
|
||||
subject, connective, obj = negative_row
|
||||
decision = decide_curriculum_question(f"Does {subject} {connective} {obj}?")
|
||||
assert decision.verdict == "refuted", decision
|
||||
assert decision.band == "curriculum_physics_causal"
|
||||
|
||||
|
||||
def test_e2e_the_independent_oracle_agrees(negative_row: tuple[str, str, str]) -> None:
|
||||
"""Two independently-written procedures must reach the same verdict, or the
|
||||
lane's `wrong=0` is measuring agreement with itself."""
|
||||
subject, connective, obj = negative_row
|
||||
gold = oracle_answer("physics", subject, connective, obj)
|
||||
served = decide_curriculum_question(f"Does {subject} {connective} {obj}?")
|
||||
assert gold.verdict == "refuted"
|
||||
assert gold.depth == 1, "a taught negative is a depth-1 statement, not a composition"
|
||||
assert served.verdict == gold.verdict
|
||||
|
||||
|
||||
def test_e2e_the_negative_premise_is_actually_compiled(
|
||||
negative_row: tuple[str, str, str],
|
||||
) -> None:
|
||||
subject, connective, obj = negative_row
|
||||
curriculum = load_curriculum("physics")
|
||||
premises, chain_ids = compile_premises(
|
||||
curriculum, "causal", query=(subject, connective, obj)
|
||||
)
|
||||
assert "physics-causal-999" in chain_ids
|
||||
assert any(p.startswith(NEGATION_PREFIX) for p in premises), premises
|
||||
|
||||
|
||||
def test_e2e_the_atom_was_unknown_before_the_negative_row() -> None:
|
||||
"""Without the fixture the same question is UNKNOWN — so the test above is
|
||||
measuring the row, not a pre-existing verdict."""
|
||||
subject, connective, obj = _UNTAUGHT_ATOM
|
||||
load_curriculum.cache_clear()
|
||||
decision = decide_curriculum_question(f"Does {subject} {connective} {obj}?")
|
||||
assert decision.verdict == "unknown", decision
|
||||
assert oracle_answer("physics", subject, connective, obj).verdict == "unknown"
|
||||
|
||||
|
||||
def test_e2e_negatives_are_excluded_from_reachability(
|
||||
negative_row: tuple[str, str, str],
|
||||
) -> None:
|
||||
"""R8 — a denial supplies no step, demonstrated on a path it would complete.
|
||||
|
||||
The fixture plants `mass does not cause charge`, and physics already teaches
|
||||
`charge causes field` (physics-causal-004). So if negatives entered the
|
||||
adjacency, `(mass, causes, field)` would report a 2-hop path built out of a
|
||||
DENIAL. `mass` has no other outgoing causal edge, so depth must stay 0.
|
||||
|
||||
Constructed this way on purpose: the assertion distinguishes the correct
|
||||
behaviour from the specific wrong one, rather than merely observing UNKNOWN
|
||||
(which both would produce).
|
||||
"""
|
||||
subject, _connective, obj = negative_row
|
||||
assert (obj, "causes", "field") in {
|
||||
(c.subject, c.connective, c.obj) for c in load_curriculum("physics").family("causal")
|
||||
}, "fixture premise moved: physics must still teach `charge causes field`"
|
||||
|
||||
verdict = oracle_answer("physics", subject, "causes", "field")
|
||||
assert verdict.verdict == "unknown"
|
||||
assert verdict.depth == 0, (
|
||||
f"reachability composed a {verdict.depth}-hop path through a denial "
|
||||
f"({subject} -/-> {obj} -> field) — ADR-0264 R8 excludes negatives from "
|
||||
"the adjacency precisely so this cannot happen"
|
||||
)
|
||||
|
||||
|
||||
def test_e2e_an_affirmative_row_in_the_same_slot_WOULD_create_that_path(
|
||||
monkeypatch: pytest.MonkeyPatch, tmp_path: Path
|
||||
) -> None:
|
||||
"""The control for the test above: the path is real when the row is positive.
|
||||
|
||||
Without this, `depth == 0` could just mean the oracle never finds 2-hop paths
|
||||
at all, and the R8 assertion would be vacuous. Same slot, same terms, only the
|
||||
polarity differs — so the two tests isolate polarity and nothing else.
|
||||
"""
|
||||
subject, _connective, _obj = _plant(
|
||||
monkeypatch, tmp_path, polarity=AFFIRMATIVE, chain_id="physics-causal-998"
|
||||
)
|
||||
verdict = oracle_answer("physics", subject, "causes", "field")
|
||||
assert verdict.verdict == "unknown", "a 2-hop path must not be ENTAILED"
|
||||
assert verdict.depth == 2, (
|
||||
f"expected the affirmative row to open a 2-hop path, got {verdict}"
|
||||
)
|
||||
load_curriculum.cache_clear()
|
||||
|
|
@ -335,11 +335,20 @@ def test_wrong_is_zero_for_every_band(report: dict) -> None:
|
|||
|
||||
|
||||
def test_gold_mix_has_no_refuted_class(report: dict) -> None:
|
||||
"""No corpus row can express a negative yet (ADR-0264 R1-R4 unimplemented), so
|
||||
`refuted` is unreachable and the mix is entailed/unknown only. Pinned so the
|
||||
polarity unit has a red test to turn green."""
|
||||
"""`refuted` is reachable in MECHANISM but absent from CONTENT.
|
||||
|
||||
ADR-0264 R1–R4/R8 are implemented, so a negative row would be compiled,
|
||||
decided and scored as `refuted` — `tests/test_curriculum_polarity.py` proves
|
||||
that end to end against a temporary corpus row. No negative row is COMMITTED,
|
||||
because authoring curriculum is Phase F and Shay's. So the shipped mix is
|
||||
still entailed/unknown only, and this stays a true statement about the corpus
|
||||
rather than about the machinery.
|
||||
"""
|
||||
for band, entry in report["classes"].items():
|
||||
assert "refuted" not in entry["gold_mix"], f"{band} produced refuted — polarity landed?"
|
||||
assert "refuted" not in entry["gold_mix"], (
|
||||
f"{band} produced refuted — a negative row was committed. That is "
|
||||
"Phase F content; update this pin deliberately alongside it."
|
||||
)
|
||||
assert set(entry["gold_mix"]) <= {"entailed", "unknown", "declined"}
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue