RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911398234161152 |
|---|---|
| author | Kozyrev, Andrei Khramov, Nikita Solovev, Gleb Podkopaev, Anton |
| author_facet | Kozyrev, Andrei Khramov, Nikita Solovev, Gleb Podkopaev, Anton |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_22846 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation Kozyrev, Andrei Khramov, Nikita Solovev, Gleb Podkopaev, Anton Machine Learning Artificial Intelligence Logic in Computer Science Software Engineering 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. |
| title | RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation |
| topic | Machine Learning Artificial Intelligence Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2505.22846 |