摘要

我们提出 miniF2F，这是一个面向形式化奥林匹克级别数学问题的语料库，旨在为神经定理证明提供一个统一的跨系统基准。当前，miniF2F 基准主要针对 Metamath、Lean、Isabelle（部分）以及 HOL Light（部分），包含 488 个问题陈述，其来源涵盖 AIME、AMC 和国际数学奥林匹克竞赛（IMO）题目，以及高中与本科阶段的数学课程内容。我们报告了基于 GPT-3 的神经定理证明器 GPT-f 的基线实验结果，并对其性能进行了分析。我们期望 miniF2F 成为一项由社区共同推动的协作项目，希望该基准能够推动神经定理证明领域的进一步发展。