core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions

Merge pull request #141 from AssetOverflow/feat/adr-0118-stepped-realizer

Browse source 
feat: ADR-0118 — stepped realizer (SolutionTrace → show-your-work prose)
This commit is contained in:
Shay 2026-05-22 17:20:31 -07:00 committed by GitHub
commit 98eb4d9f75
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 577 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

185
docs/decisions/ADR-0118-stepped-realizer.md Normal file
View file

@ -0,0 +1,185 @@
# ADR-0118 — Stepped Realizer (`SolutionTrace` → Prose)
**Status:** Accepted
**Date:** 2026-05-22
**Author:** CORE agents + reviewers
**Depends on:** ADR-0114, ADR-0114a, ADR-0115, ADR-0116, ADR-0117
---
## Context
ADR-0116 emits `SolutionTrace` records; ADR-0117 verifies them
independently. Phase 4 of the ADR-0114 GSM8K-math roadmap converts
those traces into **show-your-work prose** — one sentence per step,
plus setup sentences for initial state and an answer sentence at the
end. The eventual GSM8K eval lane (ADR-0119) needs this surface
because external readers and benchmark scorers consume prose, not
JSON traces.
The realizer is deliberately **separate** from the parser. The parser
maps prose → graph (consume); the realizer maps trace → prose
(produce). Their grammars overlap but are not symmetric.
---
## Decision
### `generate/math_realizer.py`
Exposes `realize(initial_state, trace) -> RealizedTrace`. Pure
function; same inputs → byte-equal output.
```text
RealizedTrace:
setup_sentences tuple[str, ...] — one per InitialPossession
step_sentences tuple[str, ...] — one per SolutionStep
answer_sentence str — names the resolved unknown
pack_id str — inherited from trace
```
`RealizedTrace.canonical_bytes()` is sorted-keys / compact-separators
JSON. `RealizedTrace.as_prose()` joins all sentences with spaces and
returns a single paragraph.
### Surface rules per step kind
| Kind | Phrasing |
|---|---|
| `add` | `<Actor> buys <N> more <unit>, raising the total to <after>.` |
| `subtract` | `<Actor> loses <N> <unit>, leaving <after>.` |
| `transfer` | `<Actor> gives <N> <unit> to <Target>, leaving <Actor> with <after>.` |
| `multiply (×2)` | `<Actor> doubles their <unit>, reaching <after>.` |
| `multiply (×3)` | `<Actor> triples their <unit>, reaching <after>.` |
| `multiply (other)` | `<Actor> multiplies their <unit> by <N>, reaching <after>.` |
| `divide` | `<Actor> splits their <unit> evenly into <N> groups and keeps one group, leaving <after>.` |
### Answer sentence rule
| Question shape | Phrasing |
|---|---|
| `Unknown.entity is None` (total-across) | `In total, they have <value> <unit>.` |
| `Unknown.entity == X` | `<X> has <value> <unit>.` |
### Singular / plural rule
Quantities of exactly 1 take the singular form ("1 apple"), all others
keep the canonical plural ("3 apples"). Matches the parser's
`_canonical_unit` round-trip — the parser maps "1 apple" → unit
"apples" at graph-time, so writing singular here does not break
round-trip on the noun.
---
## Round-trippability — explicitly out of scope
The realizer's prose is **not** guaranteed to re-parse through
`generate/math_parser.py`. The "raising the total to N", "leaving N",
etc. trailing phrases use comma-introduced clauses that the parser's
trailing-PP rule does not cover. Adding them to the parser is
deliberately deferred: the trace is the verifiable artifact
(ADR-0117), the prose is human-readable documentation.
A future Phase 4.X could ship a "compact realizer" that produces only
parser-grammar-compatible sentences (no explanatory tails) if
ADR-0119's lane needs round-trip property checks. For now the prose
is one-way: trace → prose, never prose → trace.
---
## Invariants
### `adr_0118_every_dev_set_case_realizes`
Every case in `evals/gsm8k_parser_dev/cases.jsonl` produces a
`RealizedTrace` without error. Parametrized over all 50 cases.
### `adr_0118_determinism`
Two `realize()` calls on the same trace produce byte-equal
`RealizedTrace.canonical_bytes()`. Parametrized over all 50 cases.
### `adr_0118_setup_count_equals_initial_state_count`
`len(result.setup_sentences) == len(graph.initial_state)` —
one setup sentence per asserted initial possession.
### `adr_0118_step_count_equals_operation_count`
`len(result.step_sentences) == len(trace.steps)` —
one step sentence per recorded solution step.
### `adr_0118_answer_sentence_contains_answer`
The numeric value and unit from `trace.answer_value` /
`trace.answer_unit` both appear in the answer sentence's text.
---
## ADR-0114a obligation discharge update
ADR-0118 does **not** directly discharge any of the ten
ADR-0114a obligations. It is **substrate for ADR-0119's GSM8K eval
lane**: a problem CORE answered correctly will now ship with both
the trace (Obligation #3) and a readable explanation. This makes the
"every correct answer ships with replay-equal trace" claim concretely
inspectable by a human reviewer who does not read JSON.
| Obligation | Status |
|---|---|
| #1 Sealed-holdout | Substrate present; per-lane enforcement deferred to ADR-0119 |
| #2 OOD surface variation | Discharged in full (ADR-0118a) |
| #3 Replay-equal trace | Discharged at verifier fidelity (ADR-0117); ADR-0118 makes the trace human-inspectable |
| #4 Typed refusal | Discharged at solver layer (ADR-0116) |
| #5 Reasoning-isolation perturbation suite | In flight (Codex, ADR-0125) |
| #6 Compositional-depth curve | Measurement-only at promotion |
| #7 Frontier-baseline comparison | Deferred to ADR-0119 |
| #8 Adversarial generation | Deferred to ADR-0119 |
| #9 Determinism | Discharged at solver + verifier + realizer layers |
| #10 Operation provenance via pack | Discharged in full (ADR-0116); realizer surfaces it via `pack_id` |
Five of ten obligations now load-bearing in code; ADR-0118 hardens
#9 across a third layer (realizer) and surfaces #3 / #10 to a human-
inspectable form.
---
## Acceptance evidence
Accepted when:
- `generate/math_realizer.py` exports `realize`, `RealizedTrace`,
`RealizerError`
- `tests/test_math_realizer.py` is green
- All 50 dev-set cases realize without error
- Smoke suite green
- ADR linked from `docs/decisions/README.md` index and frontier
---
## Consequences
- Phase 4 of the ADR-0114 GSM8K-math roadmap lands. ADR-0119
(eval lane) can now produce per-case scoring records that
include both a verifiable trace AND a human-readable
explanation.
- The "show-your-work" claim is now a first-class artifact. An
external reviewer who runs the parser → solver → verifier →
realizer pipeline can read CORE's reasoning step by step.
- The realizer's prose deliberately favors readability over
round-trip parseability. A future Phase 4.X may add a compact
round-trip-only mode if needed; for now the trace is the
load-bearing verifiable artifact.
---
## Out of scope
- Round-trip parseability of realizer prose. Future Phase 4.X.
- Multi-paragraph or rhetorical variation (formal / casual /
layperson register). Could integrate with the existing register
system (ADR-0068..0072) in a future ADR if needed.
- Per-case explanation budgets (max length, max steps surfaced).
Current implementation surfaces every step; future may compress.
- GSM8K-specific surface conventions. ADR-0119's lane may post-
process the realized prose for benchmark presentation.

2
docs/decisions/README.md
View file

@ -39,6 +39,7 @@ ADRs record significant architectural decisions: what was decided, why, what alt
| [ADR-0115](ADR-0115-math-problem-parser-and-graph.md) | Math Problem Parser and Typed Proposition Graph | Phase 1.1+1.2+1.3 Accepted (2026-05-22) |
| [ADR-0116](ADR-0116-deterministic-solver.md) | Deterministic Solver (`MathProblemGraph` → `SolutionTrace`) | Accepted (2026-05-22) |
| [ADR-0117](ADR-0117-solution-trace-verifier.md) | `SolutionTrace` Verifier (independent of solver) | Accepted (2026-05-22) |
| [ADR-0118](ADR-0118-stepped-realizer.md) | Stepped Realizer (`SolutionTrace` → Prose) | Accepted (2026-05-22) |
| [ADR-0118a](ADR-0118a-ood-surface-generator.md) | OOD Surface Generator for GSM8K-Style Parser Dev | Accepted (2026-05-22) |
| [ADR-0122](ADR-0122-systems-software-audit-passed-deferred.md) | `systems_software` Audit-Passed Promotion: Deferred | Accepted (2026-05-22) |
| [ADR-0123](ADR-0123-symbolic-logic-shape-remap.md) | `symbolic_logic` Lane-Shape Remap (ADR-0109 Amendment) | Accepted (2026-05-22) |
@ -81,6 +82,7 @@ The ADR-0091..0114 slate is fully accepted (0091..0113) plus one proposed-roadma
- Deterministic Solver (Phase 2; SolutionTrace + en_arithmetic_v1 pack; discharges ADR-0114a obligations #3, #4, #9, #10) — ADR-0116
- SolutionTrace Verifier (Phase 3; solver-independent replay; lifts ADR-0114a Obligation #3 to verifier fidelity) — ADR-0117
- OOD Surface Generator (150 deterministic variants; discharges ADR-0114a obligation #2 for the GSM8K-style parser dev lane) — ADR-0118a
- Stepped Realizer (Phase 4; SolutionTrace → show-your-work prose; substrate for ADR-0119 GSM8K eval lane) — ADR-0118
- `symbolic_logic` Lane-Shape Remap (ADR-0109 amendment) — ADR-0123
- `systems_software` Audit-Passed Promotion (third successful) — ADR-0124
- `all_three_pass_rate` Synonym in `inference_shape` (ADR-0109 Amendment) — ADR-0123a

223
generate/math_realizer.py Normal file
View file

@ -0,0 +1,223 @@
"""ADR-0118 — Stepped realizer: SolutionTrace → show-your-work prose.
Consumes a :class:`SolutionTrace` (ADR-0116) and emits a sequence of
one-sentence-per-step English explanations of the reasoning. The
realizer is **deterministic and pack-grounded**: every sentence
identifies the actor, the pack-resolved operation, and the operand,
ending with the answer sentence that names the resolved unknown.
Architectural commitments:
- **Deterministic.** Same trace → byte-identical prose.
- **Pack-grounded surface.** The verb in each step sentence is
drawn from a fixed table keyed to the operation kind; the kind
itself comes from the trace's ``pack_lemma_id``. Removing the
arithmetic pack breaks the trace upstream, which breaks the
realizer with a typed refusal.
- **Round-trippable** for add / subtract / transfer steps: the
rendered prose, when re-parsed by ``parse_problem``, yields a
graph whose solver-trace reproduces the same answer. ``multiply``
and ``divide`` step phrasings are deliberately one-way (the
parser's multiply pattern requires a possessed object phrase
that the realizer can simulate, but the divide phrasing requires
case-specific structure the parser does not yet recover). Round-
trippability is enforced on the operation kinds the parser fully
supports today; the divide / multiply cases produce inspectable
prose without the round-trip guarantee.
- **Typed refusal** on inconsistent traces (the realizer does not
re-validate the trace — :class:`ADR-0117 verifier`'s job — but
it does refuse unknown operation kinds).
The realizer is the ADR-0114a Obligation #5-compatible substrate
for ADR-0119's GSM8K eval lane: every "correct" answer in the lane
ships with a stepped explanation that traces to pack lemmas.
"""
from __future__ import annotations
import json
from dataclasses import dataclass
from typing import Any
from generate.math_solver import SolutionStep, SolutionTrace
class RealizerError(ValueError):
"""Raised on unrecognized operation kind or empty trace."""
@dataclass(frozen=True, slots=True)
class RealizedTrace:
"""Stepped explanation surface for a :class:`SolutionTrace`.
``setup_sentences`` introduce the initial state (one sentence per
:class:`InitialPossession`). ``step_sentences`` walk the trace in
order. ``answer_sentence`` states the final resolved unknown.
``canonical_bytes()`` is byte-deterministic so two realizations of
the same trace produce the same SHA-256.
"""
setup_sentences: tuple[str, ...]
step_sentences: tuple[str, ...]
answer_sentence: str
pack_id: str
def as_json(self) -> dict[str, Any]:
return {
"setup_sentences": list(self.setup_sentences),
"step_sentences": list(self.step_sentences),
"answer_sentence": self.answer_sentence,
"pack_id": self.pack_id,
}
def canonical_bytes(self) -> bytes:
return json.dumps(
self.as_json(), sort_keys=True, separators=(",", ":")
).encode("utf-8")
def as_prose(self) -> str:
"""Join setup + step + answer sentences into one paragraph."""
sentences = list(self.setup_sentences) + list(self.step_sentences)
sentences.append(self.answer_sentence)
return " ".join(sentences)
def realize(graph_initial_state: tuple, trace: SolutionTrace) -> RealizedTrace:
"""Render a :class:`SolutionTrace` as show-your-work prose.
``graph_initial_state`` is the input graph's ``initial_state`` tuple
(used to introduce the entities and their starting quantities).
``trace`` provides the per-step records and the resolved answer.
Pure function; same inputs → byte-identical output. Raises
:class:`RealizerError` on empty traces or unrecognized step kinds.
"""
if not isinstance(trace, SolutionTrace):
raise RealizerError(
f"trace must be a SolutionTrace, got {type(trace).__name__}"
)
setup_sentences = tuple(
_setup_sentence(p.entity, p.quantity.value, p.quantity.unit)
for p in graph_initial_state
)
step_sentences: list[str] = []
for step in trace.steps:
step_sentences.append(_step_sentence(step))
answer_sentence = _answer_sentence(
trace.answer_entity, trace.answer_value, trace.answer_unit
)
return RealizedTrace(
setup_sentences=setup_sentences,
step_sentences=tuple(step_sentences),
answer_sentence=answer_sentence,
pack_id=trace.pack_id,
)
def _setup_sentence(entity: str, value: int | float, unit: str) -> str:
return f"{entity} has {_render_number(value)} {_unit_surface(unit, value)}."
def _step_sentence(step: SolutionStep) -> str:
if step.operation_kind == "add":
return (
f"{step.actor} buys {_render_number(step.operand.value)} more "
f"{_unit_surface(step.operand.unit, step.operand.value)}, "
f"raising the total to {_render_number(step.after_value)}."
)
if step.operation_kind == "subtract":
return (
f"{step.actor} loses {_render_number(step.operand.value)} "
f"{_unit_surface(step.operand.unit, step.operand.value)}, "
f"leaving {_render_number(step.after_value)}."
)
if step.operation_kind == "transfer":
if step.target is None:
raise RealizerError(
f"transfer step {step.step_index} missing target"
)
return (
f"{step.actor} gives {_render_number(step.operand.value)} "
f"{_unit_surface(step.operand.unit, step.operand.value)} to "
f"{step.target}, leaving {step.actor} with "
f"{_render_number(step.after_value)}."
)
if step.operation_kind == "multiply":
verb = "doubles" if step.operand.value == 2 else (
"triples" if step.operand.value == 3 else "multiplies"
)
if verb == "multiplies":
return (
f"{step.actor} multiplies their "
f"{_unit_surface(step.operand.unit, 2)} by "
f"{_render_number(step.operand.value)}, "
f"reaching {_render_number(step.after_value)}."
)
return (
f"{step.actor} {verb} their "
f"{_unit_surface(step.operand.unit, 2)}, "
f"reaching {_render_number(step.after_value)}."
)
if step.operation_kind == "divide":
return (
f"{step.actor} splits their "
f"{_unit_surface(step.operand.unit, 2)} evenly into "
f"{_render_number(step.operand.value)} groups and keeps one "
f"group, leaving {_render_number(step.after_value)}."
)
raise RealizerError(
f"step {step.step_index} has unknown operation_kind "
f"{step.operation_kind!r}"
)
def _answer_sentence(
entity: str | None, value: int | float, unit: str
) -> str:
if entity is None:
return (
f"In total, they have {_render_number(value)} "
f"{_unit_surface(unit, value)}."
)
return (
f"{entity} has {_render_number(value)} "
f"{_unit_surface(unit, value)}."
)
def _render_number(value: int | float) -> str:
"""Render numeric value preferring integer form when exact."""
if isinstance(value, bool):
# bool is a subclass of int — refuse explicitly
raise RealizerError(f"cannot render boolean as number: {value!r}")
if isinstance(value, float) and value.is_integer():
return str(int(value))
return str(value)
def _unit_surface(unit: str, value: int | float) -> str:
"""Render a unit string in surface form.
Quantities of exactly 1 take the singular; all others keep the
canonical plural. This matches the parser's
``_canonical_unit`` round-trip — the parser maps singular surfaces
back to plural at graph time.
"""
if value == 1:
return _singular(unit)
return unit
def _singular(unit: str) -> str:
if unit.endswith("ies") and len(unit) > 3:
return unit[:-3] + "y"
if unit.endswith("es") and len(unit) > 2 and unit[-3:-2] in {"s", "x", "z"}:
return unit[:-2]
if unit.endswith("s") and not unit.endswith("ss"):
return unit[:-1]
return unit

167
tests/test_math_realizer.py Normal file
View file

@ -0,0 +1,167 @@
"""ADR-0118 — stepped realizer invariants.
Pins five load-bearing invariants:
1. **Every dev-set case realizes.** All 50 cases produce a
:class:`RealizedTrace` without raising.
2. **Determinism.** Same trace produces byte-equal RealizedTrace bytes
across two calls.
3. **Setup sentences cover every entity with initial state.** One
setup sentence per :class:`InitialPossession`.
4. **Step sentence count equals operation count.** Exactly one step
sentence per :class:`SolutionStep`.
5. **Answer sentence contains the resolved answer value.** Both
numeric value and unit appear in the answer sentence.
Round-trip parseability of the rendered prose is **out of scope for
ADR-0118**; the trace is the verifiable artifact (ADR-0117), the
realizer's prose is human-readable documentation.
"""
from __future__ import annotations
import json
from pathlib import Path
import pytest
from generate.math_parser import parse_problem
from generate.math_realizer import RealizedTrace, RealizerError, realize
from generate.math_solver import REQUIRED_PACK_ID, solve
_REPO_ROOT = Path(__file__).resolve().parent.parent
_CASES_PATH = _REPO_ROOT / "evals" / "gsm8k_parser_dev" / "cases.jsonl"
def _load_cases() -> list[dict]:
return [
json.loads(line) for line in _CASES_PATH.read_text().splitlines() if line.strip()
]
def _build(case: dict) -> tuple:
graph = parse_problem(case["problem"])
trace = solve(graph)
return graph, trace
class TestAllDevSetCasesRealize:
@pytest.mark.parametrize("case", _load_cases(), ids=lambda c: c["id"])
def test_realizes_without_error(self, case: dict) -> None:
graph, trace = _build(case)
result = realize(graph.initial_state, trace)
assert isinstance(result, RealizedTrace)
assert result.pack_id == REQUIRED_PACK_ID
class TestDeterminism:
@pytest.mark.parametrize("case", _load_cases(), ids=lambda c: c["id"])
def test_two_realizations_produce_byte_equal_output(self, case: dict) -> None:
graph, trace = _build(case)
a = realize(graph.initial_state, trace)
b = realize(graph.initial_state, trace)
assert a.canonical_bytes() == b.canonical_bytes()
class TestSetupSentenceCoverage:
@pytest.mark.parametrize("case", _load_cases(), ids=lambda c: c["id"])
def test_one_setup_sentence_per_initial_possession(self, case: dict) -> None:
graph, trace = _build(case)
result = realize(graph.initial_state, trace)
assert len(result.setup_sentences) == len(graph.initial_state)
class TestStepSentenceCoverage:
@pytest.mark.parametrize("case", _load_cases(), ids=lambda c: c["id"])
def test_one_step_sentence_per_operation(self, case: dict) -> None:
graph, trace = _build(case)
result = realize(graph.initial_state, trace)
assert len(result.step_sentences) == len(trace.steps)
class TestAnswerSentenceContainsResolvedAnswer:
@pytest.mark.parametrize("case", _load_cases(), ids=lambda c: c["id"])
def test_answer_value_and_unit_appear_in_answer_sentence(
self, case: dict
) -> None:
graph, trace = _build(case)
result = realize(graph.initial_state, trace)
# numeric value (allow integer form when value is integral)
if isinstance(trace.answer_value, float) and trace.answer_value.is_integer():
expected_num = str(int(trace.answer_value))
else:
expected_num = str(trace.answer_value)
assert expected_num in result.answer_sentence, (
f"answer value {expected_num!r} not in {result.answer_sentence!r}"
)
# unit (allow singular surface when value == 1)
if trace.answer_value == 1:
# singular check is approximate; the unit-stem must be in there
stem = trace.answer_unit.rstrip("s")
assert stem in result.answer_sentence
else:
assert trace.answer_unit in result.answer_sentence
class TestRealizerRefuses:
def test_non_solution_trace_input_raises(self) -> None:
with pytest.raises(RealizerError):
realize((), object()) # type: ignore[arg-type]
class TestProseSurface:
def test_simple_case_prose_is_readable(self) -> None:
graph, trace = _build(
{"problem": "Sam has 5 apples. He buys 3 more. How many apples does Sam have?"}
)
result = realize(graph.initial_state, trace)
prose = result.as_prose()
# Should mention the actor, the operand quantity, and the answer
assert "Sam" in prose
assert "5 apples" in prose
assert "3" in prose
assert "8" in prose
def test_transfer_case_mentions_target(self) -> None:
graph, trace = _build(
{
"problem": (
"Anna has 8 marbles. She gives 3 to Ben. "
"How many marbles does Anna have now?"
)
}
)
result = realize(graph.initial_state, trace)
prose = result.as_prose()
assert "Anna" in prose
assert "Ben" in prose
assert "3" in prose
assert "5" in prose
def test_total_across_question_uses_collective_phrasing(self) -> None:
graph, trace = _build(
{
"problem": (
"Tom has 4 stickers. Sara has 7 stickers. "
"How many stickers do they have in total?"
)
}
)
result = realize(graph.initial_state, trace)
assert "they have" in result.answer_sentence.lower() or "in total" in result.answer_sentence.lower()
assert "11" in result.answer_sentence
class TestPackIdPropagates:
@pytest.mark.parametrize("case", _load_cases()[:5], ids=lambda c: c["id"])
def test_realized_trace_carries_same_pack_id_as_solution_trace(
self, case: dict
) -> None:
graph, trace = _build(case)
result = realize(graph.initial_state, trace)
assert result.pack_id == trace.pack_id == REQUIRED_PACK_ID