IMO-AG-30

该数据集是一个包含30个经典几何问题的基准集，这些问题源自自2000年以来国际数学奥林匹克（IMO）竞赛。该数据集被适配于专门用于交互式图形证明助手的 环境。此外，该数据集专门为评估自动化推理方法的性能而设计，解决的问题数量能够反映出IMO参赛选手的技能水平。该数据集的规模为30个问题，任务是对几何问题进行自动定理证明。

This dataset is a benchmark set encompassing 30 classic geometry problems sourced from the International Mathematical Olympiad (IMO) competitions since 2000. It is tailored to the environment specifically designed for interactive graphical proof assistants. Furthermore, this dataset is purpose-built to evaluate the performance of automated reasoning methods, as the number of included problems reflects the skill level of IMO participants. Comprising 30 problems in total, the central task of this dataset is automated theorem proving for geometric problems.

搜集汇总

背景与挑战

背景概述

IMO-AG-30是一个包含30个国际数学奥林匹克（IMO）几何问题的数据集，用于评估几何定理证明器的性能。该数据集在AlphaGeometry项目中被用于测试DDAR和AlphaGeometry两种方法，其中DDAR解决了14个问题，而AlphaGeometry解决了25个问题，展示了其在不依赖人类演示的情况下解决复杂几何问题的能力。数据集作为资源文件提供，支持几何推理研究。