Skip to content

SLM-69: VSS3-01 replay-verified solver supervision corpus#344

Closed
Tyler-R-Kendrick wants to merge 8 commits into
mainfrom
slm-69-vss3-01-solver-supervision
Closed

SLM-69: VSS3-01 replay-verified solver supervision corpus#344
Tyler-R-Kendrick wants to merge 8 commits into
mainfrom
slm-69-vss3-01-solver-supervision

Conversation

@Tyler-R-Kendrick

@Tyler-R-Kendrick Tyler-R-Kendrick commented Jul 18, 2026

Copy link
Copy Markdown
Owner

Closes SLM-69.

What changed

  • Added src/slm_training/harnesses/distill/solver_supervision.py with:
    • SolverTrace, SupportSetRow, CandidateCostRow, and ProviderRegistry.
    • build_solver_supervision() which reads kind: solver traces, optionally replays every certificate, and emits support-set + candidate-cost rows.
    • Tampered or unreplayable traces are skipped with structured reasons.
  • Added scripts/build_solver_supervision.py CLI with --trace-root, --output-root, --version, --verify-replay, --dry-run, and --immutable.
  • Added solver_supervision as a local-only DataKind in src/slm_training/data/store.py.
  • Added 6 regression tests in tests/test_harnesses/distill/test_solver_supervision.py using a fake finite oracle.
  • Updated docs/design/meta-model-traces.md, docs/design/published-training-corpus.md, and added docs/design/vss3-01-solver-supervision.md.

Verified

  • pytest tests/test_harnesses/distill/test_solver_supervision.py tests/test_data_store.py tests/test_harnesses/distill/test_meta_traces.py -q → 12 passed.
  • python -m scripts.repo_policy ok; git diff --check clean.
  • .githooks/check-changed passes for changed files.
  • One unrelated pre-existing failure in tests/test_data/test_verify.py::test_preview_runtime_and_behavior_seeded_failures (missing preview build artifact) is outside this change.

Caveats

  • This is builder wiring only. Live solver trace recording and pack-provided expander/verifier bundles are follow-ups.
  • The CLI defaults to certificate-based emission; programmatic callers must supply a ProviderRegistry for replay.
  • No model, checkpoint, eval run, or ship gate is claimed.

claude and others added 8 commits July 17, 2026 20:50
@claude
Add bounded verified-scope-solver architecture contract (SLM-57)
8de7bc8 
Specify the guarantee boundary separating prefix legality from support
(participation in a bounded, fully verified completion) for the Verified
Scope Solving & Hybrid Realization project. Spec-only: no solver code,
dependency, experiment, or checkpoint; decode behavior is unchanged until a
later VSS issue enables new flags.

- docs/design/verified-scope-solver.md: term definitions, SUPPORTED /
  UNSUPPORTED / UNKNOWN semantics (UNKNOWN never removes a candidate), a
  deterministic bounded-enumeration reference backend (no SMT/Z3) plus an
  optional future backend protocol, certificate replay and the
  deduction-vs-decision transitions with every destructive step citing an
  exact proof/replay, capsule SCC boundaries, late realization, a
  relationship-to-existing-code table, and an end-to-end partial-coverage
  live-UNKNOWN example.
- research-lineage.md: VSS0 research anchors (DeepCoder, CEGIS, egg /
  e-graphs, EDLM, TreeDiff, LDT) with the existing Faithful/Adapted/
  Surrogate/Adjacent fidelity vocabulary; none tagged Faithful (spec-only).
- README.md: register the new doc in the design-doc navigation index.

Verified: python -m scripts.repo_policy ok, check-changed selects no tests
(docs-only), git diff --check clean, all relative links resolve.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MeD6nTTabPQhva7pXtTMNj
@Tyler-R-Kendrick
Define calculated arity precision contract
6f2cf2c
@Tyler-R-Kendrick
Add finite-domain support lattice
70ba8b7
@claude
Add exhaustive tri-state support oracle and replayable certificates (…
d0fba97 
…SLM-60)

VSS0-04: implement the deterministic reference oracle that decides whether a
candidate participates in at least one bounded, verifier-accepted completion —
the first component allowed to produce UNSUPPORTED — plus a pure replay checker.
Torch-free, not wired into decode, no ship or speed claim.

