QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
Published in Proceedings of the IEEE/ACM International Conference on Software Engineering (ICSE), 2025
Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. QEDCartographer combines supervised and reinforcement learning to more effectively explore the proof space, incorporating proofs’ branching structure to enable reward-free search and overcome the sparse reward problem inherent to formal verification.
Evaluated on the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects, QEDCartographer proves 21.4% of test-set theorems — outperforming all prior search-based proof-synthesis tools. Together with CoqHammer, it proves 31.8% of theorems.
Recommended citation: Sanchez-Stern, A., Varghese, A., Kaufman, Z., Zhang, D., Ringer, T., & Brun, Y. (2025). "QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning." Proceedings of ICSE 2025. Ottawa, Ontario, Canada.
Download Paper