FormalMath500, MiniF2F-Solving, PutnamBench-Solving

FormalMath500是MATH500基准的一部分的正式化；MiniF2F-Solving和PutnamBench-Solving是FTP基准MiniF2F和PutnamBench的改编版本。这些数据集旨在为正式问题解决提供基准，并用于评估FPS和D-FPS框架的性能。

FormalMath500 constitutes the formalization of a subset of the MATH500 benchmark. MiniF2F-Solving and PutnamBench-Solving are adapted variants of the MiniF2F and PutnamBench datasets belonging to the FTP benchmark. These datasets are developed to serve as benchmarks for formal mathematical problem solving, and are employed to evaluate the performance of the FPS and D-FPS frameworks.

原始信息汇总

数据集概述

基本信息

• 论文标题: 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: 解耦求解和答案验证以实现更好的人机对齐
• 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)

• 使用模型: InternLM2.5-StepProver, LeanSTaR
• 评估指标: Solved, Proven, NE-Submitted

完整证明生成(FPS)

• 使用模型: DeepSeekProver-V1.5, TheoremLlama
• 评估指标: Solved, Proven, NE-Submitted

提示方法(D-FPS)

• 方法: In-Context Learning, Hybrid CoT
• 使用模型: DeepSeek-V3
• 评估指标: Solved, NE-Submitted

基准性能

Framework	Benchmark	Method	Model	Solved↑	Proven↑	NE-Submitted↓
FPS	FormalMath500	Proof Search	InternLM2.5-StepProver	23.77%	47.55%	19.38%
		Whole-Proof Generation	DeepSeekProver-V1.5	22.22%	46.51%	14.47%
D-FPS	FormalMath500	ICL	DeepSeek-V3	13.70%		0.00%

引用

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 数据集的构建基于严格的数学问题解决框架，采用形式化定理证明（FTP）环境进行过程验证。FormalMath500 是 MATH500 基准的形式化子集，涵盖了代数、数论等多个数学领域；MiniF2F-Solving 和 PutnamBench-Solving 则分别改编自 MiniF2F 和 PutnamBench 数据集，通过重构命题将其转化为适合问题解决的形式。这些数据集的构建过程包括问题定义、形式化编码、答案验证，并利用受限命题等价性（RPE）进行答案正确性评估。

特点

这些数据集的特点在于其严格的形式化验证和广泛的数学领域覆盖。FormalMath500 包含从初级到高级的数学问题，难度层次分明；MiniF2F-Solving 和 PutnamBench-Solving 则专注于竞赛级别的数学问题，具有较高的复杂性和挑战性。所有数据集均提供形式化问题和答案，支持过程级验证，确保推理链的完整性和答案的正确性。此外，RPE 方法的应用使得答案评估更加忠实和可解释。

使用方法

这些数据集的使用方法包括在形式化定理证明环境中进行问题求解和验证。研究人员可以利用 FPS（形式化问题解决）和 D-FPS（演绎式形式化问题解决）框架，通过 Lean 4 等工具进行问题求解。数据集支持多种评估方法，包括直接答案验证和过程级验证。用户可以通过提供的代码模板和示例快速上手，进行问题求解、答案验证和模型性能评估。此外，数据集还支持与现有 FTP 方法的对比研究，为问题解决领域的研究提供全面的实验平台。

背景与挑战

背景概述

FormalMath500、MiniF2F-Solving和PutnamBench-Solving是三个专注于形式化数学问题求解的数据集，由上海交通大学的研究团队于2025年提出。这些数据集旨在填补人工智能在过程可验证性问题求解领域的空白，通过将传统数学问题转化为形式化定理证明环境中的可验证任务。FormalMath500基于MATH500基准的形式化子集，覆盖代数、数论等基础数学领域；MiniF2F-Solving和PutnamBench-Solving则分别改编自形式化定理证明基准MiniF2F和PutnamBench，难度涵盖高中竞赛至大学本科水平。这些数据集首次实现了非形式化问题求解与形式化验证的并行评估框架。

当前挑战

该系列数据集面临双重挑战：在领域问题层面，需要解决形式化数学问题求解中答案推导与过程验证的耦合难题，特别是处理存在多解情况的'find-all'类问题；在构建层面，需克服从非形式化问题到形式化表述的转换难题，包括保持原始问题的语义完整性、处理数学对象的等价表征（如集合的不同表示形式），以及设计人类可理解的评估标准。具体表现为：1）现有模型在给定真实答案时可证明47.55%的问题，但自主求解率仅23.77%，揭示答案推导的固有难度；2）数据集中31.4%的问题涉及复杂数学对象的形式化等价判断，需要开发新型验证方法。

常用场景

经典使用场景

FormalMath500, MiniF2F-Solving, PutnamBench-Solving数据集在形式化数学问题求解领域具有广泛的应用场景。这些数据集主要用于评估和验证基于人工智能的自动定理证明和数学问题求解系统的性能。在形式化数学领域，研究人员利用这些数据集来测试模型在严格数学推理、答案推导和过程验证方面的能力。数据集中的问题涵盖了从基础代数到高等数学竞赛题目的多个难度级别，为形式化推理研究提供了丰富的测试案例。

实际应用

在实际应用方面，这些数据集可广泛应用于智能教育系统、自动解题系统和数学辅助工具的开发。教育科技公司可以利用这些数据集训练能够提供分步验证的数学解题助手；科研机构可以基于这些基准开发更可靠的形式化推理引擎；数学竞赛培训系统可以集成这些数据集的验证方法，为学员提供严格正确的解题反馈。此外，数据集的形式化特性使其特别适用于需要高可靠性保障的领域，如数学软件验证和数学知识库构建。

衍生相关工作

这些数据集衍生了一系列重要的相关研究工作。基于FormalMath500，研究者开发了结合神经符号方法的数学问题求解系统；MiniF2F-Solving启发了多个将竞赛数学形式化的后续项目；PutnamBench-Solving推动了高等数学问题自动求解的研究。数据集提出的FPS（形式化问题求解）和D-FPS（演绎式FPS）框架已成为形式化推理领域的重要基准，被应用于证明搜索、全证明生成等多种推理范式的评估。相关工作还包括基于这些数据集开发的混合推理方法、验证工程技术和过程监督模型等。