Disproving Program Equivalence with LLMs

📄 arXiv: 2502.18473v1 📥 PDF

作者: Miltiadis Allamanis, Pengcheng Yin

分类: cs.SE, cs.LG

发布日期: 2025-02-05

💡 一句话要点

提出ProbeGen，利用LLM和执行反馈验证代码等价性，提升代码理解与合成。

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

关键词: 代码等价性验证 大型语言模型 代码生成 执行反馈 语义聚类

📋 核心要点

  1. 现有代码评估方法依赖人工单元测试，难以覆盖所有边界情况和实现细节，导致评估不准确。
  2. ProbeGen利用LLM生成反例来验证代码等价性，结合执行反馈提升LLM的代码理解能力。
  3. 实验表明，ProbeGen能有效识别现有基准测试中被错误判断为等价的代码，并提升代码合成性能。

📝 摘要（中文）

为了评估大型语言模型（LLM）在代码方面的能力，研究通常使用手动创建的基于单元测试的基准。然而，这些测试往往不足，遗漏了边界情况和其他特定于实现的细节。本研究引入了ProbeGen，一种白盒方法，它接受两个或多个可执行的代码片段，并搜索它们等价性的反例。比较代码语义需要对代码的深刻理解。我们证明了具有执行反馈的LLM在此任务中表现良好。在一个常见的代码合成基准中，ProbeGen否定了18%的样本，这些样本被基准提供的单元测试认为是与ground truth等价的。此外，使用ProbeGen，我们可以对LLM样本进行语义聚类以实现语义自洽性，通过统一语法上不同但语义上相似的样本，将pass@1提高10%。

🔬 方法详解

问题定义：现有代码评估方法，特别是针对LLM生成的代码，依赖于人工设计的单元测试。这些单元测试往往无法覆盖所有可能的输入和边界情况，导致一些语义上不等价的代码被错误地判断为等价。这使得对LLM代码生成能力的评估不准确，也阻碍了LLM在代码领域的进一步应用。

核心思路：ProbeGen的核心思路是利用LLM生成能够区分两个代码片段的反例，即找到一个输入，使得两个代码片段在该输入下的输出不同。通过这种方式，可以有效地验证代码的等价性。如果LLM能够生成这样的反例，则说明两个代码片段不等价；否则，可以认为它们在一定程度上是等价的。

技术框架：ProbeGen的整体框架包含以下几个主要步骤：1) 输入两个待比较的代码片段；2) 利用LLM生成一系列可能的输入；3) 在这些输入上执行两个代码片段，并比较它们的输出；4) 如果找到一个输入使得输出不同，则判定两个代码片段不等价；5) 如果没有找到这样的输入，则可以根据一定的置信度判断它们等价。该框架的关键在于如何有效地利用LLM生成高质量的输入，以及如何设计合适的执行和比较机制。

关键创新：ProbeGen的关键创新在于将LLM与代码执行反馈相结合，用于代码等价性验证。传统的代码等价性验证方法通常依赖于符号执行或形式化验证等技术，这些技术计算复杂度高，难以处理复杂的代码片段。ProbeGen利用LLM的强大代码生成能力，可以快速生成大量的测试用例，并通过执行反馈来指导LLM生成更有效的测试用例。

关键设计：ProbeGen的关键设计包括：1) 使用Prompt工程来指导LLM生成合适的输入；2) 设计了基于执行结果的反馈机制，用于指导LLM生成更有效的反例；3) 使用语义聚类方法对LLM生成的代码样本进行聚类，从而提高代码合成的性能。具体的参数设置和网络结构等技术细节在论文中没有详细描述，属于未知的实现细节。

🖼️ 关键图片

img_0

📊 实验亮点

ProbeGen在一个常见的代码合成基准测试中，否定了18%的样本，这些样本被基准提供的单元测试认为是与ground truth等价的。此外，通过使用ProbeGen进行语义聚类，将pass@1指标提高了10%，表明ProbeGen能够有效地提升代码合成的性能。

🎯 应用场景

ProbeGen可应用于代码生成模型的评估、代码调试、代码优化和软件测试等领域。通过更准确地评估代码的等价性，可以提高代码生成模型的质量，辅助开发人员发现代码中的错误，并优化代码的性能。此外，ProbeGen还可以用于自动化软件测试，提高测试的覆盖率和效率。

📄 摘要（原文）

To evaluate large language models (LLMs) for code, research has used manually created unit test-based benchmarks. However, these tests are often inadequate, missing corner cases and other implementation-specific oddities. This work introduces ProbeGen, a whitebox method that takes two or more executable pieces of code and searches for counterexamples to their equivalence. Comparing code semantics requires a deep understanding of code. We demonstrate that LLMs with execution feedback perform well at this task. In a common code synthesis benchmark, ProbeGen disproves 18% of samples considered equivalent to the ground truth by the benchmark-provided unit tests. Additionally, using ProbeGen, we can semantically cluster LLM samples for semantic self-consistency, improving pass@1 by 10% by unifying syntactically distinct but semantically similar samples.