Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad

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

论文试图解决当前大型语言模型在严谨数学推理和证明生成上的不足问题，尤其是针对复杂的数学竞赛问题（如USAMO）进行全面解决方案的评估。这是一个新问题，因为以往的研究主要关注模型对最终答案的正确性，而忽视了推理过程的质量。

论文的关键思路是通过专家人类注释员评估多个最先进的语言模型在2025年USAMO问题上的表现，不仅关注最终答案，还深入分析模型生成的推理步骤。相比现有研究，该论文首次系统性地探讨了模型在复杂数学问题中的推理能力和局限性。

实验设计包括实时评估刚发布的USAMO问题，确保任务的新颖性和挑战性。研究使用了专家级的人类评分标准，并详细记录了模型的推理失败模式。此外，论文揭示了训练优化过程中可能引入的一些不良行为或偏差。虽然没有提到代码开源，但其方法论为未来研究提供了清晰的方向，例如改进模型的推理逻辑和证明生成能力。

最近的相关研究包括：1) MathArena基准测试，专注于评估LLM在AIME等数学竞赛中的表现；2) 基于链式思维提示（Chain-of-Thought Prompting）的工作，旨在提升模型的逐步推理能力；3) DeepMind的AlphaTensor项目，探索AI在数学发现中的潜力。其他相关工作还包括‘Formal Mathematics Statement Curriculum Learning’和‘Theorem Proving in Lean with GPT-f’，这些研究都尝试将形式化数学与机器学习结合。