Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods

📄 arXiv: 2406.15540v2 📥 PDF

作者: George Granberry, Wolfgang Ahrendt, Moa Johansson

分类: cs.SE, cs.FL, cs.LG

发布日期: 2024-06-21 (更新: 2024-09-18)

💡 一句话要点

利用符号方法增强神经程序规约合成，提升C程序规约质量

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

关键词: 程序规约合成 大型语言模型 符号分析 形式化方法 C程序验证

📋 核心要点

  1. 现有方法在C程序规约合成方面存在不足，难以充分利用程序上下文信息和潜在的运行时错误。
  2. 该方法通过结合LLM和符号分析，利用Pathcrawler和EVA的输出增强LLM提示，从而生成更准确的ACSL规约。
  3. 实验表明，该方法生成的规约更具上下文感知能力，且对运行时错误更加敏感，同时对程序缺陷具有一定的鲁棒性。

📝 摘要（中文）

本文研究了如何结合大型语言模型（LLM）和符号分析来合成C程序的规约。通过使用Frama-C生态系统中的Pathcrawler和EVA这两个形式化方法工具的输出，增强LLM的提示，以生成ACSL规约语言的C程序注解。研究表明，在工作流程中加入符号分析能够显著提高注解的质量：Pathcrawler提供的输入/输出示例信息能够生成更具上下文感知能力的注解，而包含EVA报告则能生成更关注运行时错误的注解。此外，该方法能够推断程序的意图而非行为，通过为有缺陷的程序生成规约，并观察结果对缺陷的鲁棒性，验证了这一点。

🔬 方法详解

问题定义：论文旨在解决C程序规约自动合成的问题。现有的方法，特别是基于LLM的方法，在理解程序上下文、识别潜在运行时错误以及区分程序意图和行为方面存在不足，导致生成的规约质量不高。

核心思路：论文的核心思路是将LLM的生成能力与符号分析工具的精确性相结合。通过利用符号分析工具（Pathcrawler和EVA）的输出来增强LLM的提示，从而引导LLM生成更准确、更可靠的程序规约。这种结合旨在弥补LLM在形式化推理方面的不足，并利用符号分析提供的信息来提升LLM的上下文理解能力。

技术框架：整体框架包含以下几个主要步骤：1) 使用Pathcrawler和EVA等符号分析工具对C程序进行分析；2) 将分析结果（例如，输入/输出示例、运行时错误报告）作为提示信息添加到LLM的输入中；3) 使用LLM生成ACSL规约；4) 对生成的规约进行评估和验证。Pathcrawler提供输入/输出示例，EVA提供运行时错误报告。

关键创新：该方法的核心创新在于将LLM的自然语言理解和生成能力与符号分析工具的精确分析能力相结合。这种混合方法能够充分利用两者的优势，从而生成更准确、更可靠的程序规约。与单纯依赖LLM的方法相比，该方法能够更好地理解程序上下文、识别潜在的运行时错误，并区分程序意图和行为。

关键设计：论文的关键设计在于如何有效地将符号分析工具的输出融入到LLM的提示中。具体来说，Pathcrawler的输入/输出示例被用来增强LLM对程序行为的理解，而EVA的运行时错误报告则被用来引导LLM生成更关注安全性的规约。此外，论文还通过实验验证了该方法对程序缺陷的鲁棒性，表明该方法能够推断程序的意图而非行为。

🖼️ 关键图片

fig_0

📊 实验亮点

实验结果表明，通过结合Pathcrawler和EVA的输出，LLM生成的ACSL规约在上下文感知能力和运行时错误敏感性方面均有显著提升。此外，该方法对程序缺陷具有一定的鲁棒性，能够推断程序的意图而非行为，这表明该方法具有很强的实用价值。

🎯 应用场景

该研究成果可应用于软件验证、程序调试和自动化测试等领域。通过自动生成高质量的程序规约，可以提高软件开发的效率和可靠性，减少人工验证的工作量。未来，该方法可以扩展到其他编程语言和形式化方法工具，为更广泛的软件开发场景提供支持。

📄 摘要（原文）

We investigate how combinations of Large Language Models (LLMs) and symbolic analyses can be used to synthesise specifications of C programs. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA, to produce C program annotations in the specification language ACSL. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations: information about input/output examples from Pathcrawler produce more context-aware annotations, while the inclusion of EVA reports yields annotations more attuned to runtime errors. In addition, we show that the method infers rather the programs intent than its behaviour, by generating specifications for buggy programs and observing robustness of the result against bugs.