📄 论文总结
BFS-Prover-V2：基于多智能体搜索与专家迭代的定理证明系统
BFS-Prover-V2: A Multi-Agent Search and Expert Iteration System for Theorem Proving
1️⃣ 一句话总结
BFS-Prover-V2是一个针对Lean4中神经定理证明的综合训练和推理系统，通过多阶段专家迭代框架和规划器增强的多智能体搜索架构，在数学定理证明任务中实现了最先进的性能。
2️⃣ 论文创新点
1. 多回合离线强化学习框架
- 创新点是什么：受AlphaZero启发的多阶段专家迭代流程，包含自适应战术级数据过滤和周期性重训练机制
- 与已有方法的区别/改进：克服LLM智能体在长期强化学习中的性能平台期问题
- 为什么有意义：实现模型从简单问题到复杂定理的持续能力提升
2. 规划器增强的多智能体搜索架构
- 创新点是什么：使用通用推理模型作为高层规划器迭代分解复杂定理为子目标，通过并行证明智能体和共享证明缓存实现高效协作
- 与已有方法的区别/改进：大幅减少搜索空间，提升推理效率
- 为什么有意义：在形式数学基准上达到最先进性能（MiniF2F 95.08%，ProofNet 41.4%）
3. 基于困惑度的自适应数据过滤
- 创新点是什么：根据模型对策略的困惑度分布将训练数据分为低困惑度尾部、高困惑度尾部和中心分布三个区域
- 与已有方法的区别/改进：只选择中心分布的数据进行训练，避免过于简单或复杂的数据
- 为什么有意义：防止过拟合和幻觉，确保模型在能力边缘持续学习
4. 周期性软重置重训练
- 创新点是什么：定期使用当前专家模型重新解决所有过往问题，生成更简洁、直接的证明
- 与已有方法的区别/改进：通过重新合成和去噪过程增加模型熵值，重置探索潜力
- 为什么有意义：帮助模型逃离局部最优，解决性能平台期问题，保持对新难题的探索能力
3️⃣ 主要结果与价值
实验结果亮点
- 在MiniF2F测试集上达到95.08%的成功率（验证集95.49%）
- 在ProofNet测试集上达到41.4%的成功率
- 相比其他领先证明器（如r-V2-671B、Kimina-Prover-72B等）表现出显著性能提升
实际应用价值
- 为形式化数学证明提供了高效的自动化工具
- 系统能够作为真正的Lean协导器，在证明过程中随时建议下一个逻辑策略
- 多智能体架构能够处理单体证明器难以解决的复杂证明问题
4️⃣ 术语表
- BFS-Prover-V2：针对LLM定理证明训练和推理扩展问题设计的系统，采用最佳优先搜索算法和多阶段专家迭代训练
- 专家迭代（Expert Iteration）：一种强化学习过程，模型作为专家生成证明，然后利用生成的数据自我改进
- 最佳优先树搜索（BFS）：用于探索可能证明路径空间的搜索算法
- 规划器-证明器范式（Planner-Prover Paradigm）：分层推理架构，规划器负责战略分解，证明器负责具体证明
- 困惑度分布：模型对策略的困惑度概率分布，用于评估训练数据的价值
- 动态重规划（Dynamic Replanning）：当证明器无法在计算预算内证明子目标时，重新查询规划器生成修订计划的机制
- MiniF2F：高中数学竞赛测试基准，用于评估数学定理证明系统性能