FMC

FMC 数据集是由北京大学的研究团队创建的，包含3922个自然语言数学问题以及与其对应的9,787个 Lean 语言形式化问题。数据集的问题来源于国际数学奥林匹克竞赛，经过预处理和形式化流程，保证了数据集的高质量。数据集适用于自动化定理证明器，并可作为形式推理任务的基准。数据集的创建过程涉及自动化的自然语言到 Lean 语言的形式化流程，并通过反馈机制进行错误修正，确保了形式化结果的准确性和一致性。该数据集旨在推动形式化数学推理的研究，并为自动化定理证明器提供一个高难度的基准数据集。

The FMC Dataset was created by a research team from Peking University. It contains 3,922 natural language math problems and their corresponding 9,787 Lean-formalized problems. The problems in this dataset are sourced from the International Mathematical Olympiad (IMO), and have undergone preprocessing and formalization procedures to guarantee high data quality. This dataset is suitable for automated theorem provers and can serve as a benchmark for formal reasoning tasks. The creation process of the dataset involves an automated natural language-to-Lean formalization workflow, with error correction conducted via a feedback mechanism to ensure the accuracy and consistency of the formalized results. This dataset aims to advance research in formal mathematical reasoning and provide a high-difficulty benchmark dataset for automated theorem provers.

原始信息汇总

FMC数据集概述

数据集基本信息

• 名称：FMC: Formalization of Natural Language Mathematical Competition Problems
• 提出者：Jiaxuan Xie, Chengwu Liu, Ye Yuan, Siqi Li, Zhiping Xiao*, Ming Zhang*
• 相关论文：FMC: Formalization of Natural Language Mathematical Competition Problems
• 数据集地址：https://huggingface.co/datasets/JadeXie1205/FMC
• 代码仓库：https://github.com/JadeXie1205/FMC

数据集内容

• 目标：推进形式数学推理，建立自然语言数学问题与Lean形式化之间的对齐数据集。
• 规模：
  • 自然语言数学问题：3922个
  • Lean形式化问题：9787个
• 质量：64.46%的问题至少获得良好及以上质量评级
• 适用场景：作为自动定理证明器的基准数据集

技术方法

• 核心方法：基于大型语言模型的自动形式化管道，具有错误反馈功能
• 特点：
  • 完全自动化
  • 无需训练
• 实验发现：
  • 小样本学习对自动形式化性能有积极影响
  • 错误反馈对性能有积极影响
  • 增加采样数量对性能有积极影响

环境配置

• 推荐环境：Anaconda创建Python 3.8环境
• 核心依赖包：
  • torch==2.4.0
  • transformers==4.46.3
  • xformers==0.0.27.post2
  • vllm==0.6.0
  • openai==1.61.1
  • backoff

使用方式

1. 配置OpenAI API密钥、基础URL和模型名称
2. 运行命令： bash git clone https://github.com/JadeXie1205/FMC cd FMC/autoformalization_pipeline python main.py --question-file your_dataset.json --answer-root log

引用信息

bibtex @inproceedings{xie2025fmc, title={{FMC}: Formalization of Natural Language Mathematical Competition Problems}, author={Jiaxuan Xie and Chengwu Liu and Ye Yuan and Siqi Li and Zhiping Xiao and Ming Zhang}, booktitle={2nd AI for Math Workshop @ ICML 2025}, year={2025}, url={https://openreview.net/forum?id=7oRr1DQ8Gk} }

搜集汇总

数据集介绍

构建方式

在数学自动形式化领域，构建高质量的自然语言与形式语言对齐数据集是推动形式数学推理发展的关键。FMC数据集通过基于大型语言模型的自动形式化流程实现这一目标，该流程包含形式翻译、形式验证、回译和一致性检查四个阶段，并创新性地引入了错误反馈机制。研究团队从IMOmath等国际数学奥林匹克竞赛中收集了6,980道自然语言数学问题，经过几何问题过滤和子问题拆分等预处理步骤后，最终构建了包含3,922道自然语言问题与9,787个Lean形式化语句的对齐数据集，语义一致性达到81.74%。

特点

FMC数据集以其独特的奥林匹克竞赛级难度和严谨的质量控制体系脱颖而出。该数据集覆盖代数、数论等核心数学领域，问题来源横跨42个国家和地区的数学竞赛，时间跨度从1959年至2011年。通过五维质量评估体系（研究相关性、复杂度与深度、跨学科潜力、社区需求缺口和创新性）的严格筛选，64.46%的样本被评为'高于平均水平'以上。与同类数据集相比，FMC在形式验证通过率（93.39%）和语义一致性（81.74%）两个关键指标上均表现优异，特别适合作为自动定理证明系统的高难度基准测试。

使用方法

作为形式数学推理领域的重要资源，FMC数据集支持多种研究应用场景。在自动定理证明方向，研究者可使用该数据集评估证明系统处理复杂数学命题的能力；在语言模型训练方面，对齐的自然语言-Lean语句对为模型学习形式化推理提供了优质素材。使用流程建议从数据分层抽样开始，根据研究需求选择特定领域或难度级别的问题。对于形式验证任务，需配置Lean 4 REPL环境并导入Mathlib库；而语义一致性分析则可借助数据集提供的原始问题与回译文本的对比标注。实验证明，采用few-shot学习策略并结合错误反馈机制能显著提升模型在该数据集上的形式化性能。

背景与挑战

背景概述

FMC数据集由北京大学和华盛顿大学的研究团队于2025年提出，旨在解决数学竞赛问题的自动形式化难题。该数据集包含3,922个自然语言数学问题及其对应的9,787个Lean形式化表述，主要源自国际数学奥林匹克竞赛等高水平赛事。作为首个专注于奥数级别问题的形式化数据集，FMC通过基于大语言模型的错误反馈流水线实现了81.74%的语义一致性，为自动定理证明领域提供了兼具难度与规模的基准测试平台。

当前挑战

FMC数据集面临双重挑战：在领域层面，需解决形式化数学推理中自然语言与形式语言间的语义鸿沟问题，特别是几何问题的表达受限；在构建层面，需克服竞赛级问题复杂度导致的翻译错误（如条件缺失、目标错位等），以及大语言模型在一致性检查中的误判问题。数据集排除了几何问题以避免25%的错误率，同时通过五次采样迭代将形式验证通过率提升至93.39%。

常用场景

经典使用场景

在形式化数学推理领域，FMC数据集作为自然语言与Lean形式化语言对齐的奥林匹克级数学问题库，为自动定理证明系统提供了标准化的评估基准。该数据集通过大语言模型驱动的自动形式化流程，将3922道自然语言数学问题转化为9787条Lean语句，其中64.46%的样本达到中上质量水平，特别适用于验证自动定理证明器处理复杂数学命题的能力。

解决学术问题

FMC数据集有效缓解了形式化数学领域的两大核心难题：高质量形式化数据的稀缺性以及自然语言与形式语言间的语义鸿沟。通过引入带错误反馈的自动形式化流程，该工作实现了93.39%的语法验证通过率和81.74%的语义一致性，为形式化推理研究提供了规模与难度兼备的测试平台，显著推进了自动定理证明、形式化验证等方向的方法学研究。

衍生相关工作

该数据集推动了多项形式化数学领域的创新研究，包括基于强化学习的定理证明框架Safe、组合数学基准Combibench等。其构建方法启发了后续工作如Process-Driven Autoformalization对迭代形式化流程的优化，而数据集的质量评估标准更被FormalMATH等后续研究采纳为形式化语句评价的参考范式。