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

arXiv: https://arxiv.org/abs/2603.15510 · HTML: https://mlsanity.com/paper/2603.15510/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 37 references that are in the map.
- First posted on arXiv 16 Mar 2026.

## Builds on (most cited first, 6 of 6)

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [gpt-oss-120b & gpt-oss-20b Model Card](https://mlsanity.com/paper/2508.10925/) (2025)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Horn-ICE Learning for Synthesizing Invariants and Contracts](https://mlsanity.com/paper/1712.09418/) (2017)
- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)

## Abstract (arXiv)

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 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 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 20x 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 GitHub.