RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
This work addresses the challenge of automated formal verification for theorem proving researchers, though it appears incremental as it builds on existing generative AI and retrieval methods.
The paper tackles the problem of generating Rocq proofs in interactive theorem proving by proposing a multi-stage agentic system with similarity-driven retrieval, achieving up to a 28% relative performance increase and a 20% overall boost in proof success rate through multi-agent debate.
Interactive Theorem Proving was repeatedly shown to be fruitful combined with Generative Artificial Intelligence. This paper assesses multiple approaches to Rocq generation and illuminates potential avenues for improvement. We highlight the importance of thorough premise selection for generating Rocq proofs and propose a novel approach, leveraging retrieval via a self-attentive embedder model. The evaluation of the designed approach shows up to 28% relative increase of the generator's performance. We tackle the problem of writing Rocq proofs using a multi-stage agentic system, tailored for formal verification, and demonstrate its high effectiveness. We conduct an ablation study and demonstrate shows that incorporating multi-agent debate during the planning stage increases the proof success rate by 20% overall and nearly doubles it for complex theorems, while the reflection mechanism further enhances stability and consistency.