miniF2F-v2

miniF2F-v2数据集是miniF2F数据集的修订版，由香港中文大学计算机科学与工程系的研究团队创建。该数据集包含了488个定理，这些定理均来自数学竞赛，包括国际数学奥林匹克竞赛（IMO）和美国数学竞赛（AMC）。miniF2F-v2数据集对原始miniF2F中的错误和不一致进行了修正，确保了形式化和非形式化陈述的精确对应，并且所有定理都是正确且可证明的。该数据集旨在用于评估自动形式化和定理证明模型，并帮助研究者更好地理解这些模型在解决数学问题时的失败和成功模式。

搜集汇总

数据集介绍

构建方式

该数据集通过系统化修订流程构建，研究团队对原始miniF2F基准中的488个定理进行了全面验证。针对形式化陈述与非形式化陈述之间的差异，采用双重修正策略：在简化版本中确保形式化陈述精确匹配非形式化陈述；在竞赛版本中进一步还原原始数学竞赛的完整题干结构，包括保留选择题选项和隐藏已知解。所有修正均通过Lean验证器进行编译检查，并经由领域专家人工审核确认。

特点

数据集涵盖国际数学奥林匹克竞赛等权威赛事的488个定理，其核心特征体现在三个维度：在语义一致性方面，所有形式化与非形式化陈述均实现严格对应；在难度还原方面，竞赛版本完整保留了原始题目的多选项结构与未知解设定；在可验证性方面，每个定理均配备经Lean编译器验证的形式化证明。这些特性使其成为评估自动形式化与定理证明系统的可靠基准。

使用方法

研究者可将该数据集作为端到端形式推理管道的评估基准：首先将非形式化陈述输入自动形式化模型生成Lean代码，随后通过定理证明器完成形式化验证。使用时应区分两种评估模式：在简化模式下仅验证证明正确性，在竞赛模式下需额外检查证明结果与原始问题的语义一致性。数据集支持对自动形式化准确率、定理证明成功率以及全管道效能的多维度量化分析。

背景与挑战

背景概述

miniF2F-v2数据集于2025年由香港中文大学与华为香港研究中心联合发布，旨在修正原始miniF2F基准在形式化数学推理领域的系统性缺陷。该数据集聚焦于数学奥林匹克竞赛级别的定理证明任务，涵盖488个来自IMO、AMC等权威竞赛的形式化与非形式化数学命题。其核心研究在于构建能够从自然语言陈述自动形式化并完成定理证明的端到端人工智能系统，推动了自动形式化与定理证明模型的协同评估框架发展，成为衡量形式化推理进展的重要基准。

当前挑战

该数据集面临的领域挑战在于解决自然语言数学问题到形式化语言的精确转换，以及复杂定理的自动化证明。具体表现为：自动形式化模型需克服自然语言歧义与形式化语法差异导致的语义偏差；定理证明模型需应对修正后问题难度提升带来的证明长度扩展与推理复杂度增加。构建过程中需人工校正超过300个形式化命题中的假设缺失、目标简化及类型声明错误，并消除原始数据集中半数以上命题的形式化与非形式化陈述不一致问题，同时修复16个因形式化错误导致的不可证明定理。

常用场景

经典使用场景

在形式化数学推理领域，miniF2F-v2数据集作为基准测试工具被广泛应用于评估自动形式化和定理证明系统的综合性能。该数据集通过构建从自然语言问题到Lean形式化证明的完整推理流程，为研究人员提供了检验数学奥林匹克级别问题解决能力的标准化平台。其典型应用场景包括测试大型语言模型在理解自然语言数学问题、转化为形式化表述以及生成可验证证明这一完整链条中的表现，从而推动形式化推理技术的边界拓展。

衍生相关工作

基于该数据集衍生的经典工作包括Herald翻译器和Kimina证明器等前沿系统，它们在自动形式化和定理证明任务上展现了显著进步。这些工作通过利用修正后的基准进行了更可靠的评估，揭示了当前模型在数学推理链条中的瓶颈所在。此外，该数据集还促进了针对形式化表述等价性验证方法的研究，推动了自动推理评估范式的革新，为后续研究提供了重要的技术参照和发展方向。

数据集最近研究

最新研究方向

在自动定理证明领域，miniF2F-v2数据集的推出标志着形式化推理评估标准的重要演进。该数据集通过系统性修正原始版本中超过300个形式化语句的错误与简化问题，显著提升了数学奥林匹克竞赛问题的评估信度。当前研究聚焦于构建从自然语言理解到形式化证明的端到端推理系统，揭示了自动形式化模型与定理证明器之间存在的显著性能鸿沟。前沿实验表明，在修正后的数据集上，最优模型组合的准确率从原始版本的36%提升至70%，但仍远低于各组件单独评估时的表现水平。这一现象凸显了数学语言理解与形式化推理协同优化的必要性，为开发具备国际数学奥林匹克竞赛水平的人工智能系统提供了更可靠的基准框架。

相关研究论文

• 通过

  香港中文大学计算机科学与工程系 · 2025年