MiniF2F : une base de benchmark inter-systèmes pour les mathématiques de niveau olympiade formelle

Nous présentons miniF2F, un jeu de données comprenant des énoncés de problèmes mathématiques de niveau olympiade formel, conçu pour offrir une référence unifiée et trans-systèmes pour l'évaluation des preuves automatiques par réseaux neuronaux. Le benchmark miniF2F cible actuellement Metamath, Lean, Isabelle (partiellement) et HOL Light (partiellement), et se compose de 488 énoncés extraits des concours AIME, AMC et de la Olympiade internationale de mathématiques (IMO), ainsi que de contenus issus de cours de mathématiques au lycée et en licence. Nous rapportons des résultats de base obtenus avec GPT-f, un prouveur théorème neuronal fondé sur GPT-3, accompagnés d'une analyse de ses performances. Nous espérons que miniF2F deviendra un effort collaboratif de la communauté et que ce benchmark contribuera à stimuler les progrès dans le domaine de la preuve théorème neuronale.