Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs

The synthesis of inductive loop invariants remains a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue, they often fail on complex programs, producing invariants that are invalid or computationally ineffective. Although fine-tuning is a natural strategy to address these limitations, obtaining high-quality training data remains an open challenge. We first formalize the properties required for a high-quality training invariant, and then present \textsc{Wonda}, a rigorous data curation pipeline that extracts such invariants from raw verifier output via AST-based normalization followed by LLM-driven semantic rewriting and augmentation with provable quality guarantees. Fine-tuning Small Language Models (SLMs) on \textsc{Wonda}-curated data yields consistent gains across the Qwen3, Llama-3.1, and Mistral families: the 4B and 8B Qwen3 models nearly double invariant correctness and double speedup rates, while Llama-3.1-8B triples both. On the challenging InvBench suite, the same 4B model outperforms an off-the-shelf model 20$\times$ its size and matches the end-to-end verification time of GPT-OSS-120B, while a 14B Qwen3 model matches that of the frontier model GPT-5.2, all without test-time compute overhead. Our code is publicly available on \href{https://github.com/idopinto/wonda}{GitHub}.

Proving that software is mathematically free of bugs is one of computing's hardest problems; it underpins the reliability of critical systems. The main bottleneck is finding "loop invariants," logical facts that stay true every time a loop repeats and are needed to prove the code correct. AI models can guess these, but it remains hard even for frontier models. The usual fix is bigger models. We asked instead: what if the bottleneck is the quality of the examples we teach from? Existing training data comes from automated verification tools that produce correct but bloated examples. It is like learning math from complex solutions that are right but never simplified: you learn the mess instead of the idea. Our pipeline, WONDA, first strips the clutter, then uses a language model to rewrite each example into a compact and more elegant form, with every rewrite formally verified. This produced consistent gains across almost every model we trained: a 4B model outperforms one 20 times larger and rivals even bigger models, and a 14B model matches a top frontier model in end-to-end verification time. This shows that better training data, not just bigger models, can make trustworthy software verification faster and more accessible.