MPS-Prover：多视角搜索和数据精选让自动定理证明更上一层楼

在数学和计算机科学的交叉领域，有一项挑战极其艰巨的任务——自动定理证明。想象一下，你需要教会计算机像数学家那样，一步一步地推导出复杂数学定理的证明。这就像教一个从未见过厨房的人，仅凭食谱和原料清单，精确地烹饪出一道法式大餐。今天，我要为大家介绍一项由腾讯AI实验室和腾讯大语言模型部门的研究人员共同完成的最新突破——MPS-Prover（多视角搜索证明器）。这项研究由腾讯AI实验室的梁振文、宋麟峰、米海涛、俞栋和腾讯大语言模型部门的李杨、杨涛、张峰于2025年5月发布在arXiv预印本平台上。

自动定理证明是什么？简单来说，它是让计算机自动生成数学定理的形式化证明。这些证明必须严格遵循逻辑推理规则，确保每一步都是正确的。想象一下，你在解一道复杂的数学题，每一步都必须严格按照数学规则，而且不能有任何错误。计算机在做自动定理证明时，面临的挑战更大——它需要在巨大的搜索空间中找到正确的证明路径。

近年来，大型语言模型（LLMs）在这一领域展现出令人瞩目的能力。但现有的逐步证明系统（一步一步生成证明的方法）仍然面临几个主要问题：它们往往依赖有偏见的搜索引导，导致效率低下和次优的证明策略。比如，它们可能会陷入重复使用相同的证明策略而无法取得进展、选择错误的策略导致无法证明的状态，或者使用看似强大但在特定情况下无效的策略。

MPS-Prover通过两大创新解决了这些问题：一个高效的训练后数据精选策略和一个多视角树搜索机制。让我们一起来看看这个系统是如何工作的，以及它如何在多个挑战性基准测试中实现了最先进的性能。

一、理解自动定理证明的挑战

想象你正在教一个完全不懂数学的人如何解一道复杂的数学题。你不仅需要告诉他解题的每一步，还需要解释为什么这样做是正确的。而且，你不能跳过任何一个步骤，否则他就会迷失。

在自动定理证明领域，研究人员主要采用两种方法：一种是"整体证明生成"，即一次性生成完整的证明脚本；另一种是"逐步形式化证明生成"，即计算机在每一步都会提出下一个证明步骤（一个正式的策略），然后由形式化证明助手验证这一步是否正确，并提供更新后的证明状态作为反馈。

逐步方法有几个明显的优势：它允许与证明引擎持续交互，能够逐步简化搜索目标，具有更高的容错性（错误只需要回溯到前一步，而不是重新开始整个证明），而且天然适合使用树搜索方法探索不同的证明路径。

然而，逐步方法也面临一些关键挑战，如图1所示：

首先，引导节点选择的评价模型可能会产生偏见。这种偏见往往源于训练数据中某些"安全"或广泛适用的策略（如have或general-purpose simplifiers如aesop和simp_all）出现频率较高。这些策略虽然通常是有效证明的一部分，但如果模型过度依赖它们，可能无法找到最高效的证明路径，导致类似策略建议重复出现而使证明停滞不前。

其次，错误的策略应用可能导致"无法证明的状态"，比如过度简化条件。

第三，一些强大但具有条件性有效的策略（如aesop、simp_all）可能被无效地应用。语言模型可能由于这些策略在训练数据中频繁出现或它们能够产生看似有希望的局部简化而提出它们，但当状态不真正适合这种简化时，它们可能无法取得进展，甚至可能模糊前进的路径。

虽然基于最佳优先搜索（BFS）的方法在导航这个搜索空间方面显示出希望，但它们通常依赖单一评价分数来扩展节点，这仍然使它们容易受到这些失败模式的影响，特别是学习型评价模型中固有的偏见。

二、MPS-Prover的双重创新

MPS-Prover的创新之处在于它巧妙地解决了上述挑战，通过两个核心创新：

### 1. 训练数据精选策略

传统的专家迭代方法通常会统一添加所有新证明的问题，但MPS-Prover引入了明确的规则，过滤掉约40%的冗余或低价值训练示例，使模型专注于学习更复杂的推理模式。

想象你在学习做菜。如果你的食谱书中90%的内容都在教你如何煮白米饭，那么你在复杂烹饪技巧上的进步会很有限。同样，如果训练数据中充斥着太多简单的、重复的证明模式，模型就难以学习到更高级的推理策略。

具体来说，他们采取了两种过滤策略：

一是过滤短证明。研究团队排除了那些可以在3步或更少步骤内证明的定理。这些非常短的证明主要依赖于一组有限的基本策略（如rfl、simp_all或nlinarith），对高级问题解决技术的洞察很少。通过移除这些过于简单的例子，他们将初始训练数据集减少了约40%。

