新研究揭示模拟推理 AI 模型尚未达到其宣传效果之原因

当前最强大的 AI 模型声称具备“推理”能力，其内在却存在一个耐人寻味的矛盾：它们能够以惊人的准确率解决常规数学题目，但在面对设计深度数学证明的竞赛级挑战时，往往却表现不佳。

这一发现来自一篇关于模拟推理 (SR) 模型的启示性预印本研究，该研究最初发表于 3 月，4 月有更新，但多半未被新闻媒体关注。该研究作为一个有启发性的案例，展示了即便在 AI 供应商常有夸大宣传下，SR 模型在数学方面的局限性。

与传统大语言模型 (LLM) 不同，模拟推理模型经过训练后不仅输出最终答案，还会给出逐步的“思考”过程（通常称为“chain-of-thought”）来解决问题。需要注意的是，此处的“模拟”并不意味着这些模型完全不进行推理，而只是它们的推理方法未必与人类相同。这个区分十分重要，因为人类的推理本身都难以定义。

这篇题为《Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad》（证明还是虚张声势？——对 2025 年美国数学奥林匹克大赛中大语言模型的评估）的新研究论文，由苏黎世联邦理工学院 (ETH Zurich) 与索菲亚大学 INSAIT 的研究团队在 Ivo Petrov 与 Martin Vechev 的带领下完成。

在这项研究中，当研究人员让 SR 模型解答由美国数学协会主办的 2025 年美国数学奥林匹克大赛中的题目时，多数模型在生成完整数学证明方面的正确率平均不足 5% ——虽然有一款模型表现明显更好，尽管其能力依然有限。这个分数代表的是模型在多次尝试中所获得的总分占可能满分（按照官方奥林匹克大赛每题 0–7 分的标准）的平均百分比，而专家评卷人则会为证明中的每一个正确步骤给出部分分。

Proof versus answers: A different kind of test 证明与答案：不同类型的测试

要理解这一能力差距为何重要，我们首先需要了解解答数学题目与数学证明之间的差别。数学题目类似于问“2+2 等于多少？”或“解这个方程中的 x”，只需要给出正确答案；而数学证明则要求解释“为什么 2+2=4，需要用逻辑步骤证明”或“证明该公式对所有数字均成立”。证明不仅需要给出答案，更要求解释推理过程，展示某事物为何必然成立。

美国数学奥林匹克大赛 (USAMO) 是国际数学奥林匹克的预选赛，其标准远高于美国邀请数学考试 (AIME) 这类测试。虽然 AIME 的题目难度较高，但只需给出整数答案；而 USAMO 要求参赛者在九小时内、历时两天写出完整的数学证明，并对证明的正确性、完整性与清晰度进行打分。

研究人员在 2025 USAMO 刚刚发布后不久，就对多个 AI 推理模型进行了六道题目的评估，从而最大限度地降低这些题目可能曾出现在模型训练数据中的风险。被测试的模型包括 Qwen 的 QwQ-32B、DeepSeek R1、Google 的 Gemini 2.0 Flash Thinking (Experimental) 及 Gemini 2.5 Pro、OpenAI 的 o1-pro 与 o3-mini-high、Anthropic 的 Claude 3.7 Sonnet with Extended Thinking，以及 xAI 的 Grok 3。

虽然其中 Google 的 Gemini 2.5 Pro 模型获得了 42 分满分中的平均 10.1 分（约 24%），但其他模型在与 AIME 级别的基准测试相比时，表现均有大幅下降。其他评估模型的成绩则远远落后：DeepSeek R1 与 Grok 3 平均各得 2.0 分，Google 的 Flash-Thinking 得分 1.8 分，Anthropic 的 Claude 3.7 得分 1.5 分，而 Qwen 的 QwQ 与 OpenAI 的 o1-pro 均平均得分 1.2 分。OpenAI 的 o3-mini 得分最低，仅 0.9 分（约 2.1%）。在所有模型和运行中生成的近 200 个解决方案里，没有一个问题得到了满分。

尽管 OpenAI 新发布的 03 与 o4-mini-high 未被纳入此项研究评估，但研究人员在其 MathArena 网站上的基准测试显示，o3-high 模型在 USAMO 上整体得分为 21.73%，而 o4-mini-high 为 19.05%。不过这些结果可能受到污染，因为测试是在比赛结束后进行的，这意味着新版 OpenAI 模型有可能在训练数据中包含了这些题目的解答。

How the models failed 模型失败的原因

