要約
本稿では、神経論理証明（neural theorem proving）のための統一的なクロスシステムベンチマークを提供することを目的として、形式的オリンピックレベルの数学問題文から構成されるデータセット「miniF2F」を紹介する。miniF2Fベンチマークは現在、Metamath、Lean、Isabelle（部分的に）、HOL Light（部分的に）を対象としており、AIME、AMC、国際数学オリンピック（IMO）から抽出された問題文488件に加え、高校および大学初年度レベルの数学課程の教材も含まれている。本研究では、GPT-3を基盤とする神経論理証明器GPT-fを用いたベースライン結果を報告し、その性能について分析を行う。miniF2Fはコミュニティ主導の取り組みを想定しており、本ベンチマークが神経論理証明分野の進展を促進することを期待している。