FormalMATH

FormalMATH是一个包含5560个经过形式化验证的数学问题的数据集，涵盖从高中奥赛挑战到大学水平的定理，涉及代数、应用数学、微积分、数论和离散数学等多个领域。为了减少人工形式化的效率低下，我们引入了一种新颖的自动化形式化流程，该流程集成了：（1）用于自动形式化的特定大型语言模型（LLM），（2）多LLM语义验证，（3）基于否定的反驳过滤策略，使用现成的基于LLM的证明者。这种方法在手动验证之前保留了72.09%的陈述，同时确保了对原始自然语言问题的忠实性。我们对最先进的基于LLM的定理证明者的评估揭示了重大局限性：即使在实用的采样预算下，最强的模型也只能达到16.46%的成功率，表现出明显的领域偏见（例如，在代数中表现出色，但在微积分中失败）和对简化自动化策略的过度依赖。值得注意的是，我们发现在思维链推理场景中，自然语言解决方案指导与证明成功之间存在反直觉的负相关关系，这表明人类编写的非正式推理在形式推理环境中引入了噪声而不是清晰度。我们相信，FormalMATH为形式数学推理提供了一个强大的基准。FormalMATH is a dataset containing 5,560 formally verified mathematical problems, covering topics ranging from high school Olympiad challenges to university-level theorems, spanning multiple fields including algebra, applied mathematics, calculus, number theory, and discrete mathematics. To mitigate the inefficiency of manual formalization, we introduce a novel automated formalization pipeline that integrates: (1) a specialized large language model (LLM) for automatic formalization, (2) multi-LLM semantic verification, and (3) negation-based refutation filtering strategies leveraging off-the-shelf LLM-based theorem provers. This approach retains 72.09% of the statements prior to manual verification, while ensuring faithfulness to the original natural language problems. Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations: even under practical sampling budgets, the strongest models only achieve a 16.46% success rate, exhibiting pronounced domain bias (e.g., strong performance in algebra but failure in calculus) and overreliance on simplified automated strategies. Notably, we discover a counterintuitive negative correlation between natural language solution guidance and proof success in Chain-of-Thought (CoT) reasoning scenarios, suggesting that human-written informal reasoning introduces noise rather than clarity in formal reasoning environments. We believe FormalMATH provides a robust benchmark for formal mathematical reasoning.

原始信息汇总

FormalMATH 数据集概述

数据集基本信息

• 名称: FormalMATH
• 领域: 形式化数学推理
• 规模: 5,560个经过形式化验证的数学问题
• 覆盖范围: 从高中奥数题到本科级别定理，涵盖代数、应用数学、微积分、数论和离散数学等多个领域
• 基准比较: 比MiniF2F基准大22.8倍

主要特点

1. 大规模多领域基准:

   • 包含高中和本科级别的数学问题
   • 涵盖7个核心高中学科和7个本科专业领域

2. 高效的数据集创建流程:

   • 采用人机协作的自动形式化流水线
   • 结合多LLM自动形式化、语义验证和基于否定的反证策略
   • 自动验证准确率达72.09%，显著降低专家标注成本

3. LLM定理证明器的全面评估:

   • 揭示了当前系统的根本局限性
   • 最佳模型的成功率仅为16.46%
   • 发现自然语言解决方案指导可能降低证明成功率

评估结果

FormalMATH-All排行榜

模型	大小	日期	采样预算	总体表现
Kimina-Prover	7B	2025-4-14	32	16.46
STP	7B	2025-03-20	32	13.87
Goedel-Prover-SFT	7B	2025-02-11	32	13.53

FormalMATH-Lite排行榜

模型	大小	日期	采样预算	总体表现
STP	7B	2025-03-20	3200	53.17
Goedel-Prover-SFT	7B	2025-02-11	3200	49.41
DeepSeek-V1.5-RL	7B	2024-08-15	3200	50.35

常见错误模式

错误类型	DeepSeek-SFT	DeepSeek-RL	Goedel	STP
冗余假设	18.0%	34.0%	27.0%	24.0%
不完整证明	77.0%	62.0%	86.0%	44.0%
不等式处理能力不足	8.0%	13.0%	20.0%	1.0%
自动策略误用	62.0%	65.0%	78.0%	74.0%

