FormalMath500, MiniF2F-Solving, PutnamBench-Solving

FormalMath500是一个形式化的MATH500基准子集，包含387个数据点，涵盖代数、中级代数、数论、预代数和预微积分。MiniF2F-Solving是MiniF2F的重构子集，包含375个数据点，来自AIME、MATH-Algebra、AMC、IMO和MATH-Number Theory。PutnamBench-Solving是PutnamBench的重构子集，包含324个数据点，涵盖抽象代数、代数、分析、组合数学、几何、线性代数、数论、概率和集合论。

FormalMath500 is a formalized subset of the MATH500 benchmark, consisting of 387 data points covering algebra, intermediate algebra, number theory, prealgebra, and precalculus. MiniF2F-Solving is a refactored subset of MiniF2F, containing 375 data points sourced from AIME, MATH-Algebra, AMC, IMO, and MATH-Number Theory. PutnamBench-Solving is a refactored subset of PutnamBench, comprising 324 data points covering abstract algebra, algebra, analysis, combinatorics, geometry, linear algebra, number theory, probability, and set theory.

原始信息汇总

数据集概述

基本信息

• 论文标题: Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
• 论文链接: https://arxiv.org/abs/2505.04528
• 数据集链接: https://huggingface.co/collections/purewhite42/formal-problem-solving-681b573aac8f09f308bb7c66
• 许可证: Apache 2.0

研究重点

1. 问题解决的定义
2. 在现有形式化定理证明（FTP）环境中进行过程验证的问题解决

主要贡献

• FPS（形式化问题解决）：利用FTP环境进行过程验证的问题解决
• D-FPS（演绎FPS）：解耦解决和答案验证以实现更好的人类对齐
• RPE（受限命题等价）：通过形式化验证确定答案正确性的符号方法
• 三个问题解决基准：
  • FormalMath500
  • MiniF2F-Solving
  • PutnamBench-Solving

基准详情

FormalMath500

• 数据点: 387
• 分类:
  • Algebra: 123
  • Intermediate Algebra: 92
  • Number Theory: 62
  • Prealgebra: 65
  • Precalculus: 45

MiniF2F-Solving

• 数据点: 375
• 分类:
  • AIME: 30
  • MATH-Algebra: 140
  • AMC: 82
  • IMO: 3
  • MATH-Number Theory: 120

PutnamBench-Solving

• 数据点: 324
• 分类:
  • Abstract Algebra: 9
  • Algebra: 138
  • Analysis: 122
  • Combinatorics: 14
  • Geometry: 28
  • Linear Algebra: 25
  • Number Theory: 49
  • Probability: 8
  • Set Theory: 4

数据结构

每个问题包含以下字段：

• informal_problem: 自然语言描述的问题
• informal_answer: 自然语言描述的正确答案
• informal_solution: 自然语言描述的逐步解决方案
• header: 初始化形式化问题前应执行的代码
• intros: 独立变量和假设
• outros: 结论
• formal_answer: 形式化语言描述的正确答案
• formal_answer_type: 形式化语言描述的答案类型
• metainfo: 问题的元信息

评估方法

FPS评估

• Proof Search: 使用最佳优先搜索
• Whole-Proof Generation: 生成完整证明

D-FPS评估

• In-Context Learning
• Hybrid CoT

基准性能

Framework	Benchmark	Method	Model	Solved↑	Proven↑	NE-Submitted↓
FPS	FormalMath500	Proof Search	InternLM2.5-StepProver	23.77%	47.55%	19.38%
			LeanSTaR	23.51%	43.41%	20.93%
		Whole-Proof Generation	DeepSeekProver-V1.5	22.22%	46.51%	14.47%
			TheoremLlama	16.02%	4.39%	15.50%
	MiniF2F-Solving	Proof Search	InternLM2.5-StepProver	27.47%	50.67%	13.60%
			LeanSTaR	24.27%	49.33%	14.40%
		Whole-Proof Generation	DeepSeekProver-V1.5	22.40%	53.60%	10.93%
			TheoremLlama	13.07%	7.73%	8.80%
	Putnam-Solving	Proof Search	InternLM2.5-StepProver	0.00%	1.54%	28.09%
			LeanSTaR	0.00%	0.93%	41.05%
		Whole-Proof Generation	DeepSeekProver-V1.5	0.31%	1.54%	22.22%
			TheoremLlama	0.00%	0.31%	16.67%
D-FPS	FormalMath500	ICL	DeepSeek-V3	13.70%		0.00%
		Hybrid CoT	DeepSeek-V3	15.50%		1.03%
	MiniF2F-Solving	ICL	DeepSeek-V3	21.87%		0.00%
		Hybrid CoT	DeepSeek-V3	21.60%		0.00%
	Putnam-Solving	ICL	DeepSeek-V3	0.00%		0.00%
		Hybrid CoT	DeepSeek-V3	0.00%		0.31%

引用

