docs(ADR-0167): audit-as-teaching-evidence (math reader → contemplation wire) (#349)

* docs(ADR-0167): audit-as-teaching-evidence (math reader → contemplation wire)

Scoping ADR for Brief 11D Candidate E. Routes math-reader refusal audit
rows into the existing contemplation/HITL teaching corridor as a new
candidate source (`MathReaderRefusalEvidence`).

Key decisions:
- Evidence-only — never directly admits a math fact; only ratification
  through HITL queue can change runtime behaviour
- Five sub-types proposed (Lexical / Frame / Composition / Reference /
  Slot claims) mapping to the audit taxonomy
- Scope first to LexicalClaim — lowest-risk, highest-count
- Six open questions called out for the implementation ADR

ADR-0166 three-question test passes; implementation passes only when
the six open questions are answered with LexicalClaim-first scope.

No code in this PR.

* docs(ADR-0167): parallel work plan — 6-PR/3-wave dispatch across 5 model operators
This commit is contained in:
Shay 2026-05-27 06:21:43 -07:00 committed by GitHub
parent 66ef4ad07c
commit 4f0815ef9a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 501 additions and 0 deletions

View file

@ -0,0 +1,220 @@
# ADR-0167 — Audit-as-Teaching-Evidence (Math Reader → Contemplation)
**Status:** Proposed (scoping ADR; no code in this PR)
**Date:** 2026-05-27
**Author:** Shay
**Parent thesis:** [[thesis-decoding-not-generating]]
**Parent brief:** [BRIEF-11D candidate E](./BRIEF-11D-next-capability-proposal.md)
**Related:** ADR-0150/0152/0155/0161 (HITL + contemplation), ADR-0164 (reader),
ADR-0166 (measurement-capability sequencing), ADR-0057 (teaching-chain proposal)
---
## Context
The Brief 11B audit infrastructure (`generate/comprehension/audit.py`,
`evals/gsm8k_math/train_sample/v1/audit_brief_11.json`) produces a labelled
refusal taxonomy per case: every `ReaderRefusal` is decorated with a
`missing_operator` label (`pre_frame_filler_sentence`,
`multi_quantity_composition`, `unit_binding`, `pronoun_resolution`, etc.) and a
typed `AuditRow` carrying `recognized_terms`, `skipped_frame`,
`refusal_reason`, and `refusal_detail`.
Today this evidence is **terminal**. A refusal labels the failure, the audit
artifact serialises it, the operator reads it. There is no path from a
labelled refusal back into the engine's learning loop.
CORE already has a learning loop: the contemplation/HITL teaching corridor
(ADR-0150/0152/0155/0161). Today it produces `DiscoveryCandidate`s from the
*cognition* lane via `teaching/contemplation.py`. Each candidate carries a
polarity, semantic domains, evidence, and sub-questions; ratified candidates
become `TeachingChainProposal`s (ADR-0057) that extend the active teaching
corpora.
The math reader does not feed this pipeline. Its refusals discard.
## Decision
Route math-reader audit rows into the contemplation candidates pipeline as a
new candidate source: **`MathReaderRefusalEvidence`**.
The integration is *evidence-only*: an audit row becomes a candidate the
operator may ratify into a teaching chain. The chain itself is what updates
the engine's behaviour. The audit row never directly mutates a pack, a
lexicon, the reader, or the solver.
This preserves the project thesis: the engine is not adding stored items
hoping to retrieve them; it is surfacing what it failed to find in a shape
the operator can teach against.
## Why this is not a refusal-class dispatch table
Tempting alternative: `missing_operator → specialised handler`. Reject:
1. It is library-of-handlers — the same anti-pattern regex sentence templates
represented. ADR-0164 already retired that surface.
2. Every specialised handler is a new admission path, multiplying the
`wrong=0` surface area. Brief 11 §"correct-count greed" applies.
3. Handlers ossify the taxonomy. The taxonomy should be input to operator
judgement, not branch points in production code.
The dispatch table imagines the engine *resolving* the refusal in-flight.
This ADR insists the engine *records* the refusal and lets the operator
resolve it deliberately, via the existing teaching corridor.
## Why this requires an ADR before code
Cognition teaching chains encode *semantic-domain propositions*: e.g.
"`cognition.attention.is_a.cognition.faculty`". They are structurally simple:
subject, predicate, object, polarity.
Math-domain teaching chains would have to encode something different. The
audit taxonomy ranges over five distinct *kinds* of teachable claim:
1. **Lexical** — "this surface form belongs to category X"
(`lexicon_entry`, `compound_numeric_literal`, `compound_time_literal`)
2. **Frame-classifying** — "this verb opens / does not open a frame of kind
K" (`pre_frame_filler_sentence`)
3. **Structural** — "this sentence composes N possessions/operations of
different kinds" (`multi_quantity_composition`)
4. **Reference-resolving** — "this pronoun in this context refers to entity
E" (`pronoun_resolution`)
5. **Slot-completing** — "this question-target slot is filled by U"
(`question_frame_slot`, `unit_binding`)
These are not all the same shape. A single uniform `MathTeachingChain` would
either flatten them lossily, or require five sub-types. The ADR must commit
to one of:
- **5 sub-types** with explicit type tags and per-type ratification rules
- **A graph schema** (closer to `PropositionGraph`) that subsumes all five
- **A subset-first scope** (lexical only, defer the other four)
Each choice has different replay/serialisation/manifest-checksum
consequences. None can be inferred from the cognition side.
## Proposed sub-type set (provisional, for review)
If the ADR adopts the sub-types path:
| Sub-type | Maps from | Ratification primitive |
|---------------------|--------------------------------|-------------------------------------|
| `LexicalClaim` | `lexicon_entry`, compounds | Pack entry add (lemma + category) |
| `FrameClaim` | `pre_frame_filler_sentence` | Verb-category reclassification |
| `CompositionClaim` | `multi_quantity_composition` | Frame-split rule |
| `ReferenceClaim` | `pronoun_resolution` | Anaphora-resolution entry |
| `SlotClaim` | `question_frame_slot`, `unit_binding` | Slot-completion table entry |
`LexicalClaim` is the smallest, lowest-risk surface. Adopting it first
proves the wiring without committing the harder sub-types.
## Hard invariants this ADR must preserve
- **`wrong == 0`**. The audit row never directly admits a math fact. Only
ratification through the existing HITL queue can change runtime behaviour.
- **Determinism**. Audit-derived candidates must be byte-identical across
reruns (same case → same candidate → same hash). The current audit already
satisfies this via frozen-dataclass state + canonical bytes.
- **Replay equivalence** (ADR-0057). A ratified math teaching chain must
replay deterministically alongside cognition chains. The trace-hash
contract extends to math chains.
- **Pack mutation proposal-only**. Ratification proposes pack additions;
applying them is a separate, reviewed step (CLAUDE.md §"Teaching Safety").
- **No new eval lanes** (ADR-0166). This ADR builds a capability; the
existing audit + cognition lanes validate it.
## Open questions (must be resolved in the implementation ADR)
1. **Granularity of de-duplication**. Two GSM8K cases produce the same
`lexicon_entry` claim for `crayons`. Are they merged into one candidate
with two evidence rows, or kept as two candidates? (Likely: merged, by
normalised claim signature.)
2. **Provenance schema**. A `MathReaderRefusalEvidence` candidate must
carry: case_id, sentence_index, token_index, refusal_reason, audit_row
hash. Decide canonical-bytes layout before any serialisation lands.
3. **Cross-domain leakage**. Cognition chains and math chains share the
contemplation queue. Must they be partitioned? (Likely: yes, with a
`domain` discriminator on the candidate.)
4. **Ratification UX**. Workbench v1 (ADR-0160) does not render math
candidates today. Out of scope for this ADR; cite as follow-up.
5. **Failure of ratification**. If the operator rejects a candidate, the
audit row remains. Does the next refusal of the same shape re-queue it?
(Likely: yes, with a "previously rejected" annotation; no silent
suppression.)
6. **First-write target**. `LexicalClaim` ratification writes to
`language_packs/data/en_core_math_v1/lexicon/*.jsonl`. Confirm the
loader's per-category source-file path is the canonical mutation site,
not the compiled `lexicon.jsonl`.
## Sequencing
Per ADR-0166's three-question test:
- **Q1 — Capability**: A new candidate source feeding the existing
contemplation queue. Reader, audit, and contemplation already exist on
main; this ADR specifies the wire between them.
- **Q2 — Lane**: The existing
`evals/gsm8k_math/train_sample/v1/audit_brief_11.json` artifact is the
capture surface. Existing cognition-lane teaching tests validate the
ratification → replay path; the math wire reuses that contract.
- **Q3 — Invariant**: `wrong == 0` (no direct admission);
determinism (frozen state + canonical bytes); replay equivalence
(ADR-0057). All three are inherited from existing mechanisms.
Three-question test **passes for the ADR**. Implementation passes only
when the open questions above are answered with `LexicalClaim`-first scope.
## Relationship to Brief 11D
This is the speculative **Candidate E** that the 11D doc did not
enumerate. It does not displace Candidate A (continued GSM8K operator
closure). They are complementary:
- **Candidate A** ships the per-bottleneck closure fixes (the
`lexicon_entry` PR #348 is the first sub-PR).
- **Candidate E** (this ADR) makes the closure fixes *operator-ratifiable
from the audit* rather than hand-written PRs.
A reasonable ordering: A's first 12 PRs land manually (proves the
closure path is real); then E ships the ADR + `LexicalClaim` wiring so
the *third* and onward closure PRs are operator-driven through the
teaching corridor rather than hand-coded.
This is the moment the engine starts teaching itself in the domain — the
loop your thesis demands.
## Decision (pending operator ratification of this ADR)
> Math-reader refusals become teaching-corridor evidence via a new
> `MathReaderRefusalEvidence` candidate source. The audit taxonomy is the
> queue of teachable moments. The engine does not resolve refusals
> in-flight; it surfaces them in a shape the operator can ratify into a
> teaching chain that the existing pack/lexicon/contemplation machinery
> already knows how to absorb.
>
> Scope first to `LexicalClaim` (the lowest-risk, highest-count
> sub-type). Defer the four harder sub-types until the lexical wire is
> proven.
Reopening this decision requires either:
1. The cognition teaching corridor's invariants weaken (no longer a stable
substrate for the math wire), or
2. A simpler design supersedes — e.g. a graph schema that subsumes all
five sub-types without sub-typing cost.
---
## Cross-references
- [BRIEF-11D](./BRIEF-11D-next-capability-proposal.md) — strategic
recommendation this ADR extends
- [ADR-0166](./ADR-0166-measurement-capability-sequencing.md) — gating
rule answered above
- [ADR-0164](./ADR-0164-incremental-comprehension-reader.md) — the
reader whose refusals feed this wire
- [ADR-0150 / 0152 / 0155 / 0161] — the teaching corridor this wire
plugs into
- [ADR-0057](./ADR-0057-teaching-chain-proposal.md) — the
replay-equivalence contract math chains must inherit
- `evals/gsm8k_math/train_sample/v1/audit_brief_11.json` — the data
source the wire consumes

