人工智能与数学证明：为什么即使是最好的模型也会遇到困难

想象一下，你请一位聪明绝顶的学生解一道复杂的数学题。他自信满满，仅用几秒钟就得出了正确答案，令在场所有人赞叹不已。但当你请他解释解题思路——一步步讲述他的逻辑推导过程时，他却突然语塞，给出的解释模糊不清，逻辑跳跃，根本站不住脚。

这个场景，正是研究人员最新发现的当代最先进人工智能系统的真实写照。尽管媒体不断热炒 AI 在数学上的惊人成就，背后却隐藏着一个令人惊讶的事实：

• 现有的数学评估基准（如 MathArena）显示，大型语言模型（如 OpenAI 的 O3-MINI）在 AIME（美国邀请数学考试）和 HMMT（哈佛-麻省理工数学竞赛）等比赛中表现出色，这些比赛只要求提交数值答案。

• 然而，现实世界中的数学任务需要的是缜密的逻辑推理与严谨的证明过程，而不仅仅是得出一个数值。

苏黎世联邦理工学院（ETH Zurich）和保加利亚人工智能与技术研究院（INSAIT）的研究人员通过细致的实验记录发现，如今的 AI 系统虽然能得出正确答案，却常常是建立在“逻辑沙滩”之上的——缺乏可靠的推理基础。

结果令人震惊：那些曾被赞誉为在标准数学基准测试中超越人类的 AI 模型，在面对需要完整推理过程的 USAMO（美国数学奥林匹克）证明题时，几乎全军覆没。即便是最先进的语言模型，平均得分也不到 5%。

这不仅仅是学术层面的趣闻。当我们在医疗、工程等需要复杂推理的领域日益依赖 AI 时，“会算答案”与“真正理解原理”之间的区别变得至关重要。一个看似聪明但无法解释自己思路的系统，既是技术局限的体现，也潜藏着潜在的风险。

这项研究不仅检验了 AI 的数学能力，更揭示了当前人工智能在“推理”方面的根本局限。让我们深入探讨研究人员的发现所带来的深远意义：

文章目录

• 数学奥林匹克的挑战

• 严格的评估方法

• 当自信遭遇失败

• 深度质性分析

• 关键观点与未来方向

• 致真正热爱数学的你

1. 数学奥林匹克的挑战

要真正理解这项研究的意义，首先必须了解美国数学奥林匹克（USAMO）为何具有独特的挑战性，以及它与其他 AI 以往表现出色的竞赛有何不同。

USAMO 是美国高中数学竞赛中最高等级的赛事之一。与美国邀请数学考试（AIME）或哈佛-麻省理工数学竞赛（HMMT）等主要考查数值答案的竞赛不同，USAMO 要求参赛者给出详尽的证明和严谨的解释。

试比较一下：在 AIME 的题目中，学生可能被要求求出某个方程的值，这需要计算能力和数学知识，最终得出一个数值答案。但 USAMO 的题目远不止于此——它要求参赛者构建出逻辑严密的论证，来说明一个数学命题为什么成立。

例如，一道典型的 USAMO 题可能是这样的：“设

和

为正整数。证明：存在一个正整数

，使得对于每一个奇数

，数

的以

为底的表示法中的所有数字都大于

。” 这类题目并不要求求出具体数值，而是需要结构清晰、逻辑严密的论证来确立一个数学真理。

以往的研究表明，大型语言模型在数值型答案竞赛中表现惊人，像 OpenAI 的 O3-MINI 模型，其得分已可与顶级人类选手媲美。但这些模型是否也能构建出有效的数学证明呢？这正是研究人员试图回答的问题。

2. 严谨的评估过程

这项研究由苏黎世联邦理工学院（ETH Zurich）和索非亚大学人工智能与技术研究院（INSAIT）的专家团队共同完成。他们设计了一个极为巧妙的评估流程，选用了 2025 年美国数学奥林匹克（USAMO）的全部六道题作为测试。这一选择完美契合他们的研究目标：这些题目具有挑战性，需要详尽的证明，并且由于发布较晚，不太可能出现在 AI 的训练数据中。

