用大模型生成循环不变式，加速程序验证并保证正确性
Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
- 直接验证大模型生成的不变式能否助证目标断言，无需复杂后处理
- 在866个实例上验证，性能超越现有基于大模型的验证工具
- 适合关注自动化验证与大模型结合的研究者和开发者
程序验证依赖循环不变式，但自动生成强不变式仍是长期挑战。我们探究大语言模型（LLMs）是否可通过生成有用循环不变式来加速程序验证。提出Quokka框架，实现基于大模型的不变式合成，兼具正确性保障与领先性能。不同于以往将大模型输出视为需大量后处理的噪声符号材料，Quokka采用更简洁的算法设计：直接验证每个大模型生成的不变式是否有助于证明目标断言。构建涵盖866个评估实例和3589个训练实例的基准数据集，源自SV-COMP，评估了9种跨模型家族的大模型。实验表明，监督微调与Best-of-N采样带来显著提升，且Quokka持续优于先前基于大模型的验证器。代码与数据已公开于https://github.com/Anjiang-Wei/Quokka。
原文摘要 · Abstract (English)
Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We investigate whether large language models (LLMs) can accelerate program verification by generating useful loop invariants. We introduce Quokka, a framework for LLM-based invariant synthesis with soundness guarantees and state-of-the-art performance. Unlike prior work that treats LLM outputs as noisy symbolic material requiring substantial post-processing, Quokka adopts a simpler algorithm design that directly validates whether each LLM-generated invariant helps prove the target assertion. We construct a benchmark of 866 evaluation instances and 3589 training instances derived from SV-COMP, and evaluate 9 LLMs spanning multiple model families. We demonstrate that supervised fine-tuning and Best-of-N sampling yield measurable improvements, and we show that Quokka consistently outperforms prior LLM-based verifiers. Our code and data are publicly available at https://github.com/Anjiang-Wei/Quokka
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。