RocqSmith: Can Automatic Optimization Forge Better Proof Agents?

TL;DR

This paper investigates the potential of automatic AI optimization methods to improve proof agents in formal verification, finding that simple approaches are effective but still lag behind expert-designed agents.

Contribution

It evaluates various automatic optimization techniques on a formal proof agent, highlighting the effectiveness of simple methods and the gap with expert-crafted solutions.

Findings

Simple few-shot bootstrapping is most consistently effective.

Automatic methods improve performance but do not surpass expert-designed agents.

Various optimizers yield measurable improvements.

Abstract

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.