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.
@article{arxiv.2602.05762,
title = {RocqSmith: Can Automatic Optimization Forge Better Proof Agents?},
author = {Andrei Kozyrev and Nikita Khramov and Denis Lochmelis and Valerio Morelli and Gleb Solovev and Anton Podkopaev},
journal= {arXiv preprint arXiv:2602.05762},
year = {2026}
}