MiniF2F: معيار عابر للأنظمة لرياضيات الأولمبياد الرسمية على مستوى الأكاديمية

نقدّم "miniF2F"، وهو مجموعة بيانات تتضمّن صيغ مسائل رياضية رسمية على مستوى أولمبياد الرياضيات، مصمّمة لتوفير معيار موحد عبر الأنظمة المختلفة لاختبار البرهان العصبي للنظرية. يركّز معيار "miniF2F" حاليًا على أنظمة Metamath وLean وIsabelle (جزئيًا) وHOL Light (جزئيًا)، ويتكون من 488 صيغة مسألة مستمدة من مسابقات AIME وAMC والأولمبياد الدولي للرياضيات (IMO)، بالإضافة إلى مواد من المناهج الدراسية الثانوية والجامعية. نُقدّم نتائج أساسية باستخدام نموذج GPT-f، وهو مُثبت نظريات عصبي يعتمد على GPT-3، ونقدّم تحليلًا لأدائه. نهدف إلى جعل "miniF2F" مبادرة مشتركة يقودها المجتمع، ونأمل أن يسهم معيارنا في دفع التقدّم في مجال البرهان العصبي للنظرية.