core-labs/core
core-labs/core
1
0
Fork 0
Code Issues 1 Pull requests 1 Projects Releases Packages Wiki Activity
core/docs/analysis/VERIFIED-canonical-comparison-scoping-2026-06-06.md
Shay c5f0c90738 feat(derivation): math-serving reach seam — select_self_verified is policy-aware (ADR-0206 §5) 
Completes the ADR-0206 §5 math-serving deferral in its own careful PR. The GSM8K
wrong=0 serving gate, select_self_verified, now takes a ReachPolicy. This changes
NO serving behavior today — it is the safe, byte-identical, sanctioned first edit to
the most wrong=0-critical line, with a live-wiring test, so a future VERIFIED
widening has a precise, proven integration point.

Why it can't actually widen yet (the tension scoping surfaced): GSM8K wrong=0 is
ABSOLUTE (zero wrong, ever); a reliability license is STATISTICAL (a 0.99 Wilson
floor); math answers aren't disclosed like the cognition path (E). So widening the
math serve on a statistical license would eventually serve a SILENT wrong. ADR-0206
§4 foresaw this: VERIFIED is "the only state that will license widening past gold,"
and it is reserved pending a canonical-comparison pass (the soundness≠correctness
gap) that is unbuilt.

Design (safe by construction):
- select_self_verified(..., policy=STRICT_POLICY). STRICT (the default every one of
  the 5 callers passes) is the prior logic verbatim — unique answer → Resolution;
  zero-verify or disagreement → refuse. Byte-identical: the pinned serving-lane SHAs
  (demo_composition 3a3d09f3, fabrication 01e1b6b7, math_teaching_corpus eaf160d1)
  are unchanged; Resolution is unchanged; no import cycle.
- A wider reach resolves a disagreement ONLY via _canonically_verified — the VERIFIED
  gate — whose body returns None (capability unbuilt). So the widening is
  STRUCTURALLY inert: a disagreement refuses regardless of policy. wrong=0 holds by
  construction, not caller discipline. A statistical reliability license is NOT
  consulted by the math path (the cognition/math asymmetry is deliberate: cognition
  discloses, math is absolute).
- test_seam_is_live_wiring injects the gate to prove the consumer fires under a wider
  reach — and STRICT still refuses even then.

Verified: smoke (90), invariants (56), governance + selfverify + ms2 (354 incl. the
new seam tests), GSM8K serving regression byte-identical (the one red,
test_serving_unchanged_by_search expecting stale 6/44, fails identically on clean
main — a pre-existing stale artifact, not this change). Three-lens adversarial review
(byte-identity/seal, structural wrong=0 inertness, no-overclaim): all held.

The real unlock — a VERIFIED canonical-comparison producer — is scoped in
docs/analysis/VERIFIED-canonical-comparison-scoping-2026-06-06.md (recommended:
back-substitution / constraint-satisfaction on a checkable problem class). Still
deferred: SITUATE (stakes), the live FEED-BACK loop, reach_level JSONL emission.
2026-06-06 15:46:14 -07:00

4.2 KiB
Raw Blame History

Scoping: the VERIFIED canonical-comparison producer (the real math-serving unlock)

Date: 2026-06-06 · Status: scoping (no code) · Unblocks: the ADR-0206 §5 math-serving widening (the seam is built + inert; this is the gate it waits on).

The gap

select_self_verified proves soundness — grounding ∧ cue ∧ unit ∧ uniqueness — and refuses on disagreement. It does not prove correctness: that the committed value is the right answer to the question. Serving has no gold, so correctness can't be checked by comparison to an answer key. EpistemicState.VERIFIED is reserved precisely for the capability that closes this gap, and it is "the only state that will license widening past gold" (ADR-0206 §4). Until a producer exists, the math seam stays inert and the absolute wrong == 0 is safe.

Why a statistical license can't substitute

A reliability license (Step E) is a Wilson lower bound — it permits the cognition path to serve a disclosed estimate. Math answers aren't disclosed; a licensed-but-wrong math serve is a silent wrong. The absolute invariant needs absolute evidence, not a 0.99 bound. So VERIFIED must be a proof of correctness, not a confidence score.

Candidate mechanisms (in order of promise)

  1. Back-substitution / constraint satisfaction (recommended first target). For a problem reducible to a constraint system over its stated quantities, plug the candidate answer back in and verify it satisfies every constraint. This is a genuine correctness check without gold — it decides truth against the problem's own structure ("decode a reality that already is", the canonical-form thesis). Well-posed for a constraint-bearing subset (e.g., "x of the N are red, the rest blue; how many blue?" → answer must satisfy red+blue=N). The binding constraint is the same comprehension wall (word → constraint system), so scope it to shapes the reader already extracts cleanly.
  2. Independent canonical re-derivation. Stronger than today's disagreement rule: require K structurally disjoint derivations to converge on the same canonical normal form. Caveat — convergence is still evidential, not a proof; this raises confidence but does not by itself justify VERIFIED for an absolute invariant. Use only as a necessary pre-filter, never the sole gate.
  3. Reuse a domain where correctness is decidable. Deductive logic already produces proven-correct answers (the sound+complete ROBDD — project-deductive-logic-flagship). That is the existence proof that VERIFIED is real; but it flows through the logic path, not select_self_verified. A bridge would let logic-checkable arithmetic sub-claims earn VERIFIED.

Recommended arc (each its own PR, wrong=0-gated)

  1. Contract. Define VERIFIED's canonical-comparison obligation: a predicate that, given a candidate Resolution + the problem, returns proven-correct / not — with a meaningful-fail test (it must reject a sound-but-wrong answer, the 20/5==4 class).
  2. Producer for ONE checkable class (back-substitution over a constraint-bearing shape). Emit EpistemicState.VERIFIED only when the back-substitution check passes.
  3. Wire _canonically_verified (the seam's gate, already built + tested) to that producer. The math seam then widens for exactly that class — and only it.
  4. Re-pin the serving-lane SHAs under the freeze (the deferred reach_level emission; ADR-0206 §5) — re-pinning a frozen gate is a deliberate, reviewed act, with the eval delta as the truth test (sealed run must show wrong=0 preserved + the new served class).
  5. Independent oracle on a holdout (INV-25 discipline): the widened class must hold wrong=0 against a separate gold lane, not just the back-substitution check.

Honest risk

The hard part is comprehension (word → constraints), not the check. So the first producer should target the narrowest shape the reader extracts reliably, proving the mechanism end-to-end (build → emit VERIFIED → seam widens → wrong=0 holds on holdout) before widening the shape coverage. This is the "checkable-conclusion domains" direction (project-self-check-soundness-not-correctness) made concrete for math serving.