HoarePrompt: Structural Reasoning About Program Correctness in Natural Language
作者: Dimitrios Stamatios Bouras, Yihan Dai, Tairan Wang, Yingfei Xiong, Sergey Mechtaev
分类: cs.SE, cs.AI
发布日期: 2025-03-25 (更新: 2025-08-23)
💡 一句话要点
HoarePrompt：利用自然语言进行程序正确性的结构化推理。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 程序验证 自然语言处理 大型语言模型 Hoare逻辑 k-归纳法
📋 核心要点
- 现有方法难以有效验证程序与自然语言需求的一致性，大型语言模型在此任务中表现不佳，无法检测简单错误。
- HoarePrompt借鉴程序验证思想，通过LLM逐步生成程序状态的自然语言描述，并使用few-shot k-归纳法处理循环。
- 实验表明，HoarePrompt在CoCoClaNeL数据集上显著提升了程序正确性分类的MCC指标，优于现有方法。
📝 摘要（中文）
软件需求通常以自然语言表达，但针对这些需求验证程序的正确性是一个困难且未被充分探索的问题。大型语言模型（LLMs）是解决这一挑战的有希望的候选者，但我们的经验表明，它们在这项任务中效果不佳，甚至常常无法检测到简单的错误。为了解决这个差距，我们引入了HoarePrompt，这是一种新颖的方法，它将程序验证的基本思想应用于自然语言工件。受最强后置条件演算的启发，HoarePrompt采用了一种系统的、逐步的过程，其中LLM生成在各个代码点上可达程序状态的自然语言描述。为了管理循环，我们提出了few-shot驱动的k-归纳法，这是模型检查中广泛使用的k-归纳法的一种改编。一旦描述了程序状态，HoarePrompt就利用LLM来评估用这些状态描述注释的程序是否符合自然语言需求。为了评估程序正确性分类器相对于自然语言需求的质量，我们构建了一个具有挑战性的编程竞赛问题解决方案数据集CoCoClaNeL。我们的实验表明，与直接使用Zero-shot-CoT提示进行正确性分类相比，HoarePrompt将MCC提高了61%。此外，HoarePrompt优于通过基于LLM的测试生成来评估正确性的分类器，MCC提高了106%。归纳推理机制使MCC提高了26%，突显了其在管理循环方面的有效性。
🔬 方法详解
问题定义：论文旨在解决如何利用自然语言描述的需求来验证程序正确性的问题。现有方法，特别是直接使用大型语言模型（LLMs），在理解自然语言需求并将其与程序行为对齐方面存在困难，导致无法有效检测程序中的错误。现有方法缺乏结构化的推理过程，难以处理复杂的程序逻辑和循环结构。
核心思路：HoarePrompt的核心思路是将程序验证中的Hoare逻辑和最强后置条件演算的思想引入到自然语言处理中。通过逐步推导程序在不同代码点的状态描述，并使用自然语言表达，使得LLM能够更好地理解程序行为。同时，借鉴k-归纳法来处理循环，保证推理的完整性。这种结构化的推理过程能够帮助LLM更准确地判断程序是否满足自然语言需求。
技术框架：HoarePrompt的整体框架包含以下几个主要阶段：1) 状态描述生成：LLM根据程序代码，逐步生成程序在各个代码点的状态的自然语言描述。2) 循环处理：对于循环结构，采用few-shot驱动的k-归纳法，通过少量示例引导LLM进行归纳推理，生成循环不变式的自然语言描述。3) 正确性评估：LLM根据程序代码、状态描述和自然语言需求，判断程序是否满足需求。CoCoClaNeL数据集用于评估分类器的质量。
关键创新：HoarePrompt的关键创新在于将程序验证的结构化推理方法引入到自然语言处理中，使得LLM能够更好地理解程序行为和自然语言需求之间的关系。具体来说，借鉴Hoare逻辑和k-归纳法的思想，通过逐步推导程序状态和循环不变式，使得LLM能够更准确地判断程序是否满足需求。与直接使用LLM进行程序正确性判断的方法相比，HoarePrompt具有更强的推理能力和更高的准确性。
关键设计：HoarePrompt的关键设计包括：1) 使用few-shot学习来引导LLM生成状态描述和循环不变式。2) 设计合适的prompt模板，使得LLM能够更好地理解程序代码和自然语言需求。3) 使用MCC（Matthews correlation coefficient）作为评估指标，评估程序正确性分类器的质量。k-归纳法的具体实现细节，例如k值的选择，以及few-shot示例的选择策略，对最终的性能有重要影响。
🖼️ 关键图片
📊 实验亮点
实验结果表明，HoarePrompt在CoCoClaNeL数据集上显著提升了程序正确性分类的性能。与直接使用Zero-shot-CoT提示相比，HoarePrompt将MCC提高了61%。与基于LLM的测试生成方法相比，HoarePrompt的MCC提高了106%。此外，归纳推理机制使MCC提高了26%，突显了其在管理循环方面的有效性。这些结果表明，HoarePrompt是一种有效的程序正确性验证方法。
🎯 应用场景
HoarePrompt具有广泛的应用前景，可用于自动化软件测试、程序验证和代码生成等领域。它可以帮助开发人员更有效地检测程序中的错误，提高软件质量。此外，HoarePrompt还可以用于教育领域，帮助学生更好地理解程序逻辑和自然语言需求之间的关系。未来，HoarePrompt可以扩展到更复杂的程序和需求场景，例如并发程序和安全需求。
📄 摘要（原文）
While software requirements are often expressed in natural language, verifying the correctness of a program against such requirements is a hard and underexplored problem. Large language models (LLMs) are promising candidates for addressing this challenge, however our experience shows that they are ineffective in this task, often failing to detect even straightforward bugs. To address this gap, we introduce HoarePrompt, a novel approach that adapts fundamental ideas from program verification to natural language artifacts. Inspired from the strongest postcondition calculus, HoarePrompt employs a systematic, step-by-step process in which an LLM generates natural language descriptions of reachable program states at various code points. To manage loops, we propose few-shot-driven k-induction, an adaptation of the k-induction method widely used in model checking. Once program states are described, HoarePrompt leverages the LLM to assess whether the program, annotated with these state descriptions, conforms to the natural language requirements. For evaluating the quality of classifiers of program correctness with respect to natural language requirements, we constructed CoCoClaNeL, a challenging dataset of solutions to programming competition problems. Our experiments show that HoarePrompt improves the MCC by 61% compared to directly using Zero-shot-CoT prompts for correctness classification. Furthermore, HoarePrompt outperforms a classifier that assesses correctness via LLM-based test generation by an MCC increase of 106%. The inductive reasoning mechanism contributes a 26% boost to MCC, underscoring its effectiveness in managing loops.