从规范推断代码的正确性

大语言模型 (LLM) 已成为现代软件开发不可或缺的一部分，可实现大规模自动代码生成。然而，验证 LLM 生成的代码的正确性仍然是一个关键且很大程度上尚未解决的挑战。现有的方法要么依赖于多个候选代码之间的动态共识（这使得它们成本高昂且难以扩展），要么依赖于容易受到动态错误和顺序偏差影响的静态推理。在本文中，我们提出了 TRAILS~（通过输入和规范进行目标推理协议），这是一种以具体（输入、输出）对为基础的 LLM 推理的方法。 TRAILS~ 首先通过基于规范的类别划分生成不同的测试输入，然后针对候选代码执行它们，并提示 LLM 评估生成的输入-输出对是否符合规范 - 无需对代码本身进行推理。分数会根据输入进行汇总，以确定程序是否可能正确。我们在三个 LLM（Qwen3Coder-30B、Devstral-Small-24B 和 Olmo3.1-Instruct）的两个数据集 LiveCodeBench 和 CoCoClaNeL 上评估 TRAILS~，与 HoarePrompt 和零样本思想链基线进行比较。相对于零样本 COT，TRAILS~ 将马修相关系数提高了 39%，并且始终优于 HoarePrompt。除了准确性之外，TRAILS~ 在种子运行中表现出更高的稳定性，降低了对 LLM 非确定性的敏感性，并且与竞争方法相比，可以将正确的标签分配给更大的一组唯一代码样本。