BeSpec：代码生成的行为级规范对齐

LLM 在根据所需行为（意图）的自然语言描述自动生成代码方面取得了实质性进展。大多数现有方法通过执行引导的代码细化来改进生成的程序：它们生成候选解决方案，执行它，并使用反馈修补实现，同时保持底层规范不变。此工作流程隐含地假设 LLM 对意图的理解已经正确且完整。然而，在实践中，意图往往是模糊的或不明确的。因此，即使是一个有能力的模型也可能会产生错误意图的正确实现，从而使规范不匹配成为中心瓶颈。本文提出了 BeSpec，一种基于行为模型的规范调整方法。 BeSpec 将任务描述视为正确程序预期行为的部分证据。它首先构建一个显式的行为模型，这是有效输出必须满足的可检查属性。然后 BeSpec 生成候选程序，在探测输入上执行它们，并将观察到的行为与预测的行为进行比较。当观察到的行为与预测的行为不匹配时，BeSpec 要么完善规范，要么拒绝候选程序。我们使用三个 LLM 在四个基准上评估 BeSpec：CodeContests、xCodeEval、APPS 和无污染的 LiveCodeBench。相对于九个基线，BeSpec 在所有设置中实现了最高的 Pass@1 和平均通过率，相对于三个 LLM，平均 Pass@1 比最强基线提高了 8.1%--25.3%。故障分析表明，对齐后，大多数剩余错误源于算法难度，而不是对规范的误解，而消融研究证实 BeSpec 的每个主要组成部分都做出了积极贡献。