diff --git a/docs/MODEL_CARD.md b/docs/MODEL_CARD.md index aa76aeb1..f2530c6e 100644 --- a/docs/MODEL_CARD.md +++ b/docs/MODEL_CARD.md @@ -137,6 +137,7 @@ scratch-matrix clears as production readiness; silent gold-placeholder channels. | Output tokenizer | Compositional `OpenUITokenizer` (default) or V5 lexer (`DSLNativeTokenizer`) | | Decode | Grammar-constrained LTR / MaskGIT + repair levers (see design docs) | | Topology experiment | `grammar_diffusion` v2: typed production-tree expansion/contraction with bounded active nodes; no fixed canvas | +| Verified-solver decode | `verified_solver_decode` (VSS1-03) **off by default**: opt-in certificate-checked exact-closure pruning of the compiler-tree forest before soft ranking, on the DSL-native path only. **Experimental and unmeasured — no checkpoint uses it and it carries no ship/quality claim** ([config glossary](design/quality-experiment-matrix.md#configuration-glossary--verified-solver-decode-vss1-03)). | | Eval gates | Multi-suite `--ship-gates` (parse, structural, `placeholder_fidelity`, reward) | --- diff --git a/docs/design/lattice-recursive-search.md b/docs/design/lattice-recursive-search.md index 79095c04..5c03a78e 100644 --- a/docs/design/lattice-recursive-search.md +++ b/docs/design/lattice-recursive-search.md @@ -80,6 +80,25 @@ retained compiler-forest adapter and is unchanged. The full state machine and th certified-deduction / reversible-decision / local-nogood / certified-contradiction / timeout table live in [verified-scope-solver.md](verified-scope-solver.md). Not wired into decode. + +### Decode integration behind a flag (VSS1-03) + +[`dsl/solver/decode.py`](../../src/slm_training/dsl/solver/decode.py) +`solver_prune` and [`models/twotower.py`](../../src/slm_training/models/twotower.py) +`_solver_prune_forest` finally wire this hard/soft split into the compiler-tree +lattice decode: inside `_compiler_ltr_decode_one`, right after +`build_completion_forest`, the authoritative forest is projected to a +`FiniteDomainState`, exact closure runs, and the forest is pruned to the +certificate-checked live subset **before** `rank_forest` scores anything. So a +learned ranker only ever reorders candidates that survived certified deduction; it +can neither reintroduce a certified-removed path (survivors are a subset that keeps +`CompletionPath` identity and forest order) nor rescue an `UNKNOWN` into removal +(`keep_and_rank` keeps it live). A certified bottom empties the forest and reuses +the existing `LatticeSearchState` rollback rather than emitting an unverified +fallback. The whole seam is gated by `verified_solver_decode` (**default off**); +off, the lattice decode and its stats/trace output are byte-identical, so the V9 +campaign rows and all measured results below are unaffected. The enabled path is +**unmeasured** — no new campaign row, checkpoint, or ship claim. ## Constraint evidence (VSS0-02) The hard-lattice projection can now explain itself. `build_completion_forest(..., diff --git a/docs/design/quality-experiment-matrix.md b/docs/design/quality-experiment-matrix.md index cd527146..42ccdd1b 100644 --- a/docs/design/quality-experiment-matrix.md +++ b/docs/design/quality-experiment-matrix.md @@ -149,6 +149,35 @@ python -m scripts.train_rl \ python -m scripts.bench_telemetry --train-steps 8 --gen-prompts 8 ``` +## Configuration glossary — verified-solver decode (VSS1-03) + +Experimental, **disabled by default**, and **unmeasured**. These flags gate the +certificate-checked exact-closure pruning of the compiler-tree forest before soft +ranking (`docs/design/verified-scope-solver.md` → "Implemented decode +integration"). They are **not** part of any honest gate, champion recipe, or +matrix row; no row above enables them, and the honest ship policy +(`STRICT_COMPILER_TREE_POLICY`) does not set them. Enabling changes decode +behavior only for the semantic choice/compiler path on a DSL-native pack; an +unsupported tokenizer/pack raises a capability error. + +| Flag (`TwoTowerConfig` / `ModelBuildConfig`) | CLI (`evaluate_model.py`) | Default | Meaning | +| --- | --- | --- | --- | +| `verified_solver_decode` | `--verified-solver-decode` | `False` | Master switch. Off ⇒ decode is byte-identical to today. | +| `solver_max_nodes` | `--solver-max-nodes` | `512` | Enumeration node budget per decision (also bounds the token budget). | +| `solver_max_depth` | — (config/checkpoint) | `64` | Search depth budget. | +| `solver_max_backtracks` | — (config/checkpoint) | `64` | Backtrack budget. | +| `solver_max_verifier_calls` | — (config/checkpoint) | `64` | Verifier-call budget. | +| `solver_max_wall_ms` | — (config/checkpoint) | `0` | `0` = no wall timer; deterministic budgets stay authoritative. | +| `solver_unknown_policy` | `--solver-unknown-policy` | `keep_and_rank` | Only supported value: `UNKNOWN` candidates stay live for the soft ranker. | +| `solver_certificate_mode` | `--solver-certificate-mode` | `summary` | `none \| summary \| full` certificate detail. | + +```bash +# Opt-in solver-pruned decode on the honest compiler-tree path (experimental). +python -m scripts.evaluate_model --checkpoint \ + --verified-solver-decode --solver-max-nodes 512 \ + --solver-unknown-policy keep_and_rank --solver-certificate-mode summary +``` + ## Measured results (CPU, 800 steps, scratch, no DESIGN.md in context) See [quality-matrix-results.json](quality-matrix-results.json). Headline deltas vs ship memorizer: diff --git a/docs/design/verified-scope-solver.md b/docs/design/verified-scope-solver.md index b760ae0b..1e0e71a5 100644 --- a/docs/design/verified-scope-solver.md +++ b/docs/design/verified-scope-solver.md @@ -290,6 +290,65 @@ controller validates the returned sequence is a permutation and rejects any missing/extra/duplicate); `CERTIFIED_UNSAT` is impossible when any required branch was UNKNOWN or budget-truncated; every `SOLVED` carries a final verifier report. +## Implemented decode integration (VSS1-03 / SLM-63) + +[`dsl/solver/decode.py`](../../src/slm_training/dsl/solver/decode.py) adds +`solver_prune(forest, prefix_ids, provider, ...)`, and +[`models/twotower.py`](../../src/slm_training/models/twotower.py) +`_solver_prune_forest` wires it into the compiler-tree / choice decode loop +(`_compiler_ltr_decode_one`, right after `build_completion_forest`). It is gated +by eight backward-compatible, **disabled-by-default** config fields +(`verified_solver_decode=False`, `solver_max_nodes`, `solver_max_depth`, +`solver_max_backtracks`, `solver_max_verifier_calls`, `solver_max_wall_ms`, +`solver_unknown_policy="keep_and_rank"`, `solver_certificate_mode`) on +`TwoTowerConfig` / `ModelBuildConfig`; missing fields on existing checkpoints take +the defaults, so the flag round-trips through config/CLI/checkpoint metadata +without adding a model parameter. + +Per decode decision, when the flag is on and the forest is authoritative: + +```text +forest = build_completion_forest(prefix) # unchanged; the authoritative set +if forest.coverage != "complete" or not forest.paths: + return forest # closure is authoritative only over exhaustive coverage +state = completion_forest_state(prefix, forest, pack, cv, bounds) # one-hole projection +result = exact_closure(state, provider) # VSS1-01 certified fixed point +removed = {v for v in state.domain} - {v for v in result.survivors} # certified-removed only +forest' = forest keep-order minus paths whose (kind, token_ids) in removed +``` + +Honesty invariants this seam preserves (owned here): + +- **Subset, identity-preserving.** A surviving path is an original + `CompletionPath` object (full path identity and forced suffixes intact); the + order is the original forest order. Closure may only *remove*; it never invents + a candidate the forest lacked, so a later soft ranker (logits) can never + reintroduce a certified-removed candidate — it is simply absent. +- **Removal needs a replay-valid certificate.** A candidate is dropped only when + it was in the closure input domain and got certified `UNSUPPORTED` + (`removed = input_domain − survivors`); the closure re-checks each certificate + before applying it. `UNKNOWN` (partial coverage / unavailable capability / + budget) is always kept — `keep_and_rank` is the only supported policy. +- **Certified bottom ≠ fallback.** When every candidate is certified + `UNSUPPORTED`, the pruned forest is **empty**, and the existing decode + dead-end/rollback path handles it — never an unverified fallback emission. +- **Capability error, not a silent weaker path.** With the flag on, an + unsupported tokenizer/pack (`is_dsl_native_tokenizer` false) raises a clear + `ValueError` instead of quietly decoding without the solver while reporting + solver mode. +- **Model-independent enumeration.** `decode.py` is Torch-free; support + enumeration runs no denoiser forward. The reference oracle order is + model-independent; the model scores only the surviving live set afterward. + +With `verified_solver_decode=False` the seam is skipped entirely (a single +`getattr` guard), so default decode is byte-identical — pinned by +`tests/test_models/test_solver_decode_integration.py` (fixed seed/fixture parity) +and the unchanged `tests/test_models/test_compiler_decode.py`. Core +removal/keep/bottom/coverage semantics are pinned Torch-free by +`tests/test_dsl/test_solver_decode.py`. **No train, eval, benchmark, checkpoint, +or experiment ran; the enabled path is unmeasured and this makes no correctness, +readiness, speed, or ship claim.** + ## Reference support semantics | Verdict | Requirement | Removal permitted? | diff --git a/scripts/evaluate_model.py b/scripts/evaluate_model.py index 4e192a08..79c7902d 100644 --- a/scripts/evaluate_model.py +++ b/scripts/evaluate_model.py @@ -214,6 +214,20 @@ def main(argv: list[str] | None = None) -> int: parser.add_argument("--compiler-search-noise", type=float, default=0.0) parser.add_argument("--compiler-search-stagnation-patience", type=int, default=2) parser.add_argument("--compiler-search-backtrack-limit", type=int, default=8) + parser.add_argument( + "--verified-solver-decode", + action="store_true", + help="VSS1-03: prune the compiler forest via certified exact closure before ranking", + ) + parser.add_argument("--solver-max-nodes", type=int, default=512) + parser.add_argument( + "--solver-unknown-policy", choices=("keep_and_rank",), default="keep_and_rank" + ) + parser.add_argument( + "--solver-certificate-mode", + choices=("none", "summary", "full"), + default="summary", + ) parser.add_argument( "--schema-in-context", action="store_true", @@ -414,6 +428,10 @@ def main(argv: list[str] | None = None) -> int: grammar_verify_chosen_only=(True if args.verify_chosen_only else None), grammar_top_k=args.grammar_top_k, compiler_decode_mode=args.compiler_decode_mode, + verified_solver_decode=args.verified_solver_decode, + solver_max_nodes=args.solver_max_nodes, + solver_unknown_policy=args.solver_unknown_policy, + solver_certificate_mode=args.solver_certificate_mode, component_inventory_decode_weight=args.component_inventory_decode_weight, component_plan_decode_weight=args.component_plan_decode_weight, component_edge_decode_weight=args.component_edge_decode_weight, diff --git a/src/slm_training/dsl/solver/decode.py b/src/slm_training/dsl/solver/decode.py new file mode 100644 index 00000000..77d1e97f --- /dev/null +++ b/src/slm_training/dsl/solver/decode.py @@ -0,0 +1,93 @@ +"""Decode-time forest pruning via certificate-checked exact closure (VSS1-03). + +`solver_prune` adapts an authoritative :class:`CompletionForest` to a +:class:`FiniteDomainState`, runs exact closure, and returns the forest pruned to +the **certificate-checked live subset** — a subset of the original paths that +preserves full path identity/forced suffixes and the original forest order. + +Honesty invariants (owned by ``docs/design/verified-scope-solver.md``): + +* it only prunes when ``forest.coverage == "complete"`` — closure is authoritative + only over an exhaustive candidate set; a ``partial``/``none`` forest is returned + unchanged; +* ``UNKNOWN`` candidates are always kept (``keep_and_rank``); only replay-valid + ``UNSUPPORTED`` candidates are dropped, so a later soft ranker (logits) can never + reintroduce a removed candidate — it is simply absent from the pruned forest; +* a certified bottom yields an **empty** pruned forest, letting the existing decode + dead-end/rollback path handle it rather than returning an unverified fallback. + +This module is Torch-free and is **not** invoked by default decode — the caller +gates it behind a disabled-by-default flag. +""" + +from __future__ import annotations + +from slm_training.dsl.grammar.fastpath.compiler_draft import CompletionForest +from slm_training.dsl.solver.adapters import completion_forest_state +from slm_training.dsl.solver.closure import ClosureResult, SupportProvider, exact_closure +from slm_training.dsl.solver.state import SolverBounds +from slm_training.dsl.solver.support import SupportCertificate + +UNKNOWN_POLICIES = ("keep_and_rank",) + + +def _value_key(value) -> tuple[str, tuple[int, ...]]: + payload = value.payload + return ( + str(payload.get("kind", "")), + tuple(int(token) for token in payload.get("token_ids", ())), + ) + + +def solver_prune( + forest: CompletionForest, + prefix_ids, + provider: SupportProvider, + *, + pack_id: str, + constraint_version: str, + bounds: SolverBounds, + unknown_policy: str = "keep_and_rank", + state=None, + cache: dict | None = None, + certificate_store: dict[str, SupportCertificate] | None = None, +) -> tuple[CompletionForest, ClosureResult | None]: + """Return ``(pruned_forest, closure_result)`` for one decode decision. + + A forest path is removed **only** when it was in the closure's input domain and + got certified-removed (``removed = original_domain − survivors``); a candidate + the oracle never considered is always kept. ``state`` may be a pre-built + projection (e.g. the provider's own root state) so fingerprints line up with + the oracle; when ``None`` it is projected from ``forest``. ``closure_result`` is + ``None`` when no closure ran (non-``complete`` coverage or empty forest). + """ + if unknown_policy not in UNKNOWN_POLICIES: + raise ValueError(f"unsupported solver_unknown_policy: {unknown_policy!r}") + if forest.coverage != "complete" or not forest.paths: + return forest, None + + if state is None: + state = completion_forest_state( + prefix_ids=tuple(int(token) for token in prefix_ids), + forest=forest, + pack_id=pack_id, + constraint_version=constraint_version, + bounds=bounds, + ) + result = exact_closure( + state, provider, cache=cache, certificate_store=certificate_store + ) + original = state.holes[0].values if state.holes else () + survivors = result.state.holes[0].values if result.state.holes else () + # Only paths the closure actually certified-removed are dropped. + removed_keys = {_value_key(v) for v in original} - {_value_key(v) for v in survivors} + if not removed_keys: + return forest, result # nothing certified-removed -> keep identity + ordered = tuple( + path + for path in forest.paths + if (path.kind, tuple(path.token_ids)) not in removed_keys + ) + if len(ordered) == len(forest.paths): + return forest, result + return CompletionForest(ordered, forest.coverage, forest.terminals), result diff --git a/src/slm_training/harnesses/model_build/config.py b/src/slm_training/harnesses/model_build/config.py index e1a00a56..93e96524 100644 --- a/src/slm_training/harnesses/model_build/config.py +++ b/src/slm_training/harnesses/model_build/config.py @@ -122,6 +122,15 @@ class ModelBuildConfig: compiler_search_stagnation_patience: int = 2 compiler_search_backtrack_limit: int = 8 compiler_search_local_nogoods: bool = False + # VSS1-03 certified-solver decode (disabled by default; decode-time only). + verified_solver_decode: bool = False + solver_max_nodes: int = 512 + solver_max_depth: int = 64 + solver_max_backtracks: int = 64 + solver_max_verifier_calls: int = 64 + solver_max_wall_ms: int = 0 + solver_unknown_policy: str = "keep_and_rank" + solver_certificate_mode: str = "summary" decode_min_content: int = 0 # A4: 0 off | >0 floor | -1 auto-from-inventory asap_decode: bool = False # A2: ASAp-style constraint-mass removal in MaskGIT fastpath_aux_weight: float = 0.0 diff --git a/src/slm_training/harnesses/model_build/factory.py b/src/slm_training/harnesses/model_build/factory.py index 9bee0ad2..5f075d73 100644 --- a/src/slm_training/harnesses/model_build/factory.py +++ b/src/slm_training/harnesses/model_build/factory.py @@ -71,6 +71,14 @@ def apply_runtime_overrides(model: Any, config: ModelBuildConfig) -> Any: "compiler_search_stagnation_patience", "compiler_search_backtrack_limit", "compiler_search_local_nogoods", + "verified_solver_decode", + "solver_max_nodes", + "solver_max_depth", + "solver_max_backtracks", + "solver_max_verifier_calls", + "solver_max_wall_ms", + "solver_unknown_policy", + "solver_certificate_mode", "decode_min_content", "asap_decode", "fastpath_aux_weight", @@ -295,6 +303,20 @@ def _twotower_config_from_build(config: ModelBuildConfig) -> "TwoTowerConfig": ), decode_min_content=max(-1, int(getattr(config, "decode_min_content", 0) or 0)), asap_decode=bool(getattr(config, "asap_decode", False)), + verified_solver_decode=bool(getattr(config, "verified_solver_decode", False)), + solver_max_nodes=int(getattr(config, "solver_max_nodes", 512) or 512), + solver_max_depth=int(getattr(config, "solver_max_depth", 64) or 64), + solver_max_backtracks=int(getattr(config, "solver_max_backtracks", 64) or 64), + solver_max_verifier_calls=int( + getattr(config, "solver_max_verifier_calls", 64) or 64 + ), + solver_max_wall_ms=int(getattr(config, "solver_max_wall_ms", 0) or 0), + solver_unknown_policy=str( + getattr(config, "solver_unknown_policy", "keep_and_rank") + ), + solver_certificate_mode=str( + getattr(config, "solver_certificate_mode", "summary") + ), fastpath_aux_weight=getattr(config, "fastpath_aux_weight", 0.0), fastpath_gate_threshold=float( getattr(config, "fastpath_gate_threshold", 0.5) or 0.5 diff --git a/src/slm_training/models/twotower.py b/src/slm_training/models/twotower.py index 34260926..acc96be8 100644 --- a/src/slm_training/models/twotower.py +++ b/src/slm_training/models/twotower.py @@ -282,6 +282,18 @@ class TwoTowerConfig: compiler_search_stagnation_patience: int = 2 compiler_search_backtrack_limit: int = 8 compiler_search_local_nogoods: bool = False + # VSS1-03 certified-solver decode: exact closure prunes the compiler forest to + # the certificate-checked live subset before soft ranking. Disabled by default; + # ``False`` is byte-identical to existing decode. Deterministic budgets are + # authoritative (wall timer is advisory only). + verified_solver_decode: bool = False + solver_max_nodes: int = 512 + solver_max_depth: int = 64 + solver_max_backtracks: int = 64 + solver_max_verifier_calls: int = 64 + solver_max_wall_ms: int = 0 + solver_unknown_policy: str = "keep_and_rank" + solver_certificate_mode: str = "summary" # none | summary | full # A4 minimum-content decode contract (compiler-tree decode only): # 0 -> off (empty layouts remain legal completions); # >0 -> require at least this many components before EOS is admitted; @@ -3714,6 +3726,58 @@ def record_choice( ) return tuple(paths[chosen].token_ids) + def _solver_prune_forest(self, forest, prefix): + """VSS1-03: prune the compiler forest to the certified live subset. + + Only reached when ``verified_solver_decode`` is on. Runs certificate-checked + exact closure (the VSS0-04 oracle) over the forest and drops only candidates + proven ``UNSUPPORTED`` with a replay-valid certificate; ``UNKNOWN`` candidates + are kept (``keep_and_rank``) so the ordinary soft ranker still sees them. An + unsupported tokenizer/pack fails with a clear capability error (never a + silent weaker path). + """ + from slm_training.dsl.language_contract import contract_id + from slm_training.dsl.solver.closure import EnumerativeSupportProvider + from slm_training.dsl.solver.decode import solver_prune + from slm_training.dsl.solver.openui_support import ( + OpenUIForestExpander, + OpenUIWellFormedVerifier, + ) + from slm_training.dsl.solver.state import SolverBounds + from slm_training.models.dsl_tokenizer import is_dsl_native_tokenizer + + if not is_dsl_native_tokenizer(self.tokenizer): + raise ValueError( + "verified_solver_decode requires a DSL-native tokenizer/pack; " + f"{type(self.tokenizer).__name__} is unsupported" + ) + if forest.coverage != "complete" or not forest.paths: + return forest # closure is authoritative only over an exhaustive set + + max_nodes = int(getattr(self.config, "solver_max_nodes", 512) or 512) + bounds = SolverBounds( + max_tokens=max(1, max_nodes * 64), + max_nodes=max_nodes, + max_depth=int(getattr(self.config, "solver_max_depth", 64) or 64), + max_backtracks=int(getattr(self.config, "solver_max_backtracks", 64) or 64), + max_verifier_calls=int( + getattr(self.config, "solver_max_verifier_calls", 64) or 64 + ), + ) + cv = contract_id() + window = int(getattr(self.config, "grammar_draft_window", 8) or 8) + expander = OpenUIForestExpander( + self.tokenizer, prefix, pack_id="openui", constraint_version=cv, + bounds=bounds, max_path_tokens=window, + ) + provider = EnumerativeSupportProvider(expander, OpenUIWellFormedVerifier()) + policy = str(getattr(self.config, "solver_unknown_policy", "keep_and_rank")) + pruned, _result = solver_prune( + forest, prefix, provider, pack_id="openui", constraint_version=cv, + bounds=bounds, unknown_policy=policy, state=expander.root_state(), cache={}, + ) + return pruned + def _compiler_ltr_decode_one( self, ctx: torch.Tensor, @@ -3803,6 +3867,11 @@ def _compiler_ltr_decode_one( ), min_content=self._effective_min_content(slot_contract), ) + if getattr(self.config, "verified_solver_decode", False): + # VSS1-03: certified exact closure prunes the forest to the live + # subset before any soft ranking. Disabled by default (guard above), + # so the default decode path is untouched. + forest = self._solver_prune_forest(forest, prefix) # Partial coverage still contains individually grammar-admitted # paths. Tree/restricted modes must consume those paths; falling # back merely because the vocabulary is not exhaustive discards diff --git a/tests/test_dsl/test_solver_decode.py b/tests/test_dsl/test_solver_decode.py new file mode 100644 index 00000000..64a6e9c9 --- /dev/null +++ b/tests/test_dsl/test_solver_decode.py @@ -0,0 +1,152 @@ +"""VSS1-03 (SLM-63): decode-time forest pruning via exact closure — core logic. + +Torch-free unit tests for `solver_prune`: it removes a candidate only when its +UNSUPPORTED certificate replays, keeps UNKNOWN candidates, returns a subset (so a +later ranker can never reintroduce a removed candidate), leaves non-`complete` +coverage untouched, and yields an empty forest on certified bottom. The full +decode wiring/parity is covered under tests/test_models/. +""" + +from __future__ import annotations + +import hashlib + +import pytest + +from slm_training.dsl.grammar.fastpath.compiler_draft import CompletionForest, CompletionPath +from slm_training.dsl.solver.decode import solver_prune +from slm_training.dsl.solver.state import SolverBounds, SupportVerdict +from slm_training.dsl.solver.support import ( + ReplayResult, + SearchCounters, + SupportCertificate, + SupportResult, +) + +_BOUNDS = SolverBounds( + max_tokens=1000, max_nodes=1000, max_depth=32, max_backtracks=1000, + max_verifier_calls=1000, +) + + +def _sha(text: str) -> str: + return hashlib.sha256(text.encode()).hexdigest() + + +class _RuleProvider: + """Verdict is a function of the candidate's token_ids; certificates replay.""" + + def __init__(self, rule): + self._rule = rule + + @property + def backend_version(self) -> str: + return "stub/decode-v1" + + def _cert(self, state, query, verdict) -> SupportCertificate: + common = dict( + schema_version=1, query=query, verdict=verdict, problem_id=state.problem_id, + pack_id=state.pack_id, constraint_version=state.constraint_version, + bounds=state.bounds, search_order="canonical-domain-value-v1", + explored_state_fingerprints=(), verifier_profile="stub", + ) + if verdict is SupportVerdict.UNSUPPORTED: + return SupportCertificate(**common, coverage_observations=("complete",), exhausted=True) + if verdict is SupportVerdict.SUPPORTED: + return SupportCertificate( + **common, coverage_observations=("complete",), witness_source="stub", + witness_digest=_sha(query.candidate.payload_json), exhausted=False, + ) + return SupportCertificate(**common, coverage_observations=("partial",), exhausted=False) + + def check(self, state, query) -> SupportResult: + verdict = self._rule(tuple(query.candidate.payload["token_ids"])) + return SupportResult(verdict, self._cert(state, query, verdict), counters=SearchCounters(nodes=1)) + + def replay(self, certificate, *, state) -> ReplayResult: + violations = [] + if state.fingerprint != certificate.query.state_fingerprint: + violations.append("stale") + recomputed = self._rule(tuple(certificate.query.candidate.payload["token_ids"])) + if recomputed != certificate.verdict: + violations.append("verdict") + if certificate.verdict is SupportVerdict.UNSUPPORTED and not certificate.exhausted: + violations.append("not exhausted") + if self._cert(state, certificate.query, recomputed).digest != certificate.digest: + violations.append("digest") + return ReplayResult(ok=not violations, verdict=certificate.verdict, violations=tuple(violations)) + + +def _forest(coverage="complete"): + return CompletionForest( + (CompletionPath((10,), "a"), CompletionPath((20,), "b"), CompletionPath((30,), "c")), + coverage, + ("NAME", "COMPONENT"), + ) + + +def _kinds(forest): + return [p.kind for p in forest.paths] + + +def test_removes_only_certified_unsupported_and_keeps_unknown(): + rule = lambda tids: SupportVerdict.UNSUPPORTED if tids == (10,) else SupportVerdict.UNKNOWN # noqa: E731 + forest = _forest() + pruned, result = solver_prune( + forest, [1, 2, 3], _RuleProvider(rule), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + ) + # Only the certified-unsupported candidate (10,) is dropped; UNKNOWNs kept. + assert _kinds(pruned) == ["b", "c"] + # Subset of the original -> a ranker cannot reintroduce the removed candidate. + assert set(p.token_ids for p in pruned.paths) < set(p.token_ids for p in forest.paths) + assert pruned.coverage == "complete" and pruned.terminals == forest.terminals + assert result is not None and result.counters.candidates_removed == 1 + + +def test_all_unsupported_yields_empty_forest_certified_bottom(): + forest = _forest() + pruned, result = solver_prune( + forest, [1], _RuleProvider(lambda tids: SupportVerdict.UNSUPPORTED), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + ) + assert pruned.paths == () # certified bottom -> decode dead-end/rollback handles it + assert result is not None and result.state.is_bottom + + +def test_all_unknown_keeps_forest_identity(): + forest = _forest() + pruned, result = solver_prune( + forest, [1], _RuleProvider(lambda tids: SupportVerdict.UNKNOWN), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + ) + assert pruned is forest # nothing removed -> identity preserved + assert result is not None + + +def test_non_complete_coverage_is_never_pruned(): + for coverage in ("partial", "none"): + forest = _forest(coverage) + pruned, result = solver_prune( + forest, [1], _RuleProvider(lambda tids: SupportVerdict.UNSUPPORTED), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + ) + # Closure is authoritative only over an exhaustive candidate set. + assert pruned is forest + assert result is None + + +def test_unsupported_policy_rejected(): + with pytest.raises(ValueError, match="solver_unknown_policy"): + solver_prune( + _forest(), [1], _RuleProvider(lambda tids: SupportVerdict.UNKNOWN), + pack_id="openui", constraint_version="cv", bounds=_BOUNDS, + unknown_policy="drop_unknown", + ) + + +def test_decode_module_is_torch_free(): + import inspect + import slm_training.dsl.solver.decode as decode_mod + + assert "torch" not in inspect.getsource(decode_mod) diff --git a/tests/test_models/test_solver_decode_integration.py b/tests/test_models/test_solver_decode_integration.py new file mode 100644 index 00000000..34b45970 --- /dev/null +++ b/tests/test_models/test_solver_decode_integration.py @@ -0,0 +1,178 @@ +"""VSS1-03 (SLM-63): model-level decode integration for ``verified_solver_decode``. + +Torch-bearing integration tests for the compiler-tree decode seam: + +* the solver config fields default disabled and round-trip through + ``dataclasses.asdict`` (the config/checkpoint metadata path), with old + checkpoints missing the fields falling back to defaults; +* ``verified_solver_decode=False`` is byte-identical decode (the parity + regression on a fixed fixture/seed); +* ``_solver_prune_forest`` runs real certificate-checked closure over a real + ``CompletionForest`` and never invents a candidate the forest lacked; +* an unsupported tokenizer/pack raises a clear capability error rather than + silently taking a weaker path; +* the decode loop invokes the solver seam only when the flag is enabled. + +The core ``solver_prune`` removal/keep/certified-bottom/coverage semantics (with a +fake certifying provider) live in ``tests/test_dsl/test_solver_decode.py``; this +file only pins the Torch model wiring. +""" + +from __future__ import annotations + +import dataclasses + +import pytest +import torch + +from slm_training.dsl.grammar.fastpath.compiler_draft import ( + CompletionForest, + build_completion_forest, +) +from slm_training.dsl.schema import ExampleRecord +from slm_training.models.twotower import TwoTowerConfig, TwoTowerModel + +_SOLVER_DEFAULTS = { + "verified_solver_decode": False, + "solver_max_nodes": 512, + "solver_max_depth": 64, + "solver_max_backtracks": 64, + "solver_max_verifier_calls": 64, + "solver_max_wall_ms": 0, + "solver_unknown_policy": "keep_and_rank", + "solver_certificate_mode": "summary", +} + + +def _model(**config_overrides) -> TwoTowerModel: + record = ExampleRecord( + id="compiler", + prompt="card", + openui='root = Card([title])\ntitle = TextContent(":hero.title")\n', + placeholders=[":hero.title"], + split="train", + source="fixture", + ) + config = TwoTowerConfig( + context_backend="scratch", + output_tokenizer="lexer", + d_model=32, + n_heads=2, + context_layers=1, + denoiser_layers=1, + max_prompt_len=32, + max_target_len=32, + grammar_ltr_max_tokens=32, + gen_steps=1, + seed=0, + **config_overrides, + ) + model = TwoTowerModel.from_records([record], config=config, device="cpu") + model.eval() + return model + + +def test_solver_fields_default_disabled() -> None: + config = TwoTowerConfig(context_backend="scratch", output_tokenizer="lexer") + for field, expected in _SOLVER_DEFAULTS.items(): + assert getattr(config, field) == expected + assert config.verified_solver_decode is False + + +def test_solver_config_round_trips_and_old_checkpoints_default() -> None: + config = TwoTowerConfig( + context_backend="scratch", + output_tokenizer="lexer", + verified_solver_decode=True, + solver_max_nodes=8, + solver_max_depth=4, + solver_max_backtracks=3, + solver_max_verifier_calls=5, + solver_max_wall_ms=7, + solver_unknown_policy="keep_and_rank", + solver_certificate_mode="full", + ) + dumped = dataclasses.asdict(config) + for field in _SOLVER_DEFAULTS: + assert field in dumped, f"{field} missing from serialized config" + + fields = TwoTowerConfig.__dataclass_fields__ + restored = TwoTowerConfig(**{k: v for k, v in dumped.items() if k in fields}) + assert restored.verified_solver_decode is True + assert restored.solver_max_nodes == 8 + assert restored.solver_max_wall_ms == 7 + assert restored.solver_certificate_mode == "full" + + # An old checkpoint dict missing every solver field falls back to defaults + # (strict for existing tensors, tolerant only of new config defaults). + legacy = { + k: v + for k, v in dumped.items() + if k != "verified_solver_decode" and not k.startswith("solver_") + } + legacy_config = TwoTowerConfig(**{k: v for k, v in legacy.items() if k in fields}) + for field, expected in _SOLVER_DEFAULTS.items(): + assert getattr(legacy_config, field) == expected + + +def test_disabled_flag_is_decode_identical() -> None: + baseline = _model() + ctx, ctx_pad = baseline._encode_context(["card"]) + expected = baseline._compiler_ltr_decode_one( + ctx, ctx_pad, 24, mode="tree", slot_contract=None + ) + + off = _model(verified_solver_decode=False) + ctx2, ctx_pad2 = off._encode_context(["card"]) + ids = off._compiler_ltr_decode_one( + ctx2, ctx_pad2, 24, mode="tree", slot_contract=None + ) + assert torch.equal(ids, expected) + + +def test_solver_prune_forest_runs_real_closure_and_returns_subset() -> None: + model = _model(verified_solver_decode=True, solver_max_nodes=4) + prefix = [model.tokenizer.bos_id] + forest = build_completion_forest(model.tokenizer, prefix) + assert forest.coverage == "complete" and forest.paths + + pruned = model._solver_prune_forest(forest, prefix) + assert isinstance(pruned, CompletionForest) + assert pruned.coverage == forest.coverage + original = {(p.kind, tuple(p.token_ids)) for p in forest.paths} + survivors = {(p.kind, tuple(p.token_ids)) for p in pruned.paths} + # Closure may only remove candidates; it never invents one the forest lacked. + assert survivors <= original + + +def test_enabled_requires_dsl_native_tokenizer() -> None: + model = _model(verified_solver_decode=True) + prefix = [model.tokenizer.bos_id] + forest = build_completion_forest(model.tokenizer, prefix) + model.tokenizer = object() # not a DSLNativeTokenizer/pack + with pytest.raises(ValueError, match="DSL-native"): + model._solver_prune_forest(forest, prefix) + + +def test_decode_invokes_solver_only_when_enabled() -> None: + # A spy proves the flag gates the seam call without paying the (deliberately + # expensive) real-solver cost on every decode step. Returning the forest + # unchanged keeps decode on the baseline trajectory. + calls = {"n": 0} + + def _spy(forest, prefix): + calls["n"] += 1 + return forest + + off = _model(verified_solver_decode=False) + off._solver_prune_forest = _spy # type: ignore[assignment] + ctx, ctx_pad = off._encode_context(["card"]) + off._compiler_ltr_decode_one(ctx, ctx_pad, 8, mode="tree", slot_contract=None) + assert calls["n"] == 0 # disabled: seam never called + + calls["n"] = 0 + on = _model(verified_solver_decode=True) + on._solver_prune_forest = _spy # type: ignore[assignment] + ctx2, ctx_pad2 = on._encode_context(["card"]) + on._compiler_ltr_decode_one(ctx2, ctx_pad2, 8, mode="tree", slot_contract=None) + assert calls["n"] >= 1 # enabled: pruned at least once before soft ranking