技术摘要：BeSpec —— 用于代码生成的行为级规范对齐

问题陈述

大语言模型（LLMs）已经显著推进了从自然语言描述（意图）到自动化代码生成的进程。然而，现有方法主要遵循“生成后优化”的范式：即生成候选程序，针对测试进行执行，并根据反馈修复代码。这种工作流隐含地假设 LLM 对意图的初始理解是正确的。在实践中，编程任务的描述往往具有歧义或描述不足。因此，LLM 可能会生成一个逻辑连贯但实现了“错误意图”的程序。目前的优化流水线通常无法检测到这种“规范失配（specification mismatch）”，因为它们侧重于修复代码而非澄清底层的规范。此外，现有的规范对齐方法（如 Specine、SpecFix）依赖于测试级证据（将输出与预期结果进行比较）。这种方法具有局限性，因为对于复杂任务而言，测试预言机（test oracles）难以生成，且测试失败提供的信号过于粗糙，无法精准定位究竟是哪个具体的行为预期（例如：索引规则、边界条件）导致了偏差。

方法论：BeSpec

BeSpec 引入了一种行为级规范对齐方法。它不再仅仅依赖测试输出，而是将预期的解决方案分解为可检查的行为预期。该框架通过以下流水线运行：

1. 规范提取（Specification Extraction）： LLM 将自然语言意图重新表达为结构化规范，其中包含输入/输出格式、约束条件、正确性规则、边缘情况以及一个用于存放已解决解释的专用字段。
2. 预测行为流水线（Predicted Behavior Pipeline）： LLM 基于结构化规范预测一组 $m$ 个预期行为 ($B$)。这些不是完整的解决方案，而是可执行的 Python 函数（check(input, output)），用于验证特定属性，例如：
   • 黄金行为（Gold behaviors）： 满足提供的样本输入-输出对。
   • 输出行为（Output behaviors）： 语法和格式约束（例如：输出必须是 "YES" 或 "NO"）。
   • 输入行为（Input behaviors）： 规则适用的条件（例如：边界情况）。
   • 语义行为（Semantic behaviors）： 规则的逻辑推论（例如：“如果一个元素被删除，索引需要重新计算”）。
3. 观测行为流水线（Observed Behavior Pipeline）：
   • 探测场景生成（Probe Scenario Generation）： 系统生成一组多样化的有效输入场景 ($X$)，旨在测试预测的行为。
   • 候选代码生成（Candidate Code Generation）： 从结构化规范中生成 $n$ 个候选程序池。
   • 行为观测（Behavior Observation）： 在探测场景上执行候选程序。系统记录观测到的行为 ($\hat{B}$)，而无需为这些探测场景预定义期望输出。
4. 失配识别（Misalignment Identification）： 系统对比候选程序池中的预测行为 ($B$) 与观测行为 ($\hat{B}$)。
   • 如果所有候选程序都与预测一致，则认为该行为已对齐。
   • 如果候选程序出现分歧或偏离预测，系统则识别出失配（misalignment），表明规范在该特定行为上存在歧义或描述不足。
5. 规范修复（Specification Fixing）： 一旦检测到失配，LLM 会修复规范（而非代码），通过明确说明缺失或有歧义的规则（例如：澄清删除操作后的重新索引规则）。该过程循环进行：基于改进后的规范生成新候选程序，并重新检查行为。
6. 基于行为的筛选（Behavior-Grounded Selection）： 一旦实现对齐或达到预算上限，系统会选择最佳候选程序。该筛选过程优先选择满足最多预测行为并能通过公开样本的程序，利用行为检查作为超越简单测试通过的证据。

核心贡献

1. 行为级对齐： 本文将规范对齐从粗粒度的测试级证据提升到了行为级推理。它能够预测、观测并追踪可检查的行为预期，并将其溯源至模糊或缺失的规范部分。
2. BeSpec 框架： 一个集成了结构化规范提取、行为预测、基于探测输入的候选程序执行、自动规范修复以及基于行为的筛选的完整流水线。
3. 全面评估： 在三个 LLM（Qwen3-Coder, GLM-4, GPT-5-Mini）以及涵盖四个基准测试（CodeContests, xCodeEval, APPS 以及无污染的 LiveCodeBench）的六种设置下进行了评估。
4. 失效分析： 通过详细分析表明，在对齐之后，剩余的大多数错误源于算法难度而非规范理解偏差。

结果

• 性能： BeSpec 在所有设置中均取得了最高的 Pass@1 和平均通过率（APR），表现优于九种基线方法（包括 Specine 和 SpecFix）。
  • 相对于最强基线，其 Pass@1 的相对提升在 8.1% 至 25.3% 之间，APR 的相对提升在 8.7% 至 28.7% 之间（基于三种 LLM）。
  • 在无污染的 LiveCodeBench 上，BeSpec 的 Pass@1 相对最佳基线提升了 15.8%–17.7%。
• 效率： 虽然 BeSpec 比简单提示（simple prompting）消耗更多的 Token 和时间，但它比 SpecFix 更具 Token 效率，且与 Specine 相当。这种成本对于对准确性要求极高的工作负载而言是可接受的。
• 消融实验：
  • 移除行为模型（仅依赖结构化规范而不进行行为检查）会导致性能大幅下降（例如：在 CodeContests 上 Pass@1 下降了约 55%），这证实了行为模型的核心地位。
  • 较大的候选程序池通常能提高准确性，但在池规模达到 10 之后收益递减。
• 失效分析： 对齐后，BeSpec 剩余的失败主要是遵循失败（算法/逻辑错误、运行时崩溃、超时），而非弱规范错误。只有极小比例的失败（例如 GPT-5-Mini 中的 4/184）归因于弱规范，这表明对齐过程成功解决了大部分意图歧义。

意义与主张

本文主张，规范失配是 LLM 代码生成中的核心瓶颈，而目前的优化方法由于在代码层面运行，无法解决这一问题。通过将重心转向行为级推理，BeSpec 提供了一种更细粒度的信号，用于在代码生成之前识别并修复意图中的歧义。

作者断言，BeSpec 有效地澄清了规范，这一点可以从失效模式的变化中得到证实：一旦规范完成对齐，剩余的挑战主要集中在算法实现难度，而非对任务要求的误解。这表明，在采用 BeSpec 等对齐技术的前提下，未来复杂任务的代码生成改进可能更多取决于解决算法问题，而非进一步精炼意图解释。该方法在测试预言机难以生成或不存在的场景下尤为重要，因为它依赖于可检查的行为属性而非完整的测试套件。