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等竞赛。