论文
发展Agent/证明者接口：Rocq 和 Lean 中经济有效的定理证明的进化工具设计
Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
摘要
人工智能辅助数学的最新成就需要智能体与证明助手进行密集交互，以生成机器检查的证明证书。Agent通过一个接口与证明助手（例如 Rocq 或 Lean）进行交互，该接口控制Agent从证明者接收的内容以及这些交互的成本。如今，这些界面是根据为人类设计的工具改编的，而不是针对Agent进行优化的。我们提出了一种进化方法，其中前沿模型增量地提出新特征，并且只保留那些能够提高较小模型整体性能的特征。我们通过在一组精选的数学问题上开发用于 Rocq 证明者的新 MCP 服务器来证明我们方法的有效性。在 miniF2F-Rocq 的保留 \texttt{test} 拆分中，配备 rocq-mcp-evolve 的Agent在两个系列的四个模型中的成功率、每次求解成本和每次求解时间方面均优于仅公开 Rocq 编译器的基线和已建立的 MCP 服务器。尽管针对 Rocq 进行了改进，但最终的服务器已转向 Lean，从而改善了 PutnamBench 子集上每次求解的成本和时间。我们发布了 rocq-mcp-evolve 及其对 Lean 的移植。