QEDCartographer：利用无奖励强化学习自动化形式验证
摘要
形式化验证是生产可靠软件的一种有前景的方法，但手动编写验证证明的困难严重限制了其在实践中的效用。近期方法通过使用定理证明器引导对证明空间的搜索，实现了部分证明合成的自动化。然而，定理证明器仅提供最粗略的进度估计，导致搜索实际上是无导向的。为了解决这个问题，我们创建了 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%。结合了 62 种工具的 Diva 证明了 19.2%。与之前最有效的工具 Proverbot9001 相比，在两者都能证明的定理上，QEDCartographer 平均生成的证明短 34%，速度快 29%。QEDCartographer 与非基于学习的 CoqHammer 共同证明了 30.3% 的定理，而 CoqHammer 单独证明了 26.6%。我们的工作表明，强化学习是改进证明合成工具搜索机制的一个富有成果的研究方向。
引用
@article{arxiv.2408.09237,
title = {QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning},
author = {Alex Sanchez-Stern and Abhishek Varghese and Zhanna Kaufman and Dylan Zhang and Talia Ringer and Yuriy Brun},
journal= {arXiv preprint arXiv:2408.09237},
year = {2024}
}
备注
Authors could not agree on final revision. Please see author websites for individual versions of paper