MiniF2F

MiniF2F是正式的奥林匹克级数学问题陈述的数据集，旨在为神经定理证明提供统一的跨系统基准。miniF2F基准目前针对Metamath，Lean和Isabelle，由来自AIME，AMC和国际数学奥林匹克 (IMO) 的488问题陈述以及高中和本科数学课程的材料组成。

MiniF2F is a dataset of formal olympiad-level mathematical problem statements, designed to serve as a unified cross-system benchmark for neural theorem proving. The miniF2F benchmark currently supports Metamath, Lean and Isabelle, and consists of 488 problem statements sourced from AIME, AMC and the International Mathematical Olympiad (IMO), as well as materials from high school and undergraduate mathematics curricula.

搜集汇总

背景与挑战

背景概述

MiniF2F是一个正式的奥林匹克级数学问题数据集，旨在为神经定理证明提供统一的跨系统基准，覆盖Metamath、Lean和Isabelle系统。数据集包含来自AIME、AMC和国际数学奥林匹克（IMO）的488个问题陈述，以及高中和本科数学课程材料，适用于数学定理证明的研究和评估。