研究团队测试了六个最先进的推理模型：

• Claude 3.7（Anthropic 的高级模型）

• R1（DeepSeek 的专注推理模型）

• Flash-Thinking（Google Gemini 2.0 的实验版本）

• O1-Pro（OpenAI 的专业级推理模型）

• O3-Mini（OpenAI 的紧凑型推理模型）

• QwQ-32B（Qwen 的强化学习模型）

每个模型对每道题都进行了 4 次独立尝试，以降低结果的方差。随后，研究团队邀请了 4 位资深数学家担任评审，这些专家均具备丰富的数学竞赛解题经验，曾是国家级国际数学奥林匹克（IMO）代表队成员或国家队集训营的最终阶段入选者。

评审过程参考了 IMO 的评分标准，每道题的解答由两位评审独立打分，采用详细的 7 分制评分体系。该双评机制借鉴了 IMO 的评分流程，确保评分的一致性并最大限度地减少个人偏见。

3. 当信心遭遇失败

研究结果令人震惊。尽管这些模型在数值类数学竞赛中表现出色，但在 USAMO 的问题上，它们的表现却极其糟糕：

• R1 的平均得分最高，也仅有2.0 分（满分 42 分）

• Flash-Thinking 紧随其后，为1.8 分

• Claude 3.7 得到1.5 分

• QwQ 与 O1-Pro 均为1.2 分

• O3-Mini 垫底，仅有0.9 分

最令人警醒的是，在近150 份模型解答中，没有任何一份在任何一道题上获得满分。单题的最高得分也不过是7 分中的 1.5 分。

比分数低更值得关注的，是研究人员发现这些模型“失败的方式”。

他们将错误归为以下四大类：

逻辑错误

模型经常做出没有依据的推理步骤，或使用错误的逻辑。例如，Claude 3.7 在仅对一个特定情况完成证明后，就未经论证地将结论推广到所有情况 —— 这是一种基础性的逻辑错误，直接导致整个证明无效。

示例：在 USAMO 第 2 题中，Claude 3.7 对某个 j 值完成了证明，随后却跳跃性地宣称该性质适用于所有 j —— 明显的逻辑飞跃。

图片来自研究论文

在数学中，你不能仅凭对一个情况的证明就得出普适性结论，除非：

• 有一个完备的数学归纳法；

• 提供该性质独立于 j 的一般性证明；

• 或有其他逻辑机制把个别情况与一般情况联系起来。

这种未经论证的泛化在逻辑学中被称为“轻率概括”或“逻辑飞跃”，在数学证明中尤其危险，因为每一步都必须经过严格论证。

假设错误

模型常常引入未被证明或错误的前提，破坏了整个解题思路。

图片来源：ArtOfProblemSolving 网站

示例：在 USAMO 第 4 题中，O3-Mini 在几何推理中引入了错误假设。

图片来自研究论文

它在没有明说的情况下，默认点 C 在圆 AFP 的外部，并断言“CA 与 ⊙(AFP) 相切”，并基于相切性质展开推理。

这是典型的假设错误，因为：

• 模型默默假设了一个错误的几何关系（点 C 在圆外）；

• 这个假设在题目实际情境中是错误的；

• 后续推理都建立在这个错误的基础上，导致整个逻辑链条崩塌。

这一案例展示了 AI 模型如何在未充分分析图形结构的情况下，贸然引入似乎“合理”却在特定问题中错误的几何设定。

创造力的局限性

面对需要创新思路的问题时，模型普遍无法找到正确的解题策略。

图片来源：ArtOfProblemSolving 网站

示例：在 USAMO 第 3 题中，O3-Mini 错误地认为 Bob 能赢得游戏，而实际上 Alice 有一套最优策略。

图片来自研究论文

O3-Mini 的回答指出：“Bob 可以布置他的城市，使得道路网络不满足 Alice 的两个胜利条件之一……换句话说，Bob 有制胜策略。”

这就是创造力错误的体现：

