EconProver：面向自动定理证明更经济的测试时扩展
计算与语言
2025-09-17 v1 人工智能
摘要
大语言模型近期推动了自动定理证明领域的发展，通过广泛采用的测试时扩展策略（特别是反思性思维链推理和增加采样次数）获得了显著的性能提升。然而，这两者都为推理引入了巨大的计算开销。此外，现有的成本分析通常仅调节采样次数，而忽略了不同扩展策略引入的采样成本上的巨大差异。在本文中，我们系统地比较了 ATP 模型不同测试时扩展策略的效率，并证明了当前最先进的开源方法效率低下。随后，我们研究了在保持原有性能的同时显著减少 token 使用量和采样次数的方法。具体而言，我们提出了两种可集成到统一的 EconRL 流水线中以放大收益的互补方法：(1) 动态思维链切换机制，旨在减少不必要的 token 消耗；(2) 具有可训练前缀的多样化并行扩展强化学习，以在受限的采样次数下提高通过率。在 miniF2F 和 ProofNet 上的实验表明，我们的 EconProver 仅以 12% 的计算成本就实现了与基线方法相当的性能。这项工作为部署不牺牲性能的轻量级 ATP 模型提供了可操作的见解。
引用
@article{arxiv.2509.12603,
title = {EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving},
author = {Mukai Li and Linfeng Song and Zhenwen Liang and Jiahao Xu and Shansan Gong and Qi Liu and Haitao Mi and Dong Yu},
journal= {arXiv preprint arXiv:2509.12603},
year = {2025}
}