用大模型+模糊测试自动生成程序最弱前提，提升验证准确性
LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions
- 用模糊测试反馈引导大模型生成更精确的最弱前提
- 在Java数组程序上验证，结合反馈后生成结果更可靠
- 适合做形式化验证和漏洞检测的研究者参考
程序的最弱前提（WP）描述了所有终止执行都满足给定后置条件的最大初始状态集合。生成WP在验证和运行时错误检查中有重要应用。本文提出将大语言模型（LLMs）与模糊测试结合以生成WP。为此，我们引入 extit{模糊引导}（FG），利用程序执行反馈指导LLM生成正确且尽可能弱的WP。FG通过模糊测试近似验证候选WP的有效性和弱性，将结果反馈给LLM作为上下文优化。我们在一组确定性的Java数组程序上进行了全面评估，实验表明LLMs能生成可行的候选WP，且通过FG可显著提升其质量。
原文摘要 · Abstract (English)
The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of WPs is an important task with practical applications in areas ranging from verification to run-time error checking. This paper proposes the combination of Large Language Models (LLMs) and fuzz testing for generating WPs. In pursuit of this goal, we introduce \emph{Fuzzing Guidance} (FG); FG acts as a means of directing LLMs towards correct WPs using program execution feedback. FG utilises fuzz testing for approximately checking the validity and weakness of candidate WPs, this information is then fed back to the LLM as a means of context refinement. We demonstrate the effectiveness of our approach on a comprehensive benchmark set of deterministic array programs in Java. Our experiments indicate that LLMs are capable of producing viable candidate WPs, and that this ability can be practically enhanced through FG.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。