Inferring Code Correctness from Specification

📄 arXiv: 2605.29822v1 📥 PDF

作者: Tambon Florian, Papadakis Mike

分类: cs.SE, cs.AI

发布日期: 2026-05-28

💡 一句话要点

TRAILS：基于输入输出对齐规范推断代码正确性，提升LLM代码验证精度。

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

关键词: 代码正确性验证 大型语言模型 软件测试 输入输出对 规范推理

📋 核心要点

  1. 现有LLM代码验证方法依赖动态共识或静态推理，存在成本高、易受动态错误影响等问题。
  2. TRAILS通过生成多样化测试输入，执行代码并让LLM评估输入输出对是否符合规范，避免直接推理代码。
  3. 实验表明，TRAILS在准确性、稳定性和唯一代码样本覆盖率方面均优于现有方法，提升显著。

📝 摘要（中文）

大型语言模型（LLMs）已成为现代软件开发不可或缺的一部分，实现了大规模的自动化代码生成。然而，验证LLM生成的代码的正确性仍然是一个关键且很大程度上未解决的挑战。现有的方法要么依赖于多个代码候选者之间的动态共识——这使得它们成本高昂且难以扩展——要么依赖于静态推理，而静态推理容易受到动态错误和顺序偏差的影响。在本文中，我们提出了一种名为TRAILS（Targeted Reasoning Agreement via Inputs and Specifications）的方法，该方法通过具体的（输入，输出）对来支持LLM推理。TRAILS首先通过基于规范的类别划分生成多样化的测试输入，然后针对候选代码执行这些输入，并提示LLM评估结果输入-输出对是否符合规范——而无需对代码本身进行推理。分数在输入之间聚合，以确定程序是否可能正确。我们在LiveCodeBench和CoCoClaNeL两个数据集上，针对三个LLM（Qwen3Coder-30B、Devstral-Small-24B和Olmo3.1-Instruct）评估了TRAILS，并与HoarePrompt和Zero-Shot Chain-of-Thought基线进行了比较。相对于Zero-Shot COT，TRAILS将马修斯相关系数提高了高达39％，并且始终优于HoarePrompt。除了准确性之外，TRAILS还展示了跨种子运行的更高稳定性，降低了对LLM非确定性的敏感性，并且比竞争方法为更大的唯一代码样本集分配了正确的标签。

🔬 方法详解

问题定义：论文旨在解决大型语言模型（LLMs）生成的代码的正确性验证问题。现有方法，如基于动态共识的方法成本高昂且难以扩展，而基于静态推理的方法容易受到动态错误和顺序偏差的影响。这些方法无法有效且可靠地验证LLM生成的代码，阻碍了LLM在软件开发中的广泛应用。

核心思路：TRAILS的核心思路是通过具体的输入-输出对来引导LLM进行推理，而不是直接让LLM分析代码本身。这种方法避免了LLM在理解复杂代码逻辑时可能出现的错误，并利用LLM在判断输入-输出对是否符合规范方面的优势。通过聚合多个输入-输出对的评估结果，可以更准确地判断代码的正确性。

技术框架：TRAILS方法主要包含以下几个阶段： 1. 输入生成：根据代码规范，通过类别划分生成多样化的测试输入。 2. 代码执行：针对候选代码执行生成的测试输入，得到相应的输出。 3. LLM评估：提示LLM评估每个输入-输出对是否符合代码规范，无需LLM直接分析代码。 4. 结果聚合：将LLM对所有输入-输出对的评估结果进行聚合，得到最终的代码正确性评分。

关键创新：TRAILS最重要的创新在于其基于输入-输出对进行LLM推理的策略。与现有方法相比，TRAILS避免了LLM直接分析代码，从而降低了LLM出错的概率。此外，TRAILS通过生成多样化的测试输入，可以更全面地评估代码的正确性。

关键设计： * 输入生成策略：采用类别划分方法，确保生成的测试输入覆盖代码规范的各个方面。 * LLM提示工程：设计清晰明确的提示语，引导LLM专注于评估输入-输出对是否符合规范。 * 结果聚合方法：使用合适的聚合函数（例如，平均值、加权平均值）将LLM对不同输入-输出对的评估结果进行综合，得到最终的代码正确性评分。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果表明，TRAILS在LiveCodeBench和CoCoClaNeL数据集上显著优于现有方法。相对于Zero-Shot COT，TRAILS将马修斯相关系数提高了高达39％，并且始终优于HoarePrompt。此外，TRAILS还展示了更高的稳定性，降低了对LLM非确定性的敏感性，并且为更大的唯一代码样本集分配了正确的标签。

🎯 应用场景

TRAILS具有广泛的应用前景，可用于自动化软件测试、代码质量评估和LLM代码生成系统的改进。通过提高代码验证的准确性和效率，TRAILS可以帮助开发者更可靠地使用LLM生成代码，并降低软件开发和维护的成本。未来，TRAILS可以扩展到支持更复杂的代码规范和编程语言，并与其他代码分析工具集成。

📄 摘要（原文）

Large language models (LLMs) have become integral to modern software development, enabling automated code generation at scale. However, validating the correctness of LLM-generated code remains a critical and largely unsolved challenge. Existing approaches either rely on dynamic consensus across multiple code candidates - making them costly and difficult to scale - or on static reasoning that is susceptible to dynamic bugs and order bias. In this paper, we propose TRAILS~ (Targeted Reasoning Agreement via Inputs and Specifications), an approach that grounds LLM reasoning with concrete (input, output) pairs. TRAILS~ first generates diverse test inputs via category partitioning based on the specification, then executes them against the candidate code and prompts LLMs to assess whether the resulting input-output pairs conform to the specification - without ever reasoning over the code itself. Scores are aggregated across inputs, to determines whether the program is likely correct. We evaluate TRAILS~ on two datasets, LiveCodeBench and CoCoClaNeL, across three LLMs (Qwen3Coder-30B, Devstral-Small-24B, and Olmo3.1-Instruct), comparing against HoarePrompt and a Zero-Shot Chain-of-Thought baseline. TRAILS~ improves Matthew Correlation Coefficient by up to 39\% relative to Zero-Shot COT and consistently outperforms HoarePrompt. Beyond accuracy, TRAILS~ demonstrates greater stability across seeded runs, reducing sensitivity to LLM non-determinism, and assigns correct labels to a larger set of unique code samples than competing approaches.