Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad

最近为大型语言模型（LLMs）设计的数学基准测试，例如 MathArena，表明当前最先进的推理模型在像 AIME 这样的数学竞赛中取得了令人印象深刻的成绩，其中表现领先的模型 Gemini-2.5-Pro 的得分甚至可以与顶级人类选手相媲美。然而，这些基准测试仅根据最终的数值答案来评估模型的表现，忽略了对现实数学任务至关重要的严谨推理和证明生成能力。为了解决这一问题，我们引入了首个针对复杂数学问题的完整解题推理的全面评估。通过专家人工标注的方式，我们在 2025 年美国数学奥林匹克（USAMO）题目发布后的数小时内，对多个最先进的推理模型进行了评估。结果表明，所有被测试的模型都面临显著困难：只有 Gemini-2.5-Pro 获得了非 trivial 的 25% 得分，而其他所有模型的得分均低于 5%。通过对推理过程的详细分析，我们识别出了最常见的失败模式，并发现了一些由模型训练过程中采用的优化策略引发的不良现象。总体而言，我们的研究结果表明，当前的大型语言模型在处理严谨的数学推理任务时仍然力有不逮，这凸显了提升推理能力和证明生成能力的迫切需求。

论文试图解决当前大型语言模型（LLMs）在数学推理和证明生成任务中的不足，特别是针对需要严格推理和完整解题过程的复杂数学问题。这是一个新问题，因为之前的基准测试主要关注最终答案的准确性，而忽略了推理过程的质量。

论文通过引入全面评估框架，使用专家人类标注者对模型生成的完整解决方案进行评分，来衡量LLMs在USAMO级别数学问题上的表现。与仅依赖最终答案的传统方法不同，该研究强调了对推理过程和证明生成能力的深入分析。

实验设计包括对2025年USAMO的六道题目进行实时评估，揭示了当前最先进的模型（如Gemini-2.5-Pro）在严谨推理任务中的局限性。研究详细分析了模型的常见失败模式，并指出了训练优化过程中可能引入的不良行为。此外，论文提供了未来改进方向，例如增强推理能力和生成更高质量的证明。遗憾的是，文中未提及代码开源或具体数据集细节。

相关工作包括MathArena等数学基准测试的研究，以及关于AIME竞赛的模型性能评估。其他相关研究如《Evaluating Large Language Models on Mathematical Reasoning》和《ProofNet: A Framework for Generating Formal Proofs》也探讨了LLMs在数学推理领域的潜力与挑战。