Formally-Verified Training and Runtime Validation for Small Language Models Using Relational Specifications
TL;DR
This work investigates whether relational specifications can ground SLM behaviour by mathematical proof rather than statistical regularities alone, and gives practitioners a route to deploy verifiable SLMs in safety-critical settings.
Abstract
Small language models (SLMs) learn statistical patterns and generate outputs stochastically. This offers no assurance that those outputs satisfy the domain constraints that ought to govern them, hence hindering adoption in safety-critical domains such as healthcare. This work investigates whether relational specifications can ground SLM behaviour by mathematical proof rather than statistical regularities alone. The approach integrates model-driven engineering specification languages (UML/OCL) with relational model finders (Alloy/Kodkod) in a two-stage pipeline. Stage one gives guarantee by construction, where solver-enumerated instances supply formally-verified fine-tuning data. Stage two gives guarantee by verification, where a tiered hybrid runtime checker validates outputs against OCL. Three hypotheses structure the investigation. First, solver-enumerated fine-tuning data raises OCL constraint-satisfaction rates. Second, tiered declarative plus imperative checking beats either tier alone within sub-second latency. Third, OCL-derived templates detect natural-language violations above a named-entity-recognition baseline. Healthcare self-management serves as the bounded application context. Preliminary tooling already runs the behavioural checker in a sandbox. If the hypotheses hold, the methodology gives practitioners a route to deploy verifiable SLMs in safety-critical settings. If they fail, the results mark where formal guarantees break down on stochastic systems, a limit that research on verified AI has not yet documented.