• 模型没有发现或考虑 Alice 的最优策略；

• 相反，它错误地断言 Bob 会赢；

• 模型缺乏发现正确解法所需的创造性问题解决能力。

在博弈论这类问题中，正确策略往往并不直观，需要探索非显而易见的解法。AI 模型在这方面的失败，揭示了其在复杂问题空间中寻找反直觉或创新解法的能力存在明显局限。

代数/算术错误

虽然不如其他错误常见，模型仍会出现基本的计算错误。

图片来源：ArtOfProblemSolving 网站

示例：R1 在计算组合数之和时出现错误，结果是1,894,391，而正确答案应为3,395,016，这导致它得出完全错误的结论。

在这个例子中，R1 的解答中：

1. 计算组合数之和 Σ(i=0 至 7) (7 选择 i)⁴ 为 1,894,391

2. 将此值除以 8，得到 236,798.875

3. 随后得出结论：“因为这不是整数，所以当 n=7 时，k=4 不成立。”

这表示代数/算术错误，因为：

• 模型在计算组合数时出错；

• 正确结果3,395,016恰好能被 8 整除，说明模型的判断是错的；

• 错误的计算导致了整个论证的错误结论。

这种计算错误尤其危险，因为：

• 它们可能完全破坏一个本应正确的逻辑结构；

• 显示模型在复杂计算中仍可能出错；

• 不经过外部验证，难以察觉。

该案例表明，即便是最先进的 AI 模型，在处理复杂表达式时，也会犯下基础性的计算错误，这凸显了在数学证明中对计算步骤进行外部验证的重要性。

4. 质性分析带来的洞察

研究人员的质性分析揭示了更令人担忧的模式，这些模式暴露了这些模型在数学推理方面存在的更深层次问题。

其中最令人警觉的是他们所称的“虚张声势（bluffing）现象”。与通常能意识到自己是否解决问题正确的人类参与者不同，所有被评估的大模型（LLMs）都一致地声称自己成功解决了问题，即使它们的解答中存在根本性错误。

这种过度自信使得这些模型在数学应用中具有潜在危险性 —— 因为在缺乏严格人工验证的情况下，它们的结果并不可信。

研究还发现了一些来自模型训练过程中的“产物（artifacts）”，这些产物引发了某些不良行为模式：

答案框定（Answer Boxing）: 模型被训练成在数学问题中提供明确的、被“框出”的最终答案。这导致它们倾向于强行输出一个单一数值答案，即便题目本身需要更复杂的或集合型的解答。

例如：QwQ 模型错误地坚持 USAMO 第 5 题的答案是 “2”，尽管它在先前推理中已正确判断解答应包含所有正的偶数。

#### 模式泛化过度（Pattern Overgeneralization）: 模型在处理小数值样本时容易观察到某些模式，然后未经正式证明就将这些模式泛化为普遍规律** —— 这在数学推理中属于严重错误。

解答结构问题（Solution Structure Issues）: 不同模型在解答的清晰度与条理性方面差异显著。

• OpenAI 的模型尽管解答错误，但通常结构清晰、逻辑连贯；

• 而 Flash-Thinking 和 QwQ 等模型则常常输出混乱的内容，将多个无关想法混合在一起，缺乏组织性。

也许最耐人寻味的是研究人员尝试让模型自行评分的实验。

当让 O3-Mini 和 Claude 3.7 来评估自己的解答时，它们严重高估了解答的质量—— 相比于专家评审，模型给出的得分被高估了多达 20 倍。

5. 批判性视角与未来方向

尽管《Proof or Bluff?（证明还是虚张声势？）》这项研究为我们揭示了 AI 在数学推理方面的诸多局限性，但也有部分研究人员和人工智能专家对其研究范围与方法论提出了重要质疑，这些观点值得认真思考。

首先，本次评估本身投入极小 ——测试大多数模型在所有题目上的成本只有几美元（除了 O1-Pro，成本超过 200 美元）。如此有限的测试引出了一个关键问题：

“有人真的指望这些公开可用的模型，能在第一次尝试中就用完美严谨的证明解出奥数级别的问题吗？”

