ذكاء Google الاصطناعي يتفوق على أبطال الأولمبياد في اختبار FirstProof الرياضي

ظلّت الرياضيات تُعدّ دائماً آخر معاقل الذكاء البشري. ففي هذا المجال يتداخل الحدس والتفكير الإبداعي والمنطق الصارم إلى حدّ يجعل محاكاة العملية بالآلة أقرب إلى مسألة فلسفية. غير أن فريق Google DeepMind أثبت للتو أن هذا المعقل يتراجع بسرعة. فقد سجّل نظام الذكاء الاصطناعي الذي طوّره الفريق رقماً قياسياً جديداً في اختبار FirstProof، وهو من أكثر الاختبارات صرامة لأنظمة الإثبات الآلي للنظريات، وتعادل مسائله في صعوبتها مسائل الأولمبياد الدولي للرياضيات. والفائزون في هذه المسابقات هم نخبة الرياضيات في العالم وصفوة الباحثين الطلاب والتلاميذ. وها هو يظهر لهم منافس لا يحتاج إلى النوم ولا يعرف قلق الرياضي أمام الورقة البيضاء.

ولتقدير حجم ما حدث، من المهم فهم ما يميّز FirstProof عن الاختبارات الأكاديمية المعتادة. فهو ليس مسابقة في تخمين الإجابات ولا في سرعة الحساب. إنه يتطلب من النظام ألا يكتفي بذكر النتيجة الصحيحة، بل أن يبني إثباتاً موثّقاً صورياً: سلسلة من الخطوات المنطقية يمكن التحقق من كل منها آلياً، ولا تحتمل أي لبس. وهنا تحديداً تعثّرت معظم النماذج اللغوية تقليدياً، فقد كانت تجيد الاستدلال المعقول ظاهرياً، لا الاستدلال الخالي من الأخطاء. والفجوة بين «شبه صحيح» و«مُثبَت رياضياً» في هذا المجال هائلة.

أما الحل التقني الذي صنع الاختراق فهو الدمج بين نهجين معماريين مختلفين جذرياً. فقد رُبط نموذج لغوي، قادر على التفكير المرن والاستكشافي، بنظام للتحقق الصوري يؤدي دور الحَكَم الذي لا يلين. يولّد الأول الفرضيات واستراتيجيات الإثبات والخطوات الوسيطة، ويستبعد الثاني فوراً السلاسل غير السليمة منطقياً. والنتيجة أشبه بتعاون بين رياضي مبدع ومراجع دقيق يعملان معاً في الوقت الفعلي. وقد عمل الباحثون على هذا النهج منذ زمن طويل، لكن DeepMind هي التي نجحت في إيجاد الحجم والبنية اللذين يجعلان النظامين يعزز أحدهما الآخر بدلاً من أن يعيقه.

وتتجاوز أهمية هذا الإنجاز التصنيفات الأكاديمية بكثير. فالإثبات الآلي للنظريات أداة أساسية مطلوبة في مجالات عديدة. ففي هندسة البرمجيات، يتيح التحقق الصوري ضمان صحة الشيفرة رياضياً، وهذا بالغ الأهمية لأنظمة التحكم في الطائرات والأجهزة الطبية والبنية التحتية المالية. وفي التشفير، يؤكد موثوقية بروتوكولات الأمان. وفي الرياضيات البحتة، قد تساعد هذه الأنظمة الباحثين على فحص بنى معقدة يستغرق التحقق منها يدوياً سنوات. وحتى الآن كانت كل هذه التطبيقات تصطدم بقيد واحد: الأدوات القائمة تتطلب جهداً هائلاً من الخبراء لـ«ترجمة» الأفكار الرياضية إلى لغة صورية. وذكاء اصطناعي قادر على العمل بنفسه على هذا المستوى يغيّر المعادلة جذرياً.

وبالنسبة إلى الصناعة عموماً، تمثل هذه النتيجة إشارة مهمة إلى اتجاه التطور. فبعد سنوات من هيمنة نماذج لغوية تكتب وتستدل بإقناع لكنها ترتكب كثيراً أخطاء منطقية بسيطة، يبحث الباحثون بإلحاح متزايد عن معماريات هجينة تعمل فيها الشبكات العصبية مقترنة بمُحقِّقات حتمية. ونتيجة DeepMind تؤكد أن هذا المسار ينجح، وينجح بصورة لافتة. وتجري OpenAI وAnthropic ومختبرات أكاديمية حول العالم أبحاثاً مماثلة، غير أن Google هي التي تتصدر اليوم في أكثر الاختبارات الرياضية صورية.

بطبيعة الحال، لا يعني الفوز في اختبار معياري أن الذكاء الاصطناعي جاهز لتعويض علماء الرياضيات، حتى على مستوى الأولمبياد. فطرح المسائل الجديدة، واختيار اتجاهات البحث، والقفزة الحدسية نحو الفرضية الصحيحة، كل ذلك لا يزال ميداناً بشرياً. لكن الحدود تتحرك باطّراد. فما أظهرته Google DeepMind في FirstProof ليس محاكاة للتفكير الرياضي، بل معادل وظيفي له في ظروف محددة بدقة. ومع اتساع هذه الظروف، سينتقل السؤال من «هل يستطيع الذكاء الاصطناعي إثبات النظريات؟» إلى «أي النظريات سيثبتها الذكاء الاصطناعي أولاً؟».