التفكير الرياضي الرسمي على مستوى الأولمبياد مع التعلم المعزز

أحد الأهداف طويلة الأمد للذكاء الاصطناعي هو بناء أنظمة قادرة على التفكير المعقد في مجالات واسعة، وهي مهمة تتجسد في الرياضيات بمفاهيمها اللامحدودة والطلب على أدلة صارمة. وأنظمة الذكاء الاصطناعي الحديثة، التي تعتمد غالبا على البيانات البشرية، تفتقر عادة إلى التحقق الرسمي اللازم لضمان صحتها. على النقيض من ذلك، اللغات الرسمية مثل Lean¹ تقديم بيئة تفاعلية ترتكز على التفكير، ويوفر التعلم المعزز (RL) آلية للتعلم في مثل هذه البيئات. نقدم AlphaProof، وهو مستوحى من AlphaZero² الوكيل الذي يتعلم كيفية العثور على البراهين الرسمية من خلال RL من خلال التدريب على الملايين من المشكلات التي تم إضفاء الطابع الرسمي عليها تلقائيًا. بالنسبة للمشكلات الأكثر صعوبة، فإنه يستخدم Test-Time RL، وهي طريقة لتوليد والتعلم من الملايين من متغيرات المشكلة ذات الصلة في وقت الاستدلال لتمكين التكيف العميق والمحدد للمشكلة. يعمل AlphaProof بشكل كبير على تحسين النتائج الحديثة في مشاكل المنافسة في الرياضيات التاريخية. في مسابقة IMO لعام 2024، قام نظام الذكاء الاصطناعي الخاص بنا، مع AlphaProof كمحرك المنطق الأساسي، بحل ثلاث من المشاكل الخمس غير الهندسية، بما في ذلك المشكلة الأكثر صعوبة في المنافسة. بالاشتراك مع AlphaGeometry 2³، أدى هذا الأداء، الذي تم تحقيقه من خلال حساب متعدد الأيام، إلى الوصول إلى درجة تعادل درجة الحائز على الميدالية الفضية، وهي المرة الأولى التي يحقق فيها نظام الذكاء الاصطناعي أي أداء على مستوى الميدالية. يوضح عملنا أن التعلم على نطاق واسع من الخبرة الأساسية ينتج عنه عملاء لديهم استراتيجيات تفكير رياضية معقدة، مما يمهد الطريق لأداة ذكاء اصطناعي موثوقة في حل المشكلات الرياضية المعقدة.