We present miniF2F, a dataset of formal Olympiad-level mathematics problems
statements intended to provide a unified cross-system benchmark for neural
theorem proving. The miniF2F benchmark currently targets Metamath, Lean,
Isabelle (partially) and HOL Light (partially) and consists of 488 problem
statements drawn from the AIME, AMC, and the International Mathematical
Olympiad (IMO), as well as material from high-school and undergraduate
mathematics courses. We report baseline results using GPT-f, a neural theorem
prover based on GPT-3 and provide an analysis of its performance. We intend for
miniF2F to be a community-driven effort and hope that our benchmark will help
spur advances in neural theorem proving.

miniF2F 是一个 Olympiad 级别的数学问题数据集，用于在神经定理证明中提供统一的跨系统基准。使用 GPT-f 作为神经定理证明的基线调用 miniF2F，并提供了性能分析。

MiniF2F：面向正式奥林匹克数学的跨系统基准测试

MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

We explore the application of transformer-based language models to automated
theorem proving. This work is motivated by the possibility that a major
limitation of automated theorem provers compared to humans -- the generation of
original mathematical terms -- might be addressable via generation from
language models. We present an automated prover and proof assistant, GPT-f, for
the Metamath formalization language, and analyze its performance. GPT-f found
new short proofs that were accepted into the main Metamath library, which is to
our knowledge, the first time a deep-learning based system has contributed
proofs that were adopted by a formal mathematics community.

本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。