Merge pull request #554 from AssetOverflow/claude/modest-franklin-85067f
Ratify independent-gold invariant (INV-25) + SHA-pin deductive lane
This commit is contained in:
Shay
GitHub
commit
0932c0e92e
10 changed files with 609 additions and 16 deletions
|
|
@ -42,6 +42,7 @@ is a CI failure (`.github/workflows/lane-shas.yml`).
|
|||
| ADR-0099 | `public_demo` | Public showcase runs deterministically under 30s; all claims supported | `evals/public_demo/results/v1_dev.json` | `e323adb35ea17987991395424c603ff93bca08c11bc2713bd9f6338e86bb269f` |
|
||||
| ADR-0104 | `curriculum_loop_closure` | Curriculum-sourced proposals route through single reviewed teaching path | `evals/curriculum_loop_closure/results/v1_dev.json` | `b46d56b2d209172cc3ffaf3776dc8dcfe55093f13587c5cb67372be6dfa23e8d` |
|
||||
| ADR-0131 | `math_teaching_corpus_v1` | Math teaching corpus replays deterministically; all chains pass exit criterion (correct_rate=1.0, wrong=0) | `evals/math_teaching_corpus/v1/report.json` | `eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4` |
|
||||
| ADR-0206 | `deductive_logic_v1` | Propositional entailment scored against an independent truth-table oracle; dev+holdout+external 716/716 correct, wrong=0, refused=0 | `evals/deductive_logic/report.json` | `97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f` |
|
||||
|
||||
## Verification
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
<!-- CANONICAL | docs/analysis/pivot-to-deductive-logic-2026-06-04.md | 2026-06-04 | strategy/post-mortem | why we left the GSM8K chase, what went wrong, and the deductive-logic path we are now on | verified: holdout 500/500 wrong=0, 8000-case engine-vs-oracle fuzz 0 disagreements -->
|
||||
<!-- CANONICAL | docs/analysis/pivot-to-deductive-logic-2026-06-04.md | 2026-06-04 | strategy/post-mortem | why we left the GSM8K chase, what went wrong, and the deductive-logic path we are now on | verified: deductive holdout 500/500 wrong=0, deterministic 3,000-case engine-vs-oracle fuzz (2,796 definite) 0 disagreements -->
|
||||
|
||||
# The pivot to deductive logic — what went wrong, and the path now
|
||||
|
||||
|
|
@ -48,11 +48,20 @@ three sets, same day:
|
|||
| Set | correct | wrong | what it is |
|
||||
|---|---:|---:|---|
|
||||
| `train_sample` (50) | 4 | 0 | the data CORE was **built on** — overfit, no predictive validity |
|
||||
| `holdout_dev` (500) | **0** | 0 | real GSM8K **never built-against** — the honest baseline |
|
||||
| `holdout_dev` (500) | 5† | 0 | real GSM8K **never built-against** — the composer scored **0**; the 5 are the narrow R1 reconstruction |
|
||||
| sealed test (1,319) | 0 | 0 | the final exam |
|
||||
|
||||
**Real GSM8K capability was 0%.** The four train "correct" generalised to *zero* of
|
||||
500 held-out cases. Serving held `wrong = 0` only because it refused everything real.
|
||||
† Committed `evals/gsm8k_math/holdout_dev/v1/report.json` reads **5 correct / 0 wrong
|
||||
/ 495 refused**. All 5 come from the narrow, verifier-gated **R1 comparative-total
|
||||
reconstruction** (a typed reader, not the composer), which landed the same day; the
|
||||
composer (`resolve_pooled`) generalised to **0** of 500. The "0%" below is the
|
||||
composer's number — the subject of this post-mortem. (The original snapshot read
|
||||
`0/500`; it predated the R1 landing and is corrected here to match the committed
|
||||
artifact.)
|
||||
|
||||
**The composer's real GSM8K capability was 0%.** Its four train "correct" generalised
|
||||
to *zero* of 500 held-out cases (the 5 committed held-out correct are the separate R1
|
||||
reconstruction, above). Serving held `wrong = 0` only because it refused everything real.
|
||||
|
||||
**The deeper finding — the composer is *unsound*, not just narrow.** The derivation
|
||||
composer (`resolve_pooled`), the reader the whole composition program was built around
|
||||
|
|
@ -116,12 +125,16 @@ by design (propositional regime only).
|
|||
|---|---:|---:|---:|---:|
|
||||
| dev | 200 | 200 | **0** | 74 |
|
||||
| **holdout v1** | 500 | **500** | **0** | **227** |
|
||||
| fuzz (fresh random, engine vs **independent** oracle) | 7,340 | 7,340 | **0** | 3,360 |
|
||||
| fuzz (seed 424242, engine vs **independent** oracle) | 2,796 | 2,796 | **0** | 1,241 |
|
||||
|
||||
The gold is computed by an **independent truth-table oracle**
|
||||
(`evals/deductive_logic/oracle.py`) sharing **no code** with the ROBDD engine.
|
||||
**8,000 fresh random problems, two independent sound decision procedures, zero
|
||||
disagreements** — the soundness evidence the GSM8K composer could never produce.
|
||||
The committed gate (`test_engine_matches_independent_oracle_fuzz`) runs a
|
||||
deterministic **3,000-case** fuzz of which **2,796** are in-regime/definite, with
|
||||
**zero** engine-vs-oracle disagreements (a complementary 4,000-case fuzz exercises
|
||||
inconsistent-premise refusal) — the soundness evidence the GSM8K composer could
|
||||
never produce. INV-25 (`tests/test_architectural_invariants.py`) ratifies that
|
||||
independence structurally.
|
||||
|
||||
**Honest caveat (state it plainly):** propositional validity is *decidable*, so 100%
|
||||
is the expected ceiling for a correct implementation. The value is not "solved
|
||||
|
|
|
|||
|
|
@ -0,0 +1,187 @@
|
|||
<!-- CANONICAL | docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md | 2026-06-04 | strategy/architecture-plan | the universal comprehension->structure->solve->verify spine, the binding-graph interlingua, and the field<->symbol coherence gate | verified: planning-only, no ADR number assigned; Phase 0 (INV-25) shipped -->
|
||||
|
||||
# Universal structure + the field↔symbol coherence gate
|
||||
|
||||
A plan for the most robust, clean, logical, and masterful path to **breaking
|
||||
reading and inputs of any modality into a logical structure** — so the engine can
|
||||
comprehend, articulate, and solve a problem in any field for which it has adequate
|
||||
packs. GSM8K (math logic) is the first proving ground; the same spine must lift
|
||||
GSM8K *and* be confirmed by independent problem-solving in other fields.
|
||||
|
||||
This document is planning-only. It assigns no ADR number, changes no serving path,
|
||||
and introduces no capability claim. It records the architecture so later, gated
|
||||
PRs can build it without re-deriving the rationale.
|
||||
|
||||
## 0. End goal
|
||||
|
||||
```text
|
||||
input (any modality)
|
||||
-> comprehended into ONE logical structure
|
||||
-> reasoned over to produce a solution AND an articulated "understanding"
|
||||
(what the problem is, the approach)
|
||||
-> verified against INDEPENDENT gold
|
||||
-> refuses when grounding is incomplete
|
||||
```
|
||||
|
||||
Success = held-out GSM8K rises **drastically** with `wrong == 0`, **and** the
|
||||
identical machinery clears an independent gold in ≥2 other fields.
|
||||
|
||||
## 1. The honest grounding (what exists today)
|
||||
|
||||
**The bottleneck is comprehension→structure, not arithmetic.** The GSM8K composer
|
||||
is epistemically *unsafe* on real data (`resolve_pooled` = 2 right / 87 wrong on
|
||||
holdout); bespoke per-shape readers do not compose. Capability is *real* only where
|
||||
the conclusion is **checkable against independent gold** — deductive propositional
|
||||
entailment (ROBDD) vs. an independent truth-table oracle: dev 200/200, holdout
|
||||
500/500, `wrong = 0`.
|
||||
|
||||
**There are several disjoint problem-structure representations:**
|
||||
|
||||
- `generate/math_problem_graph.py::MathProblemGraph` — the GSM8K candidate-graph solver IR.
|
||||
- `generate/derivation/model.py::GroundedDerivation` — the (unsafe-as-serving) derivation reader IR.
|
||||
- `generate/binding_graph/SemanticSymbolicBindingGraph` (ADR-0132/0133/0134/0135) —
|
||||
a **field-agnostic, unit-aware, provenance-carrying, acyclic, refusal-first**
|
||||
semantic-symbolic DAG. It already unifies two domains: math (`bind_math_problem_graph`)
|
||||
and proofs (`generate/proof_chain/builder.py`, ADR-0204 — "the binding graph's first consumer").
|
||||
- `generate/proof_chain` + `generate/logic_canonical.py` (ROBDD) — the deductive decision IR.
|
||||
- `generate/graph_planner.py::PropositionGraph -> ArticulationTarget` — the *articulation* IR (for saying the answer), separate from reasoning.
|
||||
|
||||
**The reasoning readers have zero field/algebra dependency.** `generate/derivation`,
|
||||
`generate/proof_chain`, `math_solver`, `math_candidate_graph` import no
|
||||
`versor_apply` / `cga_inner` / `holonomy` / `field.propagate`. The CL(4,1) field
|
||||
engine participates in the **cognition turn loop** (capture field state, ratify
|
||||
intent, recall, identity) — **not** in problem reasoning. Any claim of
|
||||
"field-as-reasoner" is therefore currently *unverified*.
|
||||
|
||||
**The dormant lever.** The reliability gate (ADR-0175) already exposes
|
||||
`checker="t2_precision"` ("widening past gold"), but it is inert: no genuinely
|
||||
structurally-distinct second derivation exists, and nothing consumes it.
|
||||
|
||||
## 2. The synthesis — field comprehends, structure bridges, symbol verifies
|
||||
|
||||
The correct architecture is not "field OR symbol." It is a precise division of
|
||||
labor with a **checkable handshake**:
|
||||
|
||||
- **Field/manifold engine = comprehension & constraint-resolution master (right-mode).**
|
||||
A problem's entities/relations embed as geometric objects in CGA; solving =
|
||||
propagating constraints via `versor_apply` until the configuration is *coherent*
|
||||
(`versor_condition < 1e-6`). The converged field **is** the holistic understanding —
|
||||
apprehended as a whole, context-first, in CORE's *native* operations.
|
||||
- **Binding-graph DAG = interlingua / corpus callosum.** The typed, unit-checked,
|
||||
provenance-carrying form the field configuration is read **into and out of**: the
|
||||
inspectable, checkable commitment where holistic apprehension hands off to analysis
|
||||
and analysis hands corrections back. Not master, not mere servant.
|
||||
- **Symbolic servants (parser, ROBDD, solver, oracle) = analyze & dispose.** They
|
||||
verify the structure against independent gold, refute incoherence, articulate.
|
||||
They never originate truth.
|
||||
|
||||
### 2.1 Why this is correct, not a compromise
|
||||
|
||||
**The field-derivation and the symbolic-derivation are two structurally-distinct
|
||||
canonical decodings of the same problem. Their *agreement* is the `wrong = 0` gate.**
|
||||
|
||||
1. **It operationalizes the deepest axiom — "Truth is coherent."** Two independent
|
||||
canonical decodings (geometric field + algebraic ROBDD) agreeing is coherence
|
||||
across vantage points. Agreement → admit; disagreement → **refuse**. This is
|
||||
exactly McGilchrist's "right apprehends, left analyzes, right re-integrates."
|
||||
2. **It is the genuine second derivation that is currently missing.** The Tier-2
|
||||
spine and `t2_precision` lever are inert because solver-vs-verifier shares
|
||||
structure (decoration) and the two GSM8K readers never co-fire. **Field ⟂ symbol
|
||||
is that second derivation.** Activating the field as a reasoner is *what unblocks
|
||||
the dormant capability lever* — mechanism, not metaphor.
|
||||
3. **It makes the field earn its role checkably (conforms to `wrong = 0` / no
|
||||
decoration).** The field is load-bearing *only where its answer agrees with an
|
||||
independent symbolic/gold derivation*. It can never serve an unagreed answer —
|
||||
disagreement refuses. This is INV-25 (Phase 0) generalized.
|
||||
|
||||
### 2.2 Conformance to the governing axes
|
||||
|
||||
| Axis | Conformance |
|
||||
|---|---|
|
||||
| Philosophical ("decoding, not generating") | Field & symbol are two canonical decodings of a reality that already is; agreement = it tracks the canonical form. |
|
||||
| Axiomatic | Reasoning *is* `versor_apply` + `cga_inner` + `versor_condition` (the actual primitives); exact recall stays exact. |
|
||||
| Ethical / `wrong = 0` | The field never serves an unagreed answer; refusal is the correction surface. |
|
||||
| Mechanical sympathy | Field does vectorized geometric propagation (native strength, Rust-parity-ready); symbol does discrete checks. |
|
||||
| Logical per "intelligence" | Holistic grasp + analytic check + refuse-on-incoherence is what integrated understanding *is*, with the non-negotiable twist that both modes must cohere or it declines. |
|
||||
|
||||
## 3. The earning path (the field must *prove* it reasons)
|
||||
|
||||
Today the readers have zero field dependency, so field-as-reasoner is a research arc
|
||||
that earns its role on the **safest checkable micro-domain first**. A negative
|
||||
result is an acceptable, honest outcome: where the field cannot earn agreement, it
|
||||
**stays a servant** and the symbolic path carries that domain, refusing where it
|
||||
cannot verify. **No unfalsifiable "the field knows" claim ever enters the codebase.**
|
||||
|
||||
**The wedge (Phase 1.5):** *Can the field decide propositional entailment
|
||||
geometrically and agree with the ROBDD oracle on held-out, `wrong = 0`?* Logic is
|
||||
the ideal first test — the ROBDD + independent oracle already give a rock-solid gold
|
||||
(500/500). Embed atoms/clauses as geometric objects; decide entailment by
|
||||
incidence/coherence; require `field_verdict == ROBDD_verdict == oracle` on a
|
||||
held-out set. Agree → the field has earned a reasoning role and we have our first
|
||||
genuine second derivation. Cannot → we learned it cheaply and honestly.
|
||||
|
||||
## 4. Phased plan
|
||||
|
||||
- **Phase 0 — independent-gold discipline. ✅ SHIPPED.** INV-25
|
||||
(`tests/test_architectural_invariants.py`): no capability claim without an
|
||||
independent gold sharing no code with the SUT; deductive lane SHA-pinned
|
||||
(`deductive_logic_v1`). The foundation every later phase rides on.
|
||||
- **Phase 1 — canonize the universal structure.** Promote
|
||||
`SemanticSymbolicBindingGraph` to *the* documented problem-structure interlingua;
|
||||
resolve its closed-vocab placeholder (`semantic_role="unknown"`) only when a
|
||||
load-bearing consumer defines it. Add a **hemisphere-role invariant**: servant
|
||||
modules (parsers, metrics, vault) may not bypass the structure's consistency
|
||||
checks. (The taxonomy is a proposal to validate before the enforcing INV lands.)
|
||||
- **Phase 1.5 — the keystone wedge.** Field-decides-entailment vs. ROBDD oracle on
|
||||
the deductive lane. Prove (or honestly refute) field-as-reasoner on the safest
|
||||
gold. Gate to everything geometric.
|
||||
- **Phase 2 — comprehension compiler → binding graph** (finite-entity grounding
|
||||
first), with **field ⟂ symbol agreement** as the admission gate from the moment
|
||||
Phase 1.5 succeeds.
|
||||
- **Phase 3 — activate `t2_precision`.** The field⟂symbol agreement *is* the t2
|
||||
signal; wire the propose-loop consuming `checker="t2_precision"`. No invented
|
||||
second derivation needed — it is real now.
|
||||
- **Phase 4 — GSM8K on the universal structure** (the drastic-lift phase), gated by
|
||||
field⟂symbol agreement + independent gold + held-out/sealed validation (never
|
||||
train_sample — the overfit firewall). Safe by construction.
|
||||
- **Phase 5 — cross-domain confirmation.** Systems/software arena (execution = a
|
||||
third independent decoding; ADR-0199's first non-math arena), then a second
|
||||
non-executable field with a proof-checker gold. The generalization proof.
|
||||
- **Phase 6 — multimodal grounding.** Connect the sensorium modality compilers
|
||||
(`sensorium/compiler` `CompilerLike`/`CompilationUnitLike`) → binding graph. A
|
||||
modality becomes "just another reader" grounding into the universal structure;
|
||||
stays afferent/gated per ADR-0198.
|
||||
|
||||
### Cross-cutting (every phase) — checkable budgets, adjoints, phenomenology
|
||||
|
||||
- **Distortion budgets as first-class CI gates**, but *only checkable ones*:
|
||||
grounding completeness %, unit-proof coverage, acyclicity, and **structural
|
||||
perturbation stability** (paraphrase/reorder the input → the binding graph and
|
||||
answer are invariant, or it refuses). Regressions gate the build as hard as
|
||||
accuracy. This is the antidote to metric-capture (the train_sample trap).
|
||||
- **Adjoint-per-operator.** Every new transform ships with its verifier/correction
|
||||
pass + a test that it reduces a *structural* error, not just a string.
|
||||
- **Phenomenology harness.** Sample full structured articulations (the
|
||||
"understanding": problem restatement + approach) for periodic trusted review;
|
||||
qualitative depth as an explicit but *subordinate* signal (never a new truth
|
||||
criterion — that would re-open left-mode capture under a different name).
|
||||
|
||||
## 5. Risks & honest tensions
|
||||
|
||||
- **HIGH — Phase 4 `wrong = 0`.** GSM8K serving breached it before. Mitigation:
|
||||
agreement gate + independent gold + held-out/sealed + pre-push verification
|
||||
(auto-merge pipeline).
|
||||
- **MEDIUM — field-reasoning may not pan out** in a given domain. Expected and
|
||||
acceptable: it stays a servant there; the symbolic path carries it, refusing where
|
||||
unverifiable.
|
||||
- **MEDIUM — McGilchrist over-reach.** "Field as master of reasoning" is realized
|
||||
only through the *checkable* agreement gate; never asserted as unfalsifiable fact.
|
||||
- **MEDIUM — IR convergence cost.** Converge the disjoint reasoning IRs incrementally
|
||||
(adapters first, direct targeting later), never a big-bang rewrite.
|
||||
|
||||
## 6. What this supersedes
|
||||
|
||||
The earlier 554/555/556 sequence is reframed: 554 (Tier-2 verifier) was inert →
|
||||
Phase 3 done *right* (field⟂symbol is the genuine second derivation); 555
|
||||
(target-slot composition) was unsafe via the composer → Phase 4 (comprehension on
|
||||
the universal structure, gated); 556 (systems/software arena) → Phase 5.
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
<!-- CANONICAL | evals/deductive_logic/contract.md | 2026-06-04 | deductive-logic lane | what CORE's propositional entailment operator decides, and its honesty boundary | verified: holdout 500/500 correct wrong=0, 8000-case engine-vs-oracle fuzz 0 disagreements -->
|
||||
<!-- CANONICAL | evals/deductive_logic/contract.md | 2026-06-04 | deductive-logic lane | what CORE's propositional entailment operator decides, and its honesty boundary | verified: holdout 500/500 correct wrong=0, deterministic 3,000-case engine-vs-oracle fuzz (2,796 definite) 0 disagreements -->
|
||||
|
||||
# deductive-logic eval lane (ADR-0206)
|
||||
|
||||
|
|
@ -27,8 +27,14 @@ make stochastic.
|
|||
|---|---:|---:|---:|---:|---:|
|
||||
| dev | 200 | 200 | **0** | **0** | 74 |
|
||||
| **holdout v1** | 500 | **500** | **0** | **0** | **227** (117 entailed + 110 refuted) |
|
||||
| external mirror v1 | 16 | **16** | **0** | **0** | 12 |
|
||||
| fuzz (fresh random, engine vs oracle) | 7,340 | 7,340 | **0** | **0** | 3,360 |
|
||||
| external (hand-authored, illustrative) v1 | 16 | **16** | **0** | **0** | 12 |
|
||||
| fuzz (seed 424242, engine vs oracle) | 2,796 | 2,796 | **0** | **0** | 1,241 |
|
||||
|
||||
(The fuzz row is the deterministic `test_engine_matches_independent_oracle_fuzz`
|
||||
gate: 3,000 random formulas, 2,796 of them in-regime/definite, **0**
|
||||
engine-vs-oracle disagreements; a complementary 4,000-case fuzz exercises
|
||||
inconsistent-premise refusal. The property holds far more broadly than the
|
||||
committed gate — these are the numbers CI actually pins, not a headline count.)
|
||||
|
||||
**100% correct with `wrong = 0` and `refused = 0` on committed in-regime
|
||||
cases**, and the correct answers include hundreds of non-trivial multi-hop
|
||||
|
|
@ -39,8 +45,9 @@ entailments and refutations — not just `unknown` pass-throughs.
|
|||
The gold is **not** computed by the engine under test. It comes from an *independent*
|
||||
truth-table decision procedure (`oracle.py`): a separate parser + brute-force model
|
||||
enumeration over all 2^k assignments, sharing **no code** with the ROBDD engine. Two
|
||||
independently-coded sound procedures agreeing on **8,000** fresh random problems with
|
||||
**zero disagreements** is real soundness evidence — exactly the property the GSM8K
|
||||
independently-coded sound procedures agreeing on every committed case plus a
|
||||
deterministic 3,000-case fuzz (2,796 definite, **zero disagreements**) is real
|
||||
soundness evidence — exactly the property the GSM8K
|
||||
composer could never establish (it could not tell its 2 right answers from its 87
|
||||
wrong ones). A single engine/oracle disagreement fails the test suite. A refusal
|
||||
on a committed in-regime case is also a lane failure; refusal-boundary cases are
|
||||
|
|
@ -89,6 +96,6 @@ evals/deductive_logic/
|
|||
runner.py # engine vs gold; correct/wrong/refused + class breakdown
|
||||
dev/cases.jsonl # seed 20260604, 200 cases
|
||||
holdout/v1/cases.jsonl # seed 70260604, 500 cases (disjoint)
|
||||
external/v1/cases.jsonl # frozen finite-entity/proposition mirror cases
|
||||
external/v1/cases.jsonl # frozen hand-authored propositional cases (illustrative; NOT a published-benchmark mirror)
|
||||
refusal/v1/cases.jsonl # refusal-boundary cases, tested separately
|
||||
```
|
||||
|
|
|
|||
73
evals/deductive_logic/report.json
Normal file
73
evals/deductive_logic/report.json
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
{
|
||||
"adr": "ADR-0206",
|
||||
"aggregate": {
|
||||
"correct": 716,
|
||||
"n": 716,
|
||||
"refused": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
"all_correct": true,
|
||||
"lane": "deductive_logic",
|
||||
"refused_is_zero": true,
|
||||
"schema_version": 1,
|
||||
"splits": {
|
||||
"dev": {
|
||||
"all_cases_correct": true,
|
||||
"by_gold": {
|
||||
"entailed": 37,
|
||||
"refuted": 37,
|
||||
"unknown": 126
|
||||
},
|
||||
"correct_by_gold": {
|
||||
"entailed": 37,
|
||||
"refuted": 37,
|
||||
"unknown": 126
|
||||
},
|
||||
"counts": {
|
||||
"correct": 200,
|
||||
"refused": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
"n": 200
|
||||
},
|
||||
"external_v1": {
|
||||
"all_cases_correct": true,
|
||||
"by_gold": {
|
||||
"entailed": 8,
|
||||
"refuted": 4,
|
||||
"unknown": 4
|
||||
},
|
||||
"correct_by_gold": {
|
||||
"entailed": 8,
|
||||
"refuted": 4,
|
||||
"unknown": 4
|
||||
},
|
||||
"counts": {
|
||||
"correct": 16,
|
||||
"refused": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
"n": 16
|
||||
},
|
||||
"holdout_v1": {
|
||||
"all_cases_correct": true,
|
||||
"by_gold": {
|
||||
"entailed": 117,
|
||||
"refuted": 110,
|
||||
"unknown": 273
|
||||
},
|
||||
"correct_by_gold": {
|
||||
"entailed": 117,
|
||||
"refuted": 110,
|
||||
"unknown": 273
|
||||
},
|
||||
"counts": {
|
||||
"correct": 500,
|
||||
"refused": 0,
|
||||
"wrong": 0
|
||||
},
|
||||
"n": 500
|
||||
}
|
||||
},
|
||||
"wrong_is_zero": true
|
||||
}
|
||||
|
|
@ -22,6 +22,7 @@ cases live in unit tests, not in these dev/holdout formula splits.
|
|||
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import json
|
||||
import sys
|
||||
from collections import Counter
|
||||
|
|
@ -31,6 +32,14 @@ from generate.proof_chain.entail import Entailment, evaluate_entailment
|
|||
|
||||
_ROOT = Path(__file__).resolve().parent
|
||||
|
||||
# The committed splits this lane scores (refusal-boundary cases live in unit
|
||||
# tests, not here). Order is fixed for deterministic report bytes.
|
||||
_SPLITS: tuple[tuple[str, Path], ...] = (
|
||||
("dev", _ROOT / "dev" / "cases.jsonl"),
|
||||
("holdout_v1", _ROOT / "holdout" / "v1" / "cases.jsonl"),
|
||||
("external_v1", _ROOT / "external" / "v1" / "cases.jsonl"),
|
||||
)
|
||||
|
||||
|
||||
def _load(path: Path) -> list[dict]:
|
||||
with path.open(encoding="utf-8") as fh:
|
||||
|
|
@ -103,7 +112,72 @@ def _run(name: str, path: Path) -> dict:
|
|||
return report
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
def build_combined_report() -> dict:
|
||||
"""Deterministic per-split + aggregate report over the committed splits.
|
||||
|
||||
Pure over the committed ``cases.jsonl`` files: same inputs → byte-identical
|
||||
JSON (no examples lists, no timestamps), so it is safe to SHA-pin
|
||||
(``scripts/verify_lane_shas.py``). The human-facing ``_run`` stdout view
|
||||
keeps the example breakdowns; the pinned artifact carries only the counts
|
||||
that constitute the capability claim.
|
||||
"""
|
||||
splits: dict[str, dict] = {}
|
||||
aggregate = {"n": 0, "correct": 0, "wrong": 0, "refused": 0}
|
||||
for name, path in _SPLITS:
|
||||
report = build_report(_load(path))
|
||||
splits[name] = {
|
||||
"n": report["n"],
|
||||
"counts": report["counts"],
|
||||
"by_gold": report["by_gold"],
|
||||
"correct_by_gold": report["correct_by_gold"],
|
||||
"all_cases_correct": report["all_cases_correct"],
|
||||
}
|
||||
aggregate["n"] += report["n"]
|
||||
for key in ("correct", "wrong", "refused"):
|
||||
aggregate[key] += report["counts"][key]
|
||||
return {
|
||||
"schema_version": 1,
|
||||
"lane": "deductive_logic",
|
||||
"adr": "ADR-0206",
|
||||
"splits": splits,
|
||||
"aggregate": aggregate,
|
||||
"wrong_is_zero": aggregate["wrong"] == 0,
|
||||
"refused_is_zero": aggregate["refused"] == 0,
|
||||
"all_correct": all(s["all_cases_correct"] for s in splits.values()),
|
||||
}
|
||||
|
||||
|
||||
def write_combined_report(path: Path) -> dict:
|
||||
report = build_combined_report()
|
||||
path.write_text(
|
||||
json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8"
|
||||
)
|
||||
return report
|
||||
|
||||
|
||||
def main(argv: list[str] | None = None) -> int:
|
||||
parser = argparse.ArgumentParser(description=__doc__)
|
||||
parser.add_argument(
|
||||
"--report",
|
||||
type=Path,
|
||||
default=None,
|
||||
help=(
|
||||
"write the deterministic combined JSON report to this path "
|
||||
"(used by scripts/verify_lane_shas.py); default prints the "
|
||||
"human-facing per-split breakdown to stdout"
|
||||
),
|
||||
)
|
||||
args = parser.parse_args(argv)
|
||||
|
||||
if args.report is not None:
|
||||
report = write_combined_report(args.report)
|
||||
gate_ok = (
|
||||
report["wrong_is_zero"]
|
||||
and report["refused_is_zero"]
|
||||
and report["all_correct"]
|
||||
)
|
||||
return 0 if gate_ok else 1
|
||||
|
||||
reports = {
|
||||
"dev": _run("dev", _ROOT / "dev" / "cases.jsonl"),
|
||||
"holdout-v1": _run("holdout-v1", _ROOT / "holdout" / "v1" / "cases.jsonl"),
|
||||
|
|
@ -112,4 +186,8 @@ if __name__ == "__main__":
|
|||
total_wrong = sum(r["counts"]["wrong"] for r in reports.values())
|
||||
total_refused = sum(r["counts"]["refused"] for r in reports.values())
|
||||
all_correct = all(r["all_cases_correct"] for r in reports.values())
|
||||
sys.exit(0 if total_wrong == 0 and total_refused == 0 and all_correct else 1)
|
||||
return 0 if total_wrong == 0 and total_refused == 0 and all_correct else 1
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
|
|
|
|||
|
|
@ -70,6 +70,10 @@ _LANE_ADR: dict[str, tuple[str, str]] = {
|
|||
"ADR-0131",
|
||||
"Math teaching corpus replays deterministically; all chains pass exit criterion (correct_rate=1.0, wrong=0)",
|
||||
),
|
||||
"deductive_logic_v1": (
|
||||
"ADR-0206",
|
||||
"Propositional entailment scored against an independent truth-table oracle; dev+holdout+external 716/716 correct, wrong=0, refused=0",
|
||||
),
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -41,6 +41,7 @@ PINNED_SHAS: dict[str, str] = {
|
|||
"demo_composition": "3a3d09f3a87462737e615c2dd3481b9e13e5ff8fadee0043c37873494ded556d",
|
||||
"public_demo": "e323adb35ea17987991395424c603ff93bca08c11bc2713bd9f6338e86bb269f",
|
||||
"math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4",
|
||||
"deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f",
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -51,11 +52,20 @@ class LaneSpec:
|
|||
report_relative: str
|
||||
accepts_report_flag: bool = True
|
||||
extra_args: tuple[str, ...] = field(default_factory=tuple)
|
||||
# Run via ``python -m pkg.mod`` instead of ``python path/to/runner.py``.
|
||||
# Required when the runner's own directory holds a module that would shadow
|
||||
# an absolute import in script mode — e.g. the deductive lane's local
|
||||
# ``generate.py`` shadows the ``generate`` package when run as a script.
|
||||
run_as_module: bool = False
|
||||
|
||||
@property
|
||||
def runner_path(self) -> Path:
|
||||
return REPO_ROOT / self.runner_module
|
||||
|
||||
@property
|
||||
def runner_dotted(self) -> str:
|
||||
return self.runner_module.removesuffix(".py").replace("/", ".")
|
||||
|
||||
@property
|
||||
def canonical_report(self) -> Path:
|
||||
return REPO_ROOT / self.report_relative
|
||||
|
|
@ -105,6 +115,12 @@ LANE_SPECS: tuple[LaneSpec, ...] = (
|
|||
report_relative="evals/math_teaching_corpus/v1/report.json",
|
||||
accepts_report_flag=False,
|
||||
),
|
||||
LaneSpec(
|
||||
lane_id="deductive_logic_v1",
|
||||
runner_module="evals/deductive_logic/runner.py",
|
||||
report_relative="evals/deductive_logic/report.json",
|
||||
run_as_module=True,
|
||||
),
|
||||
)
|
||||
|
||||
|
||||
|
|
@ -112,7 +128,10 @@ def _invoke_runner(spec: LaneSpec, *, target_path: Path | None = None) -> Path:
|
|||
import os
|
||||
|
||||
env = {"PYTHONPATH": str(REPO_ROOT), **os.environ}
|
||||
args: list[str] = [sys.executable, str(spec.runner_path)]
|
||||
if spec.run_as_module:
|
||||
args = [sys.executable, "-m", spec.runner_dotted]
|
||||
else:
|
||||
args = [sys.executable, str(spec.runner_path)]
|
||||
if target_path is not None and spec.accepts_report_flag:
|
||||
args.extend(["--report", str(target_path)])
|
||||
args.extend(spec.extra_args)
|
||||
|
|
|
|||
|
|
@ -1032,3 +1032,213 @@ class TestINV24VaultRecallRegistry:
|
|||
f"Registered recall site(s) no longer call vault.recall(): "
|
||||
f"{sorted(unused)}\nRemove from VAULT_RECALL_SITES."
|
||||
)
|
||||
|
||||
|
||||
# ===========================================================================
|
||||
# INV-25 Independent gold — a promotable-capability lane scores against an
|
||||
# oracle that shares NO code with the system under test (SUT)
|
||||
# ===========================================================================
|
||||
#
|
||||
# Claim (the GSM8K post-mortem made structural, docs/analysis/
|
||||
# pivot-to-deductive-logic-2026-06-04.md §"the GSM8K lesson"):
|
||||
#
|
||||
# No capability claim is valid unless the gold it is measured against is
|
||||
# computed by a procedure INDEPENDENT of the engine that produced the
|
||||
# answer. A "gold" that shares code with the engine only proves the engine
|
||||
# agrees with itself — exactly the blind spot that let the GSM8K composer
|
||||
# serve 87 wrong held-out answers it could not tell from its 2 right ones.
|
||||
#
|
||||
# The deductive-logic lane is the first lane to earn a real correct number
|
||||
# (holdout 500/500, wrong=0), and it earns it honestly because its gold is an
|
||||
# independent truth-table oracle (evals/deductive_logic/oracle.py): a separate
|
||||
# tokenizer + recursive-descent parser + brute-force 2^k model enumeration
|
||||
# that imports NONE of the ROBDD engine under test. This invariant ratifies
|
||||
# that independence as a structural, meaningfully-failing property:
|
||||
#
|
||||
# 25a (structural). Each registered oracle module imports none of its SUT's
|
||||
# modules. Fails the moment an oracle is "simplified" to reuse the
|
||||
# engine — the single change that would turn independent gold into
|
||||
# self-agreement.
|
||||
# 25b (behavioral). Every committed deductive case's gold is reproduced by
|
||||
# the independent oracle AND matched by the engine: engine == oracle ==
|
||||
# committed gold. This is the anti-overfit firewall — it fails if any
|
||||
# committed gold were ever engine-derived and diverged from the oracle.
|
||||
# 25c (non-vacuity). An unsound engine (entailed<->refuted flipped) is shown
|
||||
# to disagree with the oracle on committed cases, proving 25b can fail.
|
||||
#
|
||||
# A new lane that claims a promotable/checkable capability MUST register its
|
||||
# (oracle, SUT) pair here. The CI failure is the prompt to do so.
|
||||
|
||||
from typing import NamedTuple
|
||||
|
||||
_REPO_ROOT = PROJECT_ROOT_FOR_INV21
|
||||
|
||||
|
||||
class IndependentGoldLane(NamedTuple):
|
||||
"""A lane whose gold must be independent of its system under test."""
|
||||
|
||||
name: str
|
||||
oracle_module: str # path relative to repo root
|
||||
sut_import_prefixes: tuple[str, ...] # modules the oracle MUST NOT import
|
||||
|
||||
|
||||
# The engine under test for the deductive lane is generate.proof_chain.entail,
|
||||
# built on the generate.logic_canonical ROBDD stack. The oracle must share no
|
||||
# code with any of it (it is a stdlib-only truth-table procedure today).
|
||||
INDEPENDENT_GOLD_LANES: tuple[IndependentGoldLane, ...] = (
|
||||
IndependentGoldLane(
|
||||
name="deductive_logic",
|
||||
oracle_module="evals/deductive_logic/oracle.py",
|
||||
sut_import_prefixes=(
|
||||
"generate.proof_chain",
|
||||
"generate.logic_canonical",
|
||||
"generate.logic_equivalence",
|
||||
),
|
||||
),
|
||||
)
|
||||
|
||||
_DEDUCTIVE_CASE_FILES: tuple[str, ...] = (
|
||||
"evals/deductive_logic/dev/cases.jsonl",
|
||||
"evals/deductive_logic/holdout/v1/cases.jsonl",
|
||||
"evals/deductive_logic/external/v1/cases.jsonl",
|
||||
)
|
||||
|
||||
|
||||
def _module_imports(path: Path) -> set[str]:
|
||||
"""Every absolute module name imported by ``path``.
|
||||
|
||||
Uses AST so a forbidden module mentioned only in a docstring/comment/string
|
||||
cannot trigger a false positive, and a real ``import generate.proof_chain``
|
||||
cannot hide from a substring grep.
|
||||
"""
|
||||
try:
|
||||
tree = ast.parse(path.read_text())
|
||||
except (OSError, SyntaxError):
|
||||
return set()
|
||||
mods: set[str] = set()
|
||||
for node in ast.walk(tree):
|
||||
if isinstance(node, ast.Import):
|
||||
for alias in node.names:
|
||||
mods.add(alias.name)
|
||||
elif isinstance(node, ast.ImportFrom):
|
||||
# Absolute imports only (level == 0); a relative import cannot reach
|
||||
# the SUT package from the evals oracle.
|
||||
if node.module and node.level == 0:
|
||||
mods.add(node.module)
|
||||
return mods
|
||||
|
||||
|
||||
def _imports_any_prefix(mods: set[str], prefixes: tuple[str, ...]) -> list[str]:
|
||||
hits: list[str] = []
|
||||
for mod in sorted(mods):
|
||||
for prefix in prefixes:
|
||||
if mod == prefix or mod.startswith(prefix + "."):
|
||||
hits.append(mod)
|
||||
break
|
||||
return hits
|
||||
|
||||
|
||||
def _load_deductive_cases() -> list[dict[str, Any]]:
|
||||
cases: list[dict[str, Any]] = []
|
||||
for rel in _DEDUCTIVE_CASE_FILES:
|
||||
path = _REPO_ROOT / rel
|
||||
for line in path.read_text(encoding="utf-8").splitlines():
|
||||
if line.strip():
|
||||
cases.append(json.loads(line))
|
||||
return cases
|
||||
|
||||
|
||||
class TestINV25IndependentGold:
|
||||
"""A promotable-capability lane's gold must share no code with its SUT,
|
||||
and its committed gold must be reproducible by that independent oracle."""
|
||||
|
||||
def test_registered_oracle_modules_exist(self):
|
||||
"""Drift guard: a registered oracle path that no longer exists means
|
||||
the registry is stale and the structural check below is vacuous."""
|
||||
missing = [
|
||||
lane.oracle_module
|
||||
for lane in INDEPENDENT_GOLD_LANES
|
||||
if not (_REPO_ROOT / lane.oracle_module).is_file()
|
||||
]
|
||||
assert not missing, (
|
||||
"Registered independent-gold oracle module(s) not found: "
|
||||
f"{missing}\nUpdate INDEPENDENT_GOLD_LANES in "
|
||||
"tests/test_architectural_invariants.py."
|
||||
)
|
||||
|
||||
def test_oracle_shares_no_code_with_sut(self):
|
||||
"""25a — the load-bearing structural guarantee. If any registered
|
||||
oracle imports a module of the engine it is supposed to check
|
||||
independently, the gold is not independent and this fails."""
|
||||
offenders: list[str] = []
|
||||
for lane in INDEPENDENT_GOLD_LANES:
|
||||
mods = _module_imports(_REPO_ROOT / lane.oracle_module)
|
||||
hits = _imports_any_prefix(mods, lane.sut_import_prefixes)
|
||||
if hits:
|
||||
offenders.append(f"{lane.oracle_module} imports SUT module(s) {hits}")
|
||||
assert not offenders, (
|
||||
"Independent-gold oracle shares code with its system under test:\n "
|
||||
+ "\n ".join(offenders)
|
||||
+ "\n\nThe oracle must be an independent decision procedure (a 'gold' "
|
||||
"that imports the engine only proves the engine agrees with itself — "
|
||||
"the GSM8K blind spot, INV-25). Re-implement the check independently, "
|
||||
"or — if this import is genuinely unrelated to the decision — narrow "
|
||||
"sut_import_prefixes in INDEPENDENT_GOLD_LANES with a justification."
|
||||
)
|
||||
|
||||
def test_committed_gold_is_independently_reproducible(self):
|
||||
"""25b — engine == oracle == committed gold on every committed case.
|
||||
Reproducing the committed gold with the *independent* oracle is the
|
||||
anti-overfit firewall: it fails if any gold were engine-derived and
|
||||
diverged, or if the engine ever confabulated a verdict."""
|
||||
from evals.deductive_logic.oracle import oracle_entailment
|
||||
from generate.proof_chain.entail import evaluate_entailment
|
||||
|
||||
cases = _load_deductive_cases()
|
||||
assert cases, "no committed deductive cases found — INV-25b would be vacuous"
|
||||
|
||||
oracle_mismatch: list[str] = []
|
||||
engine_mismatch: list[str] = []
|
||||
for case in cases:
|
||||
premises = tuple(case["premises"])
|
||||
query = case["query"]
|
||||
gold = case["gold"]
|
||||
if oracle_entailment(premises, query) != gold:
|
||||
oracle_mismatch.append(case["id"])
|
||||
if evaluate_entailment(premises, query).outcome.value != gold:
|
||||
engine_mismatch.append(case["id"])
|
||||
|
||||
assert not oracle_mismatch, (
|
||||
"Committed gold is NOT reproduced by the independent oracle "
|
||||
f"(first few: {oracle_mismatch[:5]}). The gold may be engine-derived "
|
||||
"or the case file drifted — regenerate gold from the oracle."
|
||||
)
|
||||
assert not engine_mismatch, (
|
||||
"Engine disagrees with committed independent gold "
|
||||
f"(first few: {engine_mismatch[:5]}). This is a wrong==0 breach on a "
|
||||
"lane that claims a promotable capability."
|
||||
)
|
||||
|
||||
def test_differential_is_non_vacuous(self):
|
||||
"""25c — proves 25b can fail. An unsound engine (entailed<->refuted
|
||||
flipped) MUST disagree with the independent oracle on committed cases;
|
||||
if it did not, 25b would be decoration (CLAUDE.md schema-defined proof
|
||||
obligations)."""
|
||||
from evals.deductive_logic.oracle import oracle_entailment
|
||||
|
||||
flip = {"entailed": "refuted", "refuted": "entailed"}
|
||||
cases = _load_deductive_cases()
|
||||
disagreements = 0
|
||||
for case in cases:
|
||||
premises = tuple(case["premises"])
|
||||
query = case["query"]
|
||||
gold = oracle_entailment(premises, query)
|
||||
unsound = flip.get(gold, gold)
|
||||
if unsound != gold:
|
||||
disagreements += 1
|
||||
assert disagreements > 0, (
|
||||
"A deliberately unsound (entailed<->refuted) engine disagreed with "
|
||||
"the oracle on ZERO committed cases — the committed set has no "
|
||||
"entailed/refuted signal, so INV-25b cannot catch a soundness break. "
|
||||
"Add non-trivial cases before claiming the lane proves capability."
|
||||
)
|
||||
|
|
|
|||
|
|
@ -91,6 +91,7 @@ class TestExpectedLaneCoverage:
|
|||
"public_demo", # ADR-0099
|
||||
"curriculum_loop_closure",
|
||||
"math_teaching_corpus_v1", # ADR-0131
|
||||
"deductive_logic_v1", # ADR-0206 — independent-oracle entailment lane
|
||||
}
|
||||
)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue