通过强化学习和递归推理自动进行形式验证

对于 大语言模型 来说，自动形式验证仍然具有挑战性，因为证明助手和验证感知语言的数据很少，并且正确性取决于满足精确的机器可检查规范，而不是生成合理的代码。本论文研究了验证者环境如何通过可验证奖励（RLVR）的强化学习和验证者引导的推理时间搜索来改进经过验证的程序和证明的 LLM 生成。首先，我们使用组相对策略优化 (GRPO) 和相关变体在 Dafny 中通过 RLVR 训练开源模型，将生成的候选者组装成完整的程序，并使用编译器和验证器结果对其进行评分。在 APPS 派生的 Dafny 数据集上进行的初步实验将经过验证的奖励从 2.2% 增加到 58.1%，但暴露了规范黑客攻击，其中模型利用弱正式规范而不是实现预期的解决方案。在过滤未指定和易受攻击的任务后，在细化基准上的多轮 RLVR 将验证通过率从 9.7% 提高到 31.1%。其次，我们在精益中开发了一个验证者引导的推理支架，它将证明生成视为对分解的子目标、验证者反馈、诊断和修复的结构化搜索。借助固定基础模型，带有验证修改器的完整支架将初始 VeriCoding 试验集的通过率从直接修复下的 46.2% 提高到 69.2%。在更大的 VERINA 数据集上，整个任务分解加上证明修订器解决了 42 个先前未解决的任务中的 7 个。我们还引入了 Dalek-Bench，一个源自 Rust $\texttt{curve25519-dalek}$ 验证项目的存储库规模精益基准；初步结果仍然疲软，表明仍需要更强有力的进展评估和针对特定任务的工具使用政策。