MiniF2F: Ein cross-system Benchmark für formale Mathematik auf Olympiade-Niveau

Wir stellen miniF2F vor, einen Datensatz formaler Mathematikaufgaben auf Olympiade-Niveau, der als einheitlicher, systemübergreifender Benchmark für neuronale Beweisführung dienen soll. Der miniF2F-Benchmark zielt derzeit auf Metamath, Lean, Isabelle (teilweise) und HOL Light (teilweise) ab und umfasst 488 Aufgabenstellungen, die aus dem AIME, AMC und der Internationalen Mathematik-Olympiade (IMO) sowie aus Materialien von Schul- und Hochschulmathematik-Kursen stammen. Wir präsentieren Baseline-Ergebnisse, die mit GPT-f erzielt wurden, einem neuronalen Beweissystem auf Basis von GPT-3, sowie eine Analyse seiner Leistungsfähigkeit. Wir sehen miniF2F als eine communitygetriebene Initiative und hoffen, dass unser Benchmark die Fortschritte in der neuronalen Beweisführung voranbringen wird.