arXiv cs.MA· Benjamin Breen, Marco Del Tredici, Jacob McCarran, Javier Aspuru Mijares, Weichen Winston Yin, Kfir Sulimany, Jacob M. Taylor, Frank H. L. Koppens, Dirk Englund·· 10 小时前AI 评分17
Ax-Prover：面向数学与量子物理定理证明的深度推理智能体框架
Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
AI 导读
Ax-Prover 是一个基于 Lean 的多智能体定理证明系统，通过 MCP 为 LLM 配备 Lean 工具，可自主运行或与人类专家协作。在公开数学基准上它与 SOTA 证明器相当，在团队新提出的抽象代数与量子理论 Lean 基准上大幅领先。该系统还帮助一位专家数学家形式化了复杂密码学定理的证明。该论文已被 arXiv 管理员撤稿。
正文 · AI 翻译
本文已被 arXiv 管理员撤回
摘要：我们提出 Ax-Prover，一个用于 Lean 中自动定理证明的多智能体系统，能够解决跨多个科学领域的问题，并可自主运行或与人类专家协作。为此，Ax-Prover 通过形式化证明生成来开展科学问题求解，这一过程既需要创造性推理，又需要严格的语法严谨性。Ax-Prover 通过模型上下文协议（MCP）为大语言模型（LLM）配备 Lean 工具来应对这一挑战，前者提供知识与推理，后者确保形式正确性。为评估其作为自主证明器的性能，我们在两个公开数学基准以及我们新引入的抽象代数和量子理论领域的两个 Lean 基准上，将我们的方法与前沿 LLM 和专用证明器模型进行了基准测试。在公开数据集上，Ax-Prover 与最先进的证明器相比具有竞争力，而在新基准上则大幅优于它们。这表明，与难以泛化的专用系统不同，我们基于工具的智能体定理证明器方法为跨多个科学领域的形式验证提供了一种可泛化的方法。此外，我们在一个实际用例中展示了 Ax-Prover 的助手能力，说明它如何帮助一位专家数学家形式化了一个复杂密码学定理的证明。
| 评论： | arXiv 管理员注：本投稿因不符合 arXiv 的研究内容质量标准已被撤回 |
| 主题： | 人工智能（cs.AI）；多智能体系统（cs.MA） |
| 引用为： | arXiv:2510.12787 [cs.AI] |
| （或 arXiv:2510.12787v5 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2510.12787 arXiv 颁发的 DOI（通过 DataCite） |
提交历史
来自：arXiv 管理员 [查看电子邮件]
[v1]
2025 年 10 月 14 日星期二 17:57:04 UTC（1,937 KB）
[v2]
2025 年 10 月 16 日星期四 14:10:07 UTC（1,937 KB）
[v3]
2025 年 11 月 13 日星期四 18:56:10 UTC（1,616 KB）
[v4]
2026 年 5 月 22 日星期五 10:39:41 UTC（2,536 KB）
[v5]
2026 年 10 月 29 日星期四 20:56:25 UTC（1 KB） （已撤回）
来源：arXiv cs.MA · arxiv.org