PRO会员通讯
当 AI 翻开奥数题，CPU 也烧了！
还记得那些被奥数题折磨得彻夜难眠的日子吗？
当你在凌晨三点对着一道几何证明题抓耳挠腮、怀疑人生的时候，你可能会想：「要是有个超级大脑能帮我解决这些问题该多好啊！」
好消息：大模型解数学题的能力很强！坏消息：它们好像也被奥数折磨得不轻。
很多针对大型语言模型（LLMs）的数学基准测试已经表明，最先进的推理模型在美国数学邀请赛（AIME）等数学竞赛中表现出色，O3-MINI 模型甚至达到了与顶尖人类参赛者相当的水平。然而，这些测试仅仅评估了最终答案，而忽略了推理和证明过程。
为弥补这一不足，专注于评估大模型数学能力的 MathArena 平台的研究人员，首次全面评估了模型解决复杂数学问题的完整推理和证明构建能力。
美国数学奥林匹克竞赛（USAMO）是全球最具挑战性的中学生数学竞赛之一。首先，该赛事强调严格证明与逻辑严谨性，题目均为证明题，要求选手通过严密的逻辑推导和完整的数学语言呈现解答，而非仅给出数值答案（如 AIME）。其次，题目难度极高，涉及数论、组合数学、代数、几何等核心领域，常需运用高级技巧（如生成函数、不等式放缩、图论构造等）。而且题目设计具有「门槛效应」：部分问题看似简单，但需洞察隐藏结构或非标准解法（如构造性证明、反证法）。
他们在 2025 年美国数学奥林匹克竞赛（USAMO）试题发布后立即测试了多个热门模型，结果令人失望：所有模型都表现欠佳，平均得分不到 5%。
通过深入分析模型的推理过程，研究人员识别出了多种常见失败模式，并发现模型训练中的某些优化策略反而产生了负面影响。
论文标题：PROOF OR BLUFF? EVALUATING LLMS ON 2025 USA MATH OLYMPIAD
论文链接：https://arxiv.org/pdf/2503.21934v1
项目主页：https://matharena.ai
项目代码：https://github.com/eth-sri/matharena
结果表明，当前的 LLM 在严格的数学推理方面，尤其是在形式化证明生成方面，仍然非常吃力。在未来的研究中，有必要改进训练方法，如纳入重证明的数据集、整合形式验证工具或开发优先考虑逻辑一致性而非答案优化的架构，弥合数值正确性与逐步证明能力之间的差距。
方法
评估基准与问题准备
研究团队选择了 USAMO 2025 作为基准测试，这是一个权威数学竞赛，包含六道需要证明的题目，为期两天。这个竞赛非常适合作为评估基准，因为题目具有挑战性，需要详细证明才能得满分，且数据未被污染.
图 1 展示了两个竞赛题目。在评估过程中，研究人员要求各模型提供全面详细的证明，并使用 LaTeX 格式。
为降低结果的变异性，每个模型对每道题目进行了四次独立解答。所有解答均经过匿名化处理并转换为 PDF 格式进行评分，评分过程中不考虑思考过程部分。
评审团队
评分团队由四位资深数学专家组成，他们都曾是国家 IMO 队成员或进入过国家队最终选拔。评审前，他们接受了详细说明评估目标和方法的指导（可在 GitHub 查阅）。团队通过 USAMO 2024 三道题目的试评分熟悉了评分标准并解决歧义。
评分流程
USAMO 2025 的六个问题均由两名评审员独立评分，每位评审员负责三个不同问题。这种借鉴 IMO 的双重评分方法确保了评分的一致性并减少了主观偏见。由于官方不发布标准答案，研究团队从可靠的数学社区资源（尤其是 AoPS 论坛）收集整理了标准化评分方案，并验证了所有解法的准确性。
遵循 USAMO 惯例，每题满分七分，对有意义的进展给予部分分。评审员根据既定标准独立评分，对不完全符合评分方案的解法也适当给分，并记录了评分理由和部分分数的合理性说明。
失败模式分类
评估者在评分过程中记录了明显的失败模式 —— 即推理中首次出现的错误或解释不充分的实例，包括逻辑缺陷、无根据的假设、数学不准确或计算错误。这些错误被具体分为四类：
逻辑：由于逻辑谬误或无根据的推理跳跃导致的错误，中断了推理过程。
假设：由于引入未经证明或不正确的假设而产生的错误，这些假设破坏了后续步骤。
创造力：由于无法识别正确方法而导致的从根本上错误的解决策略所造成的错误。
代数 / 算术：由关键的代数或算术计算错误引起的错误。
研究团队还系统性地记录了模型在生成解决方案过程中表现出的显著行为模式和趋势，以便进行深入分析。这些观察结果有助于识别模型推理能力中存在的常见问题和需要改进的方向。
结果
主要结果
研究评估了六个推理模型（QWQ、R1、FLASH-THINKING、O1-PRO、O3-MINI 和 Claude 3.7）在 2025 年 USAMO 问题上的表现。
表 1 详细分析了各模型在每个问题上的表现，平均分基于四次评估运行计算，每题满分 7 分，每次运行总分 42 分。表中还包括使用各模型的总成本数据。
评估发现，虽然当前顶尖语言模型在以数值答案为主的竞赛（如 AIME 和 HMMT）中可与顶尖人类竞争者相当，但在生成严格证明方面存在显著差距。所有评估模型的最高平均分不足 5%，近 150 个被评估的解答中无一获得满分。
所有模型都无法解决超过一个问题，这凸显了当前大型语言模型在奥林匹克级数学推理任务中的局限性。这表明现有优化方法如 GRPO 对需要高度逻辑精确性的任务可能尚不足够。
失败模式
人类参与者最常见的失误是无法找到正确解答，但他们通常能清楚判断自己是否成功解决了问题。相比之下，所有评估的大型语言模型都声称已解决问题，这对数学应用构成重大挑战，因为在缺乏严格人类验证的情况下，这些模型得出的结果不可信赖。
研究人员详细分析了评分过程中发现的错误类型。图 2 展示了评审员确定的错误类别分布。
最常见的是逻辑缺陷，包括无依据的推理步骤、错误理由或对先前进展的误解。另一个重要问题是模型倾向于将关键证明步骤视为琐碎而不提供适当证明。值得注意的是，尽管 O3-MINI 是表现最佳的推理模型之一，却经常通过将关键步骤标记为「琐碎」来跳过基本证明步骤。
研究还发现模型推理缺乏创造性，通常在所有尝试中采用相同且错误的策略，未能探索替代方法。例外是 FLASH-THINKING，它在同一运行中尝试多种策略，但仅浅层探索每种方法，未能得出有效结论。
然而，模型在代数和算术计算方面普遍表现出色，能在没有外部支持的情况下成功执行符号运算。不过，R1 表现出明显更高频率的代数或算术错误，表明这是该模型需要改进的方向。
自动评分
研究团队探索了用 LLMs 替代人类评分员的可行性，选择 O3-MINI 和 Claude 3.7 作为评分模型。两个模型均获得了评分方案、验证解决方案和评估示例参考。
表 2 显示，两个模型都未能准确评分解决方案，均系统性地高估了解答质量。具体而言，它们经常为不正确或无依据的推理授予分数，导致分数膨胀最多达到 20 倍。
值得注意的是，FLASH-THINKING 从自动评估中获得的分数明显低于其他模型，研究人员推测这可能是因为它倾向于在每次尝试中生成多个解决方案，从而混淆了基于 LLMs 的评审系统。相比之下，QWQ 获得较高分数，可能是因为它通常生成更简洁的解决方案，更便于自动评审系统理解。
定性讨论
答案框选
当前强化学习优化技术依赖从明确的最终答案中提取奖励，为此模型常被要求将最终答案放在 \boxed {} 环境中。然而，这在 USAMO 问题解答中产生了意外副作用：即使大多数评估问题不需要框选答案，模型仍习惯性地这样做。
一个典型例子是问题 5 中，QWQ 模型错误地限制自己只寻找整数解，尽管题目没有这样的要求。它坚持最终答案是 2，虽然已经正确推导出所有偶数都满足条件。这表明像 GRPO 这样的对齐技术可能无意中让模型认为每个数学问题都需要一个明确的框选答案，从而损害了其整体推理能力。
模式泛化
模型常表现出将小数值案例中观察到的模式过度泛化到更大未测试案例的倾向。虽然这种启发式方法对仅需数值答案的问题可能有效，但对于需要严格证明的问题，这种方法本质上存在缺陷。模型经常在缺乏正式证明的情况下，错误地断言小案例中观察到的模式具有普遍适用性。
解答结构与清晰度
不同模型提供的解答在清晰度和结构连贯性上存在显著差异。O3-MINI 和 O1-PRO 等模型通常以清晰、逻辑化且易于理解的方式呈现解答。相反，FLASH-THINKING 和 QWQ 等模型经常产生混乱且难以理解的回答，有时在单个解答中混合多个不相关的概念。
OpenAI 训练的模型在清晰度上的明显优势表明，专注于解答连贯性的额外训练显著提高了其可读性，这一特性在其他模型中明显受到较少重视。
所以，当下次有人警告你「AI 即将统治世界」时，不妨淡定地递给他一张奥数试卷：「先让它们过了这一关再说吧。」
