LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions

📄 arXiv: 2507.05272v2 📥 PDF

作者: Daragh King, Vasileios Koutavas, Laura Kovacs

分类: cs.SE, cs.AI, cs.LO

发布日期: 2025-07-03 (更新: 2025-12-17)

💡 一句话要点

提出结合LLM与模糊测试的Fuzzing Guidance方法，自动生成最弱前置条件

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

关键词: 最弱前置条件生成 大型语言模型 模糊测试 程序验证 自动化测试

📋 核心要点

  1. 最弱前置条件（WP）生成在程序验证和运行时错误检查中至关重要，但现有方法存在不足。
  2. 论文提出Fuzzing Guidance（FG）方法，利用模糊测试反馈指导LLM生成更准确的WP。
  3. 实验表明，LLM在生成WP方面具有潜力，且FG能有效提升LLM生成WP的质量。

📝 摘要（中文）

本文提出了一种结合大型语言模型（LLM）和模糊测试来生成最弱前置条件（WP）的新方法。程序的最弱前置条件描述了程序所有终止执行都能满足给定后置条件的初始状态的最大集合。生成WP是一项重要的任务，在验证到运行时错误检查等领域具有实际应用。为此，我们引入了“模糊测试指导”（FG），FG作为一种利用程序执行反馈来指导LLM生成正确WP的手段。FG利用模糊测试来近似检查候选WP的有效性和弱性，然后将此信息反馈给LLM，作为上下文细化的手段。我们在Java中确定性数组程序的综合基准集上证明了该方法的有效性。实验表明，LLM能够生成可行的候选WP，并且可以通过FG实际增强这种能力。

🔬 方法详解

问题定义：论文旨在解决自动生成程序最弱前置条件（WP）的问题。现有的WP生成方法可能面临效率低、难以处理复杂程序逻辑等挑战，尤其是在处理包含数组操作的程序时。因此，如何高效、准确地生成WP是一个重要的研究问题。

核心思路：论文的核心思路是结合大型语言模型（LLM）的强大代码生成能力和模糊测试的程序验证能力。LLM负责生成候选的WP，而模糊测试则用于验证这些WP的有效性和弱性。通过将模糊测试的结果反馈给LLM，可以指导LLM生成更符合要求的WP。这种思路利用了LLM的生成能力和模糊测试的验证能力，形成了一个闭环的优化过程。

技术框架：整体框架包含以下几个主要模块：1) LLM：负责根据程序代码和后置条件生成候选的WP。2) 模糊测试：对生成的WP进行验证，通过生成大量的测试用例来检查WP的有效性和弱性。3) Fuzzing Guidance (FG)：根据模糊测试的结果，生成反馈信息，指导LLM调整其生成策略。4) 迭代优化：LLM根据FG的反馈信息，重新生成WP，并重复进行模糊测试和反馈，直到生成满足要求的WP。

关键创新：该方法最重要的创新点在于将LLM和模糊测试相结合，形成了一个闭环的优化过程。传统的WP生成方法通常依赖于符号执行等技术，而该方法则利用LLM的生成能力和模糊测试的验证能力，避免了复杂的符号计算。此外，FG模块的设计也是一个创新点，它能够有效地将模糊测试的结果转化为LLM可以理解的反馈信息，从而指导LLM生成更准确的WP。

关键设计：FG模块的关键设计在于如何将模糊测试的结果转化为LLM可以理解的反馈信息。具体来说，FG会根据模糊测试的结果，生成一些正例和反例，这些例子描述了在哪些情况下WP是有效的，在哪些情况下WP是无效的。然后，FG会将这些例子作为上下文信息，输入到LLM中，指导LLM调整其生成策略。此外，论文还可能涉及到一些关于LLM的prompt设计，例如如何设计prompt来引导LLM生成符合要求的WP。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，LLM在生成WP方面具有潜力，并且通过Fuzzing Guidance（FG）的指导，LLM生成WP的质量得到了显著提升。具体性能数据未知，但论文强调FG能够实际增强LLM生成可行候选WP的能力。该方法在Java确定性数组程序的综合基准集上进行了验证。

🎯 应用场景

该研究成果可应用于软件验证、运行时错误检查和程序调试等领域。通过自动生成最弱前置条件，可以帮助开发人员更有效地验证程序的正确性，及早发现潜在的错误，并提高软件的可靠性和安全性。此外，该方法还可以用于自动化测试用例生成，提高测试效率。

📄 摘要（原文）

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.