面向LLM步骤证明器的多回合离线策略强化学习与多智能体树搜索的扩展
人工智能
2025-10-10 v2
摘要
将大语言模型（LLM）集成到自动定理证明中已展现出巨大潜力，但其在扩展训练时强化学习（RL）和推理时计算方面受到根本性制约。本文介绍了BFS-Prover-V2，一个旨在解决这一双重扩展问题的系统。我们提出了两项主要创新。第一是一种新颖的多回合离线策略RL框架，用于在训练时持续提升LLM步骤证明器的性能。该框架受AlphaZero原理启发，利用多阶段专家迭代流水线，结合自适应战术级数据过滤和周期性重训练，以克服通常限制LLM智能体长期RL的性能瓶颈。第二项创新是一种规划增强的多智能体搜索架构，用于在推理时扩展推理能力。该架构采用通用推理模型作为高层规划器，将复杂定理迭代分解为一系列更简单的子目标。这种分层方法大幅缩小了搜索空间，使一组并行证明智能体能够通过利用共享证明缓存高效协作。我们证明这种双重扩展方法在已建立的形式数学基准上取得了最先进的结果。BFS-Prover-V2在MiniF2F和ProofNet测试集上分别达到95.08%和41.4%。虽然本工作在形式数学领域得到验证，但所提出的RL和推理技术具有更广泛的适用性，可应用于其他需要长视野多回合推理和复杂搜索的领域。
引用
@article{arxiv.2509.06493,
title = {Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers},
author = {Ran Xin and Zeyu Zheng and Yanchen Nie and Kun Yuan and Xia Xiao},
journal= {arXiv preprint arXiv:2509.06493},
year = {2025}
}