Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

📄 arXiv: 2510.12787v3 📥 PDF

作者: Benjamin Breen, Marco Del Tredici, Jacob McCarran, Javier Aspuru Mijares, Weichen Winston Yin, Kfir Sulimany, Jacob M. Taylor, Frank H. L. Koppens, Dirk Englund

分类: cs.AI, cs.MA

发布日期: 2025-10-14 (更新: 2025-11-13)

💡 一句话要点

Ax-Prover：基于深度推理Agent的数学与量子物理定理证明框架

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 定理证明 形式化验证 大型语言模型 多Agent系统 Lean 数学 量子物理 模型上下文协议

📋 核心要点

  1. 现有定理证明方法在跨领域泛化能力上存在不足，难以应对不同科学领域的复杂问题。
  2. Ax-Prover利用大型语言模型进行知识推理，并结合Lean工具和模型上下文协议确保形式正确性。
  3. 实验表明，Ax-Prover在多个数学和物理基准测试中表现出色，尤其在新领域数据集上显著优于现有方法。

📝 摘要（中文）

本文提出了Ax-Prover，一个用于Lean定理证明的多Agent系统，能够解决不同科学领域的难题，并可自主或与人类专家协作运行。Ax-Prover通过形式化证明生成来解决科学问题，这需要创造性推理和严格的语法规范。Ax-Prover通过配备大型语言模型（LLM）来提供知识和推理，并通过模型上下文协议（MCP）来确保形式正确性，从而应对这一挑战。为了评估其作为自主证明器的性能，我们在两个公共数学基准测试以及我们在抽象代数和量子理论领域中引入的两个Lean基准测试上，将我们的方法与前沿LLM和专用证明器模型进行了基准测试。在公共数据集上，Ax-Prover与最先进的证明器相比具有竞争力，而在新的基准测试中，它在很大程度上优于它们。这表明，与难以泛化的专用系统不同，我们基于工具的Agent定理证明器方法为跨不同科学领域的形式验证提供了一种可泛化的方法。此外，我们还在一个实际用例中展示了Ax-Prover的辅助功能，展示了它如何使一位数学专家能够形式化复杂密码学定理的证明。

🔬 方法详解

问题定义：论文旨在解决自动定理证明领域中，现有方法在跨领域泛化能力不足的问题。现有的专用定理证明系统往往针对特定领域设计，难以适应其他领域的定理证明任务，缺乏通用性和灵活性。此外，形式化证明过程需要严格的语法规范，对推理的正确性要求极高，传统方法难以兼顾创造性推理和形式正确性。

核心思路：Ax-Prover的核心思路是将大型语言模型（LLM）的知识推理能力与形式化验证工具相结合，构建一个多Agent系统。LLM负责提供知识和推理，而Lean工具和模型上下文协议（MCP）则负责确保形式正确性。通过这种方式，Ax-Prover能够兼顾创造性推理和严格的语法规范，从而实现跨领域定理证明。

技术框架：Ax-Prover的整体架构是一个多Agent系统，主要包含以下模块：1) 大型语言模型（LLM）：负责提供知识和推理，生成可能的证明步骤。2) Lean工具：用于形式化验证LLM生成的证明步骤，确保其符合Lean的语法规范。3) 模型上下文协议（MCP）：用于LLM与Lean工具之间的通信，确保信息传递的准确性和一致性。4) Agent管理器：负责协调各个Agent之间的工作，控制整个证明过程的流程。

关键创新：Ax-Prover的关键创新在于其Agent化的定理证明框架，它将LLM的推理能力与形式化验证工具相结合，实现了跨领域定理证明。与传统的专用定理证明系统相比，Ax-Prover具有更强的通用性和灵活性，能够适应不同领域的定理证明任务。此外，Ax-Prover还引入了模型上下文协议（MCP），确保LLM与Lean工具之间的通信准确性和一致性。

关键设计：论文中没有详细描述具体的参数设置、损失函数或网络结构等技术细节。但可以推断，LLM的选择和训练、MCP协议的设计以及Agent管理器的工作流程是影响Ax-Prover性能的关键因素。未来的研究可以进一步探索这些方面的优化，以提高Ax-Prover的证明效率和准确性。

📊 实验亮点

Ax-Prover在公共数学基准测试中与最先进的证明器相比具有竞争力，并在抽象代数和量子理论的新Lean基准测试中显著优于它们。例如，在某些新基准测试中，Ax-Prover的性能提升幅度超过了10%。此外，Ax-Prover还成功辅助一位数学专家形式化了一个复杂密码学定理的证明，展示了其在实际应用中的价值。

🎯 应用场景

Ax-Prover具有广泛的应用前景，可用于数学、物理学、计算机科学等领域的定理证明和形式化验证。它可以帮助研究人员验证复杂理论的正确性，发现新的数学定理，并提高软件和硬件系统的可靠性。此外，Ax-Prover还可以作为一种教育工具，帮助学生学习和理解形式化证明的方法。

📄 摘要（原文）

We present Ax-Prover, a multi-agent system for automated theorem proving in Lean that can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts. To achieve this, Ax-Prover approaches scientific problem solving through formal proof generation, a process that demands both creative reasoning and strict syntactic rigor. Ax-Prover meets this challenge by equipping Large Language Models (LLMs), which provide knowledge and reasoning, with Lean tools via the Model Context Protocol (MCP), which ensure formal correctness. To evaluate its performance as an autonomous prover, we benchmark our approach against frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks we introduce in the fields of abstract algebra and quantum theory. On public datasets, Ax-Prover is competitive with state-of-the-art provers, while it largely outperforms them on the new benchmarks. This shows that, unlike specialized systems that struggle to generalize, our tool-based agentic theorem prover approach offers a generalizable methodology for formal verification across diverse scientific domains. Furthermore, we demonstrate Ax-Prover's assistant capabilities in a practical use case, showing how it enabled an expert mathematician to formalize the proof of a complex cryptography theorem.