验证器诊断与完整性审计驱动代码强化学习

基于摘要分析。本文研究代码生成中的强化学习奖励问题：通过有限测试不等于满足所有输入上的形式化规范，而验证器的二元反馈又可能过于稀疏，并被策略通过不当假设等方式利用。作者提出结合验证器诊断、完整性审计与多轮交互的智能体强化学习方法，目标是生成符合给定形式化规范的代码。 核心奖励不是直接采用验证器的接受或拒绝结果，而是计算候选程序已完成证明义务的加权比例，并加入来自参考证明注释的隐藏探测。完整性审计具有高于验证器结果的优先级，拒绝修改规范或将待证明结论直接作为假设的候选。训练中，模型与实时验证器进行多轮交互，并由一个单独训练、随后冻结的证明专用模型协作。这里的正确性以给定规范为边界，不能等同于程序满足所有实际需求。 作者报告，实验覆盖参数规模从1.7B到14B的Qwen3模型及35B的Qwen3.6混合专家模型；在代码生成的留出验证评估中，DafnyBench上的验证通过率从66.1%提升至93.5%，SWE-Proof上从56.3%提升至100%。摘要未明确这些数值分别对应的模型及完整划分协议。作者报告，该奖励优于所比较的其他训练信号，包括其他设置相同的二元通过／失败奖励，且代码生成任务上的优势最大。 在同时要求提交仓库补丁、并由各项目隐藏测试评分的任务中，作者报告留出问题的解决比例从59.6%提升至72.5%。作者还报告，训练后的检查点未经调整，在三个未参与训练的验证套件上均有改善，其中一个套件的语言和验证器未出现在训练中；摘要未提供逐套件分数。 复现需核对证明义务的权重、隐藏探测的构造与隔离方式、审计规则、协作模型训练方式及交互预算。完整实验协议、消融及统计信息尚未验证。本文主要对象是形式化代码生成，所给材料未提供EEG或BCI验证，不能据此推断其对神经信号建模有效。