用神经符号方法自动生成循环不变式，准确率达99.5%。
A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
- 结合大模型与霍尔逻辑，通过逆向最弱前置条件推理生成候选不变式
- 利用OpenJML的反例迭代修复，使99.5%的程序成功验证
- 适合需要高可靠性的自动化验证场景，尤其复杂多循环程序
循环不变式生成仍是自动化程序验证的关键瓶颈。现有基于大语言模型（LLM）的方法缺乏可靠结构化方法，且较少参考程序验证理论。本文提出NeuroInv，一种神经符号化循环不变式生成方法。该方法包含两个核心模块：(1) 神经推理模块，利用LLM与霍尔逻辑，通过逆向最弱前置条件推理生成并优化候选不变式；(2) 验证引导的符号模块，借助OpenJML提供的反例迭代修复不变式。我们在涵盖单循环、多序列循环、多数组、随机分支及噪声代码段的150个Java程序上评估NeuroInv，成功率达99.5%，显著优于其他方法。此外，我们引入一个包含10个更大型多循环程序的难题集（平均每个含7个循环），结果表明NeuroInv可有效扩展至更复杂的验证场景。
原文摘要 · Abstract (English)
Loop invariant generation remains a critical bottleneck in automated program verification. Recent work has begun to explore the use of Large Language Models (LLMs) in this area, yet these approaches tend to lack a reliable and structured methodology, with little reference to existing program verification theory. This paper presents NeuroInv, a neurosymbolic approach to loop invariant generation. NeuroInv comprises two key modules: (1) a neural reasoning module that leverages LLMs and Hoare logic to derive and refine candidate invariants via backward-chaining weakest precondition reasoning, and (2) a verification-guided symbolic module that iteratively repairs invariants using counterexamples from OpenJML. We evaluate NeuroInv on a comprehensive benchmark of 150 Java programs, encompassing single and multiple (sequential) loops, multiple arrays, random branching, and noisy code segments. NeuroInv achieves a $99.5\%$ success rate, substantially outperforming the other evaluated approaches. Additionally, we introduce a hard benchmark of $10$ larger multi-loop programs (with an average of $7$ loops each); NeuroInv's performance in this setting demonstrates that it can scale to more complex verification scenarios.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。