摘要

本文介绍了一种名为LLM4PR的工具，该工具结合了形式化程序细化技术和非正式的大型语言模型（LLM）方法，旨在自动化地将形式化抽象规范语句转换为可执行程序。传统的程序细化工具高度交互且缺乏自动化，而LLM虽然能够从非正式的自然语言规范自动生成代码，但生成的代码往往不可靠，且其生成过程是一个不透明的黑箱。LLM4PR通过将规范转换为前置和后置条件、自动构建基于细化计算的提示、与LLM交互生成代码，并最终验证生成的代码是否满足细化条件，从而确保代码的正确性。该工具已通过GPT4和Coq实现，并在HumanEval和EvalPlus数据集上进行了评估。

原理

LLM4PR的工作原理基于将形式化程序细化技术与LLM相结合。首先，它将规范转换为前置和后置条件，然后自动构建基于细化计算的提示，与LLM交互生成代码。生成的代码随后通过验证步骤，确保其满足细化条件，从而保证代码的正确性。这一过程中，LLM被视为“约束求解器”，其强大的扩展性和丰富的背景知识为程序细化提供了自动化的潜力。LLM4PR还结合了自动定理证明器（ATPs）来验证代码，并证明LLM所做的细化选择的正确性。

流程

LLM4PR的工作流程包括以下几个关键步骤：

1. 规范转换：将输入的规范转换为前置和后置条件。
2. 自动构建提示：基于细化计算自动构建与LLM交互的提示。
3. 代码生成：与LLM交互，生成相应的代码。
4. 代码验证：使用ATPs验证生成的代码是否满足细化条件。
5. 结果处理：如果验证成功，保存验证后的代码并生成新的规范；如果验证失败，回溯到上一步骤并重新选择细化规则生成代码。

例如，在计算实数平方根的程序中，LLM4PR首先将原始规范分解为两个部分，分别定义变量x和y，使得x² ≤ N < y²，并通过迭代使x和y逐渐接近，直到满足特定条件。每个细化步骤都可以通过其关联的规范进行验证。

应用

LLM4PR的应用前景广泛，特别是在需要高度自动化和正确性保证的软件开发领域。它可以用于自动化生成和验证复杂软件系统的代码，减少人工错误和提高开发效率。此外，随着LLM技术的进一步发展，LLM4PR有望在更多领域实现代码生成的自动化和优化。