FormalMATH

FormalMATH是一个大规模的形式数学推理基准数据集，包含5,560个经过形式验证的数学陈述，涵盖Lean4中的多个领域和难度级别。它旨在通过提供一个全面且可靠的测试平台来推动自动定理证明的研究，并引入了一个人机交互的流程，利用语言模型和自动检查来高效生成形式化的数学陈述。

FormalMATH is a large-scale benchmark dataset for formal mathematical reasoning, containing 5,560 formally verified mathematical statements spanning multiple domains and difficulty levels within Lean4. It aims to advance research in automated theorem proving by providing a comprehensive and reliable testbed, and introduces a human-machine interactive workflow that leverages language models and automated checking to efficiently generate formal mathematical statements.

原始信息汇总

FormalMATH数据集概述

基本信息

• 数据集名称: FormalMATH
• 论文标题: FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
• 论文链接: https://arxiv.org/abs/2505.02735
• 项目页面: https://sphere-ai-lab.github.io/FormalMATH/
• Hugging Face Spaces: https://huggingface.co/SphereLab

数据集简介

• 规模: 5,560个经过正式验证的数学陈述
• 领域: 涵盖多个数学领域和难度级别
• 语言: Lean4
• 目的: 为自动定理证明研究提供全面的测试基准

数据集构建流程

• 方法: 结合微调的大型语言模型和最佳N采样方法
• 验证过程:
  • 编译器检查
  • 多LLM语义验证
  • 预训练证明器的逻辑过滤
  • 最终人工审核

性能比较

最佳优先树搜索方法

方法	采样预算	Pass@K(%)
BFS(DeepSeek-V1.5-RL)	32×32×100	17.41
BFS(InternLM-V2.5)	32×32×100	25.65
BFS(BFS-Prover)	32×32×100	45.88

单次生成方法

方法	采样预算	Pass@K(%)
Kimina-Prover-7B	32	48.94
STP	3200	53.17
DeepSeek-V1.5-SFT	3200	46.82
Goedel-Prover	3200	49.41

安装与使用

环境要求

• Python 3
• Pytorch
• LEAN4
• REPL环境
• Mathlib

核心配置参数

参数	描述	默认值
--auto_dl	自动下载数据集	True
--datasets	数据集版本选择	FomaMATH-All
--generate	启用答案生成	False
--verify	启用答案验证	False
--evaluate	启用结果评估	False

快速评估

bash python FoMA_Eval.py --auto_dl --generate --verify --evaluate --datasets FomaMATH-All --model your_model_path --n 32 --nums_answer 32 --num_batches 1

引用

bibtex @misc{yu2025formalmathbenchmarkingformalmathematical, title={FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models}, author={Zhouliang Yu and Ruotian Peng and Keyi Ding and Yizhe Li and Zhongyuan Peng and Minghao Liu and Yifan Zhang and Zheng Yuan and Huajian Xin and Wenhao Huang and Yandong Wen and Ge Zhang and Weiyang Liu}, year={2025}, eprint={2505.02735}, archivePrefix={arXiv}, primaryClass={cs.AI}, url={https://arxiv.org/abs/2505.02735}, }

搜集汇总

数据集介绍

构建方式

在形式化数学推理领域，FormalMATH数据集的构建采用了创新的人机协同流水线。该流程首先利用经过微调的大型语言模型，采用最佳N采样策略自动生成形式化数学命题。随后通过多层次的自动化验证机制确保数据质量，包括编译器检查、多LLM语义验证、预训练证明器的逻辑过滤等关键技术环节，最终辅以人工审核形成闭环。这种融合前沿AI技术与人类专家智慧的构建范式，显著提升了形式化数学命题的生成效率和严谨性。

使用方法

该数据集的使用遵循模块化设计理念，通过FoMA_Eval.py脚本实现全流程管理。用户可根据需求灵活配置核心参数，包括数据集版本选择、答案生成数量、验证批处理规模等关键指标。系统支持自动下载数据集到预设路径，并提供生成、验证、评估三个独立模块的调用接口。对于需要深度定制的研究场景，用户可分别调用generate_answers.py、lean_proof_pipeline.py和evaluate_results.py子模块，实现特定环节的精细化控制。环境配置方面需预先安装Lean4证明辅助系统及相关数学库，确保验证环节的严谨性。

背景与挑战

背景概述

FormalMATH数据集由Sphere AI Lab团队于2025年推出，旨在推动形式化数学推理领域的研究。该数据集包含5,560个经过严格验证的数学命题，覆盖多个数学领域和难度级别，基于Lean4定理证明器构建。作为首个大规模形式化数学推理基准，FormalMATH通过结合大语言模型与人工验证的混合构建流程，为自动定理证明系统提供了可靠的评估平台，显著提升了AI形式化推理研究的可重复性与系统性。

当前挑战

该数据集主要面临两方面的挑战：在领域层面，形式化数学推理需要精确的逻辑表达和严格的证明验证，现有模型难以同时满足语义准确性和数学严谨性；在构建层面，数据集采用的多阶段验证流程涉及编译器检查、多模型语义验证和人工审核，其复杂的质量控制机制导致数据生成效率与规模之间存在显著权衡。此外，不同数学领域的概念体系差异也为构建统一的形式化表达框架带来挑战。

常用场景

经典使用场景

在数学自动推理领域，FormalMATH数据集为研究者提供了一个标准化的测试平台，用于评估大型语言模型在形式化数学推理任务上的表现。该数据集涵盖了多个数学领域的5,560个经过形式化验证的数学命题，能够全面测试模型在不同难度和领域的推理能力。研究者可以通过该数据集比较不同模型在定理证明任务上的性能，推动数学自动推理技术的发展。

解决学术问题

FormalMATH数据集解决了数学自动推理领域中的关键问题，包括缺乏大规模、高质量的形式化数学命题数据集的问题。该数据集通过结合人类专家和自动化验证流程，确保了命题的正确性和多样性。它为研究者提供了一个可靠的基准，用于评估和改进模型在形式化数学推理方面的能力，推动了自动定理证明和数学辅助工具的发展。

实际应用

FormalMATH数据集在实际应用中具有广泛的价值，特别是在数学教育和研究领域。它可以用于开发智能数学辅助工具，帮助学生和研究者理解和验证复杂的数学命题。此外，该数据集还可以用于训练和优化大型语言模型，使其具备更强的数学推理能力，从而在数学研究、工程计算和其他需要精确推理的领域发挥作用。

数据集最近研究

最新研究方向

在形式化数学推理领域，FormalMATH数据集作为一项开创性工作，为大型语言模型的定理证明能力评估提供了标准化基准。该数据集通过融合精调语言模型与多阶段验证流程，构建了覆盖多领域、多难度层级的5,560个形式化数学命题，显著提升了自动化推理研究的可复现性。当前研究热点集中在探索树搜索算法与单次生成模型的性能优化，如BFS-Prover在32×32×100采样预算下达到45.88%的Pass@K值，而单次生成方法中STP模型以53.17%的准确率展现出突破性进展。这些技术突破不仅推动了数学自动推理的边界，更为教育智能化、科研辅助工具等应用场景奠定了理论基础。