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
使用方式
- 配置OpenAI API密钥、基础URL和模型名称
- 运行命令： 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} }
