MiniF2F

arXiv2025-09-30 收录

下载链接：

https://github.com/openai/minif2f

下载链接

链接失效反馈

官方服务：

资源简介：

该数据集名为miniF2F，包含488个来自高中竞赛的正式数学问题，这些问题以三种形式化语言表达：Lean、HOL-Light和Isabelle。数据集涵盖了三个类别的问题：260个来自MATH数据集，160个来自实际高中竞赛，以及68个为匹配前述竞赛难度而设计的问题。总共有488个问题，其中验证集和测试集各有244个。任务是对miniF2F数据集中的问题生成形式化的草图。

The miniF2F dataset consists of 488 formal mathematical problems related to high school competitions, which are represented in three formal languages: Lean, HOL-Light, and Isabelle. The dataset covers three categories of problems: 260 sourced from the MATH dataset, 160 from real high school competitions, and 68 problems designed to match the difficulty level of the aforementioned competitions. In total, there are 488 problems, with 244 allocated to the validation set and another 244 to the test set. The task is to generate formal sketches for the problems in the miniF2F dataset.

搜集汇总

数据集介绍

构建方式

MiniF2F是一个面向奥林匹克级别数学问题的跨系统形式化基准数据集。其构建过程以手动形式化为核心，从AIME、AMC、国际数学奥林匹克（IMO）以及高中数学和本科数学课程中精选问题，并额外纳入了MATH非正式数据集中的题目。所有问题陈述均被翻译成Metamath、Lean、Isabelle和HOL Light等不同形式化系统的语言，确保跨平台一致性。数据集划分为测试集和验证集，各包含244个问题，通过分层随机抽样确保每个子集均匀覆盖问题类型和难度等级。

使用方法

MiniF2F的使用方法强调作为跨系统基准的通用性。研究人员可直接在Metamath、Lean、Isabelle或HOL Light环境中加载数据集中的问题陈述，并利用各自的定理证明工具进行求解。论文中提供了基于GPT-f和tidy基线的实验设置作为参考，例如在Lean中使用PACT方法训练模型，或在Metamath中应用基于对数概率的搜索策略。评估指标通常采用Pass@N，即多次尝试中成功证明的比例。数据集附带可选的证明文件，便于复现与比较，且鼓励用户贡献新证明以丰富基准内容。

背景与挑战

背景概述

在神经定理证明这一快速发展的领域，跨系统基准测试的缺失长期制约着模型数学推理能力的客观评估。为此，来自École Polytechnique与OpenAI的研究人员Kunhao Zheng、Jesse Michael Han和Stanislas Polu于2022年在ICLR会议上提出了MiniF2F数据集，旨在为形式化奥林匹克级别的数学问题提供统一的跨系统评估平台。该数据集包含488道精心挑选的题目，源自AIME、AMC、国际数学奥林匹克（IMO）以及高中和本科数学课程，并支持Metamath、Lean、Isabelle和HOL Light等多种形式化系统。MiniF2F的发布填补了神经定理证明领域缺乏可比性基准的空白，为衡量不同形式化系统下模型的数学推理能力奠定了重要基础，并推动了该领域向IMO大挑战的最终目标迈进。

当前挑战

MiniF2F所面临的挑战具有多重维度。在领域问题层面，神经定理证明器需要应对奥林匹克级别数学问题所要求的复杂多步推理和创造性构造，例如生成非平凡的见证或证明唯一性，这对现有模型构成显著困难；此外，几何与组合问题的形式化表述在多数系统中仍处于萌芽阶段，导致数据集在问题类型分布上存在偏差。在构建过程中，多选问题需通过仅保留正确答案来重新表述，文字题的形式化需要将自然语言中的数学概念精确建模，而要求显式给出集合或证据的问题则无法直接形式化，只能通过预先提供答案来简化任务，这可能导致人类与自动化系统在公平比较上的潜在挑战。

常用场景

经典使用场景

MiniF2F 数据集在神经定理证明领域扮演着跨系统基准测试的核心角色，其经典使用场景集中于评估和比较不同形式化系统（如 Metamath、Lean、Isabelle 和 HOL Light）上神经定理证明器的数学推理能力。通过提供 488 道来自 AIME、AMC、IMO 以及高中数学和本科课程的奥林匹克级问题，该数据集为研究者提供了一个统一且难度渐进的平台，用以衡量模型在形式化数学环境中的表现。其设计初衷源于 IMO 大挑战，旨在推动人工智能在形式化到形式化（F2F）格式下解决奥林匹克数学问题的能力，从而成为连接不同形式系统与神经推理技术的桥梁。

解决学术问题

MiniF2F 解决了神经定理证明领域长期缺乏跨系统统一基准的学术难题，打破了以往因库特定训练/测试分割而导致的系统间不可比较性。它使研究者能够客观评估模型在代数、数论和不等式等数学子领域的表现，并量化形式化系统相较于非形式化环境的优势。例如，通过在 MiniF2F 上的实验，研究者发现 GPT-f 在 Lean 上的表现（Pass@8 达 29.2%）远超在 Metamath 上的结果（Pass@8 仅 1.6%），这揭示了高级策略对提升证明效率的关键作用。该数据集的意义在于为神经定理证明提供了可重复、可扩展的评估框架，推动了该领域从孤立系统向跨平台协作的转变。

实际应用

在实际应用中，MiniF2F 主要服务于自动定理证明系统的研发与优化，尤其是在教育辅助和数学竞赛自动化领域。例如，基于该数据集的 GPT-f 模型可被用于辅助数学教学，自动生成奥林匹克级问题的形式化证明，或为人类学生提供解题思路的验证。此外，MiniF2F 的跨系统特性使其成为工业界验证形式化验证工具（如 Lean 和 Isabelle）性能的标准测试床，帮助开发者改进证明搜索算法和策略库。其实际价值还体现在促进数学库的自动化扩展，如通过模型自动发现新定理的证明，从而加速形式化数学知识的积累。

数据集最近研究