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

TL;DR

This paper introduces a data curation pipeline that improves the training of Small Language Models for program invariant synthesis, significantly enhancing their accuracy and efficiency in verification tasks.

Contribution

It presents a novel data curation method, Wonda, that refines verifier-generated invariants for effective fine-tuning of SLMs, leading to substantial performance improvements.

Findings

Fine-tuned 4B SLM matches GPT-OSS-120B utility.

Approaches state-of-the-art GPT-5.2 without extra reasoning time.

Doubles correctness and speedup on InvBench instances.

Abstract

The synthesis of inductive loop invariants is a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue, they often fail on hard instances, generating invariants that are invalid or computationally ineffective. While fine-tuning is a natural route to mitigate this limitation, obtaining high-quality training data for invariant generation remains an open challenge. We present a rigorous data curation pipeline designed to extract high-quality training signals from raw verifier-generated invariants. First, we formalize the properties required for a high-quality training invariant. Second, we propose Wonda, a pipeline that refines noisy data via AST-based normalization, followed by LLM-driven semantic rewriting and augmentation with provable quality guarantees. We demonstrate that fine-tuning Small Language Models (SLMs) on this curated dataset result in consistent and significant performance gain. In particular, a fine-tuned 4B parameter model matches the utility of a GPT-OSS-120B baseline and approaches the state-of-the-art GPT-5.2, without incurring reasoning-time overhead. On challenging instances from the recent InvBench evaluation suite, our approach doubles the invariant correctness and speedup rates of base models; and improves their Virtual Best Performance (VBP) rates on the verification task by up to 14.2%.