# RocqSmith: Can Automatic Optimization Forge Better Proof Agents?

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 21 references that are in the map.
- First posted on arXiv 5 Feb 2026.

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

- [DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines](https://mlsanity.com/paper/2310.03714/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Agentic Context Engineering: Evolving Contexts for Self-Improving Language Models](https://mlsanity.com/paper/2510.04618/) (2025)
- [Optimizing Instructions and Demonstrations for Multi-Stage Language Model Programs](https://mlsanity.com/paper/2406.11695/) (2024)
- [Security Weaknesses of Copilot-Generated Code in GitHub Projects: An Empirical Study](https://mlsanity.com/paper/2310.02059/) (2023)
- [Re-Reading Improves Reasoning in Large Language Models](https://mlsanity.com/paper/2309.06275/) (2023)
- [CoqPilot, a plugin for LLM-based generation of proofs](https://mlsanity.com/paper/2410.19605/) (2024)
- [RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation](https://mlsanity.com/paper/2505.22846/) (2025)
- [Agentic Proof Automation: A Case Study](https://mlsanity.com/paper/2601.03768/) (2026)
- [Bridging the Gap between Programming Languages and Hardware Weak Memory Models](https://mlsanity.com/paper/1807.07892/) (2018)

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

- [Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean](https://mlsanity.com/paper/2609.39544/) (2026)

## Abstract (arXiv)

This work studies the applicability of automatic AI agent optimization methods to real-world agents in formal verification settings, focusing on automated theorem proving in Rocq as a representative and challenging domain. We evaluate how different automatic agent optimizers perform when applied to the task of optimizing a Rocq proof-generation agent, and assess whether parts of the fine-grained tuning of agentic systems, such as prompt design, contextual knowledge, and control strategies, can be automated. Our results show that while several optimizers yield measurable improvements, simple few-shot bootstrapping is the most consistently effective; however, none of the studied methods matches the performance of a carefully engineered state-of-the-art proof agent.