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

📄 arXiv: 2603.15510v1 📥 PDF

作者: Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu, Nina Narodytska, Guy Katz

分类: cs.LG

发布日期: 2026-03-16

💡 一句话要点

提出Wonda数据管线，通过高质量数据训练SLM加速程序验证中的循环不变式生成。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 程序验证 循环不变式生成 数据管理 小型语言模型 形式化方法

📋 核心要点

  1. 程序验证中循环不变式生成是瓶颈，现有LLM方法在复杂场景下效果不佳，缺乏高质量训练数据。
  2. 提出Wonda数据管线，通过AST归一化、LLM语义重写和质量保证增强，生成高质量训练数据。
  3. 实验表明，基于Wonda训练的SLM性能显著提升，在InvBench上正确率和加速率翻倍，VBP提升高达14.2%。

📝 摘要（中文）

循环不变式的归纳综合是自动程序验证中的关键瓶颈。尽管大型语言模型（LLMs）在缓解此问题方面显示出希望，但它们通常在困难的实例上失败，生成无效或计算上无效的不变式。虽然微调是缓解此限制的自然途径，但获得用于不变式生成的高质量训练数据仍然是一个开放的挑战。我们提出了一种严格的数据管理流程，旨在从原始验证器生成的不变式中提取高质量的训练信号。首先，我们形式化了高质量训练不变式所需的属性。其次，我们提出了Wonda，一个通过基于AST的归一化来细化噪声数据的流程，然后通过LLM驱动的语义重写和具有可证明质量保证的增强。我们证明，在此管理的数据集上微调小型语言模型（SLMs）可带来一致且显着的性能提升。特别地，微调的4B参数模型匹配了GPT-OSS-120B基线的效用，并接近了最先进的GPT-5.2，而没有产生推理时间开销。在最近InvBench评估套件中的具有挑战性的实例上，我们的方法使基本模型的循环不变式正确性和加速率提高了一倍；并将其在验证任务上的虚拟最佳性能（VBP）率提高了高达14.2％。

🔬 方法详解

问题定义：论文旨在解决程序验证中循环不变式自动生成的问题。现有的方法，特别是基于大型语言模型的方法，在处理复杂程序时，生成的循环不变式往往无效或效率低下，导致验证失败。主要痛点在于缺乏高质量的训练数据，使得模型难以学习到正确的循环不变式生成策略。

核心思路：论文的核心思路是通过数据管理（Data Curation）来提升训练数据的质量，从而提高小型语言模型（SLM）在循环不变式生成任务上的性能。核心在于设计一个能够从原始验证器生成的不变式中提取高质量训练信号的流程。

技术框架：论文提出的Wonda管线包含以下主要阶段：1) 基于AST的归一化：对原始数据进行结构化处理，消除语法上的噪声。2) LLM驱动的语义重写：利用LLM对不变式进行语义上的优化和改进，使其更易于理解和使用。3) 质量保证增强：通过可证明的质量保证来增强数据集，确保训练数据的可靠性。

关键创新：论文的关键创新在于提出了一种系统性的数据管理流程，能够有效地从噪声数据中提取高质量的训练信号。与以往直接使用原始数据进行训练的方法不同，Wonda通过多阶段的处理，显著提升了训练数据的质量，从而提高了模型的性能。

关键设计：Wonda管线中的关键设计包括：1) AST归一化的具体规则，用于消除语法噪声。2) LLM语义重写的prompt设计和约束条件，确保重写后的不变式在语义上等价或更优。3) 质量保证增强的具体方法，例如使用形式化验证工具对生成的不变式进行验证，并根据验证结果进行筛选和修正。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，基于Wonda管线训练的4B参数SLM，性能可与GPT-OSS-120B基线模型相媲美，并接近最先进的GPT-5.2模型，且无需推理时间开销。在InvBench测试集上，循环不变式正确率和加速率提升一倍，验证任务的虚拟最佳性能（VBP）提升高达14.2%。

🎯 应用场景

该研究成果可应用于自动程序验证、软件测试和形式化方法等领域。通过提高循环不变式生成的准确性和效率，可以显著提升程序验证的自动化程度，减少人工干预，从而提高软件的可靠性和安全性。未来，该方法有望推广到其他程序分析和代码生成任务中。

📄 摘要（原文）

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%.