HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification

📄 arXiv: 2603.15617v1 📥 PDF

作者: Erik Y. Wang, Sumeet Motwani, James V. Roggeveen, Eliot Hodges, Dulhan Jayalath, Charles London, Kalyan Ramakrishnan, Flaviu Cipcigan, Philip Torr, Alessandro Abate

分类: cs.LG

发布日期: 2026-03-16

💡 一句话要点

HorizonMath：利用自动验证评估AI在数学发现方面的进展

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 数学发现 AI评估 自动验证 基准测试 大型语言模型

📋 核心要点

  1. 现有数学研究基准依赖人工验证或形式证明，成本高昂且难以扩展。
  2. HorizonMath基准专注于发现难但验证易的问题，避免数据污染，实现自动评估。
  3. 实验表明，GPT 5.4 Pro在HorizonMath上取得了潜在的新突破，改进了已知最佳结果。

📝 摘要（中文）

本文提出了HorizonMath，一个包含100多个主要为未解决问题的基准，涵盖计算和应用数学的8个领域，并配有用于自动验证的开源评估框架。该基准针对一类发现困难但验证在计算上高效且简单的问题。由于这些问题的解决方案未知，HorizonMath不受数据污染的影响，并且大多数最先进的模型得分接近0%。现有的研究级基准依赖于形式化证明验证或人工审查，这两种方法都难以扩展。使用该平台，我们发现GPT 5.4 Pro为两个问题提出了改进已知最佳已发表结果的解决方案，代表了潜在的新贡献（有待专家评审）。我们将HorizonMath作为一个开放挑战和一个不断增长的社区资源发布，其中未解决问题类别中正确的问题解决方案可能构成数学文献中的新结果。

🔬 方法详解

问题定义：论文旨在解决AI在数学发现领域进展的评估问题。现有研究级基准依赖于耗时且难以扩展的形式化证明验证或人工审查，缺乏一个能够自动验证且不易受到数据污染影响的基准。

核心思路：论文的核心思路是构建一个包含大量未解决的数学问题，且这些问题具有“发现难，验证易”的特性。通过自动验证模型给出的解决方案，可以有效评估AI在数学发现方面的能力，同时避免数据污染。

技术框架：HorizonMath基准包含以下几个主要组成部分：1) 一个包含100多个未解决数学问题的集合，涵盖计算和应用数学的8个领域；2) 一个开源评估框架，用于自动验证模型提出的解决方案；3) 一套评估指标，用于衡量模型在解决这些问题上的表现。

关键创新：HorizonMath的关键创新在于其“发现难，验证易”的问题选择策略和自动验证框架。这种设计使得该基准能够有效评估AI在数学发现方面的能力，同时避免了数据污染和人工验证的成本。

关键设计：HorizonMath在问题选择上，侧重于计算和应用数学领域，并确保问题具有明确的验证标准。评估框架则采用自动化的方式，根据问题的具体性质设计相应的验证算法。例如，对于某些问题，可以通过数值模拟或符号计算来验证解决方案的正确性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，当前最先进的模型在HorizonMath上的得分接近于0%，表明该基准具有很高的挑战性。然而，GPT 5.4 Pro在两个问题上提出了改进已知最佳已发表结果的解决方案，这表明大型语言模型在数学发现方面具有潜在的能力，但仍需专家评审确认。

🎯 应用场景

HorizonMath可用于评估和提升AI在数学、科学发现等领域的潜力。通过提供一个客观、可扩展的评估平台，它可以促进AI模型在解决复杂数学问题方面的研究，并推动相关领域的创新。此外，该基准还可以作为教育工具，帮助学生和研究人员更好地理解和应用AI技术。

📄 摘要（原文）

Can AI make progress on important, unsolved mathematical problems? Large language models are now capable of sophisticated mathematical and scientific reasoning, but whether they can perform novel research is still widely debated and underexplored. We introduce HorizonMath, a benchmark of over 100 predominantly unsolved problems spanning 8 domains in computational and applied mathematics, paired with an open-source evaluation framework for automated verification. Our benchmark targets a class of problems where discovery is hard, requiring meaningful mathematical insight, but verification is computationally efficient and simple. Because these solutions are unknown, HorizonMath is immune to data contamination, and most state-of-the-art models score near 0%. Existing research-level benchmarks instead rely on formal proof verification or manual review, both of which are expensive to scale. Using this platform, we find two problems for which GPT 5.4 Pro proposes solutions that improve on the best-known published results, representing potential novel contributions (pending expert review). We release HorizonMath as an open challenge and a growing community resource, where correct solutions to problems in the unsolved problem classes could constitute novel results in the mathematical literature.