构建智能体/证明器接口：面向Rocq和Lean成本高效定理证明的进化式工具设计

中文摘要 AI 辅助

AI辅助数学的最新成就要求智能体与证明助手进行密集交互，以生成机器可检查的证明证书。智能体通过一个接口与Rocq或Lean等证明助手交互，该接口控制智能体从证明器接收的内容以及这些交互的成本。如今，这些接口是从为人类设计的工具改编而来，并未针对智能体进行优化。我们提出一种进化方法，其中前沿模型逐步提出新功能，仅保留那些能提升较小模型整体性能的功能。我们通过在精选的数学问题集上为Rocq证明器培育一个新的MCP服务器\ me，证明了我们方法的有效性。在miniF2F-Rocq的保留测试集上，配备\ me的智能体在成功率、每次求解成本和每次求解时间方面，均优于仅暴露Rocq编译器的基线以及一个成熟的MCP服务器，涵盖来自两个家族的四种模型。尽管是为Rocq进化的，生成的服务器可迁移至Lean，在PutnamBench的一个子集上改善了每次求解的成本和时间。我们发布了\ me及其Lean移植版。

英文摘要

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, ROCQ-MCP-EVOLVE, a new MCP server for the Rocq prover. On the held-out test split of miniF2F-Rocq, an agent equipped with ROCQ-MCP-EVOLVE 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 ROCQ-MCP-EVOLVE and its port to Lean.

发表机构

• IRIF, Université Paris Cité, Inria, CNRS（IRIF，巴黎西岱大学，法国国家信息与自动化研究所，法国国家科学研究中心）
• DI ENS, PSL University, Inria（DI ENS，巴黎文理研究大学，法国国家信息与自动化研究所）

机构由 AI 辅助整理，请以论文原文为准。