腾讯AI Lab提出的MPS-Prover是一种新型自动化定理证明器，旨在提升大语言模型在严格逻辑推理中的表现。它通过创新的训练后数据筛选策略，有效剔除低价值训练样本，提升训练效率和模型准确性。同时，MPS-Prover融合启发式评估的多视角树搜索算法，结合策略有效性评分、最小化分支复杂度和最短状态优先等规则，指导搜索树的节点扩展，避免单一评估标准带来的偏差，从而有效提升搜索效率和证明质量，在多个基准上取得了当前最佳或领先的性能。

🔍MPS-Prover的核心创新在于训练后数据筛选策略，该策略能够有效剔除约40%的低价值训练样本，从而提升训练效率并保证模型在复杂策略学习上的准确性，并通过引入自然语言推理数据来缓解过拟合。

💡MPS-Prover融合了启发式评估的多视角树搜索算法，在传统最佳优先搜索和基于学习的评估模型基础上，引入策略有效性评分、最小化分支复杂度和最短状态优先三种启发式评估规则，共同指导搜索树的节点扩展，确保搜索路径的多样性。

✅实验结果表明，MPS-Prover在miniF2F等基准测试中取得了最佳性能，成功证明的问题数量显著高于其他逐步式证明器，并且生成的证明更短、策略更多样。同时，MPS-Prover还成功解决了六道国际数学奥林匹克竞赛（IMO）的题目，展示了其强大的推理能力。

腾讯 AI Lab 2025-05-22 17:04 广东

MPS-Prover 有效提升了搜索效率和证明质量，在多个基准上取得了当前最佳或领先的性能，并能生成更短、更多样的证明。

本文聚焦逐步式自动化定理证明器在复杂搜索中面临的偏见与低效困境，创新性提出多视角树搜索证明器（MPS-Prover），旨在提升大语言模型在严格逻辑推理中的表现。

自动化定理证明（ATP）旨在为数学或逻辑陈述自动生成形式化、可验证的证明，是人工智能、数学及形式化方法领域的核心挑战。通过将问题编码为形式化语言（如Lean），ATP系统能够产出由机器严格校验的证明，这对于严格的可验证性至关重要。尽管大语言模型（LLM）在非形式化数学推理任务中取得了显著进展，但在形式化定理证明领域，由于其对精确语法、语义的严格要求、巨大的证明步骤搜索空间以及高质量训练数据的稀缺，LLM仍面临巨大挑战。

目前主流的LLM辅助证明方法分为两大类：整体证明生成 (Whole-Proof)与逐步式证明生成 (Stepwise Proof)。前者将ATP视为代码生成任务，LLM一次性输出完整证明脚本，虽能利用模型宏观规划能力，但缺乏中间验证，难以应对复杂证明。后者则训练LLM在给定当前证明状态下，迭代式地提出下一步证明策略，并通过证明助手（如Lean编译器）实时验证反馈，这种方式更适应交互式探索和复杂推理。然而，逐步式证明器自身也存在关键难题，如下图所示，包括：(a) 评估模型（Critic Model）易因训练数据偏好重复推荐相似策略，导致搜索陷入局部最优；(b) 错误的策略选择可能导致后续状态不可证；(c) 某些自动化策略在不适用时被滥用，无法推进证明。

为克服上述逐步式证明器的局限性，我们提出了多视角树搜索证明器 (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，验证了多视角策略在提升搜索效率方面的优势。

证明特性分析：我们进一步对MPS-Prover与BFS及整体证明生成器（如Kimina-Prover, DeepSeek-Prover V2）生成的证明在长度和策略多样性上进行了定量分析（见下图与下表）。结果显示，MPS-Prover生成的证明不仅显著短于BFS，也远短于主流整体证明生成器。同时，其证明的策略多样性（定义为独热策略数/证明长度）也更高。这归因于逐步式证明器与Lean引擎的频繁交互、每步的自适应调整以及MPS对高进展策略的有效选择。

本研究提出了MPS-Prover，一种新颖的逐步式自动化定理证明器。通过创新的训练后数据筛选策略与融合启发式规则的多视角树搜索机制，MPS-Prover有效提升了搜索效率和证明质量，在多个基准上取得了当前最佳或领先的性能，并能生成更短、更多样的证明。

这项工作为提升大语言模型在形式化推理领域的应用提供了有效的方法论。我们的数据筛选方法为更高效的模型训练提供了借鉴；多视角搜索则展示了结合学习评估与启发式规则克服单一模型偏见、增强搜索鲁棒性的潜力。

除了在标准基准数据集上取得的优异表现外，我们的MPS-Prover成功解决了六道来自国际数学奥林匹克竞赛（IMO）的题目。这些题目分别是：imo_1964_p2, imo_1983_p6, imo_1960_p2, imo_1962_p2, imo_1968_p5_1 以及 imo_1959_p1。IMO作为全球范围内中学生数学竞赛的最高殿堂，其试题以极高的难度和对深刻数学洞察力的要求而著称，代表了数学解题能力的顶尖水平。

MPS-Prover能够在这些极具挑战性的问题上找到形式化证明，进一步凸显了其强大的推理能力和解决复杂数学难题的潜力。

更多内容，点击下方关注：