RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation

TL;DR

This paper introduces RocqStar, a novel system combining similarity-driven retrieval and agentic models to improve Rocq proof generation in formal verification, achieving significant performance gains.

Contribution

It proposes a self-attentive embedder for premise retrieval and a multi-agent system with debate and reflection mechanisms for enhanced Rocq proof generation.

Findings

Up to 28% improvement in generator performance.

20% increase in proof success rate with multi-agent debate.

Nearly doubled success rate for complex theorems.

Abstract

Interactive Theorem Proving was repeatedly shown to be fruitful when combined with Generative Artificial Intelligence. This paper assesses multiple approaches to Rocq generation and illuminates potential avenues for improvement. We identify retrieval-based premise selection as a central component of effective Rocq proof generation and propose a novel approach based on 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 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.