MiniF2F：一个用于形式化奥林匹克级别数学的跨系统基准
人工智能
2022-03-01 v2 形式语言与自动机理论
机器学习
摘要
我们提出miniF2F，一个形式化奥林匹克级别数学问题陈述的数据集，旨在为神经定理证明提供一个统一的跨系统基准。miniF2F基准目前面向Metamath、Lean、Isabelle（部分）和HOL Light（部分），由取自AIME、AMC和国际数学奥林匹克（IMO）以及高中和本科数学课程材料的488个问题陈述组成。我们报告了使用基于GPT-3的神经定理证明器GPT-f的基线结果，并提供了其性能分析。我们期望miniF2F成为一个社区驱动的努力，并希望我们的基准将有助于推动神经定理证明的进步。
引用
@article{arxiv.2109.00110,
title = {MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics},
author = {Kunhao Zheng and Jesse Michael Han and Stanislas Polu},
journal= {arXiv preprint arXiv:2109.00110},
year = {2022}
}
备注
Published as a conference paper at ICLR 2022