用反例引导大模型修复形式化证明，提升准确率与效率
ExVerus: Verus Proof Repair via Counterexample Reasoning
- 基于反例反馈，让大模型动态推理并生成归纳不变式
- 在Verus验证器上，证明成功率显著高于现有提示方法
- 适合需要高可靠性代码验证的研究者与工程团队
大语言模型在自动化形式化验证方面展现出潜力，但现有方法将证明生成视为对源代码的静态端到端预测，依赖有限的验证器反馈且无法获取程序实际行为。我们提出EXVERUS，一种基于反例引导的框架，使大模型能够通过反例行为反馈进行证明推理。当证明失败时，EXVERUS自动生成并验证反例，进而引导大模型将反例泛化为归纳不变式以阻止此类失败。实验表明，相较于最先进的基于提示的Verus证明生成器，EXVERUS在证明准确率、鲁棒性和令牌效率上均有显著提升。
原文摘要 · Abstract (English)
Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present EXVERUS, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。