以验证器为依据的智能体强化学习，实现可证明正确的代码

arXiv:2610.19298v1 公告类型：新提交 摘要：面向代码的强化学习通常以通过测试作为奖励，但模型即使通过测试，在测试未覆盖的输入上仍可能出错。相比之下，程序验证器会判定程序是否对所有输入都满足形式化规约。语言模型几乎总是仅在推理阶段与验证器配合使用，而将验证器转化为奖励信号面临两项困难。其一，验证器只报告接受或拒绝，当所有尝试均失败时，便无法提供梯度；其二，策略可能欺骗验证器，最简单的方式就是让验证器直接假定本应通过证明确立的结论成立。我们构建了一个智能体环境和奖励机制，以解决这两个问题。该奖励机制读取验证器的诊断信息，而非最终判定，根据候选程序已完成的证明义务所占的加权比例进行评分，并引入源自参考证明注解的隐藏探针作为补充。完整性审计的优先级高于验证器，会拒绝任何修改规约或将待证结论直接作为假设的候选程序。模型作为智能体，与实时运行的验证器进行多轮交互，同时由一个单独训练、参数冻结的证明专家模型提供协作。在参数规模从 1.7B 到 14B 的 Qwen3 模型以及一个 35B 的 Qwen3.6 混合专家模型上，代码生成任务在留出集上的验证通过率在 DafnyBench 上从 66.1% 提升至 93.5%，在 SWE-Proof 上从 56.3% 提升至 100%。该奖励机制优于我们比较的所有其他训练信号，包括在其他设置完全相同的条件下训练的二元通过或失败奖励，且在代码生成任务上的领先幅度最大。当智能体还必须提交代码仓库补丁，并由各项目的隐藏测试进行评估时，其解决留出问题的比例从 59.6% 提升至 72.5%。将训练得到的模型检查点不作任何改动，在三个未参与训练的验证套件上进行评估，结果在所有套件上均有提升，其中一个套件所使用的语言和验证器均未出现在训练中。