HAGeo-409 Benchmark

我们创建了HAGeo-409基准测试，该测试包含409个IMO级几何定理证明问题，通常比广泛使用的IMO-30基准测试更具难度。

We have developed the HAGeo-409 benchmark, which contains 409 IMO-level geometric theorem proving problems and is generally more challenging than the widely used IMO-30 benchmark.

原始信息汇总

HAGeo数据集概述

数据集基本信息

• 数据集名称：HAGeo-409基准测试集
• 核心任务：几何定理证明
• 状态：已发布
• 代码许可证：MIT

数据集内容与规模

• 问题数量：409个
• 问题难度：国际数学奥林匹克竞赛级别，通常比广泛使用的IMO-30基准测试集难度更大
• 难度分布：
  • 难度1–3：161个问题
  • 难度3–4：112个问题
  • 难度4–5：71个问题
  • 难度5–6：43个问题
  • 难度6–7：22个问题

数据集背景与目的

该数据集是论文《Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions》的组成部分，用于评估HAGeo框架在解决奥林匹克几何问题上的性能。HAGeo是第一个在不使用任何神经模型进行推理的情况下，在国际数学奥林匹克竞赛级别几何问题解决上达到金牌级别人类性能的框架。

评估结果

HAGeo-409基准测试结果

在HAGeo-409基准测试上，HAGeo方法在不同尝试次数下的总体解决率为：

• 尝试2048次：64.3%（263/409）
• 尝试8192次：70.2%（287/409）

作为对比：

• AlphaGeometry方法（16-64-8配置）的解决率为43.3%（177/409）
• 随机辅助点方法在尝试2048次下的解决率为49.9%（204/409），在尝试8192次下的解决率为53.3%（218/409）

IMO-30基准测试结果

在IMO-30基准测试上：

• DDAR方法解决了15个问题
• AlphaGeometry方法解决了24个问题
• 随机辅助点结合DDAR方法解决了25个问题
• HAGeo方法解决了28个问题

相关资源

• 论文地址：https://arxiv.org/abs/2512.00097
• 基准测试集地址：https://huggingface.co/datasets/HAGeo-IMO/HAGeo-409
• GitHub仓库：https://github.com/boduan1/HAGeo

搜集汇总

数据集介绍

构建方式

在几何定理证明领域，构建高质量基准数据集对于推动算法研究至关重要。HAGeo-409基准数据集的构建源于对国际数学奥林匹克（IMO）级别几何问题的系统性收集与整理，其包含409道经过严格筛选的定理证明题目。这些题目不仅覆盖了广泛的几何概念，其难度层级经过精心划分，旨在形成一个比现有IMO-30基准更具挑战性的评估体系。数据集的构建过程注重问题的代表性与难度梯度，为几何自动推理领域提供了更为坚实和全面的测试基础。

特点

该数据集的核心特点在于其卓越的难度与规模。相较于广泛使用的IMO-30基准，HAGeo-409基准通常呈现出更高的整体难度，其题目按照1至7的等级进行细致划分，从而精准刻画了从基础到顶尖的难度光谱。这种结构化的难度分布使得研究者能够深入评估算法在不同挑战级别下的性能与鲁棒性。数据集规模达到409题，为模型训练与评估提供了充足的样本，确保了结论的统计显著性与可靠性。

使用方法

该数据集主要用于评估几何自动定理证明系统的性能。研究者可将待测系统在HAGeo-409的全部或按难度分层的子集上进行测试，通过计算问题解决的成功率来量化系统能力。典型的使用流程包括将几何问题转换为系统可处理的形式化语言，运行推理引擎，并验证其生成的证明过程是否正确。数据集中包含的详细难度标签有助于进行细粒度分析，例如比较不同方法在解决高难度问题上的有效性，从而推动更高效、更鲁棒的几何推理算法的发展。

背景与挑战

背景概述

几何定理自动证明是人工智能与形式化数学交叉领域的前沿课题，旨在通过计算机构建严谨的逻辑推理链条以验证几何命题。HAGeo-409基准数据集于2025年11月由相关研究团队正式发布，其核心目标在于评估自动化系统解决国际数学奥林匹克（IMO）级别几何证明问题的能力。该数据集包含409道高难度几何问题，其整体挑战性超越了先前广泛使用的IMO-30基准，标志着几何推理自动化研究向人类金牌选手水平迈进的关键一步。数据集的建立为验证如HAGeo等新型推理框架的效能提供了标准化测试平台，推动了符号计算与启发式策略在复杂定理证明中的融合应用。

当前挑战

该数据集致力于应对几何定理自动证明领域的核心挑战，即如何让机器模拟人类解决高难度奥林匹克几何题时所需的创造性辅助构造与深层逻辑推理。具体而言，数据集中大量问题涉及非平凡的辅助线或点的引入，这对纯符号推演或穷举搜索方法构成了显著障碍。在数据集构建过程中，研究者需从海量竞赛题源中筛选并形式化表述符合IMO金牌标准的题目，确保每道题在保持原有意蕴的同时能被机器解析，这一过程涉及几何语言的形式化转换与难度等级的精确标定，以避免信息失真或偏差。

常用场景

经典使用场景

在自动定理证明领域，HAGeo-409基准测试集作为几何问题求解的高难度评估标准，其经典使用场景聚焦于测试和比较不同几何推理系统的性能。该数据集汇集了409道国际数学奥林匹克竞赛级别的几何证明题，其难度普遍超越了广泛使用的IMO-30基准。研究者通常利用此数据集，在可控的实验环境下，系统地评估诸如AlphaGeometry等先进模型在复杂几何构造与逻辑推导方面的能力极限，从而为算法优化提供精确的量化依据。

衍生相关工作

围绕HAGeo-409基准，已衍生出一系列重要的研究工作。其直接相关的HAGeo框架，首次在不依赖神经模型推理的情况下达到了金牌级别的几何问题解决水平。该基准的建立也促进了与AlphaGeometry等前沿系统的直接性能对比研究，催生了对于随机辅助点构造与演绎数据库结合等混合方法的深入探索。这些工作共同推动了自动推理领域向更高难度、更富挑战性的现实问题迈进。

数据集最近研究

最新研究方向

在自动定理证明领域，几何问题求解一直是衡量机器推理能力的重要标尺。HAGeo-409基准的提出，标志着该领域研究正朝着处理更高难度、更具挑战性的国际数学奥林匹克（IMO）级别几何问题迈进。该数据集包含409道高难度几何证明题，其整体难度显著超越了先前广泛使用的IMO-30基准，为评估模型的深度逻辑推理与构造能力提供了更为严苛的测试平台。当前的前沿研究聚焦于探索高效的启发式辅助构造策略，以突破传统演绎与代数推理引擎的局限。例如，HAGeo框架通过结合演绎数据库、代数推理与基于启发式的辅助构造搜索，在无需神经模型推理的情况下，首次达到了金牌级别的人类解题水平，这为符号人工智能与混合推理系统的发展提供了新的范式。这一进展不仅推动了自动推理技术在复杂几何问题上的边界，也对数学教育辅助工具和通用人工智能的推理能力研究产生了深远影响。