值得注意的是，过滤这些简单证明并不会降低模型解决简单问题的能力。这是因为逐步证明器的训练数据固有地包含大量"后期阶段"的证明步骤。这些步骤是在证明已经取得良好进展并接近完成时采取的，通常类似于在更简单问题中遇到的状态。因此，模型仍然通过复杂证明的中间步骤接触到足够的简单推理环境。

二是移除无效策略。他们还过滤掉了那些没有对证明状态产生有意义进展的训练数据。某些旨在简化的策略有时不会给证明状态带来任何变化，例如aesop、all_goals和simp_all。评估数据集后，他们识别并移除了约5%的此类无效策略。这种有针对性的修剪鼓励模型更好地辨别何时应该应用这些简化策略，减少过度依赖并提高证明效率。

### 2. 多视角树搜索机制

MPS-Prover的第二个关键创新是它的多视角树搜索机制。想象你在走迷宫时，不仅仅依靠一张地图，而是同时使用卫星视图、指南针和当地人的建议。这种多重指导让你更不容易走入死胡同。

传统的最佳优先搜索（BFS）方法仅基于最佳评价分数选择节点。如图2所示，MPS-Prover不仅考虑评价模型的建议，还融入了策略性设计的启发式规则，以多样化策略选择，防止陷入重复的、无效的或不可证明的状态，从而提高搜索的稳健性。

具体来说，MPS-Prover引入了三种启发式选择规则：

1. 策略有效性评分：根据策略在推进证明方面的感知效能为不同策略分配不同的分数。一般来说，那些引入新的、实质性假设或显著重构证明目标的策略，如rcases、intro、contrapose、induction或proof by contradiction（在适当应用时），会被分配更高的分数。这些通常是能够解锁新推理路径或通过分解问题来简化问题的策略。相反，辅助策略或那些专注于更局部化的简化，如norm_num和simp_all，会收到较低的分数。

2. 最小化案例分割：选择导致状态字符串中案例出现次数最少的策略。虽然像induction、constructor和split这样的策略在特定情况下是有益的，但过度的案例分割会使证明状态变得复杂。这种启发式鼓励更简单、更易管理的证明状态。

3. 最短状态偏好：优先考虑导致更短的Lean 4状态字符串的策略。与最小化案例类似，这种启发式偏好更简单、更直接的状态，有助于更高效地完成证明。

如图2所示，MPS-Prover的树搜索每次扩展步骤最多维护四个节点。具体来说，从前一次迭代中选择的节点集合开始，使用大语言模型为每个节点生成Nsamples候选策略。这会产生一个更大的潜在下一状态池（例如，如果选择了4个节点，并且Nsamples = 8，我们将有4 × 8 = 32个候选下一状态）。从这个扩展的池中：

1. 基于评价模型的预测（即与完成的距离最小的那个）选择一个节点。 2. 基于启发式规则选择额外的三个节点。每个启发式规则评估所有候选下一状态，并选择最符合其标准的那个。如果不同视角选择了相同的节点，我们只保留它一次，这意味着在这种情况下，可能会有少于四个唯一节点被带入下一个搜索迭代。

研究团队承认，每个启发式规则，包括评价模型，都有内在的偏见和限制，偏向某些证明策略或状态。然而，通过并发应用这些标准，他们显著增强了每个搜索层的多样性，确保有希望的节点被保留，而不是因为单一标准的偏见而被忽视。

三、实验证明MPS-Prover的卓越性能

为了全面评估MPS-Prover的性能，研究团队使用了两个广受认可的基准测试：

1. miniF2F：这是ATP领域的标准基准测试。问题来源于数学竞赛（AMC、AIME、IMO）以及高中和本科课程。他们使用了来自Huggingface Numina仓库的最新版本，该版本纠正了原始数据集中发现的八个错误。

2. ProofNet：这个基准测试包含371个问题，特点是本科水平的数学题。研究团队报告了其测试集上的性能。

在supervised fine-tuning（SFT）方面，他们对Qwen2.5-Math-7B-base进行了微调。SFT数据集由以下几部分组成：(1)在专家迭代过程中生成并由他们的过滤技术精选的逐步证明数据；(2)通过连接已接受的证明步骤形成的完整证明数据；(3)为搜索算法的距离评价模型训练的数据。这个聚合数据集在应用训练数据过滤方法后约为350万个问题-答案对。模型训练了3个周期，使用余弦学习率调度器，最大学习率为2 × 10^-5。累积批量大小为256。训练在8个H20 80G GPU上进行，总训练时间约为3天。

