Evolving prover interfaces improve automated math proof efficiency
Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
Artificial Intelligence
Summary
Proving math problems using computers needs a way for AI agents to talk with software that checks the proofs. The usual tools are made for humans, not these AI agents, making the process slower and costlier. The paper’s authors used a method that tries new interface features step-by-step and keeps only the improvements. They created a new tool for a prover named Rocq, which made AI agents solve math problems more successfully, faster, and cheaper. This tool also worked well when used with a different prover called Lean.
What this means in practice
- •For software engineers: Improve automated theorem proving tools to reduce cost and time when verifying complex mathematical proofs.
- •For mathematical software developers: Enhance interaction interfaces for AI-based proof assistants, leading to better performance and resource use across different systems.
Authors
Jules Viennot, Guillaume Baudart, Marc Lelarge
Abstract
Recent achievements in AI-assisted mathematics require intensive interaction of agents with proof assistants to generate machine-checked proof certificates. Agents interact with proof assistants such as Rocq or Lean through an interface that controls what the agent receives from the prover and the cost of these interactions. Today, these interfaces are adapted from tools designed for humans and not optimized for agents. We propose an evolutionary method where a frontier model incrementally proposes new features and only keeps the ones that improve the overall performance of smaller models. We demonstrate the effectiveness of our method by growing, on a curated set of mathematical problems, \rme, a new MCP server for the Rocq prover. On the held-out \texttt{test} split of miniF2F-Rocq, an agent equipped with \rme outperforms both the baseline that only exposes the Rocq compiler and an established MCP server, across four models from two families, in success rate, cost per solve, and time per solve. Although evolved for Rocq, the resulting server transfers to Lean, improving cost and time per solve on a subset of PutnamBench. We release \rme and its port to Lean.