bibtex @misc{liu2025theoremprovingformulationframework, title={Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving}, author={Qi Liu and Xinhao Zheng and Renqiu Xia and Xingzhi Qi and Qinxiang Cao and Junchi Yan}, year={2025}, eprint={2505.04528}, archivePrefix={arXiv}, primaryClass={cs.AI}, url={https://arxiv.org/abs/2505.04528}, }

搜集汇总

数据集介绍

构建方式

在数学自动推理领域，FormalMath500、MiniF2F-Solving和PutnamBench-Solving三个基准数据集的构建采用了严谨的形式化方法。数据集源自知名数学竞赛题库的精选子集，通过Lean 4定理证明环境进行形式化重构，每个问题都包含自然语言描述、形式化命题结构以及标准答案验证模块。构建过程中特别注重保持原问题的语义完整性，同时确保形式化表达与数学库Mathlib4的兼容性，采用Pantograph工具链实现机器可验证的问题表示。

使用方法

使用这些数据集时，研究者可通过三种主要范式开展实验：传统形式化问题求解(FPS)要求模型生成完整的形式化解；解耦式推理(D-FPS)支持分步生成中间解和验证证明；定理证明模式(FTP)则专注于验证给定答案的正确性。评估脚本提供标准化的测试流程，支持最佳优先搜索和整证明生成两种策略，通过配置参数可灵活控制证明搜索深度、采样温度等关键超参数。实验环境需要预先配置Lean 4工具链和Pantograph交互接口，确保形式化验证的可靠性。

背景与挑战

背景概述

FormalMath500、MiniF2F-Solving和PutnamBench-Solving数据集由上海交通大学的研究团队于2025年提出，旨在推动形式化问题求解领域的发展。这些数据集基于Lean 4定理证明环境，构建了形式化数学问题求解的标准化评估框架。研究团队通过将自然语言数学问题转化为形式化表述，实现了从传统定理证明到过程验证问题求解的范式突破。数据集覆盖代数、数论、组合数学等多个数学分支，为人工智能在数学推理领域的研究提供了重要基准。该工作发表在arXiv预印本平台，对形式化方法、自动推理和数学人工智能等交叉领域产生了显著影响。

当前挑战

该系列数据集面临的核心挑战体现在两个维度：在领域问题层面，形式化数学求解需要同时处理答案生成与正确性证明的双重任务，这对模型的符号推理和逻辑验证能力提出了极高要求。数据集构建过程中，研究团队需克服自然语言问题到形式化表述的转换难题，包括变量依赖关系的精确建模、命题条件的完整表达以及数学概念的类型系统映射。基准测试结果显示，当前最先进模型在Putnam竞赛级问题上的解决率仍接近于零，暴露出复杂数学推理任务的艰巨性。此外，保持形式化系统与自然语言问题语义的一致性，以及处理不同数学分支特有的表述规范，都是构建过程中遇到的技术瓶颈。

常用场景

经典使用场景

在形式化数学和自动定理证明领域，FormalMath500、MiniF2F-Solving和PutnamBench-Solving数据集被广泛用于评估和验证形式化问题解决（FPS）框架的有效性。这些数据集通过提供形式化的问题描述和解答，为研究人员提供了一个标准化的测试平台，用于验证自动推理系统在解决复杂数学问题时的能力。特别是在Lean 4和Mathlib 4等定理证明环境中，这些数据集被用于验证形式化证明的生成和验证过程。

解决学术问题

这些数据集解决了形式化数学和自动定理证明中的几个关键学术问题。首先，它们提供了一个标准化的基准，用于评估不同自动推理系统在解决复杂数学问题时的性能。其次，通过形式化的问题描述和解答，这些数据集帮助研究人员验证形式化证明的正确性和完整性。此外，这些数据集还促进了形式化问题解决框架（FPS）和演绎形式化问题解决（D-FPS）的发展，为自动推理系统的设计和优化提供了重要参考。

实际应用

在实际应用中，FormalMath500、MiniF2F-Solving和PutnamBench-Solving数据集被广泛应用于教育和研究领域。在教育领域，这些数据集被用于开发智能辅导系统，帮助学生理解和解决复杂的数学问题。在研究领域，这些数据集被用于验证和优化自动推理系统，特别是在形式化定理证明和数学问题解决方面。此外，这些数据集还被用于开发新的算法和技术，以提高自动推理系统在解决复杂数学问题时的效率和准确性。

数据集最近研究

最新研究方向

在形式化数学与自动推理领域，FormalMath500、MiniF2F-Solving和PutnamBench-Solving数据集正推动着形式化问题求解（FPS）研究的前沿发展。这些数据集通过将传统数学问题转化为形式化定理证明环境（如Lean 4）可处理的规范结构，为验证过程导向的数学推理建立了新范式。当前研究聚焦于三个核心方向：其一是基于确定性马尔可夫决策过程的FPS框架设计，通过InternLM2.5-StepProver等模型实现答案生成与验证的端到端自动化；其二是解耦式演绎推理（D-FPS）的探索，采用受限命题等价（RPE）技术分离求解与验证阶段，提升与人类思维的兼容性；其三是以混合思维链（Hybrid CoT）为代表的提示工程优化，在MiniF2F-Solving基准上达到21.87%的求解成功率。这些进展不仅为数学教育智能化提供了可验证的解决方案，更在形式化方法与大语言模型的交叉领域开辟了可解释性推理的新路径。