Automating Formal Verification with Reinforcement Learning and Recursive Inference

📄 arXiv: 2605.30914v1 📥 PDF

作者: Max Tan

分类: cs.LG, cs.SE

发布日期: 2026-05-29

备注: Master's thesis, 140 pages, 16 figures, 17 tables

💡 一句话要点

利用强化学习和递归推理自动化形式化验证程序生成与证明

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化验证 强化学习 大型语言模型 程序生成 自动推理

📋 核心要点

  1. 现有方法在形式化验证领域面临数据稀缺和对精确规范的高度依赖性挑战，使得大型语言模型难以生成正确的程序和证明。
  2. 论文提出利用强化学习从可验证奖励中学习，并结合验证器引导的推理时搜索，以提升LLM在形式化验证任务中的表现。
  3. 实验结果表明，该方法在Dafny和Lean环境中均取得了显著的性能提升，验证通过率分别提升至31.1%和69.2%。

📝 摘要（中文）

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

🔬 方法详解

问题定义：论文旨在解决大型语言模型在自动化形式化验证中面临的挑战，具体表现为数据稀缺和对形式规范的严格要求。现有方法难以生成满足机器可检查规范的程序和证明，导致验证通过率低。

核心思路：论文的核心思路是利用强化学习（RL）从验证器提供的奖励信号中学习，并结合验证器引导的推理时搜索，以提高LLM生成正确程序和证明的能力。通过与验证器的交互，模型可以逐步改进其生成结果，最终达到满足形式规范的目标。

技术框架：论文包含两个主要的技术框架。第一个框架是基于Dafny的RLVR，使用Group Relative Policy Optimization（GRPO）训练模型，并根据编译器和验证器的结果对生成的程序进行评分。第二个框架是基于Lean的验证器引导的推理支架，将证明生成视为分解子目标、验证器反馈和修复的结构化搜索过程。

关键创新：论文的关键创新在于将强化学习与形式化验证相结合，利用验证器作为环境，为模型提供可验证的奖励信号。此外，论文还提出了验证器引导的推理支架，通过分解任务和利用验证器反馈，实现了更有效的证明生成。

关键设计：在RLVR框架中，论文使用了Group Relative Policy Optimization（GRPO）及其变体，以提高训练效率和稳定性。在验证器引导的推理支架中，论文设计了证明修改器，用于根据验证器的反馈修复生成的证明。此外，论文还针对不同的验证环境（Dafny和Lean）设计了特定的任务分解策略和工具使用策略。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在APPS派生的Dafny数据集上，使用RLVR将验证奖励从2.2%提高到58.1%。在过滤掉欠指定和易受攻击的任务后，多轮RLVR将验证通过率从9.7%提高到31.1%。在Lean环境中，带有证明修改器的完整支架将初始VeriCoding试点集的通过率从直接修复下的46.2%提高到69.2%。

🎯 应用场景

该研究成果可应用于软件安全、硬件验证等领域，通过自动化形式化验证，可以有效减少软件漏洞和硬件错误，提高系统的可靠性和安全性。此外，该方法还可以用于教育领域，帮助学生学习形式化验证技术，并提高其编程能力。

📄 摘要（原文）

Automated formal verification remains challenging for large language models because data for proof assistants and verification-aware languages is scarce, and correctness depends on satisfying precise machine-checkable specifications rather than producing plausible code. This thesis studies how verifier environments can improve LLM generation of verified programs and proofs through reinforcement learning from verifiable rewards (RLVR) and verifier-guided inference-time search. First, we train open-source models in Dafny with RLVR using Group Relative Policy Optimization (GRPO) and related variants, assembling generated candidates into complete programs and scoring them with compiler and verifier outcomes. Initial experiments on an APPS-derived Dafny dataset increased verified reward from 2.2% to 58.1%, but revealed specification hacking, where models exploit weak formal specifications instead of implementing the intended solutions. After filtering underspecified and vulnerable tasks, multi-turn RLVR on the refined benchmark improves the verified pass rate from 9.7% to 31.1%. Second, we develop a verifier-guided inference scaffold in Lean that treats proof generation as structured search over decomposed subgoals, verifier feedback, diagnostics, and repair. With a fixed base model, the full scaffold with proof reviser improves pass rate on an initial VeriCoding pilot set from 46.2% under direct repair to 69.2%. On the larger VERINA dataset, whole-task decomposition plus proof reviser solves 7 of 42 previously unsolved tasks. We also introduce Dalek-Bench, a repository-scale Lean benchmark derived from the Rust $\texttt{curve25519-dalek}$ verification project; preliminary results remain weak, indicating that stronger progress evaluation and task-specific tool-use policies are still needed.