用高质量数据训练小模型，大幅提升程序验证中循环不变式的生成准确率和速度。
Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
- 通过语法树归一化与语义重写，从验证器输出自动提取可靠不变式数据。
- 在小模型上微调后，正确率翻倍，验证速度提升2-3倍，性能超越大模型。
- 适合关注程序验证、自动化推理的开发者与研究者使用。
归纳循环不变式的合成仍是自动化程序验证的关键瓶颈。尽管大语言模型（LLMs）在缓解此问题方面展现潜力，但在复杂程序上常生成无效或计算低效的不变式。虽微调是自然对策，但获取高质量训练数据仍具挑战。本文首次形式化定义高质量训练不变式所需属性，并提出Wonda数据清洗流程：基于抽象语法树（AST）归一化，结合大模型驱动的语义重写与可证明质量保证，从原始验证器输出中提取高质不变式。在Wonda数据上微调小型语言模型（SLMs），对Qwen3、Llama-3.1及Mistral系列均取得一致提升：4B与8B Qwen3模型将不变式正确率几乎翻倍，速度提升两倍；Llama-3.1-8B模型则三项指标均提升三倍。在具有挑战性的InvBench基准上，相同4B模型性能达同规模模型20倍，媲美GPT-OSS-120B端到端验证时间，而14B Qwen3模型性能接近前沿模型GPT-5.2，且无需测试时额外算力。代码已开源。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。