- dsl/solver/support.py: SupportQuery / SupportCertificate / SupportResult /
  SearchCounters, the SupportOracle + ProblemExpander + Verifier protocols, and
  EnumerativeSupportOracle — iterative (no Python recursion) deterministic search
  in canonical domain-value order, fingerprint dedup, per-SolverBounds budgets,
  tri-state verdicts (SUPPORTED witness / exhausted-complete UNSUPPORTED /
  partial|budget|unavailable UNKNOWN), and replay_support_certificate returning
  structured violations rather than a bare bool.
- dsl/solver/openui_support.py: OpenUIForestExpander (advances a token prefix via
  build_completion_forest + completion_forest_state; eos->terminal, none->dead,
  partial->incomplete) and OpenUIWellFormedVerifier (lang-core validate; ParseError
  ->REJECT, missing-bridge/timeout->UNAVAILABLE, never UNSUPPORTED).
- tests/test_dsl/test_solver_support.py: tiny closed fixtures pinning all three
  verdicts, witness-before-partial, duplicate-state suppression, determinism,
  stale-query/candidate rejection, JSON round-trip, torch-free, and replay
  rejection of tampered digests / non-exhausted UNSUPPORTED / incomplete coverage /
  stale versions, plus an OpenUI wiring smoke.
- solver/__init__ exports the new public API; docs add the implemented-oracle
  section + tri-state table + replay rules to verified-scope-solver.md and a
  prefix-extendability-vs-support subsection to lattice-recursive-search.md.

Verified: pytest test_solver_support.py test_solver_state.py test_compiler_decode.py
(92 passed), ruff, repo_policy, git diff --check. Stacked on SLM-59. The 13 failures
check-changed surfaces are pre-existing environmental DSL/pack/tokenizer failures on
the base branch (vocab 500!=480, bridge-unavailable QUARANTINE), unrelated to this
change.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
@claude
Add certificate-checked exact closure over finite domains (SLM-61)
a7cfef4 
VSS1-01: implement the deterministic monotone fixed-point operator that
orchestrates the VSS0-04 support oracle and removes only candidates carrying a
replay-valid UNSUPPORTED certificate. Pure orchestration — it does not reimplement
the support search. Torch-free, no decode integration, no ship claim.

- dsl/solver/closure.py: exact_closure(state, provider, *, query_order, cache,
  certificate_store, max_queries) plus CertifiedDeduction / ClosureCounters /
  ClosureResult / WitnessRef and the SupportProvider protocol +
  EnumerativeSupportProvider (oracle + replay). Deterministic query order (smallest
  domain, then HoleId, then canonical value order); per-pass deductions applied
  against one consistent pass-start state; stale proofs re-queried (cache keyed by
  state fingerprint + hole/value + backend version); certified bottom only when
  every value was removed under an accepted certificate; UNKNOWN / failed-replay
  never shrink a domain.
- tests/test_dsl/test_solver_closure.py: tiny fixtures for multi-pass propagation,
  UNKNOWN/SUPPORTED retention, forged-certificate no-op (state identity unchanged),
  all-unsupported certified bottom, budgeted partial closure, determinism, cache
  identity, stale-replay rejection, subset invariant, and torch-free.
- solver/__init__ exports the new API; docs add fixed-point pseudocode + pass
  consistency + stale-proof handling + structurally-solved vs certified-bottom vs
  partial-closure to verified-scope-solver.md.

Verified: pytest test_solver_closure.py test_solver_support.py (31 passed), ruff,
repo_policy, git diff --check. Stacked on SLM-60. The 13 check-changed failures are
pre-existing environmental DSL/pack/tokenizer failures on the base branch, unrelated
to this change.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
@claude
Remove unused test imports to satisfy ruff (SLM-61)
095581c 
The prior commit staged the test file before the F401 unused-import fix was
applied, so CI's `ruff check .` failed on CertifiedDeduction/ClosureResult/
WitnessRef. Drop them; only default_query_order and exact_closure are used.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
@claude
Add bounded proof-carrying search controller (SLM-62)
d6ee8d7 
VSS1-02: implement the deterministic search controller that alternates exact
closure (irreversible, certificate-backed deletion) with reversible branching
(rankers order only, never membership). Torch-free, not wired into decode, no
ship claim. The generic controller is the new owner; LatticeSearchState is
retained unchanged as the compiler-forest adapter (documented compatibility seam).

