LLM 与模糊测试协同：一种自动生成最弱前置条件的新方法
软件工程
2025-12-18 v2 人工智能
计算机科学中的逻辑
摘要
程序的最弱前置条件（WP）描述了使程序所有终止执行均满足给定后置条件的最大初始状态集合。生成 WP 是一项重要任务，在从程序验证到运行时错误检查等领域具有实际应用。本文提出将大型语言模型（LLM）与模糊测试相结合以生成 WP。为实现此目标，我们引入了模糊测试指导（Fuzzing Guidance，FG）；FG 利用程序执行反馈，作为一种引导 LLM 生成正确 WP 的手段。FG 利用模糊测试来近似检查候选 WP 的有效性与弱性，随后将此信息反馈给 LLM 作为上下文优化的手段。我们在一套全面的 Java 确定性数组程序基准集上展示了该方法的有效性。实验表明，LLM 能够生成可行的候选 WP，且该能力可通过 FG 得到实质性增强。
引用
@article{arxiv.2507.05272,
title = {LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions},
author = {Daragh King and Vasileios Koutavas and Laura Kovacs},
journal= {arXiv preprint arXiv:2507.05272},
year = {2025}
}