Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Project Aletheia: Verifier-Guided Distillation of Backtracking for Small Language Models

Aradhya Dixit, Tianxi Liang, Jai Telang

TL;DR

This work tackles the fragility of small language models on constraint-satisfaction tasks by introducing Verifier-Guided Distillation, which teaches backtracking and error repair rather than only final answers. The method synthesizes backtracking-rich teacher traces, validates them with symbolic verification, and conducts matched control/treatment distillation using LoRA fine-tuning on a 7B-class model, with explicit negative constraints that surface failures. Key contributions include a verified “golden” SAT training dataset, a control dataset lacking backtracking signals, and an empirical demonstration that rare explicit backtracking behavior can be induced in small models (BER up to 0.05 on 40 instances). The findings suggest a data-topology mechanism: exposing recoverable errors during training enables latent verification capabilities that can improve on-device reasoning, with potential extensions to RL, curricula over failure modes, richer instrumentation, and generalization beyond SAT.

Abstract

Small Language Models (SLMs, under 10B parameters) are attractive for private, on-device deployment, yet they frequently fail on strict constraint-satisfaction problems due to linear, overconfident reasoning traces that do not recover from early mistakes. We introduce Verifier-Guided Distillation, a training protocol that transfers the process of error repair - explicit conflict detection and backtracking - rather than only correct final answers. By training a 7B model on verified reasoning traces that include mistakes and self-corrections, we show that latent verification behavior can emerge in small models, enabling them to occasionally stop, detect contradictions, and revise earlier assumptions.

Project Aletheia: Verifier-Guided Distillation of Backtracking for Small Language Models

TL;DR

This work tackles the fragility of small language models on constraint-satisfaction tasks by introducing Verifier-Guided Distillation, which teaches backtracking and error repair rather than only final answers. The method synthesizes backtracking-rich teacher traces, validates them with symbolic verification, and conducts matched control/treatment distillation using LoRA fine-tuning on a 7B-class model, with explicit negative constraints that surface failures. Key contributions include a verified “golden” SAT training dataset, a control dataset lacking backtracking signals, and an empirical demonstration that rare explicit backtracking behavior can be induced in small models (BER up to 0.05 on 40 instances). The findings suggest a data-topology mechanism: exposing recoverable errors during training enables latent verification capabilities that can improve on-device reasoning, with potential extensions to RL, curricula over failure modes, richer instrumentation, and generalization beyond SAT.

Abstract

Small Language Models (SLMs, under 10B parameters) are attractive for private, on-device deployment, yet they frequently fail on strict constraint-satisfaction problems due to linear, overconfident reasoning traces that do not recover from early mistakes. We introduce Verifier-Guided Distillation, a training protocol that transfers the process of error repair - explicit conflict detection and backtracking - rather than only correct final answers. By training a 7B model on verified reasoning traces that include mistakes and self-corrections, we show that latent verification behavior can emerge in small models, enabling them to occasionally stop, detect contradictions, and revise earlier assumptions.
Paper Structure (33 sections, 11 equations, 1 figure, 1 algorithm)

This paper contains 33 sections, 11 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Method: Verifier-Guided Distillation
  3. Problem Setup (SAT as Constraint Satisfaction)
  4. Verification and Dataset Construction
  5. Negative Constraint Injection (Backtracking-Supervision Trace Synthesis)
  6. Teacher policy.
  7. Why "negative" constraints help.
  8. Trace format.
  9. Symbolic Verification and "Golden" Dataset Construction
  10. Control vs. Treatment: Matched Ablation of Backtracking Signal
  11. Treatment (Aletheia traces).
  12. Control (Linearized traces).
  13. Student Training (LoRA Distillation Under Edge Constraints)
  14. Objective.
  15. LoRA parameterization.
  16. ...and 18 more sections

Figures (1)

  • Figure 1: End-to-end Verifier-Guided Distillation pipeline. Teacher generates backtracking traces under Negative Constraint Injection; PySAT verifies final assignments; control vs. treatment adapters are trained and evaluated via adapter hot-swapping.