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。
正文 · AI 翻译
摘要：近期 AI 辅助数学的成果需要智能体与证明助手进行密集交互，以生成机器可检验的证明证书。智能体通过一个接口与 Rocq 或 Lean 等证明助手交互，该接口控制智能体从证明器接收到的内容以及这些交互的成本。如今，这些接口改编自为人类设计的工具，并未针对智能体进行优化。我们提出一种进化方法，其中前沿模型逐步提出新功能，并仅保留那些能提升较小模型整体性能的功能。我们通过在一个精选的数学问题集上培育 ROCQ-MCP-EVOLVE（一个面向 Rocq 证明器的新 MCP 服务器）来证明该方法的有效性。在 miniF2F-Rocq 的留出测试集上，配备 ROCQ-MCP-EVOLVE 的智能体在成功率、每次求解成本和每次求解时间方面，均优于仅暴露 Rocq 编译器的基线以及一个已有的 MCP 服务器，且跨越两个模型家族的四个模型。尽管是为 Rocq 进化而来，所得服务器可迁移至 Lean，在 PutnamBench 的一个子集上改善了每次求解的成本和时间。我们发布 ROCQ-MCP-EVOLVE 及其到 Lean 的移植版本。
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2609.39544 [cs.AI] |
| （或 arXiv:2609.39544v3 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2609.39544 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Jules Viennot [查看邮箱]
[v1]
2026年9月30日星期三 11:44:15 UTC（255 KB）
[v2]
2026年10月1日星期四 08:57:55 UTC（255 KB）
[v3]
2026年10月8日星期四 13:42:28 UTC（255 KB）
来源：arXiv cs.AI · arxiv.org