证明也有「选择困难症」？腾讯AI Lab与大模型研究部联手打造 MPS-Prover ，多视角破解形...

正文

请到「今天看啥」查看全文

多视角树搜索证明器 (MPS-Prover)

为克服上述逐步式证明器的局限性，我们提出了 多视角树搜索证明器 (MPS-Prover) ，其核心包含两项关键创新：

1. 高效的训练后数据筛选策略 ：针对当前专家迭代方法中普遍存在的训练数据冗余问题，我们设计了明确的筛选规则，有效剔除约40%的低价值训练样本。此举在显著提升训练效率的同时，保证甚至提升了模型在复杂策略学习上的准确性，并通过引入自然语言推理数据缓解了对形式化策略生成的过拟合。

2. 融合启发式评估的多视角树搜索算法 ：在传统最佳优先搜索（BFS）和基于学习的评估模型基础上，我们引入了三种精心设计的启发式评估规则，共同指导搜索树的节点扩展：

• 策略有效性评分 ：为不同策略（如 rcases,intro等结构性策略 vs. norm_num,simp_all等辅助性策略）赋予不同权重，优先探索对证明目标有更大影响的路径。详细评分表格在论文附录中。

• 最小化分支复杂度 ：优先选择导致证明状态中 case（分支）数量最少的策略，鼓励更简洁的证明路径。

• 最短状态优先 ：优先选择产生更短Lean 4证明状态字符串的策略，倾向于更直接、易于管理的证明状态。

如上图所示，在每个搜索层，MPS-Prover会从LLM为当前节点生成的候选策略中，并行地根据评估模型预测以及上述三条启发式规则各选取一个最优后续节点（若多个视角选出相同节点则仅保留一个），从而确保搜索路径的多样性，避免单一评估标准带来的偏差，有效跳出局部最优和不可证状态。

主要性能 ：如下表所示，MPS-Prover在所有参与比较的逐步式证明器中取得了最佳性能。在miniF2F上，MPS-Prover成功证明了244个问题中的185个，相较于先前最佳的BFS-Prover提升了约3个百分点。在7B模型级别，其性能仅次于通过更大模型蒸馏而来的DeepSeek-Prover-V2 (CoT)，显示了我们方法在同等规模直接训练模型中的领先性。

固定预算下的性能对比 ：为公平比较MPS与BFS在同等计算资源下的效率，我们对比了MPS pass@k与BFS pass@4k的性能。如下图所示，MPS在各预算水平下均持续优于BFS，验证了多视角策略在提升搜索效率方面的优势。

请到「今天看啥」查看全文