arXiv cs.AI· Jules Viennot, Guillaume Baudart, Marc Lelarge·· 9 天前AI 评分30
面向 Rocq 与 Lean 的智能体/证明器接口进化：用进化式工具设计实现低成本定理证明
Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
AI 导读
研究者提出一种进化式方法，让前沿模型逐步为证明器接口提出新功能，只保留能提升小模型整体表现的部分，据此培育出 Rocq 证明器的新 MCP 服务器 ROCQ-MCP-EVOLVE。
正文 · 原文
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, 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.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2609.39544 [cs.AI] |
| (or arXiv:2609.39544v3 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2609.39544 arXiv-issued DOI via DataCite |
Submission history
From: Jules Viennot [view email]
[v1]
Wed, 30 Sep 2026 11:44:15 UTC (255 KB)
[v2]
Thu, 1 Oct 2026 08:57:55 UTC (255 KB)
[v3]
Thu, 8 Oct 2026 13:42:28 UTC (255 KB)
来源：arXiv cs.AI · arxiv.org