Code Agent 如何在生成补丁后加入形式化验证与候选补丁筛选？

Code Agent 生成补丁后，不能把“代码能应用”或“某个测试通过”直接等同于修复完成。更可靠的做法是建立分层候选筛选管线：先淘汰语法、构建和静态检查失败的补丁，再用故障复现用例确认问题确实消失，用正常功能测试排除回归，最后只对适合建模的关键性质调用形式化验证器。形式化验证不是替代测试的万能终点，而是候选补丁经过低成本筛选后的一道高保证关卡。

为什么生成之后必须保留多个候选

同一个缺陷往往存在多种表面合理的修改。一个候选可能只让触发用例通过，却破坏正常路径；另一个候选修改范围过大，难以审查；还有的补丁语法正确，却依赖错误的隐含前提。若 Agent 只生成一次并立即提交，验证阶段只能接受或推翻唯一答案，失败后又要从零开始，既浪费上下文，也丢失已经正确的部分。

PatchPilot 将修复工作组织为复现、定位、生成、验证和细化五个阶段。其关键思想是，失败反馈应继续作用于当前补丁，而不是每轮完全重新生成。对工程系统而言，这意味着生成器输出的是带计划、假设和变更范围的候选集合；验证器产生结构化证据；筛选器依据固定规则排序；细化器只修复已经定位的失败点。

先定义“合格补丁”而不是只定义分数

候选筛选应先设置不可妥协的门槛。补丁必须能够干净应用，修改文件在允许范围内，解析和构建成功，故障复现用例从失败变为通过，相关正常用例继续通过，并且没有触发安全、依赖或接口兼容性禁令。任何硬门槛失败，候选都不能仅凭较高的模型评分晋级。

通过硬门槛后，才使用软指标排序，例如修改行数、影响的公共接口数量、测试覆盖增量、静态分析告警数、运行时间和补丁复杂度。推荐把排序写成显式元组，而不是让 LLM 凭整体印象选择：

rank = (
    formal_status_priority,
    regression_failures,
    risk_rule_violations,
    changed_public_interfaces,
    changed_lines,
    runtime_cost,
)

这里的形式化状态至少要区分 proved、counterexample、unknown 和 not_applicable。unknown 不能当成通过，not_applicable 也不应惩罚那些本来就不适合形式化建模的业务补丁。固定排序规则让同一候选集得到可复现的结果，也便于审计为什么某个补丁胜出。

第一层：低成本确定性过滤

Agent 生成候选后，首先检查补丁是否能应用、是否越过文件白名单、是否包含无关格式化，以及是否引入生成物或秘密信息。随后运行解析器、格式检查、类型检查和增量构建。这一层成本低、反馈明确，应在昂贵测试和求解之前完成。

静态分析结果要绑定到具体文件、行号、规则和符号。例如“变量可能为空”比一整段工具日志更适合回馈模型。对于编译错误，还应截取首个根因及其依赖诊断，避免 Agent 被大量级联错误带偏。未通过这一层的候选可以修复一轮，但不应进入形式化验证。

第二层：故障 PoC 与正常功能测试

修复验证至少需要两类测试。故障 PoC 是能够稳定触发原问题的最小输入，用于证明候选确实改变了失败行为。正常功能测试来自相关模块或历史测试集，用于确认修复没有破坏原有正确路径。只跑 PoC 容易得到针对单一样例的过拟合补丁，只跑现有回归测试又可能根本没有覆盖新报告的问题。

PoC 本身也要先校准：它必须在基线版本失败，在已知正确版本或明确预期下通过，并且重复运行结果稳定。若 PoC 在原始代码上不失败，就不能用它筛选补丁。对时间、并发或随机相关问题，应固定环境并记录重试统计，而不是把一次偶然通过当作修复证据。

候选测试可以采用逐级扩大的方式：先跑单个 PoC，再跑直接相关测试文件，然后跑模块测试，最后按风险决定是否运行全库测试。每一级都设置时间上限并缓存未改动依赖。这样能快速淘汰明显错误候选，同时把计算资源集中到更有希望的补丁上。

第三层：把需求转成可求解的规格

形式化验证需要明确规格。对一个纯函数，可以表达输入前置条件、返回值后置条件和异常行为；对状态更新，可以表达不变量，例如余额不为负、索引始终处于边界内、权限检查不能被绕过。LLM 可以根据问题描述、代码和测试提出候选规格，但不能同时担任最终裁判。

规格生成后应进行独立审查。首先检查规格是否可满足，避免一个永远为假的前置条件让任何实现都“被证明正确”；其次运行突变或反例测试，确认错误实现会被规格拒绝；最后由求解器检查补丁是否在限定模型下满足性质。规格、环境假设、超时和求解器版本都必须随结果保存。

