QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
作者: Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Dylan Zhang, Talia Ringer, Yuriy Brun
分类: cs.SE, cs.LG, cs.PL
发布日期: 2024-08-17 (更新: 2024-12-17)
备注: Authors could not agree on final revision. Please see author websites for individual versions of paper
DOI: 10.1109/ICSE55347.2025.00033
💡 一句话要点
QEDCartographer：利用无奖励强化学习自动化形式化验证
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)
关键词: 形式化验证 自动化证明 强化学习 无奖励学习 定理证明
📋 核心要点
- 形式化验证依赖手动编写证明，效率低且难度大，现有自动化方法依赖定理证明器，但其提供的进度估计粗糙，导致搜索效率低下。
- QEDCartographer结合监督学习和强化学习，利用证明的分支结构进行无奖励搜索，克服了形式化验证中稀疏奖励的难题，提升搜索效率。
- 实验结果表明，QEDCartographer在CoqGym基准测试中显著优于现有工具，证明成功率更高，生成的证明更短且速度更快。
📝 摘要（中文）
形式化验证是生成可靠软件的一种有前景的方法，但手动编写验证证明的难度严重限制了其在实践中的效用。最近的方法通过使用定理证明器引导搜索证明空间来自动化一些证明合成。不幸的是，定理证明器仅提供对进度的最粗略估计，导致实际上是无方向的搜索。为了解决这个问题，我们创建了QEDCartographer，这是一种自动证明合成工具，它结合了监督学习和强化学习，以更有效地探索证明空间。QEDCartographer结合了证明的分支结构，实现了无奖励搜索，克服了形式化验证中固有的稀疏奖励问题。我们使用来自124个开源Coq项目的68.5K定理的CoqGym基准评估QEDCartographer。QEDCartographer完全自动地证明了21.4%的测试集定理。先前的基于搜索的证明合成工具Tok、Tac、ASTactic、Passport和Proverbot9001仅依赖于监督学习，分别证明了9.6%、9.8%、10.9%、12.5%和19.8%。Diva结合了62个工具，证明了19.2%。与最有效的先前工具Proverbot9001相比，QEDCartographer产生的证明平均短34%，速度快29%（针对两种工具都证明的定理）。QEDCartographer和非学习的CoqHammer一起证明了30.3%的定理，而CoqHammer单独证明了26.6%。我们的工作表明，强化学习是改进证明合成工具搜索机制的一个富有成果的研究方向。
🔬 方法详解
问题定义：论文旨在解决形式化验证中手动编写证明效率低下的问题。现有方法依赖定理证明器引导搜索，但定理证明器提供的进度估计过于粗糙，导致搜索效率低下，难以找到有效的证明路径。
核心思路：论文的核心思路是结合监督学习和强化学习，更有效地探索证明空间。通过引入证明的分支结构，实现无奖励搜索，从而克服形式化验证中固有的稀疏奖励问题。这种方法允许模型在没有明确奖励信号的情况下学习有效的证明策略。
技术框架：QEDCartographer的整体框架包含以下几个主要模块：1) 数据收集：利用CoqGym基准收集大量的Coq项目定理及其证明。2) 监督学习：使用收集的数据训练一个策略网络，用于预测给定状态下应该采取的证明步骤。3) 强化学习：利用强化学习算法，在证明空间中进行探索，学习更有效的证明策略。关键在于使用无奖励强化学习，避免了手动设计奖励函数的困难。4) 证明合成：将训练好的策略网络应用于新的定理，自动生成证明。
关键创新：最重要的技术创新点在于使用无奖励强化学习进行证明搜索。与传统的强化学习方法不同，QEDCartographer不需要手动设计奖励函数，而是利用证明的分支结构，将证明过程视为一个状态转移过程，通过学习状态之间的转移概率来优化证明策略。这克服了形式化验证中稀疏奖励的问题，使得模型能够更有效地探索证明空间。
关键设计：QEDCartographer的关键设计包括：1) 策略网络结构：策略网络用于预测给定状态下应该采取的证明步骤，其结构对性能至关重要。具体网络结构未知。2) 强化学习算法：选择合适的强化学习算法对于训练模型的性能至关重要。论文中使用的具体算法未知。3) 证明状态表示：如何有效地表示证明状态，以便模型能够学习到有效的证明策略，是一个关键问题。具体的状态表示方法未知。
🖼️ 关键图片
📊 实验亮点
QEDCartographer在CoqGym基准测试中取得了显著成果，自动证明了21.4%的测试集定理，优于先前的工具Tok (9.6%)、Tac (9.8%)、ASTactic (10.9%)、Passport (12.5%)和Proverbot9001 (19.8%)。与Proverbot9001相比，QEDCartographer生成的证明平均短34%，速度快29%。QEDCartographer与CoqHammer结合，证明了30.3%的定理，高于CoqHammer单独证明的26.6%。
🎯 应用场景
QEDCartographer可应用于软件可靠性验证、编译器验证、操作系统内核验证等领域，通过自动化形式化验证过程，提高软件的可靠性和安全性，降低开发和维护成本。该研究的未来影响在于推动形式化验证技术的普及，使其能够更广泛地应用于实际软件开发中。
📄 摘要（原文）
Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding a search through the proof space using a theorem prover. Unfortunately, the theorem prover provides only the crudest estimate of progress, resulting in effectively undirected search. To address this problem, we create QEDCartographer, an automated proof-synthesis tool that combines supervised and reinforcement learning to more effectively explore the proof space. QEDCartographer incorporates the proofs' branching structure, enabling reward-free search and overcoming the sparse reward problem inherent to formal verification. We evaluate QEDCartographer using the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects. QEDCartographer fully automatically proves 21.4% of the test-set theorems. Previous search-based proof-synthesis tools Tok, Tac, ASTactic, Passport, and Proverbot9001, which rely only on supervised learning, prove 9.6%, 9.8%, 10.9%, 12.5%, and 19.8%, respectively. Diva, which combines 62 tools, proves 19.2%. Comparing to the most effective prior tool, Proverbot9001, QEDCartographer produces 34% shorter proofs 29% faster, on average over the theorems both tools prove. Together, QEDCartographer and non-learning-based CoqHammer prove 30.3% of the theorems, while CoqHammer alone proves 26.6%. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools' search mechanisms.