MPS-Prover：利用多视角搜索与数据策展提升步进式定理证明能力

形式语言中的自动化定理证明（Automated Theorem Proving, ATP）仍然是人工智能领域一项艰巨的挑战，它需要严谨的逻辑推理并驾驭庞大的搜索空间。尽管大型语言模型（LLMs）已展现出令人鼓舞的性能，但现有的逐步证明器通常面临有偏搜索引导的问题，导致效率低下和次优的证明策略。本文引入了多视角搜索证明器（MPS-Prover），这是一种新颖的逐步ATP系统，旨在克服这些限制。MPS-Prover整合了两项关键创新：一项高效的后训练数据筛选策略，该策略可在不牺牲性能的情况下，剪除约40%的冗余训练数据；以及一种多视角树搜索机制。这种搜索机制将学习到的评论家模型与精心设计的启发式规则相结合，以实现策略选择的多样化，避免陷入无用的状态，并增强搜索的鲁棒性。广泛的评估表明，MPS-Prover在多个具有挑战性的基准测试上，包括 miniF2F 和 ProofNet，均取得了最先进的性能，超越了先前拥有 70 亿参数的模型。此外，我们的分析显示，与现有逐步证明和整体证明方法相比，MPS-Prover 生成的证明显著更短且更具多样性，这突显了其效率和效能。我们的工作提升了基于 LLM 的形式化推理能力，并为开发更强大的定理证明器提供了鲁固的框架和全面的分析。