miniF2F_v1

MiniF2F v1数据集包含488条陈述，展示的是奥林匹克级别的数学问题，旨在评估神经数学推理能力。这些数据来源于多种数学竞赛，包括美国数学邀请赛（AIME）、美国数学竞赛（AMC）、国际数学奥林匹克竞赛（IMO），以及高中和本科数学课程的相关材料。

The MiniF2F v1 dataset consists of 488 statements, showcasing Olympic-level mathematical problems designed to evaluate neural mathematical reasoning abilities. The data originates from various mathematical competitions, including the United States Mathematical Invitational Examination (AIME), the American Mathematics Competition (AMC), the International Mathematical Olympiad (IMO), as well as relevant materials from high school and undergraduate mathematics courses.

原始信息汇总

MiniF2F数据集概述

数据集简介

• 目标：为基于不同形式系统的自动定理证明系统提供共享基准评估
• 内容来源：奥林匹克竞赛题目(AMC/AIME/IMO)及高中/本科数学课程习题
• 覆盖形式系统：Lean、Metamath、Hol Light、Isabelle
• 许可协议：
  • Lean：Apache License
  • Metamath：MIT License
  • Hol Light：FreeBSD License
  • Isabelle：Apache License

统计信息

形式系统	测试集数量	验证集数量
Lean	244	244
Metamath	244	244
Isabelle	244	244
Hol Light	165	165

数据结构

• 划分方式：
  • valid：验证集（用于系统设计）
  • test：测试集（保留用于最终评估）
• 命名规范：
  • 竞赛题目：竞赛缩写-年份-题号（如imo-1990-p3）
  • MATH数据集题目：mathd-类别-编号（如mathd-algebra-125）
  • 其他题目：类别提示-唯一名称（如induction-11div10tonmn1ton）

版本信息

• 当前版本：v1
• 冻结日期：2021年8月
• 包含题目：244道
• 完整覆盖系统：Lean和Metamath
• 分支地址：https://github.com/openai/miniF2F/tree/v1

引用信息

• 论文标题：MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
• 作者：Zheng, Kunhao; Han, Jesse Michael; Polu, Stanislas
• 预印本：https://arxiv.org/abs/2109.00110
• BibTeX引用： bibtex @article{zheng2021minif2f, title={MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics}, author={Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas}, journal={arXiv preprint arXiv:2109.00110}, year={2021} }

贡献说明

• 接受贡献类型：新题目、缺失题目翻译、错误修复、补充证明等
• 使用要求：报告结果时需注明使用版本

搜集汇总

数据集介绍

构建方式

MiniF2F数据集是一个跨形式系统的数学基准测试集，旨在为自动化定理证明系统提供共享的评估标准。该数据集通过整合来自奥林匹克数学竞赛（如AMC、AIME、IMO）以及高中和本科数学课程的习题构建而成。每个问题都以唯一名称标识，并为每个目标形式系统（如Lean、Metamath、HOL Light和Isabelle）生成相应的文件。数据集分为验证集和测试集，验证集用于系统设计中的早期停止、强化学习等，测试集则用于最终评估。

特点

MiniF2F数据集的特点在于其跨形式系统的兼容性，涵盖了多种形式化数学系统，如Lean、Metamath、HOL Light和Isabelle。每个问题文件包含问题陈述，并可能附带示例证明。数据集采用模块化结构，问题命名遵循特定规则，便于检索和分类。此外，数据集通过开源许可证（如MIT和Apache）发布，鼓励社区贡献和协作。

使用方法

使用MiniF2F数据集时，用户需根据目标形式系统选择相应的文件。例如，对于Lean系统，用户需安装elan并克隆项目仓库，随后通过`leanpkg configure`和`leanpkg build`命令配置和构建项目。数据集中的问题以定理形式定义，用户可通过提供的脚本检查格式和风格。对于其他形式系统（如Metamath、HOL Light和Isabelle），用户需遵循各自系统的文件结构和命名规范。数据集的使用无需附加义务，但鼓励用户将新证明贡献回项目。

背景与挑战

背景概述

MiniF2F_v1数据集是一个专注于形式化数学的基准测试集，旨在为自动化定理证明系统提供一个共享的评估平台。该数据集由Kunhao Zheng、Jesse Michael Han和Stanislas Polu等研究人员于2021年创建，主要包含来自奥林匹克数学竞赛（如AMC、AIME、IMO）以及高中和大学数学课程的习题。MiniF2F的独特之处在于其跨系统特性，支持多种形式化系统，如Lean、Metamath、Hol Light和Isabelle。该数据集的发布为形式化数学领域的研究提供了重要的参考标准，推动了自动化定理证明技术的发展。

当前挑战

MiniF2F_v1数据集在构建和应用过程中面临多重挑战。首先，形式化数学问题的跨系统翻译需要高度的精确性和一致性，以确保不同系统之间的可比性。其次，数据集的构建涉及大量手动工作，包括问题陈述的标准化和证明的验证，这对研究人员的时间和专业知识提出了较高要求。此外，尽管数据集已覆盖多个形式化系统，但在某些系统中（如Hol Light和Isabelle）的翻译仍处于进行中，这限制了其全面应用的潜力。最后，数据集的扩展和维护需要持续的社区贡献，以确保其能够反映最新的研究进展和实际需求。

常用场景

经典使用场景

MiniF2F数据集作为形式化数学领域的基准测试工具，广泛应用于自动化定理证明系统的评估与比较。其经典使用场景包括在Lean、Metamath、HOL Light和Isabelle等不同形式化系统中，对奥林匹克数学竞赛题目及高中、大学数学课程中的习题进行形式化验证。通过提供统一的测试集和验证集，MiniF2F为研究人员提供了一个标准化的平台，用于测试和优化自动化推理算法的性能。

解决学术问题

MiniF2F数据集解决了自动化定理证明领域中的关键问题，即如何在不同形式化系统之间进行公平且可重复的性能评估。通过提供跨系统的基准测试，该数据集使得研究人员能够直接比较不同系统的表现，从而推动形式化数学工具的发展。此外，MiniF2F还为机器学习模型在数学推理任务中的应用提供了高质量的训练和测试数据，促进了形式化数学与人工智能的交叉研究。

衍生相关工作

MiniF2F数据集催生了一系列相关研究工作，特别是在自动化定理证明和形式化数学领域。例如，基于MiniF2F的研究成果推动了Lean和Metamath等系统的优化，提升了其处理复杂数学问题的能力。此外，该数据集还激发了机器学习与形式化数学结合的新方向，如使用强化学习技术生成数学证明。这些工作不仅扩展了MiniF2F的应用范围，也为形式化数学领域注入了新的活力。