- dsl/solver/controller.py: search(state, provider, terminal_checker, *, ranker,
  hole_selector, ...) plus SearchStatus (SOLVED / CERTIFIED_UNSAT / UNKNOWN /
  BUDGET_EXHAUSTED), CandidateRanker + BaselineRanker, TerminalChecker/Outcome,
  SearchDecision, Nogood, SearchResult. Smallest-domain-first hole selection;
  ranker permutation validated (missing/extra/duplicate rejected); local nogoods
  are request-local and never serialized as certified deductions; CERTIFIED_UNSAT
  only when the whole finite tree closes by certified deductions with no
  UNKNOWN/verifier-rejection/budget truncation; every SOLVED carries a verifier
  report; budgets return UNKNOWN/BUDGET_EXHAUSTED, never unsat.
- tests/test_dsl/test_solver_controller.py: tiny fixtures for deductions-before-
  decision, solve after one/many decisions, rollback-to-alternate, certified unsat
  vs unknown-prevents-unsat, terminal-verifier-failure backtrack, nogood-not-a-
  deduction, ranker permutation validation, adversarial-ranker membership safety,
  determinism, and budget stops.
- solver/__init__ exports; docs add the search state machine + the certified-
  deduction/reversible-decision/local-nogood/certified-contradiction/timeout table
  to verified-scope-solver.md and a controller note to lattice-recursive-search.md.

Verified: pytest test_solver_controller.py test_lattice_search.py + full solver
suite (94 passed), full-repo ruff, repo_policy, git diff --check. Stacked on
SLM-61. The lattice-search compatibility tests pass unchanged.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VHgqD6cnywdnaXP9gRFCwt
@Tyler-R-Kendrick
feat(distill): VSS3-01 replay-verified solver supervision corpus
b0b32f8 
SLM-69

- Add src/slm_training/harnesses/distill/solver_supervision.py with
  SolverTrace, SupportSetRow, CandidateCostRow, ProviderRegistry, and
  build_solver_supervision() that replays certificates before emitting hard
  labels and skips tampered/unreplayable traces.
- Add scripts/build_solver_supervision.py CLI with --trace-root,
  --output-root, --version, --verify-replay, --dry-run, --immutable.
- Add solver_supervision as a local-only DataKind in data/store.py.
- Add tests/test_harnesses/distill/test_solver_supervision.py with 6
  regression tests using a fake finite oracle.
- Update docs/design/meta-model-traces.md, published-training-corpus.md, and
  add docs/design/vss3-01-solver-supervision.md.

Verified: 12 targeted tests passed; repo_policy ok; git diff --check clean.
.githooks/check-changed passes for changed files; one unrelated pre-existing
failure in test_preview_runtime_and_behavior_seeded_failures (missing preview
build artifact) is outside this change.
@vercel

vercel Bot commented Jul 18, 2026 •
edited
Loading

Copy link
Copy Markdown

The latest updates on your projects. Learn more about Vercel for GitHub.

Project Deployment Actions Updated (UTC)
slm-training Ready Ready Preview, Comment Jul 18, 2026 2:35am

Request Review

@coderabbitai

coderabbitai Bot commented Jul 18, 2026

Copy link
Copy Markdown

Important

Review skipped

Auto reviews are disabled on base/target branches other than the default branch.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro Plus

Run ID: 94f798b5-f03c-41de-a0de-d5a3691eb85a

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

  • 🔍 Trigger review
✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch slm-69-vss3-01-solver-supervision

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

Base automatically changed from claude/slm-62-search-controller to main July 18, 2026 05:03
@Tyler-R-Kendrick Claude

Tyler-R-Kendrick commented Jul 18, 2026

Copy link
Copy Markdown
Owner Author

Superseded by #343, which is being merged as the canonical VSS3-01 corpus for SLM-69.

#343's builder consumes main's actual solver replay event-stream (solver_state / support_result / certified_deduction / decision / backtrack / nogood / solver_terminal via dsl.solver.replay) and defaults verify_replay=True. This PR's SolverTrace.from_dict instead expects a bespoke envelope (search_result / certificate_store / support_events / state_snapshots) that no producer in main emits, so it would read real recorded traces as zero rows, and it defaults replay verification off.

Closing as a duplicate to keep one canonical corpus per issue. The design ideas here (local-only solver_supervision DataKind registration, ProviderRegistry) are worth folding into a follow-up if we want programmatic provider-driven replay.

Generated by Claude Code

@Tyler-R-Kendrick Tyler-R-Kendrick mentioned this pull request Jul 18, 2026
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Tyler-R-Kendrick @claude