实验结果令人印象深刻。在miniF2F测试集上，MPS-Prover成功证明了244个问题中的185个，准确率达到75.82%，显著超过了之前的最先进逐步证明器BFS-prover。在所有7B参数类模型中（包括整体证明和逐步生成方法），MPS-Prover的性能仅次于DeepSeek-Prover-V2（Distilled, CoT）。考虑到他们的7B模型是从一个明显更大的模型蒸馏而来，这一结果尤为令人印象深刻。相比之下，MPS-Prover是直接通过7B规模的迭代细化进行训练的。

另一个值得注意的发现是MPS-Prover即使在受限的搜索预算下也表现出色。在评估的最小搜索预算下，MPS-Prover在miniF2F上达到了67.62%的通过率，显著优于InternLM（50.7%）和Hunyuan Prover（59.84%）在类似最小条件下的表现。令人印象深刻的是，这种基本性能已经超过了几个强大基线（如Goedel-prover和InternLM2.5-StepProver）报告的最大性能，这表明他们的方法表现出优秀的稳定性和高效性，无需穷尽搜索努力即可实现有竞争力的结果。

在更具挑战性的ProofNet基准测试上，MPS-Prover取得了32.97%的成功率，超过了所有其他7B基线模型，包括使用思维链（CoT）推理的DeepSeek-Prover-V2。

研究团队还进行了在固定预算下的比较。考虑到MPS每次迭代天然会探索更多分支，为确保公平比较，他们将MPS的pass@k与BFS的pass@4k在类似算力下进行了对比。如图3所示，MPS在分配相似计算资源时始终优于BFS。在最低预算下（MPS pass@1 vs. BFS pass@4），MPS达到67.62%（165/244）的成功率，略高于BFS的66.39%（162/244）。随着预算增加，这种优势变得更加明显，突显了MPS多样化探索策略的有效性。

四、深入分析：证明长度与多样性

为了进一步研究不同搜索策略生成的证明特征，研究团队对MPS和标准BFS（使用基于树的距离预测作为评价标准）进行了量化比较。他们通过使用相同的大语言模型骨干并只分析MPS和BFS都成功证明的定理集来确保公平比较。

图4a展示了证明长度的分布，以策略步骤数量衡量（分组为1-9和10+类别）。很明显，MPS生成的证明平均比BFS找到的证明显著更短，如虚线所示的平均值。MPS生成更多步骤较少的证明，而BFS表现出更多较长证明的长尾分布。这表明MPS中的多样化引导信号有助于避免无效策略序列或局部最优，导致更简洁的解决方案。

图4b说明了证明策略多样性的分布。多样性定义为证明中使用的唯一策略数量除以其总长度（步骤数）。分数越接近1表示相对于长度的策略多样性越高。结果清楚地表明，MPS生成的证明具有比BFS证明明显更高的平均多样性分数（见均值线）。虽然两种方法都能生成具有最大多样性的证明（分数=1.0），但BFS产生了更多多样性分数非常低的证明。这凸显了MPS在促进探索和利用更广泛策略范围方面的有效性，而BFS则仅由评价模型引导，更容易出现重复使用策略的情况。

研究团队还分析了证明特征，通过比较MPS-Prover与两个领先的整体证明生成器（Kimina-Prover-Preview和DeepSeek-Prover-V2）在170个共同解决的miniF2F问题上生成的证明长度。表4显示，MPS-Prover生成的证明明显更短（平均长度3.44步），相比之下Kimina的平均长度为15.91步，DeepSeek-Prover-V2为52.16步。

研究者将这种差异归因于操作上的不同：像MPS-Prover这样的逐步证明器受益于与Lean引擎的频繁交互。每次策略执行都会更新证明状态，允许证明器通过将新状态视为子问题来自适应地优化其策略。这种迭代过程，结合优先考虑有影响力步骤的策略级搜索，有助于发现更直接的解决方案。相比之下，整体证明系统通常最初就计划整个证明，动态适应有限，可能导致更长，尽管正确的证明脚本。

五、案例研究：MPS-Prover的优势

为了提供对证明策略和生成解决方案差异的更细微理解，研究团队对特定定理进行了案例研究，比较了MPS-Prover与Kimina-Prover和DeepSeek-Prover V2生成的证明，并展示了MPS-Prover独特解决的问题。

例如，在algebra_absapbon1pabsapbleqsumabsaon1pabsa定理（该定理涉及分式不等式证明）中，MPS-Prover生成了仅8行的极其简洁证明。关键步骤包括利用rw进行基于非负性的目标重写，使用by_cases进行情况分析（例如a = 0），然后高效使用field_simp与相关假设如abs_nonneg和mul_nonneg。证明以refine'结合div_nonneg和强大的终结器如nlinarith和positivity结束。每一步似乎都取得了实质性进展，通常通过有效利用内置的Mathlib引理和策略显著简化目标或完成部分证明。

