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
研究重点
- 问题解决的定义
- 在现有形式化定理证明（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}, }
