用输入输出对验证大模型生成代码的正确性,效果更准更稳。
Inferring Code Correctness from Specification
- 基于规范生成多样测试输入,让大模型判断输出是否符合预期。
- 相比基线方法,准确率提升39%,且对随机性不敏感。
- 适合需要高可靠性的自动化代码验证场景。
大型语言模型(LLMs)已成为现代软件开发中自动化代码生成的核心工具,但验证其生成代码的正确性仍是关键且未解决的挑战。现有方法要么依赖多个代码候选的动态共识,成本高难扩展;要么依赖静态推理,易受动态漏洞和顺序偏差影响。本文提出TRAILS~(基于输入与规范的目标推理一致性),通过具体(输入,输出)对来约束大模型推理。TRAILS~首先根据规范进行类别划分生成多样测试输入,执行后让大模型评估结果是否符合规范——无需直接分析代码本身。通过聚合多个输入的评分,判断程序是否可能正确。在LiveCodeBench和CoCoClaNeL两个数据集上,针对Qwen3Coder-30B、Devstral-Small-24B和Olmo3.1-Instruct三类模型进行评估,相比零样本思维链基线,TRAILS~将马修相关系数提升最高达39%,并持续优于HoarePrompt。此外,该方法在不同种子运行下表现更稳定,降低大模型随机性带来的影响,并能为更多唯一代码样本正确标注。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。