用进化方法为 Rocq 和 Lean 设计智能体/证明器接口，降低定理证明成本
Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
AI 导读
研究者提出一种进化方法，由前沿模型逐步提出新接口功能，只保留能提升小模型整体表现的部分，并据此培育出面向 Rocq 证明器的新 MCP 服务器 rme。在 miniF2F-Rocq 的留出 test 划分上，配备 rme 的智能体在来自两个模型族的四个模型上，成功率、单次求解成本和单次求解时间均优于仅暴露 Rocq 编译器的基线以及一个已有 MCP 服务器。该服务器虽为 Rocq 进化而来，却能迁移到 Lean，在 PutnamBench 子集上改善成本与时间，作者已开源 rme 及其 Lean 移植版。