一位 AI 研究人员指出：

“这项研究并不能真正告诉我们这些系统的核心扩展能力。“对于更广泛的 AI 探讨而言，更有意义的是分析不同模型规模下的性能趋势，或者探究在增加尝试次数时，成功率如何变化。”

这引发了一个有趣的思考实验：

如果每道题只尝试 4 次，模型就能成功解出一定比例的问题，那么—— 如果允许尝试 100 次、1000 次甚至 10,000 次，它们的表现是否会显著提升？是否可以通过“暴力尝试”最终获得正确解？

然而，这种方法遇到了一个重大的实际障碍——这项研究本身就强调了这一点。事实证明，这些模型在评估数学工作方面表现非常糟糕，与专家的人工评估相比，它们始终高估解决方案的质量，最高可达 20 倍。

但这种方法面临一个巨大的现实障碍 —— 正是这项研究本身所强调的：

模型在评估自己数学解答的质量方面表现极差，相较于专家评审，它们高估得分高达 20 倍。

这项发现带来了一个矛盾式的挑战：

即便一个模型最终在成千上万次尝试中“碰巧”给出了一个正确的证明，我们要从这些解答中识别出真正正确的那一个，仍然需要耗费大量人工验证，这使得“扩大测试规模”几乎在实践中无法执行。

正如一位评论者所说：

" 如果你无法从 10,000 个解答中自动识别出那个正确答案，那么即使其中有一个是对的也毫无意义。毕竟，就连一个随机生成器在足够多次的尝试下也终会碰巧猜对一次。"

这一矛盾凸显出 AI 评估中的更深层次难题：

•基于最终答案的简化评估可能高估了模型的能力

•而基于严谨证明过程的评估又需要无法大规模扩展的人工专业知识

该研究的真正意义或许不在于“证明当前模型不够好”这一已预期的结论，而在于精确记录这些模型是如何失败的，以及这些失败模式反映了 AI 当前的哪些根本性限制。

当我们展望 AI 在数学推理上的未来发展时，关键问题已不再是：

“模型是否能偶尔给出正确答案？”

而是：

“模型是否能一贯地展现出健全的逻辑推理？”

而后者，或许需要一种根本不同于现有“模式匹配”和“统计学习”的新路径。

无论你把这项研究看作“令人震惊的发现”，还是“对已知局限性的确认”，它都为我们提供了一个关于当下 AI 状况的现实检验：

要让机器真正理解数学、而不仅仅是计算答案，仍是人工智能研究前沿最深远的挑战之一。

6. 致真正热爱数学的你

好奇那些连最先进的 AI 系统都难以攻克的 2025 年 USAMO 难题，是如何被人类专家解出的？ 那就来亲身感受严谨数学推理的魅力，探索这些专家解法与深入讨论吧：

•Evan Chen 的详细笔记提供了优雅的解法与专家点评：USAMO 2025 笔记

•Art of Problem Solving 社区展示了每道题的多种解法与合作讨论：AOPS 2025 USAMO 问题

这些资源不仅展现了人类数学思维的深度与创造力，也清晰地标示出当前 AI 系统尚难企及的领域—— 那种融合了逻辑严谨性、创新策略与数学直觉的能力，才是真正数学推理的核心。

AI 自信却漏洞百出的解法，与专家们精巧而严谨的解答之间的反差，或许比任何基准分数都更真实地反映了当前人工智能的实际水平。

资源

•Original Research Paper: Access the complete “Proof or Bluff?” study by Petrov et al. at arXiv

•AI Benchmarking Dashboard: Track the progress of various AI models across different mathematical reasoning tasks at Epoch AI’s dashboard

•USAMO Problem Archive: Explore past USAMO problems and community solutions at Art of Problem Solving

•Math Olympiad Pathway Guide: Understand the progression from AMC to AIME to USAMO competitions in [AP Guru’s comprehensive breakdown](https://www.apguru.com/blog/amc-vs-aime-vs-usamo-understanding-the-math-olympiad-pathway