RocqSmith: Can Automatic Optimization Forge Better Proof Agents?

Andrei Kozyrev, Nikita Khramov, Denis Lochmelis +3

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 a…