BriefGPT.xyz
Aug, 2021
MiniF2F：面向正式奥林匹克数学的跨系统基准测试
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
HTML
PDF
Kunhao Zheng, Jesse Michael Han, Stanislas Polu
TL;DR
miniF2F是一个Olympiad级别的数学问题数据集，用于在神经定理证明中提供统一的跨系统基准。使用GPT-f作为神经定理证明的基线调用miniF2F，并提供了性能分析。
Abstract
We present
minif2f
, a dataset of formal Olympiad-level
mathematics
problems statements intended to provide a unified cross-system
benchmark
→