相关资源

• 论文: FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

搜集汇总

数据集介绍

构建方式

FormalMATH数据集通过一种新颖的人机交互自动形式化流程构建，该流程结合了专门的大型语言模型（LLMs）进行语句自动形式化、多LLM语义验证以及基于否定的反证过滤策略。这一方法显著降低了专家标注成本，在人工验证前保留了72.09%的语句，同时确保了与原始自然语言问题的高度一致性。

使用方法

FormalMATH数据集主要用于评估基于大型语言模型的定理证明器的形式化数学推理能力。研究人员可以通过该数据集测试模型在不同数学领域的表现，分析模型在证明搜索、语义对齐和跨领域泛化等方面的局限性。数据集支持标准Pass@K评估指标，并允许通过树形并行验证等优化技术高效验证证明的正确性。

背景与挑战

背景概述

FormalMATH是由SphereLab M-A-P团队于2025年提出的一个大规模Lean4基准数据集，专注于形式化数学推理能力的评估。该数据集包含5,560个经过形式化验证的数学问题，涵盖从高中奥数到本科水平的多个数学领域，如代数、应用数学、微积分、数论和离散数学等。FormalMATH的创建旨在解决现有基准在范围和规模上的局限性，为自动定理证明系统提供更全面和严格的评估平台。该数据集通过引入一种新颖的人机协同自动形式化流程，显著降低了专家标注成本，同时确保了与原始自然语言问题的高度一致性。

当前挑战

FormalMATH面临的主要挑战包括：1) 领域问题的挑战：现有定理证明系统在处理形式化数学推理时表现出明显的领域偏差，如在代数领域表现良好但在微积分领域表现不佳；2) 构建过程的挑战：自动形式化过程中需要精确地将自然语言问题转化为Lean4语句，同时确保语义正确性，这一过程即使对人类专家也极具挑战性。此外，数据集的构建还面临验证形式化语句的正确性和语义对齐的双重技术难题，这需要结合Lean4编译器检查和多LLM语义验证等多种技术手段。

常用场景

经典使用场景

FormalMATH数据集被广泛用于评估大型语言模型在形式化数学推理中的能力，特别是在Lean4环境下验证数学定理的自动证明。该数据集涵盖了从高中奥林匹克数学题到本科水平的数学问题，涉及代数、数论、离散数学等多个领域。

解决学术问题

FormalMATH解决了现有形式化数学推理基准在范围、规模和性能饱和等方面的局限性。它提供了一个大规模、多样化的数据集，能够更全面地评估模型在不同数学领域的推理能力，同时揭示了现有模型在跨领域泛化和复杂推理中的不足。

实际应用

在实际应用中，FormalMATH可用于开发和优化基于大型语言模型的定理证明系统，帮助研究人员识别和解决模型在形式化数学推理中的特定弱点。此外，它还可用于教育领域，作为自动辅导系统的基础，帮助学生理解和解决复杂的数学问题。

数据集最近研究

最新研究方向

FormalMATH数据集在形式化数学推理领域的最新研究方向主要集中在以下几个方面：首先，通过引入大规模Lean4基准测试，该数据集覆盖了从高中奥林匹克竞赛到本科水平的多样化数学领域问题，显著扩展了现有基准的范围和规模。其次，研究团队提出了一种创新的人机协同自动形式化流程，结合了专用大型语言模型（LLMs）的语句自动形式化、多LLM语义验证以及基于否定的反证过滤策略，有效降低了专家标注成本并确保了与原始自然语言问题的语义一致性。此外，该数据集揭示了当前基于LLM的定理证明器在跨领域泛化能力、自动化策略依赖以及自然语言引导对形式推理的负面影响等方面的显著局限性，为未来改进自动定理证明系统的鲁棒性和推理复杂性提供了重要方向。

相关研究论文

• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

  香港中文大学, 西湖大学, M-A-P, 52077AI, 加州大学洛杉矶分校, 德国图宾根马克斯·普朗克智能系统研究所 · 2025年