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

arXiv: https://arxiv.org/abs/2505.22846 · HTML: https://mlsanity.com/paper/2505.22846/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 18 of its 39 references that are in the map.
- First posted on arXiv 28 May 2025.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 18 of 18)

- [Representation Learning with Contrastive Predictive Coding](https://mlsanity.com/paper/1807.03748/) (2018)
- [CodeBERT: A Pre-Trained Model for Programming and Natural Languages](https://mlsanity.com/paper/2002.08155/) (2020)
- [Encouraging Divergent Thinking in Large Language Models through Multi-Agent Debate](https://mlsanity.com/paper/2305.19118/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [A Structured Self-attentive Sentence Embedding](https://mlsanity.com/paper/1703.03130/) (2017)
- [MapCoder: Multi-Agent Code Generation for Competitive Problem Solving](https://mlsanity.com/paper/2405.11403/) (2024)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [A Peek into Token Bias: Large Language Models Are Not Yet Genuine Reasoners](https://mlsanity.com/paper/2406.11050/) (2024)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://mlsanity.com/paper/2410.15700/) (2024)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)
- [Rethinking InfoNCE: How Many Negative Samples Do You Need?](https://mlsanity.com/paper/2105.13003/) (2021)
- [CoqPilot, a plugin for LLM-based generation of proofs](https://mlsanity.com/paper/2410.19605/) (2024)
- [Tactic Learning and Proving for the Coq Proof Assistant](https://mlsanity.com/paper/2003.09140/) (2020)
- [Bridging the Gap between Programming Languages and Hardware Weak Memory Models](https://mlsanity.com/paper/1807.07892/) (2018)
- [Learning Structure-Aware Representations of Dependent Types](https://mlsanity.com/paper/2402.02104/) (2024)

## Built on by (most cited first, 4 of 4)

- [TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow](https://mlsanity.com/paper/2601.17332/) (2026)
- [RocqSmith: Can Automatic Optimization Forge Better Proof Agents?](https://mlsanity.com/paper/2602.05762/) (2026)
- [SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematics](https://mlsanity.com/paper/2606.29894/) (2026)
- [ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents](https://mlsanity.com/paper/2610.03796/) (2026)

## Abstract (arXiv)

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.