def verify_candidate(candidate, spec, limits):
    model = translate(candidate, spec)
    result = solver.check(model, timeout=limits.timeout)
    if result == SAT:
        return {"status": "counterexample", "model": solver.model()}
    if result == UNSAT:
        return {"status": "proved", "scope": spec.scope}
    return {"status": "unknown", "reason": solver.reason_unknown()}

常见编码方式是寻找违反后置条件或不变量的输入。如果求解器返回 SAT，模型就是反例，可转换成新的测试并送回细化阶段；返回 UNSAT，表示在当前抽象、边界和假设范围内没有反例；返回 unknown，则只能说明求解未完成。报告必须写清证明范围，不能把有界整数、简化容器或有限循环下的结论宣传为对整个生产系统的绝对保证。

如何让 Z3 参与真实修复流程

Z3 适合验证可表达为逻辑约束的局部性质，例如整数边界、条件分支覆盖、状态转换、不变量和部分集合关系。Agent 可把目标函数抽取为无副作用核心，使用符号输入执行补丁前后逻辑，再断言“存在满足前置条件但违反后置条件的输入”。求解到反例时，将具体输入加入测试集；没有反例时，把证明范围作为候选证据。

不适合直接交给 SMT 求解器的部分包括复杂 I/O、网络时序、动态框架行为和大型对象图。此时可以验证一个抽象模型，而把模型与实现之间的对应关系交给类型检查、契约断言和测试补强。形式化层应该允许 not_applicable，而不是为了覆盖率强行生成没有约束力的规格。

PatchPilot 的形式化验证仍属于早期探索，论文只对 SWE-bench Lite 中 11 个补丁进行了尝试。因此，更稳妥的落地方式是先选择高风险且容易形式化的函数建立试点，统计规格有效率、求解时间、反例价值和人工接受率，再逐步扩大范围。

候选之间如何比较与去重

多候选不等于盲目增加采样次数。生成阶段可以使用不同修复计划产生少量有差异的候选，例如最小局部修改、恢复不变量和替换错误调用三种策略。随后按补丁语义和变更区域去重，避免把只差变量名或格式的结果重复验证。

筛选器为每个候选维护证据包，包括生成计划、差异摘要、静态检查结果、PoC 结果、回归测试结果、形式化状态、反例和成本。只有硬门槛全部通过的候选才参与最终排序。若两个补丁证据相同，优先选择改动范围更小、公共接口影响更少、与既有代码模式更一致的方案。

不要用通过测试数量直接相加作为总分。一个候选通过一千个无关测试，却让核心 PoC 失败，仍然是不合格补丁。测试需要按必要性和相关性分层，安全规则、PoC 与关键不变量拥有否决权。

利用反例进行增量细化

验证失败后，反馈应描述“哪条性质在什么输入下失败”，并保留候选中已经通过的部分。细化器收到反例、失败断言和相关代码片段，只允许修改必要区域。新补丁必须重新通过之前的全部门槛，不能因为修复了新反例就跳过旧测试。

可以为细化循环设置两个条件：如果候选通过全部要求，立即成为合格候选；如果尚未通过，但比上一轮新增通过了一项有效检查，则允许继续细化；若没有任何证据改善，或重复触发同一反例，就停止该分支。这个策略利用部分正确性，同时避免无限修补。

完整的发布闸门

一个可落地的 Code Agent 流程是：复现问题并固定 PoC，定位根因与必要上下文，生成三到五个有计划差异的补丁，执行低成本过滤，逐级运行 PoC 和回归测试，为适用候选生成并审查形式化规格，调用求解器获得证明、反例或未知状态，再依据硬门槛和显式排序选择最终补丁。

最终输出不只包含代码，还应包含验证清单：基线如何失败、补丁后哪些测试通过、哪些测试未运行、形式化验证采用了什么规格和边界、是否存在 unknown，以及为什么选择该候选。只要这些证据无法完整回答，Agent 就应把补丁标记为待审查，而不是宣称已经正确。

实施时应避免的三个误区

第一个误区是让 LLM 生成宽松规格，再用该规格证明自己的补丁。必须通过可满足性检查、错误实现拒绝测试和人工抽查约束规格质量。第二个误区是把 UNSAT 简写成“程序绝对正确”，实际结论只在当前模型与边界内成立。第三个误区是对所有候选都直接求解，导致验证成本失控；应先用确定性廉价检查缩小集合。

形式化验证真正带来的价值，不是给补丁贴上一个神秘的“已证明”标签，而是把模糊的正确性争论变成可检查的规格，把失败变成具体反例，再让候选筛选由证据驱动。与 PoC、回归测试、静态分析和有限细化组合后，Code Agent 才能在成本可控的前提下，逐步提高补丁的可信度。