Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions docs/design/quality-experiment-matrix.md
Original file line number Diff line number Diff line change
Expand Up @@ -1693,3 +1693,4 @@ self-distillation, trajectory RL) are in
| E63 | Gate calibration | ECE / selective accuracy / abstention on `FastPathGate` | proposed |
| E64 | Trajectory-aligned RL | MDPO/d1-style on intermediate MaskGIT states | proposed |
| E65 | Schema generalization | Held-out schemas / rename / `toy-layout` transfer | proposed |
| VSS3-02 | Cost-to-go energy ranker | `cost_to_go_loss_weight` + `cost_to_go_hidden_dim` | wired |
2 changes: 1 addition & 1 deletion docs/design/research-lineage.md
Original file line number Diff line number Diff line change
Expand Up @@ -527,7 +527,7 @@ batch here avoids treating adjacent papers as independent evidence for one lever
| [DeepCoder](https://arxiv.org/abs/1611.01989) (Balog et al., ICLR 2017) | **Adjacent** | Learned search-guidance / candidate ranking; the contract keeps learned scores soft (`rank_forest`) and does not reimplement its attribute predictor or DSL |
| Counterexample-guided (neural) synthesis / CEGIS — see the *LLM-Modulo / CEGIS planning* anchor above and R19/R23 in [lattice-recursive-search.md](lattice-recursive-search.md) | **Adapted boundary** | Deduction-vs-decision split and local nogoods adopt the counterexample → refinement principle; neural synthesis training is not reimplemented |
| [egg / e-graphs](https://arxiv.org/abs/2004.03082) (Willsey et al., POPL 2021) | **Adjacent** | Post-realization canonicalization is motivated by equality saturation, but the contract is not an e-graph / equality-saturation engine (cf. `iter-e252-canonicalizer-20260716.md`) |
| EDLM — energy-based diffusion language model (2024) | **Adjacent** | Energy/score-based candidate ranking is analogous to the soft-scoring layer; no EDLM training or energy head is implemented or assumed |
| EDLM — energy-based diffusion language model (2024) | **Adapted boundary** | VSS3-02 wires a small regression+pairwise cost-to-go head on TwoTower that ranks live solver candidates (not a full EDLM); fixture-level head-only training, no production energy model or ship claim |
| [TreeDiff](https://arxiv.org/abs/2508.01473) (Zeng et al., 2025) | **Adapted boundary** | Tree-edit diffusion informs late realization against AST/choice IR; architecture and training remain future empirical work (as R13) |
| [Lattice Deduction Transformer](https://arxiv.org/abs/2605.08605) (Davis et al., 2026) | **Adapted** | Monotone lattice projection plus rollback are the closure/deduction model; LDT architecture, alpha supervision, and training remain future work (as R7) |

Expand Down
43 changes: 43 additions & 0 deletions docs/design/verified-scope-solver.md
Original file line number Diff line number Diff line change
Expand Up @@ -286,6 +286,35 @@ 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 cost-to-go energy ranker (VSS3-02 / SLM-70)

[`dsl/solver/energy_ranker.py`](../../src/slm_training/dsl/solver/energy_ranker.py)
adds `CandidateEnergyInput`, `CandidateEnergyOutput`, and `EnergyCandidateRanker`.
The ranker wraps a `CandidateEnergyScorer` and returns a **permutation** of the
exact live candidates supplied by the solver. It fail-closed falls back to the
canonical value order when the scorer returns the wrong length, non-finite
values, a membership change, or raises an exception.

[`models/twotower.py`](../../src/slm_training/models/twotower.py) adds an optional
`cost_to_go_head` auxiliary MLP, plus `score_candidates(...)` and
`cost_to_go_loss(...)`. The loss consumes `CandidateCostRow` records from the
VSS3-01 replay-verified supervision corpus and:

- masks rows where `cost_observed=False` from the regression loss,
- adds a pairwise ranking loss over candidates sharing the same `(state_fingerprint, hole_id)`,
- reports `cost_to_go_regression_loss`, `cost_to_go_pairwise_loss`, and `cost_to_go_observed_rows`.

[`harnesses/model_build/cost_to_go_train.py`](../../src/slm_training/harnesses/model_build/cost_to_go_train.py)
provides a head-only trainer that freezes the TwoTower backbone and optimizes only
the new head, analogous to `trust_train.py`.

Runtime contract:

- Exact closure computes the hard live set **before** energy scoring.
- Energy output may change candidate order, expanded nodes, backtracks, and latency only.
- Invalid scorer output triggers the configured deterministic fallback and records the fallback; membership is unchanged.
- The ranker never certifies support, suppresses `UNKNOWN`, or bypasses the final verifier.

## Reference support semantics

| Verdict | Requirement | Removal permitted? |
Expand Down Expand Up @@ -401,6 +430,7 @@ the closure.
| `HoleId`, `SolverBounds`, `DomainValue`, `HoleDomain`, `FiniteDomainState` (`dsl/solver/state.py`) | Immutable JSON-safe finite-domain carrier with canonical hard-state identity and monotone operations. | **Implemented by VSS0-03.** Torch-free and not invoked by default; soft scores and proof artifacts remain outside the state. |
| `completion_forest_state` (`dsl/solver/adapters.py`) | One-hole projection of full compiler completion paths plus coverage and `UNKNOWN` provenance. | **Implemented by VSS0-03.** Retains the compiler as owner; a singleton solves only the projection. |
| `verification capsule`, `proof certificate` | Not implemented yet. | **Future VSS issues.** Capsule solving and replayable proof ownership are not duplicated here. |
| `EnergyCandidateRanker` / `cost_to_go_head` (`dsl/solver/energy_ranker.py`, `models/twotower.py`) | Optional learned cost-to-go ranking over the exact live candidate set. | **Implemented by VSS3-02.** Permutation-only; fail-closed fallback on invalid output. No support certification or verifier bypass. |

## End-to-end example (partial coverage → live `UNKNOWN`)

Expand Down Expand Up @@ -527,3 +557,16 @@ integration, no learned energy, no persistent clause DB, and **no ship claim**.
Verified: `python -m pytest tests/test_dsl/test_solver_controller.py
tests/test_dsl/test_lattice_search.py -q` (94 in the full solver+compat suite) and
`python -m scripts.repo_policy`.

2026-07-18 — VSS3-02 / SLM-70 implements the cost-to-go energy scorer wiring:
`EnergyCandidateRanker` enforces permutation-only ordering with fail-closed
fallback, `TwoTowerModel` grows an optional `cost_to_go_head` trained from
`CandidateCostRow` records, and `cost_to_go_train.py` provides a head-only trainer.
Pinned by tiny closed fixtures (`tests/test_dsl/test_energy_ranker.py`,
`tests/test_models/test_cost_to_go.py`): ranker permutation/fallback, lower-cost
candidates receiving lower energy after overfit, `cost_observed=False` rows masked
from regression, and old checkpoints loading with the new head allowed as missing.
No full train/eval/benchmark/checkpoint was run, and **no ship or speed claim** is
made. Verified: `python -m pytest tests/test_dsl/test_energy_ranker.py
tests/test_models/test_cost_to_go.py tests/test_dsl/test_solver_controller.py -q`
(45 passed) and `python -m scripts.repo_policy`.
52 changes: 52 additions & 0 deletions docs/design/vss3-02-cost-to-go.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
# VSS3-02: Train a cost-to-go energy scorer that ranks live solver candidates only

**Issue:** SLM-70
**Status:** wiring / fixture evidence. No train, eval, benchmark, model, checkpoint, or ship claim.

## What was added

A cost-to-go energy scorer that plugs into the verified-scope solver as a permutation-only ranker.

Solver-side contract in `src/slm_training/dsl/solver/energy_ranker.py`:

- `CandidateEnergyInput` / `CandidateEnergyOutput` — typed scoring envelope.
- `CandidateEnergyScorer` protocol and `EnergyCandidateRanker` implementing `CandidateRanker`.
- Fail-closed fallback: wrong-length, non-finite, membership-changing, or exception-throwing scorer output returns the canonical value order and records the fallback.

Model-side head in `src/slm_training/models/twotower.py`:

- `TwoTowerConfig` fields `cost_to_go_loss_weight` and `cost_to_go_hidden_dim`.
- Optional `cost_to_go_head` MLP built with `isolated_aux_init` when enabled.
- `score_candidates(state, hole_id, values, context_prompt=None)` returns `CandidateEnergyOutput`.
- `cost_to_go_loss(rows, prompts=None)` regresses `log1p(nodes + verifier_calls + backtracks + depth)` for rows with `cost_observed=True` and adds a pairwise ranking loss over candidates sharing the same `(state_fingerprint, hole_id)`.
- `UNKNOWN`/censored rows (`cost_observed=False`) are masked from the regression loss.
- Prefix `"cost_to_go_head."` added to optimizer groups and `allowed_missing` checkpoint set.

Harness wiring:

- `src/slm_training/harnesses/model_build/config.py` and `factory.py` propagate the new config fields.
- `scripts/train_model.py` accepts `--cost-to-go-loss-weight` and `--cost-to-go-hidden-dim`.
- `src/slm_training/harnesses/model_build/cost_to_go_train.py` provides head-only training (freeze backbone, optimize head) and a checkpoint-save path.
- `scripts/train_cost_to_go.py` thin CLI over the head-only trainer.

## Verified

- `ruff check` passes on touched files.
- `python -m compileall` passes.
- `pytest tests/test_dsl/test_energy_ranker.py tests/test_models/test_cost_to_go.py tests/test_dsl/test_solver_controller.py -q` → 45 passed.
- `python -m scripts.repo_policy` ok.
- `git diff --check` clean.
- `.githooks/check-changed` → all checks passed (590 passed across targeted suites).

## Design boundaries preserved

- `EnergyCandidateRanker` validates that output is a permutation of the exact live values; it cannot add or drop candidates.
- The energy head is trained only from replay-verified `CandidateCostRow` records; `cost_observed=False` rows are not treated as negatives.
- No support certification, verifier bypass, or unconstrained fallback is introduced.
- Old checkpoints load cleanly with the new head allowed as missing.

## Caveats

- This is fixture wiring only: the head trains on tiny synthetic rows in tests and has not been trained on a real VSS3-01 corpus or evaluated on a solver benchmark.
- Candidate features are currently the raw `token_ids` payload from `DomainValue`; richer state/hole features are future work.
- No checkpoint ship, model-card, or readiness claim is made.
38 changes: 38 additions & 0 deletions scripts/train_cost_to_go.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
#!/usr/bin/env python3
"""Train only the VSS3-02 cost-to-go head from a solver-supervision corpus."""

from __future__ import annotations

import argparse
from pathlib import Path

from slm_training.harnesses.model_build.cost_to_go_train import (
train_cost_to_go_from_paths,
)


def main(argv: list[str] | None = None) -> int:
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("--checkpoint", type=Path, required=True)
parser.add_argument("--rows", type=Path, required=True)
parser.add_argument("--out-dir", type=Path, required=True)
parser.add_argument("--steps", type=int, default=40)
parser.add_argument("--batch-size", type=int, default=8)
parser.add_argument("--lr", type=float, default=1e-3)
parser.add_argument("--device", default="cpu")
args = parser.parse_args(argv)
summary = train_cost_to_go_from_paths(
checkpoint=args.checkpoint,
rows_path=args.rows,
out_dir=args.out_dir,
steps=args.steps,
batch_size=args.batch_size,
lr=args.lr,
device=args.device,
)
print(summary)
return 0


if __name__ == "__main__":
raise SystemExit(main())
14 changes: 14 additions & 0 deletions scripts/train_model.py
Original file line number Diff line number Diff line change
Expand Up @@ -571,6 +571,18 @@ def main(argv: list[str] | None = None) -> int:
default=0.0,
help="Cheap structural force-align aux loss weight (0 disables).",
)
parser.add_argument(
"--cost-to-go-loss-weight",
type=float,
default=0.0,
help="VSS3-02: weight for solver cost-to-go regression+pairwise loss (0 disables).",
)
parser.add_argument(
"--cost-to-go-hidden-dim",
type=int,
default=0,
help="VSS3-02: hidden dimension for the cost-to-go MLP head (0 disables).",
)
parser.add_argument(
"--grad-accum",
type=int,
Expand Down Expand Up @@ -798,6 +810,8 @@ def main(argv: list[str] | None = None) -> int:
fuse_ltr_loss=fuse_ltr,
grammar_fastpath=True,
fastpath_aux_weight=args.fastpath_aux_weight,
cost_to_go_loss_weight=args.cost_to_go_loss_weight,
cost_to_go_hidden_dim=args.cost_to_go_hidden_dim,
grammar_trust_model=args.grammar_trust_model,
noise_rate=args.noise_rate,
eval_every=args.eval_every,
Expand Down
12 changes: 12 additions & 0 deletions src/slm_training/dsl/solver/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,13 @@
default_hole_selector,
search,
)
from slm_training.dsl.solver.energy_ranker import (
CandidateEnergyInput,
CandidateEnergyOutput,
CandidateEnergyScorer,
EnergyCandidateRanker,
make_stub_energy_scorer,
)
from slm_training.dsl.solver.closure import (
CertifiedDeduction,
ClosureCounters,
Expand Down Expand Up @@ -54,8 +61,12 @@

__all__ = [
"BaselineRanker",
"CandidateEnergyInput",
"CandidateEnergyOutput",
"CandidateEnergyScorer",
"CandidateRanker",
"CertifiedDeduction",
"EnergyCandidateRanker",
"ClosureCounters",
"ClosureResult",
"DomainValue",
Expand Down Expand Up @@ -93,5 +104,6 @@
"completion_forest_state",
"default_query_order",
"exact_closure",
"make_stub_energy_scorer",
"replay_support_certificate",
]
156 changes: 156 additions & 0 deletions src/slm_training/dsl/solver/energy_ranker.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,156 @@
"""Cost-to-go energy ranker for the verified solver (VSS3-02 / SLM-70).

The ranker has no authority over candidate membership, support, or final
verification. It only orders the exact live candidates supplied by the solver.
"""

from __future__ import annotations

from dataclasses import dataclass
from typing import TYPE_CHECKING, Protocol, runtime_checkable

from slm_training.dsl.solver.controller import CandidateRanker
from slm_training.dsl.solver.state import DomainValue, FiniteDomainState, HoleId

if TYPE_CHECKING:
import torch


@dataclass(frozen=True)
class CandidateEnergyInput:
"""Features for one scoring call."""

state_fingerprint: str
state_features: torch.Tensor
hole_features: torch.Tensor
candidate_ids: tuple[DomainValue, ...]
candidate_features: torch.Tensor


@dataclass(frozen=True)
class CandidateEnergyOutput:
"""Energy scores for the supplied candidates."""

energies: torch.Tensor # shape [num_live_candidates]
candidate_ids: tuple[DomainValue, ...]
scorer_id: str


@runtime_checkable
class CandidateEnergyScorer(Protocol):
"""Callable that scores live candidates without altering membership."""

def __call__(
self,
state: FiniteDomainState,
hole_id: HoleId,
values: tuple[DomainValue, ...],
) -> CandidateEnergyOutput: ...


class EnergyCandidateRanker(CandidateRanker):
"""Permutation-only ranker backed by an energy scorer.

Falls back to the canonical value order when the scorer returns an invalid
result (wrong length, non-finite values, or membership change).
"""

def __init__(
self,
scorer: CandidateEnergyScorer,
*,
ranker_id: str | None = None,
fallback: str = "deterministic",
) -> None:
self._scorer = scorer
self._ranker_id = ranker_id or f"energy-{getattr(scorer, 'scorer_id', id(scorer))}"
self._fallback = fallback
self._fallback_count = 0

@property
def ranker_id(self) -> str:
return self._ranker_id

@property
def fallback_count(self) -> int:
return self._fallback_count

def rank(
self,
state: FiniteDomainState,
hole_id: HoleId,
values: tuple[DomainValue, ...],
) -> tuple[DomainValue, ...]:
import torch

if not values:
return tuple(values)
try:
output = self._scorer(state, hole_id, values)
except Exception: # noqa: BLE001
self._fallback_count += 1
return tuple(values)

if not isinstance(output, CandidateEnergyOutput):
self._fallback_count += 1
return tuple(values)

if len(output.candidate_ids) != len(values) or len(output.energies) != len(
values
):
self._fallback_count += 1
return tuple(values)

if set(output.candidate_ids) != set(values):
self._fallback_count += 1
return tuple(values)

if not torch.isfinite(output.energies).all():
self._fallback_count += 1
return tuple(values)

# Lower energy ranks earlier.
order = torch.argsort(output.energies, stable=True)
ranked = tuple(output.candidate_ids[int(i)] for i in order.tolist())
if set(ranked) != set(values) or len(ranked) != len(values):
self._fallback_count += 1
return tuple(values)
return ranked


def make_stub_energy_scorer(
scorer_id: str = "stub-v1",
) -> CandidateEnergyScorer:
"""Return a deterministic scorer that assigns lower energy to shorter payloads.

Useful for fixture tests: it never touches a model and always returns finite
energies for the exact supplied values.
"""

def scorer(
state: FiniteDomainState,
hole_id: HoleId,
values: tuple[DomainValue, ...],
) -> CandidateEnergyOutput:
import torch

energies = torch.tensor(
[float(len(str(value.payload_json))) for value in values],
dtype=torch.float32,
)
return CandidateEnergyOutput(
energies=energies,
candidate_ids=values,
scorer_id=scorer_id,
)

return scorer


__all__ = [
"CandidateEnergyInput",
"CandidateEnergyOutput",
"CandidateEnergyScorer",
"EnergyCandidateRanker",
"make_stub_energy_scorer",
]
3 changes: 3 additions & 0 deletions src/slm_training/harnesses/model_build/config.py
Original file line number Diff line number Diff line change
Expand Up @@ -253,6 +253,9 @@ class ModelBuildConfig:
speculative_successor: bool = False # E74 successor-state cache
speculative_fanout: int = 2
speculative_overlap: bool = False
# VSS3-02 (SLM-70): cost-to-go energy head for solver candidate ranking.
cost_to_go_loss_weight: float = 0.0
cost_to_go_hidden_dim: int = 0
# Hugging Face Bucket for durable checkpoints (full HF-context trains).
# None → default hf://buckets/TKendrick/OpenUI when sync is enabled.
# Empty string → disable auto bucket selection.
Expand Down
Loading
Loading