View file

@ -0,0 +1,281 @@
# ADR-0167 — Parallel Work Plan
**Date:** 2026-05-27
**Parent ADR:** [ADR-0167](../decisions/ADR-0167-audit-as-teaching-evidence.md)
**Goal:** Land the LexicalClaim-first slice of the math reader → contemplation
wire across four cooperating operators in two waves, with strict
worktree isolation and shared invariants.
---
## Shared constraints (every brief)
- Open dedicated `git worktree add` per the parallel-agent worktree rule
- `wrong == 0` non-negotiable; verify against case `gsm8k-train-sample-v1-0050`
whenever runtime is touched
- No new canonical eval lanes (ADR-0166)
- No teaching-store / pack mutation as direct side effect of the wire — pack
writes happen only through ratified handlers
- `uv venv` / `uv pip install` / `uv run` — never `pip --break-system-packages`,
never `/tmp` scratch venvs
- Stage explicit files; never `git add -A`; NEVER commit `engine_state/`
- Cognition teaching-corridor tests must remain green at every layer
---
## Wave 1 — Foundation (single blocking brief)
Until Wave 1 lands, Wave 2 cannot start. Wave 1 ships one PR.
### W1-A — Schema + canonical-bytes for `MathReaderRefusalEvidence`
**Recommended operator:** **Opus 4.6/4.7**
**Why this model:** Deepest reasoning. The output is an architectural
schema that has to be right the first time (it's the type every Wave 2
brief depends on). One file of types + one file of round-trip tests.
**Deliverables:**
- `teaching/math_evidence.py` (new) — frozen dataclass
`MathReaderRefusalEvidence` with:
- `case_id: str`
- `sentence_index: int`
- `token_index: int`
- `refusal_reason: str`
- `missing_operator: str | None`
- `claim_signature: str` (normalised dedup key — see W2-B)
- `evidence_hash: str` (canonical-bytes sha256)
- `audit_row: AuditRow` (existing type from `generate/comprehension/audit.py`)
- `sub_type: Literal["lexical", "frame", "composition", "reference", "slot"]`
- `teaching/math_evidence.py` includes `to_canonical_bytes()` mirroring
`state.to_canonical_bytes()` patterns (sort keys, omit None, decimal
canonicalisation if needed)
- `tests/test_math_evidence_schema.py` (new):
- Round-trip canonical bytes determinism (same input → byte-identical hash)
- Frozen-dataclass immutability
- `claim_signature` is stable across two refusals with the same surface
semantics (placeholder; W2-B finalises the normalisation rules)
- Cross-sub-type hash distinctness (lexical claim for `crayons` ≠ frame
claim for `crayons`)
**Out of scope for W1-A:**
- Audit-to-evidence adapter (that's W2-A)
- Dedup policy implementation (W2-B specifies; W1-A only places the field)
- Ratification handlers (W2-D)
**Exit:** PR merged to main; the type is importable; tests are green;
no runtime change outside `teaching/`.
---
## Wave 2 — Parallel build (four briefs, dispatched in one message)
All four branch off `main` (post-W1-A merge). Each in its own worktree.
Each opens its own PR.
### W2-A — Audit → candidate adapter
**Recommended operator:** **GPT-5.3-Codex** (or Sonnet 4.6 as second choice)
**Why this model:** Mechanical wiring with a defined contract. Codex
excels at "take type A, produce type B, write tests." Short cycle time.
**Deliverables:**
- `teaching/math_contemplation.py` (new) — function
`audit_to_evidence(audit_rows: list[AuditRow]) -> list[MathReaderRefusalEvidence]`
- Maps `missing_operator``sub_type` per the table in ADR-0167
- Computes `evidence_hash` from `MathReaderRefusalEvidence.to_canonical_bytes()`
- Leaves `claim_signature` as the empty string for non-lexical sub-types
(W2-B fills it for lexical)
- `tests/test_math_contemplation_adapter.py` — 8+ tests:
- Round-trip from `audit_brief_11.json` produces N evidence records
(one per refused case)
- Determinism: same audit input → byte-identical evidence list
- Mapping table is exhaustive (no `missing_operator` falls through to
`None` sub_type)
- Empty audit → empty evidence list
**Dependencies:** Wave 1 (`MathReaderRefusalEvidence` type)
**Exit:** Adapter callable from a test; cognition tests untouched.
### W2-B — Dedup policy + claim signature normalisation (LexicalClaim only)
**Recommended operator:** **Sonnet 4.6**
**Why this model:** Pure-Python text-normalisation work with clear
invariants. Sonnet is fast and reliable on this shape. Output is
tightly scoped and testable.
**Deliverables:**
- `teaching/math_claim_signature.py` (new) — function
`lexical_claim_signature(surface: str, refusal_detail: str) -> str`
- Normalisation rules (deterministic; documented in module docstring):
- Lowercase the surface
- Strip leading/trailing punctuation
- Encode the unknown-token from `refusal_detail` literally
- Hash with sha256, return hex
- Update `teaching/math_contemplation.py` (W2-A's file) so that lexical
sub_type evidence carries the computed signature; non-lexical pass
empty string (deferred to follow-up ADR)
- `tests/test_math_claim_signature.py` — 10+ tests:
- Identical surface → identical signature
- Different surface → different signature
- Punctuation strip leaves the same signature
- Two GSM8K cases both refusing on `crayons` produce one signature
- Real-data sanity: run over `audit_brief_11.json`, assert no false
collisions among the actual `lexicon_entry` cases
**Dependencies:** Wave 1; coordinates with W2-A on which file owns the
signature call.
**Exit:** Lexical evidence rows carry a stable signature; dedup test
proves identical claims collapse.
### W2-C — Cross-domain partition audit + discriminator
**Recommended operator:** **Gemini** (long-context, mechanical audit)
**Why this model:** This is a scan-many-files survey: find every
contemplation/teaching code path that touches `DiscoveryCandidate`,
identify where `domain` discrimination must be added, list every test
that touches the candidate type, propose minimal surgical patches.
Gemini's long-context window suits the scan; the architecture call
remains the operator's.
**Deliverables (docs + minimal-impl PR):**
- `docs/handoff/ADR-0167-W2C-cross-domain-audit.md` (new) — survey of
every code path that constructs or consumes `DiscoveryCandidate`,
with explicit yes/no on whether each path needs to read a `domain`
field
- Minimal `domain: Literal["cognition", "math"]` field added to
`DiscoveryCandidate` (default `"cognition"` to keep existing cognition
tests passing without changes)
- `tests/test_candidate_domain_partition.py` — assert:
- Existing cognition candidates default to `domain="cognition"`
- A math candidate can be constructed with `domain="math"`
- Round-trip serialisation preserves the field
**Hard constraint:** all existing cognition teaching-corridor tests must
remain green with zero modification.
**Dependencies:** Wave 1 (so the audit can reference the math evidence
type accurately).
**Exit:** Domain field present; cognition tests green; survey doc
identifies any remaining partition risk for Wave 3.
### W2-D — `LexicalClaim` ratification handler
**Recommended operator:** **GPT-5.5 / 5.4** (highest-stakes implementation;
needs GitHub connector access for cross-PR coordination)
**Why this model:** Touches the highest-risk surface: pack files. Needs
the most careful handling of wrong=0, manifest checksum, and
ratification provenance. GPT-5.5's longer-step coding plus GitHub
connector keeps it coordinated with #348's lexicon work.
**Deliverables:**
- `teaching/math_lexical_ratification.py` (new) — function
`apply_lexical_claim(claim: MathReaderRefusalEvidence, category: str,
reviewer: str) -> RatificationReceipt`
- Writes to `language_packs/data/en_core_math_v1/lexicon/<category>.jsonl`
with the rules established by #348 (alphabetical sort, provenance tag,
alias-vs-lemma decision)
- Provenance tag: `phase_2_reader_ratified_<reviewer>_<YYYY-MM-DD>`
- Manifest checksum recompute decision: source-file edits do NOT
regenerate `lexicon.jsonl` (matches #348's pattern); document this in
the function's docstring
- `RatificationReceipt` includes: target_file, lemma, category,
provenance, file_sha256_before, file_sha256_after, evidence_hash
- `tests/test_math_lexical_ratification.py` — 10+ tests, including:
- Round-trip: write a lemma, verify it loads through `load_lexicon`
- Idempotency: applying the same claim twice raises a deterministic
`AlreadyRatified` error (no silent dup)
- Manifest checksum invariant: source-file write does not change
`manifest.json`'s declared checksum
- Hazard pin: ratifying `does` as `accumulation_verb` (mis-category)
raises `WrongZeroViolationCandidate` (because case 0050's `does`
is currently `modal_aux` and reclassifying would risk wrong>0)
- Workbench integration is **out of scope** (ADR-0167 §"Open Questions
Q4"); the function returns a receipt, the workbench wiring is a
follow-up PR.
**Dependencies:** Wave 1; coordinates with #348's pack patterns.
**Exit:** Operator can call `apply_lexical_claim()` from a Python
session to ratify a single lexical evidence row; all tests green.
---
## Wave 3 — Integration + regression (after Wave 2 fully lands)
Single brief; sequential after all Wave 2 PRs merge.
### W3-A — End-to-end determinism + cognition regression
**Recommended operator:** **Opus 4.6/4.7** (or Sonnet 4.6 if Opus is
busy)
**Why this model:** Verification work; the test suite is the contract.
Deep reasoning helps spot subtle invariant breaks across the wire.
**Deliverables:**
- `tests/test_math_evidence_e2e.py` — end-to-end test:
- Load audit_brief_11.json
- Adapter produces evidence list
- Two reruns produce byte-identical evidence list (replay equivalence)
- Ratify one lexical claim
- Re-run audit; the previously-refused case now passes through that
lemma (advances `unknown_word` row by one)
- Cognition teaching-corridor regression: existing
`evals/identity_divergence/` lanes still green
- Update `evals/gsm8k_math/train_sample/v1/audit_brief_11.md` with a
"post-W2 baseline" row in the taxonomy table
**Hard constraint:** if any cognition test breaks, the wire is not
ready to merge.
**Exit:** Full LexicalClaim slice operational; ready for first
operator-driven math ratification.
---
## Dispatch protocol
When ready to launch Wave 2:
```text
Single message → three Agent tool calls in parallel:
1. subagent_type=general-purpose → W2-A brief (Codex-style ops)
2. subagent_type=general-purpose → W2-B brief (Sonnet-style ops)
3. subagent_type=general-purpose → W2-C brief (Gemini-style ops)
+ separate dispatch to GPT-5.5 via GitHub connector → W2-D brief
```
W2-D goes to GPT-5.5 separately because the ratification handler
touches the highest-risk surface and benefits from human-paced review
coordination via the connector.
Wave 3 is single-operator, dispatched after Wave 2 fully merges.
---
## Operator workload (rough estimate)
| Wave | Brief | Operator | Effort |
|------|-------|----------|-------:|
| 1 | W1-A | Opus | small |
| 2 | W2-A | Codex | small |
| 2 | W2-B | Sonnet | small |
| 2 | W2-C | Gemini | medium |
| 2 | W2-D | GPT-5.5 | medium |
| 3 | W3-A | Opus | small |
Six PRs total. Two waves of true parallelism. One serial foundation,
one serial integration. Every wave gate is `wrong == 0` + cognition
tests green.
---
## What this plan does NOT do
- Does **not** add new eval lanes (ADR-0166)
- Does **not** wire workbench v1 (ADR-0167 §Q4 — out of scope)
- Does **not** ship the four non-lexical sub-types (deferred to ADR-0168+)
- Does **not** mutate cognition packs (math wire only)
- Does **not** auto-ratify anything (HITL always)