使用 LLM 生成的反例改进动态规范推断

契约断言（例如前提条件、后置条件和不变量）在软件开发中发挥着至关重要的作用，支持程序验证、测试生成和调试等应用程序。尽管有好处，但由于手动生成此类断言的困难，合约断言的采用受到限制。基于动态分析的方法（例如 Daikon）可以通过从执行跟踪推断表达性断言来帮助完成此任务。然而，这些方法的一个根本弱点是它们依赖于用于动态分析的测试套件的彻底性。当这些测试套件不包含足够多样化的测试时，推断的断言通常不可概括，导致无效候选者（误报）的比例很高，必须手动过滤掉。在本文中，我们探索使用 大语言模型 (LLM) 自动生成尝试使生成的断言无效的测试。我们的结果表明，最先进的 LLM 可以生成有效的反例，有助于丢弃 SpecFuzzer 推断出的高达 11.68% 的无效断言。此外，当将这些 LLM 生成的反例纳入动态分析过程时，我们观察到相对于从评估基准收集的真实情况，推断规范的精度提高了 7%，且不影响召回率。