Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline

📄 arXiv: 2507.15855v4 📥 PDF

作者: Yichen Huang, Lin F. Yang

分类: cs.AI

发布日期: 2025-07-21 (更新: 2025-09-30)

💡 一句话要点

提出模型无关的验证与精炼流程，在IMO 2025问题上取得突破

🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 数学奥赛 大语言模型 验证与精炼 模型无关 复杂推理

📋 核心要点

  1. 现有大语言模型在奥赛级别数学题上表现不佳，缺乏深度推理和创造力。
  2. 提出模型无关的验证与精炼流程，提升模型解决复杂数学问题的能力。
  3. 在IMO 2025上，该流程结合多个领先模型，准确率显著提升至85.7%。

📝 摘要（中文）

国际数学奥林匹克（IMO）被广泛认为是高中数学的世界锦标赛。IMO问题以其难度和新颖性而闻名，需要深刻的洞察力、创造力和严谨性。尽管大型语言模型在许多数学基准测试中表现良好，但它们通常难以解决奥林匹克级别的问题。我们使用精心设计的提示，构建了一个模型无关的验证与精炼流程。我们证明了其在最近的IMO 2025上的有效性，避免了模型在比赛前发布的数据污染。配备三个领先模型（Gemini 2.5 Pro、Grok-4或GPT-5）中的任何一个，我们的流程正确解决了6个问题中的5个（约85.7%的准确率）。这与它们的基线准确率形成鲜明对比：通过选择32个候选解决方案中的最佳方案，Gemini 2.5 Pro为31.6%，Grok-4为21.4%，GPT-5为38.1%。这种显著的改进表明，实现高级AI推理不仅需要开发更强大的基础模型，还需要设计有效的方法来充分利用它们在复杂任务中的潜力。

🔬 方法详解

问题定义：论文旨在解决大型语言模型在国际数学奥林匹克（IMO）问题上的表现不佳的问题。现有的方法，例如直接使用大型语言模型生成答案，或者简单地选择多个候选答案中的最佳答案，都无法达到令人满意的准确率，因为IMO问题需要深度推理、创造性和严谨性。

核心思路：论文的核心思路是构建一个模型无关的验证与精炼流程。该流程不依赖于特定的模型架构，而是通过迭代地验证和改进候选解决方案，逐步逼近正确答案。这种方法旨在利用大型语言模型的生成能力，同时通过验证步骤来纠正错误和提高准确性。

技术框架：该流程包含两个主要阶段：验证阶段和精炼阶段。在验证阶段，模型生成多个候选解决方案，并使用验证机制（例如，形式化验证或逻辑推理）来评估每个解决方案的正确性。在精炼阶段，模型根据验证结果，对错误的解决方案进行修改和改进，并重新进行验证。这个过程迭代进行，直到找到一个被验证为正确的解决方案，或者达到预定的迭代次数。

关键创新：该方法最重要的技术创新点在于其模型无关性。这意味着该流程可以与任何大型语言模型结合使用，而不需要针对特定模型进行定制。此外，验证与精炼的迭代过程能够有效地纠正模型在推理过程中产生的错误，从而提高整体的准确率。

关键设计：论文中关键的设计包括精心设计的提示（prompt），用于引导大型语言模型生成候选解决方案。此外，验证机制的选择也非常重要，需要根据问题的特点选择合适的验证方法。例如，对于几何问题，可以使用几何定理进行验证；对于代数问题，可以使用代数恒等式进行验证。迭代次数和精炼策略也是需要仔细调整的参数。

📊 实验亮点

实验结果表明，该验证与精炼流程能够显著提升大型语言模型在IMO 2025问题上的表现。配备Gemini 2.5 Pro、Grok-4或GPT-5，该流程的准确率达到约85.7%，远高于这些模型的基线准确率（分别为31.6%、21.4%和38.1%）。这表明该流程能够有效地利用现有模型的潜力，解决奥赛级别的复杂数学问题。

🎯 应用场景

该研究成果可应用于提升AI在复杂推理和问题解决方面的能力，例如自动化定理证明、科学发现、软件验证等领域。通过结合验证与精炼流程，可以更有效地利用大型语言模型的潜力，解决传统AI方法难以处理的复杂问题，推动人工智能在科学研究和工程实践中的应用。

📄 摘要（原文）

The International Mathematical Olympiad (IMO) is widely regarded as the world championship of high-school mathematics. IMO problems are renowned for their difficulty and novelty, demanding deep insight, creativity, and rigor. Although large language models perform well on many mathematical benchmarks, they often struggle with Olympiad-level problems. Using carefully designed prompts, we construct a model-agnostic, verification-and-refinement pipeline. We demonstrate its effectiveness on the recent IMO 2025, avoiding data contamination for models released before the competition. Equipped with any of the three leading models -- Gemini 2.5 Pro, Grok-4, or GPT-5 -- our pipeline correctly solved 5 out of the 6 problems ($\approx$85.7% accuracy). This is in sharp contrast to their baseline accuracies: 31.6% (Gemini 2.5 Pro), 21.4% (Grok-4), and 38.1% (GPT-5), obtained by selecting the best of 32 candidate solutions. The substantial improvement underscores that the path to advanced AI reasoning requires not only developing more powerful base models but also designing effective methodologies to harness their full potential for complex tasks.