HorizonMath：通过自动验证衡量AI在数学发现方面的进展 HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification
首个大规模未解数学问题的自动化验证基准，评估AI的数学发现能力
前置知识
生成器-验证器gap
这是指某类数学问题的一个关键特性：生成候选解非常困难，需要深刻的数学洞察力和创造性的推理，但验证一个候选解是否正确却相对容易，可以通过确定的、可计算的程序来完成。比如，寻找一个数学常数的闭式表达式很难，但将一个表达式与高精度数值进行比较就很简单；构造一个优化的离散对象很难，但检查它是否满足所有约束条件很容易。这个gap的存在使得我们可以用自动化的方式验证AI提出的数学候选解，而不需要昂贵的人工评审或复杂的证明系统。
理解这个概念是理解本文核心创新的关键。HorizonMath基准的整个设计哲学就是基于这个gap，通过选择那些难以产生但容易验证的问题，构建了一个可以自动化评估但又能真正测试数学发现能力的基准。
闭式表达式
闭式表达式是指用一个有限的、显式的符号公式来表示数学对象，而不是用无限级数、极限、积分或递归定义等形式。例如，求和级数的平方等于pi的平方除以6，其中pi的平方除以6就是闭式表达式。在本文中，闭式表达必须是有理数、代数数、标准超越常数和初等函数以及特定特殊函数的有限组合。不允许包含未计算的积分、无限级数、极限、隐式定义或数值近似。
本文基准中的很大一部分问题要求模型发现数学常数的闭式表达式，这测试了AI进行符号推理和数学猜想的能力。
对角Ramsey数
对角Ramsey数是图论中的一个经典概念，定义为满足以下条件的最小整数：任何包含该数量的顶点的完全图，用两种颜色给边着色后，必然包含一个单色团。经典界是2的k/2次方小于等于R(k,k)小于等于4的k次方。2023年，Campos等人在改进CGMS模板方面取得突破，首次实现了指数级的上界改进，证明R(k,k)小于等于4减epsilon的k次方。后续工作优化了模板，将指数底数c降低到约3.7992。这个问题的难度在于找到满足多个复杂数学条件的函数。
这是本文中GPT 5.4 Pro提出改进解决方案的两个问题之一，理解这个问题的背景可以让我们更好地评估AI提出改进的价值和意义。
数据污染
数据污染是指评估基准中的问题及其答案出现在模型的训练数据中，导致模型可能只是记忆了答案而不是真正理解了问题。这对于数学推理基准尤其严重，因为高知名度的数学问题及其解答很可能出现在互联网上或学术论文中，而这些材料经常被纳入大型语言模型的训练语料。当基准问题有已知解答时，就存在模型通过训练数据作弊的可能性。
HorizonMath的一个关键优势就是免疫数据污染，因为所有未解问题的答案都不存在于任何训练语料中。
差分三角集
差分三角集是一个组合设计理论中的概念。一个n乘以k+1的DTS数组，其中每行严格递增且归一化，即0等于a的i,0小于a的i,1小于...小于a的i,k。定义集合D为所有行内的正差。有效性约束要求D中所有元素必须互不相同。DTS的范围定义为所有条目中的最大值。最小scope DTS问题要求找到满足约束的DTS，使得scope尽可能小。
这是HorizonMath中的一个代表性优化问题，属于benchmark_best_known类别。
研究动机
现有的数学推理基准如MATH、GSM8K已经饱和，前沿模型在这些基准上达到近乎完美的准确率。即使是最具挑战性的基准，如IMO-Bench和Putnam-Bench，也都是评估已知解决方案的问题，无法衡量AI系统是否能够产生新颖的数学结果。测量未解决问题上的能力本身就很困难，因为解决方案是未知的。现有研究级基准依赖于形式化证明验证或人工评审，两者都难以扩展。此外，基准中问题的解答可能已经出现在模型的训练数据中，导致数据污染问题。
本文的目标是本文的目标是创建一个大规模的、免疫数据污染的、可自动化验证的数学发现基准，用以系统性地衡量AI在自主数学研究方面的进展。具体来说，目标是建立一个包含超过100个predominantly未解问题的基准，这些问题来自应用数学和计算数学的8个领域，覆盖闭式表达发现、离散构造优化和存在性问题三个类别。每个问题都没有已知的精确或最优解，因此不存在数据污染。同时，这些问题可以利用生成器-验证器gap进行自动化验证。
与已有工作不同的是，本文的独特切入角度在于识别并利用三类具有生成器-验证器gap的数学问题：闭式表达发现问题、构造和优化问题、存在性问题。与依赖形式化证明或人工评审的现有基准不同，HorizonMath专注于可以通过高精度数值比较和确定性约束检查来自动化验证的问题。与FrontierMath、IMProofBench和First Proof等保持问题集私有或依赖人工评估的基准不同，HorizonMath是完全开源的。
核心方法
HorizonMath的整体思路是建立一个包含未解数学问题的基准，每个问题都具有明确的答案形式和可自动化的验证方法。基准遵循四个设计原则：首先，每个问题必须要求一个明确的数学对象作为答案，而不是自然语言证明；其次，这个答案必须可以通过简单的确定性计算程序进行客观验证；第三，问题必须需要长期的数学推理，并抵抗标准计算算法的解决；第四，每个问题必须具有科学意义，即来自数学文献或活跃研究。通过这些原则筛选的问题，可以利用其内在的生成器-验证器gap进行自动化评估。
核心创新点是识别并系统化地利用三类具有生成器-验证器gap的数学问题，将它们组织成一个统一的基准和自动化验证框架。与依赖形式化证明系统或人工评审的现有方法不同，HorizonMath专注于那些候选解难以产生但可以通过确定性计算高效验证的问题。这意味着评估几乎完全是计算性的，避免了形式化证明验证的可扩展性瓶颈和人工评审的主观性。另一个关键创新是严格定义可接受的解的形式，确保提出的解决方案具有数学意义且不是作弊。
方法步骤详情
方法步骤包括问题收集、分类、验证框架设计和评估流程实现。第一步是问题收集：使用AI驱动的搜索工具和人工验证来识别来自研究文献的候选问题，涵盖三个类别。第二步是问题分类：每个问题沿三个轴进行分类：结构输出类型、可解性级别和数学领域。第三步是验证框架设计：模型被提示生成一个自包含的Python函数，严格的可接受性标准通过系统提示和基于LLM的可接受性检查器强制执行。第四步是评估模式：对于ground_truth_computable问题，闭式表达式通过mpmath评估到高精度并与参考值比较；对于benchmark_best_known问题，模型的输出通过问题特定的验证器评分；对于new_construction问题，通过确定性检查验证提议的对象是否满足所有所需属性。
技术新颖性
技术新颖性体现在多个方面。首先，HorizonMath是首个专注于未解数学问题的大规模基准，免疫数据污染。其次，自动化的评估pipeline完全消除了对人工评审的需求，使用高精度数值比较和确定性约束检查器。第三，严格的可接受性标准和LLM驱动的可接受性检查器确保了提出的解决方案是数学合理的。第四，开源的评估基础设施使得可复现和独立评估成为可能。第五，实验结果显示GPT 5.4 Pro在两个问题上提出了可能优于已知基准的解决方案，这是首个证据表明AI系统可能开始具备在特定设置下进行数学研究的能力。
实验结果
核心发现是现有前沿模型在HorizonMath上的表现仍然很差，确认基准测量了现有AI系统未具备的能力。评估了三个最先进的模型：GPT 5.4 Pro、Gemini 3.1 Pro和Claude Opus 4.6。在所有级别的问题上，只有GPT 5.4 Pro取得了任何进展。它提议了两个来自Level 1类别的可能优于已知基准结果的新颖解决方案：Thin-Triangle Kakeya和Asymptotic Upper Bound Constant for Diagonal Ramsey Numbers问题。Gemini 3.1 Pro和Opus 4.6没有产生任何通过可接受性检查器或验证器的新颖解决方案。在10个Level 0问题上，Gemini 3.1 Pro和Opus 4.6对3个问题产生了有效解决方案，而GPT 5.4 Pro正确解决了5个问题。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| Full Dataset (All Levels) | Passing Candidate Solutions | GPT 5.4 Pro: 7, Gemini 3.1 Pro: 0, Claude Opus 4.6: 0 | Human baseline: 0 | GPT 5.4 Pro是唯一产生新颖解决方案的模型 |
| Level 0 Problems (Human-Solvable) | Accuracy | GPT 5.4 Pro: 50%, Gemini 3.1 Pro: 30%, Claude Opus 4.6: 30% | Human baseline: 100% | GPT 5.4 Pro在可解问题上表现最好，但仍未达到人类水平 |
| Thin-Triangle Kakeya (128 slopes) | Area(E) | 约0.10915 | 约0.11481 (AlphaEvolve) | 约0.00566减少 (4.93% reduction) |
| Asymptotic Upper Bound Constant for Diagonal Ramsey Numbers | Upper bound base c | 约3.6961 | 约3.7992 (Gupta-Ndiaye-Norin-Wei, 2024) | 约0.1031减少 (2.71% reduction) |
局限与改进
局限性包括几个方面。首先，匹配高精度数值参考，即使到20个小数位，也不正式证明闭式表达式是完全正确的。其次，可接受性检查器可能偶尔接受利用微妙漏洞的解决方案或拒绝使用不寻常但合法构造的有效解决方案。第三，当前的基准仅限于三类问题，不包括需要基于证明的验证的开放问题。第四，基准目前的规模为101个问题，虽然相对较大但仍有限。第五，实验结果显示前沿模型在未解决问题上的得分接近0%，这意味着基准目前可能太难。
独立分析的弱点
独立分析的弱点包括：1）基准的三类问题可能无法覆盖数学研究的全部范围，特别是基于证明的数学贡献。2）严格的可接受性标准虽然防止了作弊，但也可能限制了模型的创造性表达。3）自动化验证虽然高效，但不能提供形式化的证明保证。4）可接受性检查器使用LLM本身可能存在偏见或错误。5）基准中的问题可能偏向于那些具有明确的数值或构造目标的领域。改进方向包括：扩展基准以包含需要证明验证的开放问题；放宽可接受性标准；改进可接受性检查器；增加更多样化的问题类型；扩展实验范围。
未来方向
未来研究方向包括：1）扩展基准以接受简化但不一定是精确闭式形式的解决方案，这在物理等领域特别有用；2）超越当前三类问题，扩展到需要基于证明的验证的开放问题，与形式化系统如Lean集成；3）将基准扩展到更多数学领域；4）增加更多级别和难度梯度的问题；5）开发更复杂的验证机制；6）研究如何自动生成或发现适合该基准的新问题；7）探索将HorizonMath与形式化证明系统深度集成。
复现评估
HorizonMath是完全开源的，包括问题定义、真值计算和验证脚本。然而，实验依赖于三个最先进的模型API服务，这些是专有的。评估过程中涉及高精度数值计算，需要一定的计算资源。对于某些问题，验证使用Mathematica进行精确有理算术，可能需要额外的软件许可。基准的模块化设计使得添加新问题和修改验证器相对容易。总体而言，HorizonMath的复现难度适中，虽然评估基础设施是开源的，但模型API的专有性质和成本可能限制某些研究者的复现能力。
论文图表