Mathematics with large language models as provers and verifiers

📄 arXiv: 2510.12829v3 📥 PDF

作者: Hieu Le Duc, Leo Liberti

分类: cs.CL, cs.AI, cs.LG, cs.LO

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

💡 一句话要点

利用大型语言模型作为证明器和验证器解决数学问题

🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 定理证明 数学推理 形式化验证 ChatGPT GPT-5 Lean证明助手

📋 核心要点

  1. 现有定理证明方法在处理复杂数学问题时效率较低，且难以避免幻觉问题，导致证明过程不可靠。
  2. 论文提出一种基于大型语言模型的协同证明框架，利用多个模型实例分别担任证明器和验证器角色，互相验证。
  3. 实验结果表明，该方法在解决IMO难题和验证数论猜想方面取得了显著进展，证明了其有效性。

📝 摘要（中文）

本文探讨了大型语言模型在定理证明方面的能力，尤其是在解决复杂数学问题（如国际数学奥林匹克竞赛题）和验证数学猜想方面的进展。研究报告了一种利用ChatGPT的定理证明方法，该方法采用多个GPT-5模型实例作为证明器和验证器协同工作。为了确保证明的可靠性，最终证明通过Lean证明助手进行形式化验证，并且Lean代码的前提和结论的一致性由人工验证。该方法成功解决了2025年IMO六道题中的五道，并验证了[Cohen, Journal of Integer Sequences, 2025]中六十六个数论猜想中的约三分之一。

🔬 方法详解

问题定义：论文旨在解决复杂数学问题的自动定理证明问题。现有方法，如传统的定理证明器，在处理需要创造性思维的问题时表现不佳，并且大型语言模型在生成证明时容易出现“幻觉”，即生成不正确的数学陈述。

核心思路：论文的核心思路是利用大型语言模型（LLM）的强大推理能力和生成能力，同时引入验证机制来减少LLM的“幻觉”问题。通过让不同的LLM实例扮演证明者和验证者的角色，互相检查，提高证明的可靠性。

技术框架：该方法的核心框架包含以下几个阶段：1) 问题提出：将数学问题输入到证明器LLM；2) 证明生成：证明器LLM生成初步证明；3) 证明验证：验证器LLM对证明进行验证，指出潜在错误；4) 迭代优化：证明器根据验证结果进行修正，重复证明生成和验证过程，直到验证器认为证明正确；5) 形式化验证：将最终证明转换为Lean证明助手代码，进行形式化验证；6) 人工验证：人工检查Lean代码的前提和结论是否与原始问题一致。

关键创新：该方法的主要创新在于将多个LLM实例协同工作，分别担任证明者和验证者的角色，形成一个闭环的反馈系统。这种协同验证机制能够有效地减少LLM的“幻觉”问题，提高证明的可靠性。此外，使用Lean证明助手进行形式化验证，进一步增强了证明的严谨性。

关键设计：论文中关键的设计包括：1) 使用GPT-5模型作为证明器和验证器；2) 设计了证明生成和验证的迭代流程；3) 使用Lean证明助手进行形式化验证；4) 人工验证Lean代码的正确性。具体的参数设置和损失函数等技术细节在论文中没有详细说明，属于未知信息。

📊 实验亮点

该研究成功地使用ChatGPT解决了2025年IMO六道题中的五道，并验证了[Cohen, Journal of Integer Sequences, 2025]中六十六个数论猜想中的约三分之一。这些结果表明，大型语言模型在定理证明方面具有巨大的潜力。

🎯 应用场景

该研究成果可应用于自动定理证明、数学教育、科学研究等领域。通过构建更强大的自动定理证明系统，可以加速数学研究的进程，并为解决复杂的科学问题提供新的工具。在教育领域，可以辅助学生学习数学，提高解题能力。

📄 摘要（原文）

During 2024 and 2025 the discussion about the theorem-proving capabilities of large language models started reporting interesting success stories, mostly to do with difficult exercises (such as problems from the International Mathematical Olympiad), but also with conjectures [Feldman & Karbasi, arXiv:2509.18383v1] formulated for the purpose of verifying whether the artificial intelligence could prove it. In this paper we report a theorem proving feat achieved by ChatGPT by using a protocol involving different prover and verifier instances of the gpt-5 model working collaboratively. To make sure that the produced proofs do not suffer from hallucinations, the final proof is formally verified by the lean proof assistant, and the conformance of premises and conclusion of the lean code is verified by a human. Our methodology is by no means complete or exact. It was nonetheless able to solve five out of six 2025 IMO problems, and close about a third of the sixty-six number theory conjectures in [Cohen, Journal of Integer Sequences, 2025].