حل هندسة الأولمبياد بدون عروض بشرية

تلخيص تمثل إثبات النظريات الرياضية على مستوى الأولمبياد علامة بارزة في التفكير الآلي على مستوى الإنسان 1–4، نظرًا لصعوبتها المعروفة بين أفضل المواهب في الرياضيات ما قبل الجامعة. ومع ذلك، فإن الأساليب الحالية في التعلم الآلي غير قابلة للتطبيق على معظم المجالات الرياضية بسبب التكلفة العالية لترجمة الإثباتات البشرية إلى تنسيق يمكن التحقق منه آليًا. وتكون المشكلة أشد في الهندسة بسبب التحديات الفريدة في الترجمة 1،5، مما يؤدي إلى نقص حاد في بيانات التدريب. نحن نقترح AlphaGeometry، وهو مثبت نظري لهندسة الطائرات الإقليدية يتجنب الحاجة للعروض البشرية من خلال تركيب الملايين من النظريات والإثباتات عبر مستويات مختلفة من التعقيد. AlphaGeometry هو نظام رمزي عصبي يستخدم نموذج لغوي عصبي، تم تدريبه من الصفر على بياناتنا الاصطناعية واسعة النطاق، لتوجيه محرك الاستنتاج الرمزي عبر نقاط تفرع لا نهائية في مشاكل صعبة. في مجموعة اختبار تضم 30 مشكلة من أحدث مشاكل الأولمبياد، تحل AlphaGeometry 25 منها، متفوقة على أفضل طريقة سابقة استطاعت حل عشرة مشاكل فقط، وتقترب من أداء متوسط الفائزين بميدالية الذهب في الأولمبياد الدولي الرياضي (IMO). من الجدير بالذكر أن AlphaGeometry تنتج إثباتات قابلة للقراءة البشرية، وتحل جميع مشاكل الهندسة في IMO 2000 و2015 تحت تقييم خبير بشري، وتكتشف نسخة عامة من نظرية مترجمة في IMO عام 2004.