MiniF2F

displayName: MiniF2F
license:
- Apache 2.0
mediaTypes:
- Text
paperUrl: https://arxiv.org/pdf/2109.00110v2.pdf
publishDate: "2022"
publishUrl: https://github.com/openai/miniF2F
publisher:
- University of Pittsburgh
- École polytechnique
- OpenAI
tags:
- Olympic
- Mathematical problems
taskTypes:
- Automated Theorem Proving

---
# 数据集介绍
## 简介
MiniF2F是正式的奥林匹克级数学问题陈述的数据集，旨在为神经定理证明提供统一的跨系统基准。miniF2F基准目前针对Metamath，Lean和Isabelle，由来自AIME，AMC和国际数学奥林匹克 (IMO) 的488问题陈述以及高中和本科数学课程的材料组成。
## 引文
```
@article{zheng2021minif2f,
title={MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics},
author={Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas},
journal={arXiv preprint arXiv:2109.00110},
year={2021}
}
```

## Download dataset
:modelscope-code[]{type="git"}

显示名称：MiniF2F
许可证：Apache 2.0
媒体类型：文本
论文链接：https://arxiv.org/pdf/2109.00110v2.pdf
发布年份："2022"
发布地址：https://github.com/openai/miniF2F
发布机构：匹兹堡大学、巴黎综合理工学院、OpenAI
标签：奥林匹克级数学问题
任务类型：自动定理证明（Automated Theorem Proving）

---

# 数据集介绍
## 简介
MiniF2F是面向形式化奥林匹克级数学问题题干的数据集，旨在为神经定理证明（Neural Theorem Proving）提供统一的跨系统评测基准。该基准目前适配Metamath、Lean与Isabelle三类定理证明系统，数据集包含488道取自美国数学邀请赛（American Invitational Mathematics Examination, AIME）、美国数学竞赛（American Mathematics Competitions, AMC）以及国际数学奥林匹克（International Mathematical Olympiad, IMO）的问题题干，以及高中与本科数学课程的相关教学素材。
## 引文

@article{zheng2021minif2f,
title={MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics},
author={Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas},
journal={arXiv preprint arXiv:2109.00110},
year={2021}
}

## 数据集下载
:modelscope-code[]{type="git"}

搜集汇总

背景与挑战

背景概述

MiniF2F是一个包含488个奥林匹克级别数学问题的数据集，用于神经定理证明的跨系统基准测试，支持Metamath、Lean和Isabelle系统，数据来源包括AIME、AMC和IMO等竞赛。