在论文中，研究人员归纳出几种典型的错误模式。AI 的输出中经常存在逻辑漏洞，即缺乏数学证明所需的充分论证，其中包含基于未经验证假设的论据，并且即使在出现自相矛盾结果后，错误的推理方法依然持续输出。

其中一个具体例子涉及 2025 USAMO 的第 5 题。该题要求模型找出所有正整数 k，使得一个涉及二项式系数之和的值在 k 次方后，无论选取哪个正整数 n，都能得到一个整数。在这个问题上，Qwen 的 QwQ 模型犯了一个明显错误：在允许非整数情况出现的环节，它错误地排除了非整数可能性。尽管该模型在推理过程中正确确定了必要条件，但这个错误导致了其最终答案错误。

也许最值得注意的是，这些 AI 模型往往以肯定语气输出错误答案，并没有显示出对其模拟推理过程中错误的任何不确定性或“意识”。研究人员注意到，即使证明中存在重大缺陷，模型也未曾表现出任何谨慎态度。

研究人员认为，这种失败部分源自模型训练与优化的方式。例如，他们观察到一些很可能是常见基准训练优化策略所产生的痕迹。在不适合证明的情况下，模型有时会错误地强制套用寻找最终“框选”答案的限制（指的是基准测试中常要求模型将最终数值答案格式化，用 LaTeX 命令 \boxed{} 框起，以便自动化系统能轻松提取和评分），或者在没有提供必需论证的情况下，把从少量样例中学到的模式过度泛化。

The illusion of math fluency 数学流畅性的幻觉

上述数学题与证明之间的性能差距暴露出模式匹配与真正数学推理之间的区别。当前的 SR 模型在遇到训练数据中出现过的类似模式任务时，能够输出相对准确的数值答案，但缺乏证明数学所需的更深层次的“概念理解” —— 这种理解要求构建全新的逻辑论证，表达抽象概念，并在初步方法失效时调整策略。

那么，既然 chain-of-thought 与模拟推理技术能够改善结果，它们为何未能实现更深层次的数学推理呢？答案在于研究人员所称的“推理时计算”扩展。当大语言模型使用 chain-of-thought 技术时，它们会投入更多计算资源，通过一系列较小且更具针对性的步骤遍历其潜在空间（即神经网络数据中概念之间的连接）。每一步中间推理结果作为下一步推理的上下文，有效地限制了模型输出，使得准确性提高并减少虚构内容的产生。

正如大语言模型研究工程师 Sebastian Raschka 在博客中解释的那样：“推理模型要么明确展示其思考过程，要么在内部处理这一过程，这使它们在处理复杂任务（如数学问题）时表现得更好。”

但从根本上讲，所有基于 Transformer 的 AI 模型都是模式匹配的机器。它们借用数据样例中所包含的推理技能。由此可以解释奥林匹克研究中的独特现象：这些模型在标准问题上表现卓越，因为逐步推理过程与其训练数据中的模式相吻合，但在面对需要更深数学洞察的新型证明问题时便崩溃。这种改善很可能来自多个小预测任务中统计概率的提高，而不是一次大规模的预测飞跃。

即便如此，正如 Gemini 2.5 Pro 的结果所显示，随着 SR 模型能力的提升，未来它们可能逐步缩小这一“推理”差距，能够在潜在空间中建立更深的多维联系。未来的训练技术或模型架构可能最终会教授这些模型所需的所有推理模式，从而使其在深度推理方面达到与人类顶尖水平相当的境界。但目前这仍然只是猜想。

What comes next 未来展望

尽管有望在不久将来取得改进，但当前的研究结果表明，仅仅通过扩大现有 SR 模型架构和训练方法的规模，可能无法弥合通向真正数学推理的鸿沟。这些局限性并非个案：在另一项近期研究中（Gary Marcus 在其关于《Proof or Bluff》论文的博客中有所提及），来自宾夕法尼亚州立大学的 Hamed Mahdavi 及其来自纽约市立大学、纽约大学和 Autodesk 的合作者对大语言模型进行类似高级数学挑战的评估，并得出了相近的结论。

鉴于上述所展示的不足，一些研究人员正在探索改善 AI 推理的替代方案。这些方案包括整合符号推理引擎、开发更优的证明验证技术以及引入自洽性检查。DeepMind 的 AlphaGeometry 就是一例，该系统结合了神经网络与符号 AI 中常见的形式化方法。尽管这类“神经符号系统”可能无法找出证明，但其架构可以防止生成虚构的错误证明，从而直接应对了 SR 模型评估中观察到的一项关键失败模式。