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 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 26.6%. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools' search mechanisms.
@inproceedings{Sanchez-Stern25icse,
author = {Alex Sanchez-Stern and Abhishek Varghese and Zhanna Kaufman and
Dylan Zhang and Talia Ringer and Yuriy Brun},
title =
{QEDCartographer:
Automating Formal Verification Using Reward-Free Reinforcement Learning},
booktitle = {Proceedings of the 47th International Conference on Software Engineering (ICSE)},
venue = {ICSE},
address = {Ottawa, ON, Canada},
month = {April},
date = {28--30},
year = {2025},
accept = {$\frac{46}{523} \approx 8.8\%$ (1st cycle direct accept, without revision)},
pages = {307--320},
doi = {10.1109/ICSE55347.2025.00033},
note = {ACM artifact badges granted:
Artifact Available.
DOI:
10.1109/ICSE55347.2025.00033, arXiv:
abs/2408.09237},
abstract = {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 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 26.6%. Our work demonstrates that
reinforcement learning is a fruitful research direction for improving
proof-synthesis tools' search mechanisms.},
}