Towards Large Language Model Aided Program Refinement
作者: Yufan Cai, Zhe Hou, Xiaokun Luan, David Miguel Sanan Baena, Yun Lin, Jun Sun, Jin Song Dong
分类: cs.SE, cs.AI, cs.CL
发布日期: 2024-06-26
💡 一句话要点
LLM4PR：结合大语言模型与形式化方法实现程序自动精化
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 程序精化 大语言模型 形式化验证 代码生成 自动化
📋 核心要点
- 现有程序精化工具自动化程度低，依赖人工交互，效率受限。
- LLM4PR结合形式化方法与LLM，利用LLM生成代码草案，再用形式化方法验证和保证正确性。
- 实验表明，该方法在程序精化任务上具有潜力，验证了结合LLM与形式化方法的有效性。
📝 摘要（中文）
程序精化涉及将形式化的高级规范语句转换为可执行程序，同时保持正确性。传统的程序验证工具对程序精化的支持高度依赖交互，缺乏自动化。另一方面，大型语言模型（LLM）的出现使得从非正式的自然语言规范自动生成代码成为可能。然而，LLM生成的代码通常不可靠。此外，LLM提供的从规范到代码的不透明过程是一个不受控制的黑盒。我们提出了LLM4PR，该工具结合了形式化程序精化技术与基于LLM的非正式方法，以（1）将规范转换为前置条件和后置条件，（2）自动构建基于精化演算的提示，（3）与LLM交互以生成代码，最后，（4）验证生成的代码是否满足精化演算的条件，从而保证代码的正确性。我们使用GPT4、Coq和Coqhammer实现了我们的工具，并在HumanEval和EvalPlus数据集上对其进行了评估。
🔬 方法详解
问题定义：程序精化旨在将高级形式化规范转换为可执行代码，同时保证正确性。现有方法主要依赖人工交互和形式化验证工具，自动化程度低，效率不高。LLM虽然可以从自然语言生成代码，但其生成过程不透明，结果不可靠，缺乏形式化保证。
核心思路：LLM4PR的核心思路是结合LLM的代码生成能力和形式化方法的验证能力。利用LLM生成代码的草案，然后使用形式化方法验证其正确性，并根据验证结果进行修正，从而实现自动化的程序精化。
技术框架：LLM4PR包含以下几个主要阶段：1) 将规范转换为前置条件和后置条件；2) 基于精化演算自动构建提示（prompt）；3) 与LLM交互，根据提示生成代码；4) 使用形式化验证工具（如Coq）验证生成的代码是否满足精化演算的条件。如果验证失败，则调整提示并重新生成代码，直到验证通过。
关键创新：该方法最重要的创新点在于将LLM的代码生成能力与形式化方法的验证能力相结合，克服了LLM生成代码不可靠的缺点，同时提高了程序精化的自动化程度。与传统方法相比，LLM4PR能够自动生成代码草案，并使用形式化方法保证其正确性，从而减少了人工干预。
关键设计：LLM4PR的关键设计包括：1) 如何将自然语言规范转换为形式化的前置条件和后置条件；2) 如何根据精化演算自动构建有效的提示，引导LLM生成符合要求的代码；3) 如何选择合适的LLM和形式化验证工具，并进行有效的集成；4) 如何设计迭代的验证和修正流程，保证最终生成的代码的正确性。论文中使用了GPT4作为LLM，Coq和Coqhammer作为形式化验证工具。
🖼️ 关键图片
📊 实验亮点
LLM4PR在HumanEval和EvalPlus数据集上进行了评估，结果表明该方法能够有效地生成正确的代码。具体的性能数据和对比基线在论文中进行了详细的展示。实验结果验证了将LLM与形式化方法相结合的有效性，并表明LLM4PR在程序精化任务上具有潜力。
🎯 应用场景
LLM4PR可应用于软件开发的自动化，尤其是在需要高可靠性和安全性的领域，如嵌入式系统、金融系统和安全关键系统。它可以帮助开发人员快速生成代码，并保证代码的正确性，从而提高开发效率和软件质量。未来，该方法有望扩展到更复杂的程序精化任务，并与其他自动化工具集成。
📄 摘要（原文）
Program refinement involves correctness-preserving transformations from formal high-level specification statements into executable programs. Traditional verification tool support for program refinement is highly interactive and lacks automation. On the other hand, the emergence of large language models (LLMs) enables automatic code generations from informal natural language specifications. However, code generated by LLMs is often unreliable. Moreover, the opaque procedure from specification to code provided by LLM is an uncontrolled black box. We propose LLM4PR, a tool that combines formal program refinement techniques with informal LLM-based methods to (1) transform the specification to preconditions and postconditions, (2) automatically build prompts based on refinement calculus, (3) interact with LLM to generate code, and finally, (4) verify that the generated code satisfies the conditions of refinement calculus, thus guaranteeing the correctness of the code. We have implemented our tool using GPT4, Coq, and Coqhammer, and evaluated it on the HumanEval and EvalPlus datasets.