ما يدّعيه البحث
نشر فريق في غوغل ديب مايند تقريراً محكّماً عن نظام ذكاء اصطناعي يعثر على براهين رياضية ويعرضها للتحقق الآلي أثناء عمله. البحث، وعنوانه “Advancing Mathematics Research with AI-Driven Formal Proof Search” لتسوكالاس وزملائه، صدر في مجلة ساينس يوم 8 أكتوبر.
النظام، ألفابروف نيكسوس، مبني حول نموذج جيميناي 3.1 برو. يكتب البرهان بلغة لين، وهي لغة صورية يتحقق فيها البرنامج من كل خطوة منطقية، ورسائل الخطأ من المدقق توجّه المسودة التالية. وفي المسائل الفرعية الأصعب يستطيع تسليم العمل إلى ألفابروف، أداة البرهنة المتخصصة لدى ديب مايند.
اختار الباحثون 353 مسألة مفتوحة من مجموعة إردوش وصاغوها بلغة لين. وأغلق النظام تسعاً منها، أي نحو 2.5%، اثنتان منها ظلتا بلا حل 56 عاماً. وبرهن كذلك 44 حدسية من الموسوعة الإلكترونية لمتتاليات الأعداد الصحيحة، وحسم سؤالاً مفتوحاً في الهندسة الجبرية، وحسّن حداً معروفاً في أمثلة المين-ماكس، وهي تقنية تُستخدم في تدريب بعض نماذج الذكاء الاصطناعي.
الجزء المثير هو تحليل الحذف
تفيد ديب مايند بأن النظام حل المسائل التسع نفسها من دون ألفابروف. ووجد تحليل حذف أن تركيبة أبسط، يسمّيها البحث الوكيل أ، بلغت التسع نفسها، وهي نقطة أثارها جوزيب كورتو من جامعة كتالونيا المفتوحة ضمن تعليقات الخبراء التي جمعها مركز ساينس ميديا في إسبانيا. ويقرأ كورتو النتيجة بوصفها علامة على إفراط هندسي، ويرى أن البحث يحمل تناقضات منهجية.
أما اعتراضه الأمضى فيتعلق بما يشتريه التحقق الصوري وما لا يشتريه. فلين، كما يشير، يضمن أن البرهان صحيح منطقياً، ولا يضمن أن العبارة التي صاغها أحدهم هي المسألة التي قصد صياغتها. فنقل حدسية غير صورية إلى لين يظل خطوة بشرية، والخطأ هناك يعبر المدقق سليماً.
كيف تُقرأ تسع من 353
المقام مهم. فهذه تسع نجاحات ضمن مجموعة محددة اختارها الفريق وصاغها بنفسه، وليست قدرة عامة على إسقاط حدسيات شهيرة. ويشير بابلو هايا كول من جامعة مدريد المستقلة، في المجموعة نفسها من التعليقات، إلى المنهجية لا إلى العدد: القيمة في طريقة قابلة للتكرار لتوليد اكتشافات رياضية، لا في التسع ذاتها.
ويطرح خافيير أرامايونا، مدير المعهد الإسباني للعلوم الرياضية، المشكلة الناتجة عن وصول براهين مدققة آلياً أسرع مما يقرأها أحد: كثير من النتائج التي يولّدها الذكاء الاصطناعي متحقق منها ومع ذلك غير مفهوم بالكامل. ووصفه تيودورو كالونخي من جامعة بلد الوليد بأنه بحث عالي الجودة ومحاولة مبكرة، وفيه مجال واسع للتحسين.
المقارنة مع المختبر الآخر
الطريق الذي سلكه هذا العمل جزء من القصة. فقد نشرت ديب مايند حلول إردوش علناً قبل صدور البحث، ثم أرسلت العمل إلى تحكيم الأقران. وسلكت أوبن إيه آي الطريق الآخر فأودعت مئات البراهين المولّدة بالذكاء الاصطناعي في مستودع شيفرة، وهو ما دفع مجموعة من علماء الرياضيات إلى الدعوة لمقاطعة الشركة في وقت سابق من هذا الشهر.
وما يستحق المتابعة هو هل تصمد ملفات لين أمام التدقيق الخارجي، وهل تتبيّن إحدى الصياغات التسع معبّرة عن شيء غير مسألة إردوش التي تحمل اسمها. هذا الفحص متاح الآن لأي شخص، وهو الحجة العملية لصالح الطريق الذي اختارته ديب مايند.
