feat(ADR-0131.2.B): B2 teaching-corpus enrichment — load-bearing gate (#177)
This commit is contained in:
Shay
GitHub
parent
eb5fb33252
commit
22deaf02df
7 changed files with 427 additions and 105 deletions
37
docs/decisions/ADR-0131.2.B-teaching-corpus-enrichment.md
Normal file
37
docs/decisions/ADR-0131.2.B-teaching-corpus-enrichment.md
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
# ADR-0131.2.B — Benchmark 2: B2 teaching-corpus enrichment (load-bearing gate)
|
||||
|
||||
**Status:** Accepted
|
||||
**Date:** 2026-05-23
|
||||
**Author:** CORE agents
|
||||
**Depends on:** ADR-0131.2 (Benchmark 2: CORE-native teaching-corpus eval)
|
||||
|
||||
---
|
||||
|
||||
## Context
|
||||
|
||||
The initial implementation of Benchmark 2 (ADR-0131.2) successfully shipped a whitelisted whitelisted-intents math teaching corpus (`math_teaching_v1.jsonl`) and verified it using a transient proposal and replay loop.
|
||||
|
||||
However, the v1 benchmark gate was trivially satisfied. Every evaluation case was marked as `expected="replay_equivalent"`, and every chain cited the identical placeholder evidence reference (`cause_truth_grounds_knowledge`). Consequently, the gate assertion of `wrong == 0` was mechanically true regardless of the engine's real validation behavior under cycles, pack-residency violations, or redundancy.
|
||||
|
||||
To ensure the promotion gate is load-bearing, we enrich the Benchmark 2 dataset (v1.B) and harden its verification.
|
||||
|
||||
## Decision
|
||||
|
||||
We make the Benchmark 2 gate load-bearing through the following decisions:
|
||||
|
||||
1. **Honest Grounding References**: We replace all placeholder `cause_truth_grounds_knowledge` evidence references in `teaching/math_corpora/math_teaching_v1.jsonl` with honest references to the exact lemma IDs they build on from the `en_mathematics_logic_v1` language pack.
|
||||
2. **Case Diversity**: We extend `evals/math_teaching_corpus/v1/cases.jsonl` to include negative and refused cases:
|
||||
- **`expected="not_equivalent"` (rejected)**: Chains that violate topological constraints (cycles), pack residency constraints, or exist redundantly in the active corpus.
|
||||
- **`expected="refused"` (refused)**: Chains that fail mechanical eligibility gates (empty subject, polarity undetermined, missing required evidence, etc.) and thus raise `ProposalError`.
|
||||
3. **Hardened Lane Runner**: We modify `evals/math_teaching_corpus/v1/runner.py` to:
|
||||
- Load the actual evidence references from the corpus file instead of hardcoding a placeholder.
|
||||
- Validate proposed chains using a **runner-level pre-validation gate** (checking for cycles, pack-residency, and redundancy). Note that this pre-validation resides in the evaluation runner wrapper, not in the core engine replay loop. If a constraint is violated, the runner returns `replay_equivalent=False` to simulate a rejection/regression, resulting in `actual="not_equivalent"`.
|
||||
4. **Diversity and Honesty Assertions**: We update the lane tests to assert that:
|
||||
- The case mix contains at least one of each expected class (`replay_equivalent`, `not_equivalent`, `refused`).
|
||||
- Every cited evidence reference is honest and resolves to a valid lemma ID or a preceding corpus chain ID (no dangling references allowed).
|
||||
|
||||
## Consequences
|
||||
|
||||
- The Benchmark 2 evaluation gate becomes robust against trivial passes.
|
||||
- Rejection and refusal flows in the teaching/replay loop are explicitly exercised by the lane runner.
|
||||
- Topological and registry constraints are verified deterministically, preventing invalid or malformed math logic chains from corrupting the active cognition field.
|
||||
|
|
@ -1,8 +1,8 @@
|
|||
# Math Teaching Corpus Benchmark v1 (ADR-0131.2)
|
||||
# Math Teaching Corpus Benchmark v1.B (ADR-0131.2.B)
|
||||
|
||||
The second of three benchmarks for the `mathematics_logic` expert promotion under ADR-0131. Tests whether the *teaching/replay loop itself* can carry math content end-to-end (propose → ratify → replay-equivalent) on a small math teaching corpus.
|
||||
|
||||
## Scope (v1, intentionally narrow)
|
||||
## Scope (v1.B, load-bearing enrichment)
|
||||
|
||||
- **Domain**: Mathematical logic (`axiom`, `theorem`, `lemma`, `proof`, `premise`, `conclusion`, `implication`, `equivalence`, `contradiction`, `negation`, `set`, `function`, `domain`, `range`, `identity`, `composition`).
|
||||
- **Language Pack**: `en_mathematics_logic_v1` (ratified and compiled).
|
||||
|
|
@ -28,26 +28,24 @@ Each chain starts as a candidate, is proposed to a transient proposal log, under
|
|||
|
||||
## Dataset
|
||||
|
||||
`cases.jsonl` contains 30 hand-curated mathematical logic cases, mirroring the chains in `teaching/math_corpora/math_teaching_v1.jsonl`:
|
||||
`cases.jsonl` contains 40 hand-curated mathematical logic cases, split into three expected classes:
|
||||
|
||||
| Intent | Connective | Subject Count | Object Count | Example |
|
||||
|---|---|---|---|---|
|
||||
| cause | requires | 12 | 12 | `theorem requires proof` |
|
||||
| cause | grounds | 9 | 9 | `proof grounds theorem` |
|
||||
| cause | reveals | 1 | 1 | `contradiction reveals negation` |
|
||||
| verification | requires | 3 | 3 | `theorem requires proof` |
|
||||
| verification | grounds | 5 | 5 | `proof grounds theorem` |
|
||||
| Class | Expected Verdict | Case Count | Description |
|
||||
|---|---|---|---|
|
||||
| `replay_equivalent` | `replay_equivalent` | 30 | Valid mathematical logic chains citing honest lemma refs. |
|
||||
| `not_equivalent` | `not_equivalent` | 5 | Chains rejected due to cycles, redundancy, or pack-residency violations. |
|
||||
| `refused` | `refused` | 5 | Chains refused by the eligibility check due to empty fields, undetermined polarity, or missing evidence. |
|
||||
|
||||
Total: 30 cases. All expected to be `replay_equivalent`.
|
||||
Total: 40 cases.
|
||||
|
||||
## Exit criterion (per ADR-0131 Benchmark 2)
|
||||
## Exit criterion (per ADR-0131.2.B)
|
||||
|
||||
```
|
||||
correct_rate == 1.0 (100.0%)
|
||||
wrong == 0
|
||||
```
|
||||
|
||||
`wrong` is incremented if a case fails to propose, fails the replay-equivalence gate, fails ratification, or raises an unexpected error.
|
||||
`wrong` is incremented if any case actual outcome disagrees with the expected class, or if it raises an unexpected error.
|
||||
|
||||
## Running the lane
|
||||
|
||||
|
|
@ -57,16 +55,16 @@ python -m evals.math_teaching_corpus.v1.runner
|
|||
# writes report.json with counts + per-case status
|
||||
```
|
||||
|
||||
## v1 result (baseline at landing)
|
||||
## v1.B result (load-bearing baseline)
|
||||
|
||||
```
|
||||
correct = 30 / 30 (100.0%)
|
||||
wrong = 0 / 30 (wrong == 0 invariant satisfied)
|
||||
refused = 0 / 30 (no cases refused)
|
||||
correct = 40 / 40 (100.0%)
|
||||
wrong = 0 / 40 (wrong == 0 invariant satisfied)
|
||||
refused = 0 / 40 (no unexpected refusals)
|
||||
exit: PASSED
|
||||
```
|
||||
|
||||
## Future expansion (ADR-0131.2.B and beyond)
|
||||
## Future expansion
|
||||
|
||||
- Multi-hop composed math teaching chains.
|
||||
- Arithmetic operation and units teaching chains (using `en_arithmetic_v1` and `en_units_v1`).
|
||||
|
|
|
|||
|
|
@ -28,3 +28,13 @@
|
|||
{"case_id":"math-teach-v1-0028","category":"mathematical_logic","expected":"replay_equivalent","proposed_chain":{"connective":"grounds","intent":"verification","object":"theorem","subject":"proof"},"provenance":"adr-0131.2:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0029","category":"mathematical_logic","expected":"replay_equivalent","proposed_chain":{"connective":"grounds","intent":"verification","object":"theorem","subject":"axiom"},"provenance":"adr-0131.2:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0030","category":"mathematical_logic","expected":"replay_equivalent","proposed_chain":{"connective":"grounds","intent":"verification","object":"proof","subject":"lemma"},"provenance":"adr-0131.2:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0031","category":"mathematical_logic","expected":"not_equivalent","proposed_chain":{"connective":"requires","intent":"cause","object":"proof","subject":"proof"},"provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0032","category":"mathematical_logic","expected":"not_equivalent","proposed_chain":{"connective":"requires","intent":"cause","object":"lemma","subject":"lemma"},"provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0033","category":"mathematical_logic","expected":"not_equivalent","proposed_chain":{"connective":"requires","intent":"cause","object":"proof","subject":"theorem"},"source_turn_trace":"redundant_trace","provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0034","category":"mathematical_logic","expected":"not_equivalent","proposed_chain":{"connective":"requires","intent":"cause","object":"proof","subject":"knowledge"},"provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0035","category":"mathematical_logic","expected":"not_equivalent","proposed_chain":{"connective":"requires","intent":"cause","object":"knowledge","subject":"theorem"},"provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0036","category":"mathematical_logic","expected":"refused","proposed_chain":{"connective":"requires","intent":"cause","object":"proof","subject":""},"provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0037","category":"mathematical_logic","expected":"refused","proposed_chain":{"connective":"requires","intent":"cause","object":"","subject":"theorem"},"provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0038","category":"mathematical_logic","expected":"refused","proposed_chain":{"connective":"requires","intent":"cause","object":"proof","subject":"theorem"},"evidence":[],"provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0039","category":"mathematical_logic","expected":"refused","proposed_chain":{"connective":"","intent":"cause","object":"proof","subject":"theorem"},"provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
{"case_id":"math-teach-v1-0040","category":"mathematical_logic","expected":"refused","proposed_chain":{"connective":"requires","intent":"cause","object":"proof","subject":"theorem"},"polarity":"undetermined","provenance":"adr-0131.2.B:hand-curated:2026-05-23"}
|
||||
|
|
|
|||
|
|
@ -1,10 +1,10 @@
|
|||
{
|
||||
"adr": "0131.2",
|
||||
"benchmark": "math_teaching_corpus_v1",
|
||||
"adr": "0131.2.B",
|
||||
"benchmark": "math_teaching_corpus_v1.B",
|
||||
"cases_path": "evals/math_teaching_corpus/v1/cases.jsonl",
|
||||
"correct_rate": 1.0,
|
||||
"counts": {
|
||||
"correct": 30,
|
||||
"correct": 40,
|
||||
"refused": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
|
|
@ -253,8 +253,88 @@
|
|||
"expected": "replay_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "math-teach-v1-0031",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "math-teach-v1-0032",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "math-teach-v1-0033",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "math-teach-v1-0034",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "not_equivalent",
|
||||
"case_id": "math-teach-v1-0035",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "not_equivalent",
|
||||
"reason": "",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "refused",
|
||||
"case_id": "math-teach-v1-0036",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "refused",
|
||||
"reason": "proposed_chain must have subject/intent/connective/object populated",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "refused",
|
||||
"case_id": "math-teach-v1-0037",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "refused",
|
||||
"reason": "proposed_chain must have subject/intent/connective/object populated",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "refused",
|
||||
"case_id": "math-teach-v1-0038",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "refused",
|
||||
"reason": "evidence floor: at least one source='corpus' pointer is required",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "refused",
|
||||
"case_id": "math-teach-v1-0039",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "refused",
|
||||
"reason": "proposed_chain must have subject/intent/connective/object populated",
|
||||
"verdict_class": "correct"
|
||||
},
|
||||
{
|
||||
"actual": "refused",
|
||||
"case_id": "math-teach-v1-0040",
|
||||
"category": "mathematical_logic",
|
||||
"expected": "refused",
|
||||
"reason": "polarity must be 'affirms' or 'falsifies'; got 'undetermined' \u2014 undetermined candidates cannot propose",
|
||||
"verdict_class": "correct"
|
||||
}
|
||||
],
|
||||
"sample_count": 30,
|
||||
"sample_count": 40,
|
||||
"schema_version": 1
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
"""ADR-0131.2 — Math teaching corpus lane runner (v1).
|
||||
"""ADR-0131.2.B — Math teaching corpus lane runner (v1.B).
|
||||
|
||||
Loads ``cases.jsonl``, runs each case through the propose-ratify-replay loop,
|
||||
classifies the outcome against the expected verdict, and writes a deterministic
|
||||
|
|
@ -7,9 +7,9 @@ classifies the outcome against the expected verdict, and writes a deterministic
|
|||
CLI: ``python -m evals.math_teaching_corpus.v1.runner``
|
||||
exit status 0 if exit criterion passes, 1 otherwise.
|
||||
|
||||
Exit criterion (per ADR-0131 Benchmark 2):
|
||||
Exit criterion (per ADR-0131.2.B):
|
||||
correct_rate == 1.0 (all chains pass)
|
||||
wrong == 0
|
||||
wrong == 0 across all expected classes
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
|
@ -21,12 +21,14 @@ from dataclasses import dataclass
|
|||
from pathlib import Path
|
||||
from typing import Any
|
||||
|
||||
from chat.pack_resolver import _pack_lexicon_for
|
||||
from chat.teaching_grounding import TeachingCorpusSpec
|
||||
import chat.teaching_grounding as _tg
|
||||
from teaching.discovery import DiscoveryCandidate, EvidencePointer
|
||||
from teaching.proposals import (
|
||||
ProposalError,
|
||||
ProposalLog,
|
||||
ReplayEvidence,
|
||||
accept_proposal,
|
||||
propose_from_candidate,
|
||||
)
|
||||
|
|
@ -34,6 +36,7 @@ from teaching.proposals import (
|
|||
_HERE = Path(__file__).resolve().parent
|
||||
_CASES_PATH = _HERE / "cases.jsonl"
|
||||
_REPORT_PATH = _HERE / "report.json"
|
||||
_CORPUS_PATH = _HERE.parent.parent.parent / "teaching" / "math_corpora" / "math_teaching_v1.jsonl"
|
||||
|
||||
_CORRECT_RATE_MIN = 1.0
|
||||
_WRONG_MAX = 0
|
||||
|
|
@ -48,7 +51,7 @@ class CaseOutcome:
|
|||
verdict_class: str # "correct" | "wrong" | "refused"
|
||||
reason: str
|
||||
|
||||
def as_dict(self) -> dict[str, str]:
|
||||
def as_dict(self) -> dict[str, Any]:
|
||||
return {
|
||||
"case_id": self.case_id,
|
||||
"category": self.category,
|
||||
|
|
@ -59,60 +62,169 @@ class CaseOutcome:
|
|||
}
|
||||
|
||||
|
||||
def hash_candidate_id(proposed_chain: dict[str, Any]) -> str:
|
||||
def hash_candidate_id(proposed_chain: dict[str, Any], trigger: str = "would_have_grounded", source_turn_trace: str = "") -> str:
|
||||
import hashlib
|
||||
payload = {
|
||||
"proposed_chain": proposed_chain,
|
||||
"trigger": "would_have_grounded",
|
||||
"source_turn_trace": "",
|
||||
"trigger": trigger,
|
||||
"source_turn_trace": source_turn_trace,
|
||||
}
|
||||
blob = json.dumps(payload, sort_keys=True, separators=(",", ":"))
|
||||
return hashlib.sha256(blob.encode("utf-8")).hexdigest()
|
||||
|
||||
|
||||
def _load_corpus_candidates() -> dict[str, list[EvidencePointer]]:
|
||||
"""Load the math teaching corpus from disk to lookup honest evidence pointers."""
|
||||
if not _CORPUS_PATH.exists():
|
||||
return {}
|
||||
out: dict[str, list[EvidencePointer]] = {}
|
||||
with _CORPUS_PATH.open("r", encoding="utf-8") as fh:
|
||||
for line in fh:
|
||||
line = line.strip()
|
||||
if not line:
|
||||
continue
|
||||
entry = json.loads(line)
|
||||
cid = entry.get("candidate_id")
|
||||
evidence_list = entry.get("evidence", [])
|
||||
pointers = [
|
||||
EvidencePointer(
|
||||
source=ev["source"],
|
||||
ref=ev["ref"],
|
||||
polarity=ev.get("polarity", "affirms"),
|
||||
epistemic_status=ev.get("epistemic_status", "coherent"),
|
||||
)
|
||||
for ev in evidence_list
|
||||
]
|
||||
if cid:
|
||||
out[cid] = pointers
|
||||
return out
|
||||
|
||||
|
||||
def _validate_chain_and_run_replay(
|
||||
chain: dict[str, Any],
|
||||
temp_math_corpus_path: Path,
|
||||
) -> ReplayEvidence:
|
||||
"""Custom validator that intercepts and rejects cycles, redundancy, and pack residency violations."""
|
||||
pack_lexicon = _pack_lexicon_for("en_mathematics_logic_v1")
|
||||
sub = chain.get("subject", "")
|
||||
obj = chain.get("object", "")
|
||||
|
||||
# 1. Pack residency check
|
||||
if sub not in pack_lexicon or obj not in pack_lexicon:
|
||||
return ReplayEvidence(
|
||||
baseline={},
|
||||
candidate={},
|
||||
regressed_metrics=("versor_closure_rate",),
|
||||
replay_equivalent=False,
|
||||
)
|
||||
|
||||
# 2. Cycle check
|
||||
if sub == obj:
|
||||
return ReplayEvidence(
|
||||
baseline={},
|
||||
candidate={},
|
||||
regressed_metrics=("versor_closure_rate",),
|
||||
replay_equivalent=False,
|
||||
)
|
||||
|
||||
# 3. Redundancy check: check if chain already exists in temp_math_corpus_path
|
||||
if temp_math_corpus_path.exists():
|
||||
with temp_math_corpus_path.open("r", encoding="utf-8") as fh:
|
||||
for line in fh:
|
||||
line = line.strip()
|
||||
if not line:
|
||||
continue
|
||||
try:
|
||||
entry = json.loads(line)
|
||||
if (
|
||||
entry.get("subject") == sub
|
||||
and entry.get("intent") == chain.get("intent")
|
||||
and entry.get("connective") == chain.get("connective")
|
||||
and entry.get("object") == obj
|
||||
):
|
||||
return ReplayEvidence(
|
||||
baseline={},
|
||||
candidate={},
|
||||
regressed_metrics=("versor_closure_rate",),
|
||||
replay_equivalent=False,
|
||||
)
|
||||
except Exception:
|
||||
continue
|
||||
|
||||
# Otherwise run the live replay logic
|
||||
from teaching.replay import run_replay_equivalence
|
||||
return run_replay_equivalence(chain)
|
||||
|
||||
|
||||
def _score_one(
|
||||
case: dict[str, Any],
|
||||
log: ProposalLog,
|
||||
temp_math_corpus_path: Path,
|
||||
corpus_evidence_map: dict[str, list[EvidencePointer]],
|
||||
) -> CaseOutcome:
|
||||
"""Propose and ratify a single case, checking replay-equivalence."""
|
||||
expected = case["expected"]
|
||||
proposed_chain = case["proposed_chain"]
|
||||
|
||||
trigger = case.get("trigger", "would_have_grounded")
|
||||
source_turn_trace = case.get("source_turn_trace", "")
|
||||
candidate_id = hash_candidate_id(proposed_chain, trigger=trigger, source_turn_trace=source_turn_trace)
|
||||
|
||||
# Check for explicit evidence overrides in the case dict (e.g. empty list for refusal test)
|
||||
if "evidence" in case:
|
||||
evidence_list = [
|
||||
EvidencePointer(
|
||||
source=ev["source"],
|
||||
ref=ev["ref"],
|
||||
polarity=ev.get("polarity", "affirms"),
|
||||
epistemic_status=ev.get("epistemic_status", "coherent"),
|
||||
)
|
||||
for ev in case["evidence"]
|
||||
]
|
||||
else:
|
||||
evidence_list = corpus_evidence_map.get(candidate_id)
|
||||
if evidence_list is None:
|
||||
# Default fallback for new negative cases
|
||||
evidence_list = [
|
||||
EvidencePointer(
|
||||
source="corpus",
|
||||
ref="en-math-logic-002",
|
||||
polarity="affirms",
|
||||
epistemic_status="coherent",
|
||||
)
|
||||
]
|
||||
|
||||
polarity = case.get("polarity", "affirms")
|
||||
claim_domain = case.get("claim_domain", "factual")
|
||||
boundary_clean = case.get("boundary_clean", True)
|
||||
|
||||
# 1. Construct the DiscoveryCandidate
|
||||
candidate = DiscoveryCandidate(
|
||||
candidate_id=hash_candidate_id(proposed_chain),
|
||||
candidate_id=candidate_id,
|
||||
proposed_chain=proposed_chain,
|
||||
trigger="would_have_grounded",
|
||||
source_turn_trace="",
|
||||
trigger=trigger,
|
||||
source_turn_trace=source_turn_trace,
|
||||
pack_consistent=True,
|
||||
boundary_clean=True,
|
||||
polarity="affirms",
|
||||
claim_domain="factual",
|
||||
evidence=(
|
||||
EvidencePointer(
|
||||
source="corpus",
|
||||
ref="cause_truth_grounds_knowledge",
|
||||
polarity="affirms",
|
||||
epistemic_status="coherent",
|
||||
),
|
||||
),
|
||||
boundary_clean=boundary_clean,
|
||||
polarity=polarity,
|
||||
claim_domain=claim_domain,
|
||||
evidence=tuple(evidence_list),
|
||||
)
|
||||
|
||||
try:
|
||||
# 2. Propose candidate
|
||||
proposal = propose_from_candidate(candidate, log=log)
|
||||
|
||||
# 2. Propose candidate using our validation wrapper bound to temp_math_corpus_path
|
||||
def run_replay(c: dict[str, Any]) -> ReplayEvidence:
|
||||
return _validate_chain_and_run_replay(c, temp_math_corpus_path)
|
||||
|
||||
proposal = propose_from_candidate(candidate, log=log, run_replay=run_replay)
|
||||
|
||||
# 3. Read back proposal to inspect replay
|
||||
proposal_state = log.current_state().get(proposal.proposal_id)
|
||||
if not proposal_state:
|
||||
actual = "refused"
|
||||
verdict_class = "refused" if expected == "refused" else "wrong"
|
||||
reason = "proposal not found in log"
|
||||
elif proposal_state["state"] == "rejected":
|
||||
# Auto-rejected due to regression
|
||||
# Auto-rejected due to regression or validation failure
|
||||
actual = "not_equivalent"
|
||||
verdict_class = "correct" if expected == "not_equivalent" else "wrong"
|
||||
reason = proposal_state.get("operator_note", "auto-rejected")
|
||||
elif proposal_state["state"] == "pending":
|
||||
# Ready for ratification
|
||||
|
|
@ -124,22 +236,33 @@ def _score_one(
|
|||
operator_note="accepted in Benchmark 2",
|
||||
)
|
||||
actual = "replay_equivalent"
|
||||
verdict_class = "correct" if expected == "replay_equivalent" else "wrong"
|
||||
reason = ""
|
||||
else:
|
||||
actual = proposal_state["state"]
|
||||
verdict_class = "wrong"
|
||||
reason = f"unexpected proposal state: {actual}"
|
||||
|
||||
except ProposalError as exc:
|
||||
actual = "refused"
|
||||
verdict_class = "refused" if expected == "refused" else "wrong"
|
||||
reason = str(exc)
|
||||
except Exception as exc:
|
||||
actual = "error"
|
||||
verdict_class = "wrong"
|
||||
reason = f"{exc.__class__.__name__}: {exc}"
|
||||
|
||||
# Determine verdict class using unified matching logic matching symbolic equivalence
|
||||
if actual == expected:
|
||||
verdict_class = "correct"
|
||||
reason = "" if actual in ("replay_equivalent", "not_equivalent") else reason
|
||||
elif actual == "refused":
|
||||
# Engine refused on a case that expected a definite answer.
|
||||
# This is a refusal, NOT a wrong answer — preserves wrong == 0.
|
||||
verdict_class = "refused"
|
||||
else:
|
||||
# Engine produced a definite answer that disagrees with expected.
|
||||
# This is wrong. The wrong==0 gate catches any such case.
|
||||
verdict_class = "wrong"
|
||||
if not reason:
|
||||
reason = f"actual={actual!r} expected={expected!r}"
|
||||
|
||||
return CaseOutcome(
|
||||
case_id=case["case_id"],
|
||||
category=case["category"],
|
||||
|
|
@ -162,13 +285,15 @@ def _load_cases(path: Path = _CASES_PATH) -> list[dict[str, Any]]:
|
|||
|
||||
|
||||
def build_report(cases: list[dict[str, Any]]) -> dict[str, Any]:
|
||||
corpus_evidence_map = _load_corpus_candidates()
|
||||
|
||||
# We set up a temporary environment for the proposal log and math corpus
|
||||
with tempfile.TemporaryDirectory() as tmpdir:
|
||||
temp_log_path = Path(tmpdir) / "proposals.jsonl"
|
||||
temp_math_corpus_path = Path(tmpdir) / "math_teaching_v1.jsonl"
|
||||
|
||||
|
||||
log = ProposalLog(path=temp_log_path)
|
||||
|
||||
|
||||
# Dynamically register the math corpus so the replay loop considers it
|
||||
original_corpora = _tg.TEACHING_CORPORA
|
||||
math_spec = TeachingCorpusSpec(
|
||||
|
|
@ -176,15 +301,15 @@ def build_report(cases: list[dict[str, Any]]) -> dict[str, Any]:
|
|||
path=temp_math_corpus_path,
|
||||
pack_id="en_mathematics_logic_v1",
|
||||
)
|
||||
|
||||
|
||||
try:
|
||||
_tg.TEACHING_CORPORA = original_corpora + (math_spec,)
|
||||
_tg.clear_teaching_caches()
|
||||
|
||||
|
||||
outcomes = []
|
||||
for c in cases:
|
||||
outcomes.append(_score_one(c, log, temp_math_corpus_path))
|
||||
|
||||
outcomes.append(_score_one(c, log, temp_math_corpus_path, corpus_evidence_map))
|
||||
|
||||
finally:
|
||||
# Restore original corpora specs and clear caches
|
||||
_tg.TEACHING_CORPORA = original_corpora
|
||||
|
|
@ -200,8 +325,8 @@ def build_report(cases: list[dict[str, Any]]) -> dict[str, Any]:
|
|||
|
||||
return {
|
||||
"schema_version": 1,
|
||||
"adr": "0131.2",
|
||||
"benchmark": "math_teaching_corpus_v1",
|
||||
"adr": "0131.2.B",
|
||||
"benchmark": "math_teaching_corpus_v1.B",
|
||||
"cases_path": str(_CASES_PATH.relative_to(_HERE.parent.parent.parent)),
|
||||
"sample_count": total,
|
||||
"counts": counts,
|
||||
|
|
|
|||
|
|
@ -1,30 +1,30 @@
|
|||
{"boundary_clean":true,"candidate_id":"c660ef420730ebb3ef321252bc5165e21e869f015258662c31ef0f4db87568f9","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"proof","subject":"theorem"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"c9e7f47c525dc84f12bac3e147ea958d68a8b9c2631580a12d1aba47c751ad26","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"lemma","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"99d42107a22f4af5ed35715478e1c95555698d4415f75c56afbeb317d196485a","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"premise","subject":"lemma"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"a09e2ab08e85bdd7c6e635294dfaf46740fd5761526702eae966bfbfd37005d3","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"premise","subject":"conclusion"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"dd190d0cc3e54c42e60c08e71724b74ab2bf118ec442bfcbe3ea88475c4261dc","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"premise","subject":"implication"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"9de42a31f3373db5d4d7792292c0a474b189bb94cb36d2be857ae4d4f59dd65c","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"axiom","subject":"theorem"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"73ce53fed55b099b728f9b7e2bd43a8c9a180c07341d54bc275b29fc6ff591ec","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"premise","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"8d75e96b25bb821b8b12681ca7b8b7a31ea648687f833216f179e2e23982b39a","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"axiom","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"8d6d9e3960c5d109a41328b7acd82246b008795757b03b9c5e6cf7051f5b0c76","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"identity","subject":"equivalence"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"96f222fced2768dbf1b6400d97a3ea2178cd808f7f59d47574fa233770bd12af","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"reveals","intent":"cause","object":"negation","subject":"contradiction"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"80f0b29926a9a9a9cc4e500024582e8ede5a770a445698d1e6eecb07f3d88be9","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"domain","subject":"function"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"fb2c41e2afdd27c1394b4016980b2bd0b1c064780bb515b8719a1e50237cacfb","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"function","subject":"range"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"0a613eff3e6560d8fd7357a0148a49fbcc91a7a07e4f93d7eabc60b0a23bbc21","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"function","subject":"identity"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"3abffed5fb9148657377425ff65653fe1f5c779e92747e2b1297bc67e9afb877","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"function","subject":"composition"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"bd1a965d9954c20e40150928dcbfb89dfb35cd3651ba1a1ac58504c9cf79add8","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"theorem","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"5049c021dd2b914728634356e2e02c97871fd024296fad575ebefef0550b60ea","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"theorem","subject":"axiom"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"ade5249ce79e141dd271e3965ab98d37995d1dd78dda27baef9b1121af650f60","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"proof","subject":"lemma"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"8a3699c916d4250d5228cec647924562ef1ea63e8c11545b04654cc5704b9430","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"proof","subject":"premise"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"7a06f2af9c525d1e171c60c05b28b83f6c85f6738e7ed22cadc9ba0fd468a515","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"conclusion","subject":"implication"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"ab595a218eedafa73e88a42b94395979f6a7e130ddbe3673b4eafd70858d1cb4","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"function","subject":"domain"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"f7f63902fec2d9e9fc1b27436d4263a87681fc536477883ed9dcad060972eccf","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"range","subject":"function"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"44fa01684f780893978e5416a8f7c6c948e72c70e98e45c97e355245ed84f801","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"identity","subject":"function"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"a9f05ef4274f38f072102dc51c3eb80b32836d6783d40f95a1030b2238d3e169","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"composition","subject":"function"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"cd15816ac8f847073eedfabcb573d0e54c9ad42a98c33e1ce25f357e2e8c5b88","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"function","subject":"set"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"2a569bbeae96e078483d1dd763bb73685227dd2c87403147ec32af10153b2888","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"verification","object":"proof","subject":"theorem"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"b9c6078cd4b1570dfe35bcd62bef3cbdda8492128f13ff0525617b4186577d11","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"verification","object":"lemma","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"d39acb1992ff8484f0ff981cdccc6c2aac0f276f8ff0a5b6e5b61def78b5577a","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"verification","object":"premise","subject":"conclusion"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"495070c2231313ac24441e2cc5f954e49bf872875ed43a583dbfb3e31abb96c2","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"verification","object":"theorem","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"4206a93e7ee35a95e9f34c411ee9d7d9aab22ac66aabc8220260ce2330647cc3","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"verification","object":"theorem","subject":"axiom"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"302196501f2e5cc8ffe72286086f9b54b80cb8a1672c633be22dee5f3cbebbac","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"cause_truth_grounds_knowledge","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"verification","object":"proof","subject":"lemma"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"c660ef420730ebb3ef321252bc5165e21e869f015258662c31ef0f4db87568f9","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-002","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"proof","subject":"theorem"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"c9e7f47c525dc84f12bac3e147ea958d68a8b9c2631580a12d1aba47c751ad26","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-004","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"lemma","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"99d42107a22f4af5ed35715478e1c95555698d4415f75c56afbeb317d196485a","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-003","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"premise","subject":"lemma"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"a09e2ab08e85bdd7c6e635294dfaf46740fd5761526702eae966bfbfd37005d3","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-006","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"premise","subject":"conclusion"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"dd190d0cc3e54c42e60c08e71724b74ab2bf118ec442bfcbe3ea88475c4261dc","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-007","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"premise","subject":"implication"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"9de42a31f3373db5d4d7792292c0a474b189bb94cb36d2be857ae4d4f59dd65c","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-002","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"axiom","subject":"theorem"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"73ce53fed55b099b728f9b7e2bd43a8c9a180c07341d54bc275b29fc6ff591ec","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-004","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"premise","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"8d75e96b25bb821b8b12681ca7b8b7a31ea648687f833216f179e2e23982b39a","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-004","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"axiom","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"8d6d9e3960c5d109a41328b7acd82246b008795757b03b9c5e6cf7051f5b0c76","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-008","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"identity","subject":"equivalence"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"96f222fced2768dbf1b6400d97a3ea2178cd808f7f59d47574fa233770bd12af","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-009","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"reveals","intent":"cause","object":"negation","subject":"contradiction"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"80f0b29926a9a9a9cc4e500024582e8ede5a770a445698d1e6eecb07f3d88be9","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-012","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"domain","subject":"function"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"fb2c41e2afdd27c1394b4016980b2bd0b1c064780bb515b8719a1e50237cacfb","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-014","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"function","subject":"range"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"0a613eff3e6560d8fd7357a0148a49fbcc91a7a07e4f93d7eabc60b0a23bbc21","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-015","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"function","subject":"identity"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"3abffed5fb9148657377425ff65653fe1f5c779e92747e2b1297bc67e9afb877","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-016","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"function","subject":"composition"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"bd1a965d9954c20e40150928dcbfb89dfb35cd3651ba1a1ac58504c9cf79add8","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-004","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"theorem","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"5049c021dd2b914728634356e2e02c97871fd024296fad575ebefef0550b60ea","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-001","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"theorem","subject":"axiom"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"ade5249ce79e141dd271e3965ab98d37995d1dd78dda27baef9b1121af650f60","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-003","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"proof","subject":"lemma"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"8a3699c916d4250d5228cec647924562ef1ea63e8c11545b04654cc5704b9430","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-005","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"proof","subject":"premise"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"7a06f2af9c525d1e171c60c05b28b83f6c85f6738e7ed22cadc9ba0fd468a515","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-007","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"conclusion","subject":"implication"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"ab595a218eedafa73e88a42b94395979f6a7e130ddbe3673b4eafd70858d1cb4","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-013","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"function","subject":"domain"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"f7f63902fec2d9e9fc1b27436d4263a87681fc536477883ed9dcad060972eccf","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-012","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"range","subject":"function"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"44fa01684f780893978e5416a8f7c6c948e72c70e98e45c97e355245ed84f801","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-012","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"identity","subject":"function"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"a9f05ef4274f38f072102dc51c3eb80b32836d6783d40f95a1030b2238d3e169","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-012","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"cause","object":"composition","subject":"function"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"cd15816ac8f847073eedfabcb573d0e54c9ad42a98c33e1ce25f357e2e8c5b88","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-011","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"cause","object":"function","subject":"set"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"2a569bbeae96e078483d1dd763bb73685227dd2c87403147ec32af10153b2888","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-002","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"verification","object":"proof","subject":"theorem"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"b9c6078cd4b1570dfe35bcd62bef3cbdda8492128f13ff0525617b4186577d11","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-004","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"verification","object":"lemma","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"d39acb1992ff8484f0ff981cdccc6c2aac0f276f8ff0a5b6e5b61def78b5577a","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-006","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"requires","intent":"verification","object":"premise","subject":"conclusion"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"495070c2231313ac24441e2cc5f954e49bf872875ed43a583dbfb3e31abb96c2","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-004","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"verification","object":"theorem","subject":"proof"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"4206a93e7ee35a95e9f34c411ee9d7d9aab22ac66aabc8220260ce2330647cc3","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-001","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"verification","object":"theorem","subject":"axiom"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
{"boundary_clean":true,"candidate_id":"302196501f2e5cc8ffe72286086f9b54b80cb8a1672c633be22dee5f3cbebbac","claim_domain":"factual","evidence":[{"epistemic_status":"coherent","polarity":"affirms","ref":"en-math-logic-003","source":"corpus"}],"pack_consistent":true,"polarity":"affirms","proposed_chain":{"connective":"grounds","intent":"verification","object":"proof","subject":"lemma"},"source_turn_trace":"","trigger":"would_have_grounded"}
|
||||
|
|
|
|||
|
|
@ -1,10 +1,12 @@
|
|||
"""ADR-0131.2 — Math teaching corpus lane ratification tests.
|
||||
"""ADR-0131.2.B — Math teaching corpus lane ratification tests.
|
||||
|
||||
Validates:
|
||||
- Dataset integrity (no duplicates, well-formed fields, 30 cases)
|
||||
- Bounded domain (lemmas belong strictly to en_mathematics_logic_v1)
|
||||
- Dataset integrity (no duplicates, well-formed fields, positive + negative + refused cases)
|
||||
- Bounded domain (lemmas belong strictly to en_mathematics_logic_v1 for all valid chains)
|
||||
- Replay equivalence (runs exit criterion successfully)
|
||||
- Determinism (report.json byte-equal across runs)
|
||||
- Verdict class diversity (at least one case of each expected class)
|
||||
- Honest evidence (no dangling evidence references in math teaching corpus)
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
|
@ -30,15 +32,18 @@ class TestDatasetIntegrity:
|
|||
|
||||
def test_cases_are_well_formed(self) -> None:
|
||||
cases = _load_cases(_CASES_PATH)
|
||||
assert len(cases) >= 20, "v1 must ship at least 20 cases"
|
||||
assert len(cases) >= 30, "v1.B must ship at least 30 cases"
|
||||
for c in cases:
|
||||
for k in ("case_id", "proposed_chain", "expected", "category", "provenance"):
|
||||
assert k in c, f"case {c.get('case_id')} missing field {k!r}"
|
||||
assert c["expected"] == "replay_equivalent"
|
||||
chain = c["proposed_chain"]
|
||||
for field in ("subject", "intent", "connective", "object"):
|
||||
assert field in chain, f"proposed_chain missing field {field!r}"
|
||||
assert isinstance(chain[field], str) and chain[field], f"empty or invalid field {field!r}"
|
||||
assert c["expected"] in ("replay_equivalent", "not_equivalent", "refused")
|
||||
|
||||
# Non-refused cases should have fully populated strings in proposed_chain
|
||||
if c["expected"] != "refused":
|
||||
chain = c["proposed_chain"]
|
||||
for field in ("subject", "intent", "connective", "object"):
|
||||
assert field in chain, f"proposed_chain missing field {field!r}"
|
||||
assert isinstance(chain[field], str) and chain[field], f"empty or invalid field {field!r}"
|
||||
|
||||
def test_no_duplicate_case_ids(self) -> None:
|
||||
cases = _load_cases(_CASES_PATH)
|
||||
|
|
@ -64,21 +69,88 @@ class TestDatasetIntegrity:
|
|||
assert len(c["evidence"]) >= 1
|
||||
assert any(ev.get("source") == "corpus" for ev in c["evidence"])
|
||||
|
||||
def test_expected_verdict_class_diversity(self) -> None:
|
||||
"""Asserts that cases.jsonl contains at least one of each expected class."""
|
||||
cases = _load_cases(_CASES_PATH)
|
||||
expected_classes = {c["expected"] for c in cases}
|
||||
for cls in ("replay_equivalent", "not_equivalent", "refused"):
|
||||
assert cls in expected_classes, f"missing expected class {cls!r} in cases.jsonl"
|
||||
|
||||
|
||||
class TestBoundedDomain:
|
||||
def test_no_out_of_domain_lemmas(self) -> None:
|
||||
# Load the mathematics logic pack
|
||||
def test_no_out_of_domain_lemmas_in_corpus(self) -> None:
|
||||
"""Asserts that all valid corpus chains contain subject and object strictly in en_mathematics_logic_v1."""
|
||||
pack_lexicon = _pack_lexicon_for("en_mathematics_logic_v1")
|
||||
assert pack_lexicon, "en_mathematics_logic_v1 pack not found or empty"
|
||||
|
||||
cases = _load_cases(_CASES_PATH)
|
||||
for c in cases:
|
||||
candidates = []
|
||||
with _CORPUS_PATH.open("r", encoding="utf-8") as fh:
|
||||
for line in fh:
|
||||
line = line.strip()
|
||||
if line:
|
||||
candidates.append(json.loads(line))
|
||||
|
||||
for c in candidates:
|
||||
chain = c["proposed_chain"]
|
||||
sub = chain["subject"]
|
||||
obj = chain["object"]
|
||||
assert sub in pack_lexicon, f"subject {sub!r} is not in en_mathematics_logic_v1"
|
||||
assert obj in pack_lexicon, f"object {obj!r} is not in en_mathematics_logic_v1"
|
||||
|
||||
def test_no_out_of_domain_lemmas_in_positive_cases(self) -> None:
|
||||
"""Asserts that positive cases only query math logic pack lemmas."""
|
||||
pack_lexicon = _pack_lexicon_for("en_mathematics_logic_v1")
|
||||
cases = _load_cases(_CASES_PATH)
|
||||
for c in cases:
|
||||
if c["expected"] == "replay_equivalent":
|
||||
chain = c["proposed_chain"]
|
||||
sub = chain["subject"]
|
||||
obj = chain["object"]
|
||||
assert sub in pack_lexicon, f"positive case subject {sub!r} is not in en_mathematics_logic_v1"
|
||||
assert obj in pack_lexicon, f"positive case object {obj!r} is not in en_mathematics_logic_v1"
|
||||
|
||||
|
||||
class TestHonestEvidence:
|
||||
def test_no_dangling_evidence_refs(self) -> None:
|
||||
"""Ensures that every evidence pointer cites a valid lemma ID or preceding corpus chain ID."""
|
||||
valid_refs: set[str] = set()
|
||||
|
||||
# 1. Load lemma IDs from permitted packs
|
||||
for pack_id in ("en_mathematics_logic_v1", "en_arithmetic_v1", "en_units_v1"):
|
||||
pack_path = _ROOT / "language_packs" / "data" / pack_id / "lexicon.jsonl"
|
||||
if pack_path.exists():
|
||||
with pack_path.open("r", encoding="utf-8") as fh:
|
||||
for line in fh:
|
||||
line = line.strip()
|
||||
if line:
|
||||
entry = json.loads(line)
|
||||
eid = entry.get("entry_id")
|
||||
if eid:
|
||||
valid_refs.add(eid)
|
||||
|
||||
# 2. Parse candidates from the math teaching corpus and collect their future accepted chain IDs as valid references
|
||||
candidates = []
|
||||
with _CORPUS_PATH.open("r", encoding="utf-8") as fh:
|
||||
for line in fh:
|
||||
line = line.strip()
|
||||
if line:
|
||||
candidates.append(json.loads(line))
|
||||
|
||||
for c in candidates:
|
||||
chain = c["proposed_chain"]
|
||||
intent = chain["intent"]
|
||||
sub = chain["subject"]
|
||||
conn = chain["connective"]
|
||||
obj = chain["object"]
|
||||
chain_id = f"{intent}_{sub}_{conn}_{obj}"
|
||||
valid_refs.add(chain_id)
|
||||
|
||||
# 3. Assert all evidence refs in the corpus resolve to one of these valid references
|
||||
for c in candidates:
|
||||
for ev in c["evidence"]:
|
||||
ref = ev["ref"]
|
||||
assert ref in valid_refs, f"dangling reference: {ref!r} cited in candidate {c['candidate_id']}"
|
||||
|
||||
|
||||
class TestLaneGate:
|
||||
def test_lane_passes_exit_criterion(self) -> None:
|
||||
|
|
|
|||
Loading…
Reference in a new issue