docs(ADR-0169): CompositionClaim ratification doctrine + adapter (#391)
PR-α of the CompositionClaim wave (CC-1 brief in
docs/handoff/COMPOSITIONCLAIM-BRIEF-PACK.md). Pure docs; no runtime
mutation. Authors two ADRs mirroring ADR-0168 / ADR-0168.1 structure:
- ADR-0169 — CompositionClaim ratification doctrine (parent ADR-0167)
- ADR-0169.1 — MathCompositionClaimProposal adapter (parent ADR-0169)
CompositionClaim is the next sub-type from ADR-0167 FOLLOWUPS §1 and
the highest-leverage missing handler: 20 of 47 audit refusals in
evals/gsm8k_math/train_sample/v1/audit_brief_11.json
(quantity_extraction = 12 + multi_quantity_composition = 8; corrects
the §1 hint's 8+11 = 19 to the audited 20).
Initial SAFE_COMPOSITION_CATEGORIES allowlist:
- multiplicative_composition
- additive_composition
- subtractive_composition
Distributive / ratio / comparative / percentage / unit-conversion /
time / chained compositions are explicitly deferred.
Case 0050 hazard pin is mandated in the acceptance gates section.
Prior-ADR compatibility audit covers ADR-0056, 0057, 0114a, 0164,
0165, 0166, 0167, 0168, 0172. ADR-0057 evidence floor preserved via
the adapter (ADR-0169.1) — audit evidence stays source="math_audit",
never laundered as source="corpus".
Mutation boundary limits accepted proposals to appending reviewed
composition-pattern artifacts under
language_packs/data/en_core_math_v1/compositions/{category}.jsonl;
solver, parser, decomposer, frame-opener, and lexical surfaces remain
untouched.
This commit is contained in:
Shay
GitHub
parent
5adbfa9df9
commit
b51d204898
2 changed files with 972 additions and 0 deletions
599
docs/decisions/ADR-0169-compositionclaim-ratification.md
Normal file
599
docs/decisions/ADR-0169-compositionclaim-ratification.md
Normal file
|
|
@ -0,0 +1,599 @@
|
|||
# ADR-0169 — CompositionClaim Ratification Doctrine
|
||||
|
||||
**Status:** Proposed (doctrine/scoping ADR; no runtime mutation in this PR)
|
||||
**Date:** 2026-05-27
|
||||
**Author:** Shay
|
||||
**Parent:** [ADR-0167](./ADR-0167-audit-as-teaching-evidence.md)
|
||||
**Related:** ADR-0056, ADR-0057, ADR-0114a, ADR-0164, ADR-0165, ADR-0166, ADR-0168, ADR-0172, ADR-0167 FOLLOWUPS §1
|
||||
|
||||
---
|
||||
|
||||
## Context
|
||||
|
||||
ADR-0167 scoped the first math-teaching corridor to `LexicalClaim` only.
|
||||
ADR-0168 extended doctrine to `FrameClaim` — bounded frame-opening
|
||||
admissibility under deterministic replay-constrained ratification.
|
||||
|
||||
`CompositionClaim` is the next sub-type in the queue from ADR-0167
|
||||
FOLLOWUPS §1 and is, by counted audit evidence, the highest-leverage
|
||||
remaining handler:
|
||||
|
||||
- 12 `quantity_extraction` refusals
|
||||
- 8 `multi_quantity_composition` refusals
|
||||
|
||||
— **20 of 47** audit refusals in `evals/gsm8k_math/train_sample/v1/audit_brief_11.json`,
|
||||
all carrying `refusal_reason="incomplete_operation"`.
|
||||
|
||||
> **Correction note.** ADR-0167 FOLLOWUPS §1 priority hint quoted
|
||||
> "8+11 = 19 cases" for CompositionClaim. The actual audit count in
|
||||
> `audit_brief_11.json` is **12 + 8 = 20** (`quantity_extraction` = 12,
|
||||
> `multi_quantity_composition` = 8). This ADR uses the audit count.
|
||||
|
||||
`CompositionClaim` is qualitatively different from both LexicalClaim and
|
||||
FrameClaim.
|
||||
|
||||
A `LexicalClaim` says:
|
||||
|
||||
> "surface form X belongs to lexical category Y"
|
||||
|
||||
A `FrameClaim` says:
|
||||
|
||||
> "surface form X opens (or does not open) a semantic frame of class K"
|
||||
|
||||
A `CompositionClaim` says:
|
||||
|
||||
> "surface pattern X composes a set of recognized quantities into a
|
||||
> single derived quantity under composition category C"
|
||||
|
||||
That is an **arithmetic-chain admissibility decision**.
|
||||
|
||||
A `CompositionClaim` decides whether a frame which already recognized
|
||||
its slots is permitted to fold multiple bound quantities into one
|
||||
operand for downstream solver invocation. The hazard is direct and
|
||||
asymmetric:
|
||||
|
||||
- a mistaken lexical entry creates noise
|
||||
- a mistaken frame opener creates false reasoning structure
|
||||
- a mistaken composition pattern **admits arithmetic errors**
|
||||
|
||||
A wrong composition does not pollute the graph topology. It pollutes
|
||||
the operand fed to the solver. That is closer to the `wrong > 0`
|
||||
surface than any prior sub-type.
|
||||
|
||||
This is the first ADR-0167 sub-type whose failure mode is:
|
||||
|
||||
> producing a numerically wrong but structurally well-formed answer
|
||||
|
||||
That is materially worse than refusal and materially worse than
|
||||
graph fabrication, because the operator-facing trace looks correct.
|
||||
|
||||
---
|
||||
|
||||
## Prior ADR compatibility audit
|
||||
|
||||
This ADR is not final until it remains compatible with prior ADR doctrine.
|
||||
The following audit was performed before opening implementation work.
|
||||
|
||||
| Prior ADR | Load-bearing rule | ADR-0169 compatibility result |
|
||||
|---|---|---|
|
||||
| ADR-0056 | Contemplation is cognitive only; no corpus mutation; reviewed evidence boundaries matter | Compatible. ADR-0169 keeps composition evidence proposal-only during contemplation; no corpus mutation. |
|
||||
| ADR-0057 | Replay-equivalence is precondition, not permission; operator accept required; proposal logs append-only; reviewed-corpus evidence floor for cognition `TeachingChainProposal` | Compatible with constraint. CompositionClaim MUST use the math-specific proposal/ratification adapter (see ADR-0169.1) to preserve ADR-0057 discipline without laundering audit evidence as cognition corpus evidence. |
|
||||
| ADR-0114a | Zero wrong, typed refusal, adversarial misparse=0, determinism, operation provenance | Compatible *and* elevates wrong=0 to first-class concern: composition is the closest sub-type to the arithmetic surface, so case 0050 and recognized-but-uninjectable hazards are mandatory pins. |
|
||||
| ADR-0164 | Incremental reader over semantic categories; no hidden best guess; new categories/rules require ADR | Compatible. CompositionClaim ratifies reviewed composition-pattern membership only; no dynamic pattern synthesis. |
|
||||
| ADR-0165 | Regex only at lexeme level; never grammar templates | Compatible with care. Composition patterns are *structural shape patterns* over already-recognized quantity slots, not grammar templates over raw text. Pattern catalog stays at the *bound-slot composition* level (e.g. `each <count> @ <one_unit_cost>` once both slots are bound), not at the sentence level. |
|
||||
| ADR-0166 | Capability before measurement; no new eval lanes ahead of operators | Compatible. ADR-0169 is doctrine/capability scoping only and explicitly forbids new eval lanes in the implementation PR. |
|
||||
| ADR-0167 | Audit rows become teaching evidence; LexicalClaim first; harder sub-types require their own ADR | Compatible. ADR-0169 is the explicit follow-on sub-type ADR called out in FOLLOWUPS §1. |
|
||||
| ADR-0168 | FrameClaim is bounded frame-opening; allowlisted categories; refusal-first; proposal-only mutation | Compatible. CompositionClaim is **downstream of** FrameClaim and consumes already-opened frames; it never invents frames. |
|
||||
| ADR-0172 | Math-corpus decomposition mechanism — contemplation, decomposer, workbench corridor (Tier 1.5) | Compatible. ADR-0169 introduces the next `change_kind` (`composition_reclassification`) and the next ratifiable handler in the corridor ADR-0172 established. |
|
||||
|
||||
### Resolved tension: ADR-0057 evidence floor
|
||||
|
||||
ADR-0057's ordinary `TeachingChainProposal` eligibility requires at
|
||||
least one `source="corpus"` evidence pointer. Math-domain
|
||||
CompositionClaims originate from audit/refusal artifacts, not from the
|
||||
cognition teaching corpus.
|
||||
|
||||
ADR-0169 therefore does **not** weaken ADR-0057.
|
||||
|
||||
Implementation MUST use the math-specific proposal/ratification
|
||||
adapter (`MathCompositionClaimProposal`) defined in ADR-0169.1, whose
|
||||
evidence floor is `MathReaderRefusalEvidence` plus replay-admissibility
|
||||
evidence, while preserving ADR-0057's append-only / replay /
|
||||
operator-review discipline.
|
||||
|
||||
What is forbidden:
|
||||
|
||||
- treating audit evidence as cognition corpus evidence
|
||||
- bypassing the reviewed-evidence floor
|
||||
- auto-accepting because replay passed
|
||||
- mutating runtime composition behavior outside the proposal/review boundary
|
||||
- creating a second sub-type adapter that mimics ADR-0057 without these gates
|
||||
|
||||
This section is the compatibility trip-wire for any implementation PR.
|
||||
|
||||
---
|
||||
|
||||
## Decision
|
||||
|
||||
`CompositionClaim` ratification is permitted only as a deterministic,
|
||||
replay-equivalent, operator-reviewed proposal surface with explicit
|
||||
hazard pins and category allowlists.
|
||||
|
||||
This ADR does **not** approve runtime implementation.
|
||||
|
||||
This ADR defines:
|
||||
|
||||
- what a `CompositionClaim` is
|
||||
- what it is allowed to mutate
|
||||
- what it is forbidden to mutate
|
||||
- the replay obligations required before implementation
|
||||
- the initial safe composition-category surface
|
||||
- the explicit non-goals
|
||||
|
||||
Implementation is deferred to a follow-on PR (CC-2 in
|
||||
`docs/handoff/COMPOSITIONCLAIM-BRIEF-PACK.md`) that must prove the
|
||||
acceptance gates below.
|
||||
|
||||
---
|
||||
|
||||
## Definition of a CompositionClaim
|
||||
|
||||
A `CompositionClaim` is a reviewed assertion that a structural
|
||||
shape pattern over already-bound quantity slots composes those
|
||||
quantities into one derived operand under a named composition
|
||||
category.
|
||||
|
||||
Canonical shape:
|
||||
|
||||
```text
|
||||
(surface_pattern, composition_category, polarity)
|
||||
```
|
||||
|
||||
Where:
|
||||
|
||||
- `surface_pattern` is a deterministic structural pattern over
|
||||
already-recognized slots (e.g. `bound(count) bound(unit_cost)`),
|
||||
not a regex over raw text;
|
||||
- `composition_category` is one entry of the
|
||||
`SAFE_COMPOSITION_CATEGORIES` allowlist;
|
||||
- `polarity` is `"affirms"` (this pattern composes under category C)
|
||||
or `"falsifies"` (this pattern does NOT compose, refuse).
|
||||
|
||||
Examples (initial scope only):
|
||||
|
||||
| Pattern (shape over bound slots) | Category | Meaning |
|
||||
|---|---|---|
|
||||
| `bound(count) × bound(unit_cost)` | `multiplicative_composition` | total cost = count × unit_cost |
|
||||
| `bound(qty_a) + bound(qty_b)` (independent named quantities in same frame) | `additive_composition` | aggregate = qty_a + qty_b |
|
||||
| `bound(initial) − bound(removed)` | `subtractive_composition` | remainder = initial − removed |
|
||||
|
||||
The claim concerns:
|
||||
|
||||
- composition admissibility for a *recognized* slot tuple
|
||||
- which operator binds those slots into one operand
|
||||
- composition refusal stability when the pattern does not apply
|
||||
|
||||
It does NOT assert:
|
||||
|
||||
- frame admissibility (that is FrameClaim)
|
||||
- entity identity
|
||||
- quantity correctness (the slots are already bound)
|
||||
- reference resolution (that is ReferenceClaim)
|
||||
- slot completion (that is SlotClaim)
|
||||
- solver validity
|
||||
|
||||
Those remain separate sub-types.
|
||||
|
||||
---
|
||||
|
||||
## Why CompositionClaim is dangerous
|
||||
|
||||
Composition patterns sit immediately upstream of solver invocation.
|
||||
|
||||
- a lexical error may fail to ground
|
||||
- a frame error may fabricate a graph
|
||||
- **a composition error feeds a wrong number to a correct solver**
|
||||
|
||||
The principal hazard is:
|
||||
|
||||
```text
|
||||
recognized-and-well-formed-but-wrongly-composed operand
|
||||
```
|
||||
|
||||
This is the asymmetric failure mode that produces:
|
||||
|
||||
- a structurally clean trace
|
||||
- a typed, frame-opened, slot-bound graph
|
||||
- an operator-plausible suggested CLI
|
||||
- and a numerically wrong answer
|
||||
|
||||
Specifically threatening:
|
||||
|
||||
- GSM8K train-sample case **0050** (the canary preventing `pre_frame_filler`
|
||||
fixes from drifting into `wrong > 0`) — case 0050 illustrates how a
|
||||
composition mis-assignment can land a graph that *looks* admissible
|
||||
- recognized-but-uninjectable skip-only fallback
|
||||
- partial-graph greed promoted to full graph by a permissive
|
||||
composition pattern
|
||||
- multi-quantity initial-state frames silently collapsing 3 distinct
|
||||
quantities into a sum that the original story did not require
|
||||
|
||||
The system must therefore prefer:
|
||||
|
||||
```text
|
||||
refuse > leave the operand unbound > compose under an unproven pattern
|
||||
```
|
||||
|
||||
at all times.
|
||||
|
||||
---
|
||||
|
||||
## Initial safe category scope
|
||||
|
||||
Initial implementation scope MUST be allowlist-only.
|
||||
|
||||
No freeform composition invention.
|
||||
No dynamic pattern synthesis.
|
||||
No embedding-nearest-pattern fallback.
|
||||
No "majority vote" across competing categories.
|
||||
|
||||
Initial safe categories:
|
||||
|
||||
| Category | Scope |
|
||||
|---|---|
|
||||
| `multiplicative_composition` | `bound(count) × bound(one_unit_cost)` — produces a total under a single named unit semantic |
|
||||
| `additive_composition` | sum of *independent* named quantities sharing the same frame and unit (e.g. apples + apples) |
|
||||
| `subtractive_composition` | initial − removed, both bound in the same frame, sharing unit |
|
||||
|
||||
Allowlist (canonical):
|
||||
|
||||
```text
|
||||
SAFE_COMPOSITION_CATEGORIES = {
|
||||
"multiplicative_composition",
|
||||
"additive_composition",
|
||||
"subtractive_composition",
|
||||
}
|
||||
```
|
||||
|
||||
Explicitly excluded initially:
|
||||
|
||||
| Deferred category | Reason |
|
||||
|---|---|
|
||||
| `distributive_composition` | requires nested frame interaction; multi-operator semantics |
|
||||
| `ratio_composition` | unit-changing operation; demands SlotClaim for the denominator unit |
|
||||
| `comparative_composition` | demands ReferenceClaim and ordering semantics |
|
||||
| `percentage_composition` | requires `fraction_percentage_literal` recognizer (separate sub-type) |
|
||||
| `unit_conversion_composition` | requires `unit_binding` slot doctrine (SlotClaim) |
|
||||
| `time_composition` | `compound_time_literal` is its own recognizer concern |
|
||||
| `chained_composition` | composition-of-compositions; explicitly deferred until the three primitives prove stable |
|
||||
|
||||
The decomposer dispatch table (`teaching/math_contemplation.py`, see
|
||||
CC-3) maps the audit's `(refusal_reason, missing_operator)` pairs into
|
||||
`composition_reclassification` only when the target category is in
|
||||
`SAFE_COMPOSITION_CATEGORIES`. Anything else routes to
|
||||
`injector_sub_shape` (the catch-all) — refuse-first.
|
||||
|
||||
---
|
||||
|
||||
## Mutation boundary
|
||||
|
||||
A `CompositionClaim` ratification MAY mutate only:
|
||||
|
||||
- reviewed composition-pattern registries:
|
||||
`language_packs/data/en_core_math_v1/compositions/{category}.jsonl`
|
||||
- proposal-layer artifacts (append-only proposal log)
|
||||
|
||||
A `CompositionClaim` ratification MUST NOT directly mutate:
|
||||
|
||||
- solver logic
|
||||
- parser traversal order
|
||||
- decomposer dispatch (heuristic changes ship as their own reviewed PR,
|
||||
not as a side effect of ratification)
|
||||
- runtime graph execution
|
||||
- arithmetic operators
|
||||
- refusal logic
|
||||
- graph verifier semantics
|
||||
- frame-opener registries (those are FrameClaim's surface)
|
||||
- lexical registries (those are LexicalClaim's surface)
|
||||
|
||||
The runtime consumes ratified composition data only through existing
|
||||
reviewed pack-loading mechanisms.
|
||||
|
||||
No direct hot-path mutation. No live-running registry edits.
|
||||
|
||||
---
|
||||
|
||||
## Replay obligations
|
||||
|
||||
Before implementation, the following replay obligations must be proven.
|
||||
|
||||
### 1. Deterministic claim signature
|
||||
|
||||
Equivalent refusals MUST produce identical normalized claim signatures.
|
||||
|
||||
Canonical identity must include:
|
||||
|
||||
- normalized surface pattern (over bound-slot shape, not raw text)
|
||||
- normalized composition category
|
||||
- polarity
|
||||
- audit-row digest
|
||||
- refusal category (`incomplete_operation`)
|
||||
- missing operator (`quantity_extraction` | `multi_quantity_composition`)
|
||||
|
||||
Equivalent evidence MUST deduplicate.
|
||||
|
||||
---
|
||||
|
||||
### 2. Replay equivalence
|
||||
|
||||
Ratified `CompositionClaim`s MUST replay identically across:
|
||||
|
||||
- in-process runs
|
||||
- cross-process runs (subprocess test)
|
||||
- reordered candidate queues (queue-order independence)
|
||||
- repeated ingestion of the same audit evidence (idempotency)
|
||||
|
||||
No queue-order dependence.
|
||||
|
||||
---
|
||||
|
||||
### 3. wrong==0 preservation
|
||||
|
||||
The implementation must prove:
|
||||
|
||||
```text
|
||||
new composition admission cannot silently convert a prior refusal
|
||||
into an incorrect arithmetic answer
|
||||
```
|
||||
|
||||
This specifically requires hazard pins for:
|
||||
|
||||
- **case 0050** (`gsm8k-train-sample-v1-0050`) — pin in
|
||||
`tests/test_math_composition_ratification.py::test_case_0050_hazard_pin`;
|
||||
the case must remain refused after any synthetic CompositionClaim
|
||||
ratification in the allowlist
|
||||
- recognized-but-uninjectable fallback
|
||||
- partial graph acceptance
|
||||
- multi-quantity initial-state collapse (e.g. case 0042: 3 quantities)
|
||||
- operand swap (subtractive composition with reversed minuend/subtrahend)
|
||||
|
||||
---
|
||||
|
||||
### 4. Refusal stability
|
||||
|
||||
Previously refusing cases MAY become:
|
||||
|
||||
- correctly admitted (with a verified arithmetic answer)
|
||||
- still refused
|
||||
|
||||
They MUST NOT become:
|
||||
|
||||
- partially admitted
|
||||
- ambiguously admitted
|
||||
- non-deterministically admitted
|
||||
- structurally admitted with a wrong operand
|
||||
|
||||
Refusal stability MUST be verified across the **full**
|
||||
`audit_brief_11.json` corpus, not just the 20 composition cases.
|
||||
|
||||
---
|
||||
|
||||
## Partition guarantees
|
||||
|
||||
CompositionClaims inherit the ADR-0167 domain partition.
|
||||
|
||||
Math-domain composition claims:
|
||||
|
||||
- use math-domain replay gates
|
||||
- use math-domain contemplation routing
|
||||
- do not borrow cognition corpus evidence
|
||||
- do not reuse cognition semantic-domain classifiers
|
||||
- do not produce cognition `TeachingChainProposal` records
|
||||
|
||||
Cross-domain leakage is prohibited.
|
||||
|
||||
The cognition `TeachingChainProposal` flow MUST NOT see math
|
||||
`MathCompositionClaimProposal` records and vice versa. This is a hard
|
||||
partition test in the implementation PR (mirror
|
||||
`tests/test_math_frame_ratification.py::test_partition_*`).
|
||||
|
||||
---
|
||||
|
||||
## Refusal-first doctrine
|
||||
|
||||
The system must continue preferring:
|
||||
|
||||
```text
|
||||
refuse > speculate
|
||||
```
|
||||
|
||||
throughout CompositionClaim processing.
|
||||
|
||||
Specifically forbidden:
|
||||
|
||||
- nearest-pattern guessing
|
||||
- probabilistic fallback category selection
|
||||
- majority-vote composition admission
|
||||
- confidence-threshold operand coercion
|
||||
- dynamic composition synthesis at runtime
|
||||
- "best guess" multiplication vs addition when both slots present
|
||||
|
||||
A composition the engine cannot prove under an allowlisted category
|
||||
remains a refusal event.
|
||||
|
||||
The teaching corridor exists precisely so the engine does not need to
|
||||
invent arithmetic structure at runtime.
|
||||
|
||||
---
|
||||
|
||||
## Non-goals
|
||||
|
||||
This ADR does NOT approve:
|
||||
|
||||
- ReferenceClaim
|
||||
- SlotClaim
|
||||
- `distributive_composition`, `ratio_composition`,
|
||||
`comparative_composition`, `percentage_composition`,
|
||||
`unit_conversion_composition`, `time_composition`,
|
||||
`chained_composition`
|
||||
- dynamic composition synthesis
|
||||
- graph-schema replacement
|
||||
- automatic composition learning
|
||||
- runtime self-modification
|
||||
- autonomous pack mutation
|
||||
- embedding-derived arithmetic repair
|
||||
- a reviewed math corpus substrate (deferred — see ADR-0169.1
|
||||
"Why not a reviewed math corpus first?")
|
||||
|
||||
This ADR also does NOT attempt to solve:
|
||||
|
||||
- generalized arithmetic reasoning
|
||||
- open-ended quantity composition
|
||||
- unit-changing operations
|
||||
- multi-step arithmetic chains
|
||||
|
||||
The target is bounded deterministic composition admission for audited
|
||||
GSM8K-style reasoning surfaces under three allowlisted primitives.
|
||||
|
||||
---
|
||||
|
||||
## Sequencing
|
||||
|
||||
Per ADR-0166:
|
||||
|
||||
### Q1 — Capability
|
||||
|
||||
Adds one new operator-ratifiable admissibility surface:
|
||||
|
||||
```text
|
||||
bound-slot shape pattern -> reviewed composition category
|
||||
```
|
||||
|
||||
using the existing audit → contemplation → replay → HITL corridor
|
||||
established by ADR-0167 and ADR-0172.
|
||||
|
||||
### Q2 — Lane
|
||||
|
||||
**No new eval lane.**
|
||||
|
||||
Existing:
|
||||
|
||||
- GSM8K audit lane (`evals/gsm8k_math`)
|
||||
- contemplation replay lane (`core eval math-contemplation`)
|
||||
- wrong==0 gates
|
||||
- determinism checks
|
||||
|
||||
remain the proof surface.
|
||||
|
||||
### Q3 — Invariant
|
||||
|
||||
Must preserve:
|
||||
|
||||
- `wrong == 0`
|
||||
- replay equivalence
|
||||
- deterministic claim hashing
|
||||
- refusal-first semantics
|
||||
- explicit operator ratification
|
||||
- reviewed mutation only
|
||||
- domain partition (math vs cognition)
|
||||
|
||||
The implementation PR passes only when all seven are mechanically proven.
|
||||
|
||||
---
|
||||
|
||||
## Acceptance gates for implementation PR
|
||||
|
||||
A future implementation PR (CC-2) must provide:
|
||||
|
||||
- deterministic claim canonicalization tests
|
||||
- cross-process replay-equivalence tests (subprocess)
|
||||
- queue-order independence tests (A→B == B→A ratify)
|
||||
- duplicate ratification idempotency tests (`AlreadyRatified` on second call)
|
||||
- evidence-tampering rejection tests
|
||||
- **case 0050 hazard pin** — mandatory; mirror
|
||||
`tests/test_math_frame_ratification.py::test_case_0050_hazard_pin`;
|
||||
case 0050 must remain refused after any synthetic CompositionClaim
|
||||
ratification under the initial allowlist
|
||||
- recognized-but-uninjectable regression pins
|
||||
- refusal-stability regression suite across the **full**
|
||||
`audit_brief_11.json` corpus
|
||||
- cross-domain partition tests (cognition `TeachingChainProposal` flow
|
||||
must NOT see math CompositionClaims and vice versa)
|
||||
- no-corpus-mutation proof (cognition corpus bytes unchanged during
|
||||
math composition replay)
|
||||
- no-runtime-hotpatch proof (solver / parser / decomposer / graph
|
||||
verifier bytes unchanged)
|
||||
- audit-evidence-not-laundered-as-corpus test (the adapter must emit
|
||||
`source="math_audit"`, never `source="corpus"`)
|
||||
- workbench dispatch test: `composition_reclassification` routes to
|
||||
`CompositionClaim`, not 501
|
||||
- proposed_change_kind Literal accepts `composition_reclassification`
|
||||
- W1 round-trip test extended for the new `change_kind`
|
||||
|
||||
without introducing:
|
||||
|
||||
- new eval lanes
|
||||
- stochastic routing
|
||||
- runtime graph guessing
|
||||
- categories outside `SAFE_COMPOSITION_CATEGORIES`
|
||||
|
||||
---
|
||||
|
||||
## Relationship to ADR-0167 and ADR-0168
|
||||
|
||||
ADR-0167 established:
|
||||
|
||||
```text
|
||||
audit rows become teaching evidence
|
||||
```
|
||||
|
||||
ADR-0168 established:
|
||||
|
||||
```text
|
||||
frame-opening semantics may become reviewed teaching evidence
|
||||
```
|
||||
|
||||
ADR-0169 establishes:
|
||||
|
||||
```text
|
||||
composition patterns over already-bound slots may become reviewed
|
||||
teaching evidence — but only under deterministic replay-constrained
|
||||
doctrine, and only inside an allowlisted category surface, because
|
||||
composition errors are the closest sub-type to direct arithmetic
|
||||
wrongness
|
||||
```
|
||||
|
||||
The escalation is intentional:
|
||||
|
||||
- LexicalClaim teaches vocabulary
|
||||
- FrameClaim teaches admissibility structure
|
||||
- CompositionClaim teaches arithmetic-chain admissibility
|
||||
|
||||
Each step is materially more dangerous than the last and therefore
|
||||
requires explicit doctrine before implementation.
|
||||
|
||||
---
|
||||
|
||||
## Decision
|
||||
|
||||
> CORE may extend the ADR-0167 teaching corridor from lexical and
|
||||
> frame ratification into bounded composition-pattern ratification,
|
||||
> provided:
|
||||
>
|
||||
> - replay equivalence remains deterministic
|
||||
> - `wrong == 0` hazard pins hold (case 0050 mandatory)
|
||||
> - composition categories remain explicitly allowlisted
|
||||
> - runtime speculation remains prohibited
|
||||
> - all mutation remains proposal-reviewed and replay-auditable
|
||||
> - the math-domain proposal/ratification adapter (ADR-0169.1) is
|
||||
> used; audit evidence is never laundered as cognition corpus
|
||||
> evidence
|
||||
>
|
||||
> Refusal remains preferable to speculative arithmetic composition.
|
||||
|
||||
Reopening this ADR requires evidence that:
|
||||
|
||||
1. the replay obligations cannot be satisfied mechanically, or
|
||||
2. a graph-schema approach supersedes sub-type ratification entirely, or
|
||||
3. composition wrong-rate cannot be held at zero under the proposed
|
||||
allowlist (in which case the allowlist contracts, not expands).
|
||||
|
|
@ -0,0 +1,373 @@
|
|||
# ADR-0169.1 — MathCompositionClaimProposal Adapter
|
||||
|
||||
**Status:** Proposed (design bridge; no runtime CompositionClaim admission in this PR)
|
||||
**Date:** 2026-05-27
|
||||
**Author:** Shay
|
||||
**Parent:** [ADR-0169](./ADR-0169-compositionclaim-ratification.md)
|
||||
**Related:** ADR-0057, ADR-0163, ADR-0164, ADR-0166, ADR-0167, ADR-0168, ADR-0168.1, ADR-0172
|
||||
|
||||
---
|
||||
|
||||
## Context
|
||||
|
||||
ADR-0169 identified a required compatibility bridge before any
|
||||
CompositionClaim implementation can land.
|
||||
|
||||
ADR-0057 ordinary `TeachingChainProposal` eligibility requires a
|
||||
reviewed `source="corpus"` evidence pointer. That is correct for
|
||||
cognition teaching chains, where the claim is grounded in reviewed
|
||||
teaching-corpus material.
|
||||
|
||||
Math-domain CompositionClaims originate elsewhere:
|
||||
|
||||
```text
|
||||
MathReaderRefusalEvidence / audit rows
|
||||
```
|
||||
|
||||
— specifically the 20 rows in
|
||||
`evals/gsm8k_math/train_sample/v1/audit_brief_11.json` under
|
||||
`refusal_reason="incomplete_operation"` with `missing_operator` in
|
||||
`{"quantity_extraction", "multi_quantity_composition"}`.
|
||||
|
||||
Those rows are legitimate evidence of a teachable composition gap,
|
||||
but they are not cognition corpus evidence and must never be laundered
|
||||
into cognition corpus pointers.
|
||||
|
||||
Therefore CompositionClaim cannot simply reuse ordinary
|
||||
`TeachingChainProposal` as-is without either:
|
||||
|
||||
1. weakening ADR-0057's reviewed-evidence floor, or
|
||||
2. falsely treating audit evidence as cognition corpus evidence.
|
||||
|
||||
Both are forbidden.
|
||||
|
||||
This ADR is structurally analogous to ADR-0168.1
|
||||
(`MathFrameClaimProposal`). The same bridge logic applies, with the
|
||||
data shape and evidence floor specialized to composition.
|
||||
|
||||
---
|
||||
|
||||
## Decision
|
||||
|
||||
Choose a math-specific proposal/ratification adapter:
|
||||
|
||||
```text
|
||||
MathCompositionClaimProposal
|
||||
```
|
||||
|
||||
instead of creating a reviewed math corpus artifact first.
|
||||
|
||||
This adapter preserves ADR-0057's discipline:
|
||||
|
||||
- append-only proposal log
|
||||
- replay-equivalence/admissibility as precondition, not permission
|
||||
- explicit operator review before mutation
|
||||
- no deletion
|
||||
- no auto-accept
|
||||
- no active-pack mutation during replay
|
||||
|
||||
but gives math-domain audit evidence its own honest evidence floor.
|
||||
|
||||
---
|
||||
|
||||
## Why not a reviewed math corpus first?
|
||||
|
||||
A reviewed math corpus may eventually be useful, but it is premature
|
||||
for the second math sub-type bridge (FrameClaim is the first; see
|
||||
ADR-0168.1).
|
||||
|
||||
Creating it now would require deciding:
|
||||
|
||||
- corpus schema
|
||||
- corpus lifecycle
|
||||
- corpus indexing semantics
|
||||
- corpus replay integration
|
||||
- whether frame evidence, slot evidence, composition evidence, and
|
||||
reference evidence share one corpus or separate corpora
|
||||
- how accepted math evidence relates to pack manifests
|
||||
|
||||
That is a larger substrate decision than CompositionClaim needs.
|
||||
|
||||
The adapter remains narrower:
|
||||
|
||||
```text
|
||||
one claim type
|
||||
one proposal surface
|
||||
one replay gate
|
||||
one operator acceptance boundary
|
||||
```
|
||||
|
||||
It keeps the capability path moving without inventing a new corpus
|
||||
family before the need is proven across at least two sub-types
|
||||
(FrameClaim and CompositionClaim) and converged.
|
||||
|
||||
When (and only when) the third or fourth math sub-type adapter is
|
||||
needed, the case for collapsing them into a reviewed math corpus
|
||||
becomes load-bearing. Not yet.
|
||||
|
||||
---
|
||||
|
||||
## Data shape
|
||||
|
||||
A future implementation should define a frozen, canonicalizable data
|
||||
shape similar to:
|
||||
|
||||
```python
|
||||
@dataclass(frozen=True, slots=True)
|
||||
class MathCompositionClaimProposal:
|
||||
proposal_id: str
|
||||
claim_signature: str
|
||||
surface_pattern: str # normalized structural pattern over bound slots
|
||||
composition_category: str # must be in SAFE_COMPOSITION_CATEGORIES
|
||||
polarity: Literal["affirms", "falsifies"]
|
||||
evidence: tuple[MathReaderRefusalEvidence, ...]
|
||||
replay_evidence: AdmissibilityReplayEvidence | None
|
||||
review_state: Literal["pending", "accepted", "rejected", "withdrawn"]
|
||||
operator_note: str
|
||||
provenance: MathProposalProvenance | None
|
||||
```
|
||||
|
||||
Mirror the structure of `MathFrameClaimProposal` (ADR-0168.1) exactly,
|
||||
swapping `surface_form` / `frame_category` for `surface_pattern` /
|
||||
`composition_category`.
|
||||
|
||||
This is deliberately not a `TeachingChainProposal` because its
|
||||
evidence floor is not cognition corpus evidence.
|
||||
|
||||
It is also deliberately not a runtime composition registry entry. It
|
||||
is a proposal.
|
||||
|
||||
---
|
||||
|
||||
## Evidence floor
|
||||
|
||||
A `MathCompositionClaimProposal` is eligible only if it has:
|
||||
|
||||
1. at least one audit/refusal evidence pointer,
|
||||
2. a deterministic audit-row digest,
|
||||
3. a normalized claim signature,
|
||||
4. a known `missing_operator` subtype mapping to `CompositionClaim`
|
||||
(i.e. `quantity_extraction` or `multi_quantity_composition`),
|
||||
5. an allowlisted `composition_category` (one of
|
||||
`SAFE_COMPOSITION_CATEGORIES` from ADR-0169),
|
||||
6. `boundary_clean=True`, and
|
||||
7. `polarity in {"affirms", "falsifies"}`.
|
||||
|
||||
Audit evidence must include enough provenance to replay the claim:
|
||||
|
||||
- case id
|
||||
- sentence index
|
||||
- frame index when available
|
||||
- bound-slot tuple digest (the slot shape over which the composition
|
||||
pattern is asserted)
|
||||
- missing operator
|
||||
- refusal reason (`incomplete_operation`) and refusal detail
|
||||
- recognized terms digest
|
||||
- audit row canonical digest
|
||||
|
||||
The evidence pointer source must be a math-specific value such as:
|
||||
|
||||
```text
|
||||
source="math_audit"
|
||||
```
|
||||
|
||||
It must **not** be `source="corpus"` unless and until a real reviewed
|
||||
math corpus exists. This is the no-laundering trip-wire shared with
|
||||
ADR-0168.1.
|
||||
|
||||
---
|
||||
|
||||
## Replay gate
|
||||
|
||||
The adapter uses the math-domain replay gate:
|
||||
|
||||
```text
|
||||
run_admissibility_replay_gate
|
||||
```
|
||||
|
||||
(the same gate used by `MathFrameClaimProposal`), parameterized by the
|
||||
composition-pattern target artifact rather than the frame target
|
||||
artifact.
|
||||
|
||||
Replay remains a precondition, not permission.
|
||||
|
||||
If replay regresses any protected metric (`wrong == 0`, refusal
|
||||
stability, partition, determinism), the proposal auto-transitions to
|
||||
`rejected` with an `auto_rollback_regression` note.
|
||||
|
||||
If replay passes, the proposal remains `pending` until explicit
|
||||
operator review. This preserves ADR-0057's "replay is precondition,
|
||||
not permission" rule.
|
||||
|
||||
---
|
||||
|
||||
## Accepted proposal effect
|
||||
|
||||
Accepting a `MathCompositionClaimProposal` may only append (or propose
|
||||
append) to a reviewed composition-pattern artifact:
|
||||
|
||||
```text
|
||||
language_packs/data/en_core_math_v1/compositions/{category}.jsonl
|
||||
```
|
||||
|
||||
where `{category}` is one of the entries in `SAFE_COMPOSITION_CATEGORIES`.
|
||||
|
||||
It must not directly mutate:
|
||||
|
||||
- active runtime state
|
||||
- solver code
|
||||
- parser code
|
||||
- decomposer code (heuristic changes are their own reviewed PR)
|
||||
- graph verifier code
|
||||
- arithmetic semantics
|
||||
- frame-opener registries (FrameClaim's surface)
|
||||
- lexical registries (LexicalClaim's surface)
|
||||
- cognition corpus
|
||||
- cognition packs
|
||||
|
||||
Acceptance should produce an append-only provenance record linking:
|
||||
|
||||
```text
|
||||
proposal_id -> claim_signature -> target artifact row -> reviewer
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
## Idempotency
|
||||
|
||||
`proposal_id` must derive from canonical claim identity, not clock
|
||||
time.
|
||||
|
||||
Recommended identity:
|
||||
|
||||
```text
|
||||
sha256(
|
||||
domain
|
||||
| subtype # "composition_claim"
|
||||
| surface_pattern # normalized bound-slot shape
|
||||
| composition_category
|
||||
| polarity
|
||||
| evidence_digest_set
|
||||
)
|
||||
```
|
||||
|
||||
Equivalent evidence should deduplicate. Adding a second audit row for
|
||||
the same claim may either:
|
||||
|
||||
1. append evidence to the existing proposal record, or
|
||||
2. create a new event referencing the existing proposal id.
|
||||
|
||||
It must not create a second independent mutation opportunity for the
|
||||
same claim.
|
||||
|
||||
Calling `apply_composition_claim()` a second time on an already-ratified
|
||||
proposal must raise `AlreadyRatified` (mirror
|
||||
`teaching/math_frame_ratification.py` semantics).
|
||||
|
||||
---
|
||||
|
||||
## Partition guarantees
|
||||
|
||||
The adapter is math-domain only.
|
||||
|
||||
It must not:
|
||||
|
||||
- consume cognition corpus evidence,
|
||||
- emit cognition `TeachingChainProposal` records,
|
||||
- append to cognition chains,
|
||||
- read cognition semantic-domain classifiers,
|
||||
- use cognition replay gates,
|
||||
- be visible to cognition contemplation/proposal flows.
|
||||
|
||||
It may share infrastructure patterns from ADR-0057 and from
|
||||
`MathFrameClaimProposal` (ADR-0168.1), but not evidence identity.
|
||||
|
||||
The partition test in the implementation PR
|
||||
(`tests/test_math_composition_ratification.py::test_partition_cognition_proposals_not_seen`)
|
||||
must mechanically pin that cognition `TeachingChainProposal` records
|
||||
do not flow into the math composition handler and vice versa.
|
||||
|
||||
---
|
||||
|
||||
## Trip-wires that close the ADR-0057 compatibility gap
|
||||
|
||||
The implementation PR must mechanically prove each of:
|
||||
|
||||
1. **No corpus laundering.** The adapter emits `source="math_audit"`
|
||||
and never `source="corpus"`. Pinned by
|
||||
`test_audit_evidence_not_laundered_as_corpus`.
|
||||
2. **Append-only proposal log.** No deletion path; rejected/withdrawn
|
||||
states are transitions, not removals.
|
||||
3. **Replay is precondition, not permission.** Replay pass leaves the
|
||||
proposal `pending`. Operator accept is required for mutation.
|
||||
4. **Replay regression auto-rejects.** Any regression in `wrong`,
|
||||
refusal stability, partition, or determinism flips the proposal to
|
||||
`rejected` with an `auto_rollback_regression` note.
|
||||
5. **Deterministic proposal id.** `proposal_id` is derived from
|
||||
canonical claim identity; equivalent evidence produces equivalent
|
||||
ids across processes.
|
||||
6. **Active-pack bytes unchanged during replay.** The replay gate must
|
||||
not mutate `language_packs/data/en_core_math_v1/**` byte content
|
||||
until operator accept lands.
|
||||
7. **No cross-domain emission.** The handler does not produce
|
||||
cognition-domain artifacts.
|
||||
8. **Allowlist enforcement.** A `composition_category` outside
|
||||
`SAFE_COMPOSITION_CATEGORIES` raises `WrongCompositionCategory`
|
||||
before any provenance is written.
|
||||
|
||||
---
|
||||
|
||||
## Acceptance gates for implementation
|
||||
|
||||
A future implementation PR must prove:
|
||||
|
||||
- deterministic claim signature
|
||||
- deterministic proposal id
|
||||
- duplicate evidence deduplication
|
||||
- append-only proposal log behavior
|
||||
- replay-gate selection = math admissibility replay
|
||||
- replay pass leaves proposal pending, not accepted
|
||||
- replay regression auto-rejects
|
||||
- operator accept is required for mutation
|
||||
- accept writes only the reviewed math composition target artifact
|
||||
- active corpus and active pack bytes are unchanged during replay
|
||||
- audit evidence is never serialized as cognition corpus evidence
|
||||
- case 0050 remains safe under any synthetic ratification in the
|
||||
initial allowlist
|
||||
- recognized-but-uninjectable remains refused unless fully admitted
|
||||
correctly
|
||||
- multi-quantity initial-state cases (e.g. case 0042 with 3 quantities)
|
||||
do not silently collapse under an unproven aggregation
|
||||
- subtractive composition does not silently swap minuend and subtrahend
|
||||
|
||||
---
|
||||
|
||||
## Non-goals
|
||||
|
||||
This ADR does not implement:
|
||||
|
||||
- CompositionClaim runtime admission
|
||||
- composition-pattern artifact schema (deferred to the implementation PR;
|
||||
the JSONL layout under `language_packs/data/en_core_math_v1/compositions/`
|
||||
is the artifact target but its row schema is not fixed here)
|
||||
- workbench rendering
|
||||
- ReferenceClaim
|
||||
- SlotClaim
|
||||
- reviewed math corpus substrate
|
||||
- automatic acceptance
|
||||
- additional composition categories beyond the ADR-0169 initial allowlist
|
||||
|
||||
This is only the bridge decision that makes future CompositionClaim
|
||||
implementation compatible with ADR-0057.
|
||||
|
||||
---
|
||||
|
||||
## Decision summary
|
||||
|
||||
> Use a dedicated `MathCompositionClaimProposal` adapter for
|
||||
> math-domain CompositionClaim evidence. Preserve ADR-0057's
|
||||
> replay/review discipline, but do not impersonate ADR-0057's cognition
|
||||
> corpus evidence floor. Audit evidence stays audit evidence;
|
||||
> operator-reviewed accepted proposals may later append to a reviewed
|
||||
> math composition artifact under deterministic replay gates, scoped
|
||||
> to the `SAFE_COMPOSITION_CATEGORIES` allowlist defined in ADR-0169.
|
||||
Loading…
Reference in a new issue