لقد طور جوجل ديب مايند AlphaProof، وهو نظام ذكاء اصطناعي حقق أداء ميدالية فضية في الأولمبياد الدولي للرياضيات لعام 2024، مسجلاً 28 من أصل 42 نقطة. كان النظام على بعد نقطة واحدة فقط من الذهب في أبرز منافسة رياضيات لطلاب الجامعات في العالم. يُظهر هذا الاختراق تقدماً في قدرة الذكاء الاصطناعي على التعامل مع البراهين الرياضية المعقدة.
لقد تفوقت الحواسيب منذ زمن طويل في الحسابات لكنها كانت تواجه صعوبات في الاستدلال المنطقي المطلوب للرياضيات المتقدمة. يعالج الذكاء الاصطناعي الجديد من جوجل ديب مايند، AlphaProof، هذا الأمر من خلال تحقيق أداء ميدالية فضية في الأولمبياد الدولي للرياضيات لعام 2024 (IMO)، أبرز منافسة رياضيات على مستوى المدارس الثانوية. تضمنت الأولمبياد ست مشكلات قيمتها سبع نقاط لكل منها، بإجمالي 42 نقطة. تطلبت الميداليات الذهبية 29 نقطة أو أكثر، حققتها 58 من أصل 609 مشاركين، بينما ذهبت الفضية لمن حصلوا على 22-28 نقطة، مع 123 متلقياً. سجل AlphaProof 28 نقطة، حل أربع مشكلات بشكل مستقل لـ21 نقطة وعتمد على AlphaGeometry 2 المتخصصة لمشكلة الهندسة للوصول إلى مستوى الفضية.
بدأ تطوير AlphaProof بتجاوز نقص البيانات التدريبية للبراهين الرياضية الرسمية. استخدم الفريق برمجية Lean، وهي أداة للتعريفات والتحققات الرياضية الدقيقة. لتوسيع مجموعة البيانات، دربوا نموذج لغة كبير Gemini لترجمة العبارات الرياضية باللغة الطبيعية إلى Lean، مولدين حوالي 80 مليون عبارة رسمية. كما شرح توماس هوبيرت، باحث في ديب مايند ومؤلف رئيسي، «الصعوبة الرئيسية في العمل مع اللغات الرسمية هي أن هناك بيانات قليلة جداً». رغم العيوب، «هناك العديد من الطرق التي يمكن من خلالها الاستفادة من الترجمات التقريبية»، أضاف.
تعتمد بنية النظام على AlphaZero من ديب مايند، تجمع شبكة عصبية مدربة من خلال التجربة والخطأ مع خوارزمية بحث شجري لاستكشاف مسارات البرهان. تكافئ البراهين الصحيحة وتعاقب الخطوات غير الفعالة، معززة الحلول الأنيقة. إضافة جديدة، التعلم بالتعزيز في وقت الاختبار (TTRL)، تسمح لـAlphaProof بتوليد تنويعات للمشكلات الصعبة للتدريب الفوري، محاكية حل المشكلات البشري. «كنا نحاول تعلم هذه اللعبة من خلال التجربة والخطأ»، قال هوبيرت.
ومع ذلك، تطلب AlphaProof مساعدة بشرية لصياغة المشكلات في Lean واستغرق عدة أيام لكل مشكلة صعبة، مستهلكاً مئات أيام-TPU، بعيداً جداً عن حدود الوقت البشرية البالغة 4.5 ساعات لكل جلسة. حل ستة بشر فقط أصعب مشكلة؛ كان AlphaProof السابع. يعترف ديب مايند بالتكاليف الحوسبية العالية لكنه يهدف إلى التحسين لاستخدام أوسع. «لا نريد التوقف عند منافسات الرياضيات. نريد بناء نظام ذكاء اصطناعي يمكن أن يساهم حقاً في الرياضيات على مستوى البحث»، قال هوبيرت. يخطط الفريق لبرنامج مختبرين موثوقين لمشاركة أداة AlphaProof مع علماء الرياضيات.
يُفصل العمل في ورقة نشرت في مجلة Nature لعام 2025 (DOI: 10.1038/s41586-025-09833-y).