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

93 0 0

文章摘要

自动化定理证明（ATP）是人工智能、数学及形式化方法领域的核心挑战，旨在为数学或逻辑陈述自动生成形式化、可验证的证明。尽管大语言模型（LLM）在非形式化数学推理任务中取得了显著进展，但在形式化定理证明领域，LLM仍面临巨大挑战，主要由于其对精确语法、语义的严格要求、巨大的证明步骤搜索空间以及高质量训练数据的稀缺。目前主流的LLM辅助证明方法分为整体证明生成与逐步式证明生成。逐步式证明生成虽然更适应交互式探索和复杂推理，但其自身也存在关键难题，如评估模型易因训练数据偏好重复推荐相似策略，导致搜索陷入局部最优，错误的策略选择可能导致后续状态不可证，以及某些自动化策略在不适用时被滥用，无法推进证明。

为克服逐步式证明器的局限性，提出了多视角树搜索证明器（MPS-Prover），其核心包含两项关键创新：高效的训练后数据筛选策略和融合启发式评估的多视角树搜索算法。高效的训练后数据筛选策略有效剔除了约40%的低价值训练样本，显著提升了训练效率，同时保证甚至提升了模型在复杂策略学习上的准确性。融合启发式评估的多视角树搜索算法引入了三种精心设计的启发式评估规则，共同指导搜索树的节点扩展，包括策略有效性评分、最小化分支复杂度和最短状态优先。这些规则确保了搜索路径的多样性，避免单一评估标准带来的偏差，有效跳出局部最优和不可证状态。

MPS-Prover在所有参与比较的逐步式证明器中取得了最佳性能。在miniF2F上，MPS-Prover成功证明了244个问题中的185个，相较于先前最佳的BFS-Prover提升了约3个百分点。在7B模型级别，其性能仅次于通过更大模型蒸馏而来的DeepSeek-Prover-V2 (CoT)，显示了该方法在同等规模直接训练模型中的领先性。在固定预算下的性能对比中，MPS在各预算水平下均持续优于BFS，验证了多视角策略在提升搜索效率方面的优势。此外，MPS-Prover生成的证明不仅显著短于BFS，也远短于主流整体证明生成器，同时其证明的策略多样性也更高。

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