相比之下，Kimina-Prover对同一问题的解决方案长达约40行，主要依赖一系列have语句引入中间引理。虽然逻辑合理，但这种明确陈述和证明多个中间步骤的方法导致了更冗长的证明。

DeepSeek-Prover V2的证明最长，约60行。它也广泛使用have引入并证明一系列引理，但这些引理的证明及其后续应用被分解为许多细粒度步骤。虽然展示了复杂的理解能力，但整体证明由于每个组件的详细、一步一步的推导而变得相当冗长。

在另一个例子imo_1962_p2中（一个涉及不等式和平方根的问题），MPS-Prover再次生成了非常短的证明。它有效使用refine'构建连接，然后利用强大的重写和简化策略如rw、field_simp、norm_num和nlinarith，通常链接或与特定假设一起应用。

这些案例研究强调了MPS-Prover通过其逐步搜索和选择高进展策略的趋势，倾向于生成更简洁的证明，通过有效利用强大的内置Mathlib功能。而整体证明系统，尽管能够进行复杂的推理和规划，但由于其倾向于将问题分解为许多更简单的、明确陈述的中间步骤，可能会生成更长的证明，这些步骤可能受到初始、可能更冗长的计划的限制。

此外，研究团队还展示了一个MPS-Prover成功解决而其他两个系统都失败的问题：amc12a_2020_p7。这个问题涉及基于序列a(k)^3特定值的求和评估。MPS-Prover解决方案的关键在于使用induction'作为初始步骤，然后广泛使用simp_all简化目标，以及interval_cases处理特定范围内的自然数变量。MPS-Prover成功找到了这种特定组合的策略，特别是关键的induction'和有效使用interval_cases，这突显了多视角方法在导航复杂搜索空间时的优势。

六、未来发展方向与局限性

尽管MPS-Prover在逐步自动定理证明方面取得了显著进展，但研究团队也承认逐步范式本身存在某些固有限制，特别是与整体证明生成方法相比。

当前逐步证明器（包括MPS-Prover）的一个主要限制在于处理引入复杂、嵌套证明义务的策略，如需要自己的子证明的新引理。整体证明系统可以生成包含通过have语句引入并随后证明辅助引理的完整证明脚本。然而，对于与Lean 4引擎交互的纯逐步证明器，如果策略尝试引入未经证明的引理或需要立即满足子证明的复杂结构，Lean引擎通常会引发错误并停止该证明路径。证明器无法轻易"暂停"主证明，独立证明引理，然后恢复，所有这些都在单个交互步骤中完成。

这意味着MPS-Prover，像其他当前的逐步证明器一样，在自主发现和利用不在上下文或标准库中的复杂中间引理方面不太擅长。虽然多视角搜索可以使用现有策略找到高效路径，但它不固有支持自包含方式生成和证明新的、非平凡引理，就像整体证明生成器可能计划的那样。这限制了证明器将非常复杂的问题分解为更可管理的、依赖引理的子问题的能力。

研究团队将解决这一限制作为未来工作的关键方向。正如他们在结论中提到的，探索结合MPS-Prover的逐步搜索能力与整体证明生成方法的全局规划和引理处理优势的混合方法，可能会提供一条有前途的道路来克服这一挑战，进一步扩大自动证明定理的范围。

七、结论与影响

MPS-Prover的创新展示了如何通过训练数据的精心设计和先进的搜索策略来提高自动定理证明的性能。事实上，MPS-Prover不仅在性能上超越了其他逐步证明器，还在生成的证明简洁性和多样性方面表现出色。

这项研究对人工智能和形式化数学领域有几个重要影响：

首先，它展示了大型语言模型在逐步自动定理证明中的强大能力，进一步证明了人工智能在数学推理中的潜力。其次，MPS-Prover生成的证明更短、更多样，这表明它不仅能找到正确的证明，还能找到更高效的路径。这对于实际应用中的形式验证特别有价值。第三，该研究为未来的混合证明器开发提供了有价值的见解，结合了逐步和整体方法的优势。

随着自动定理证明系统的不断发展，我们可以期待它们在形式化重要数学定理、验证软件和硬件系统，甚至可能帮助数学家验证新猜想方面发挥越来越重要的作用。MPS-Prover是这一激动人心旅程中的重要一步，为探索更强大、更可靠的自动定理证明系统提供了坚实的框架和全面的分析。