一句话：提出结合监督与无奖励强化学习的证明合成工具 QEDCartographer，利用证明分支结构提升 Coq 定理自动证明率。
形式验证能提升软件可靠性，但人工编写证明极为困难。现有证明合成工具依赖定理证明器的粗粒度进度信号，搜索近乎无方向。QEDCartographer 结合监督学习与强化学习，将证明的分支结构纳入搜索，实现无奖励强化学习以缓解稀疏奖励问题。在含 124 个 Coq 项目、68.5K 条定理的 CoqGym 基准上，它全自动证明 21.4% 的测试定理，优于此前最优的纯监督学习工具 Proverbot9001 (19.8%) 和组合 62 个工具的 Diva (19.2%)；相比 Proverbot9001，平均证明短 26%、快 27%。与 CoqHammer 结合可证明 31.8%，表明强化学习是改进证明合成搜索的有效方向。
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 proofsynthesis tool that combines supervised and reinforcement learning to more effectively explore the proof space. QEDCartographer incorporates the proofs' branching structure, enabling rewardfree search and overcoming the sparse reward problem inherent to formal verification. We evaluate QEDCartographer using the CoqGym benchmark of 68.5 K theorems from 124 open-source Coq projects. QEDCartographer fully automatically proves$\mathbf{2 1. 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 26 % shorter proofs 27 % faster, on average over the theorems both tools prove. Together, QEDCartographer and non-learning-based CoqHammer prove 31.8 % of the theorems, while CoqHammer alone proves$\mathbf{2 6. 6 \%}$. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools' search mechanisms.
DOI 原文 ·
@inproceedings{paperbot8875,
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},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00033}
}