用强化学习和验证器引导搜索，提升大模型生成可验证程序的能力
Automating Formal Verification with Reinforcement Learning and Recursive Inference
- 通过可验证奖励强化学习，让模型在Dafny中从2.2%到58.1%的验证成功率
- 在精炼数据集上多轮训练后，验证通过率提升至31.1%，减少漏洞利用
- 在Lean中构建分步证明搜索框架，使验证通过率从46.2%提升至69.2%
自动化形式化验证对大语言模型仍具挑战，因证明助手和验证感知语言的数据稀缺，且正确性依赖精确可机器检查的规范而非合理代码。本文研究如何通过强化学习从可验证奖励（RLVR）和验证器引导的推理时搜索，改善大模型生成可验证程序与证明的能力。首先，在Dafny中使用组相对策略优化（GRPO）等变体训练开源模型，将生成候选合并为完整程序，并以编译器与验证器结果评分。在基于APPS的Dafny数据集上，验证奖励从2.2%提升至58.1%，但发现模型存在规范滥用现象。过滤不明确与脆弱任务后，多轮RLVR在精炼基准上将通过率从9.7%提升至31.1%。其次，在Lean中开发验证器引导的推理框架，将证明生成视为分步子目标搜索，结合验证反馈、诊断与修复。固定基线模型下，完整框架加证明修正器使初始VeriCoding测试集通过率从46.2%升至69.2%；在更大规模VERINA数据集上，全任务分解加证明修正器解决了7个此前未解任务。还引入Dalek-Bench，一个源自Rust curve25519-dalek验证项目的仓库级Lean基准，初步结果仍弱，表明更强的进度评估与任务特定工具使用策略仍需改进。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。