وكلاء الذكاء الاصطناعي يحوّلون في 24 يومًا برهانًا من 15 ألف صفحة إلى 43 مليون سطر من الكود ويكتشفون خطأ عمره 40 عامًا

قامت مجموعة من عشرات من وكلاء الذكاء الاصطناعي، في غضون 24 يومًا، بإعادة كتابة أحد أضخم البراهين الرياضية في التاريخ — نحو 15 ألف صفحة من النص، عمل عليها كبار علماء الرياضيات لعقود — في صيغة يفهمها الحاسوب: أكثر من 43 مليون سطر من الكود، يتحقق منه برنامج تحقق خطوة بخطوة. وفي خضم هذه العملية، اكتشف الوكلاء ثغرة منطقية في الاستدلال ظلت خافية لقرب 40 عامًا.

ماذا يعني "صوغ" برهان رياضيًا

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

يتجلى حجم هذه العملية في حساب بسيط: 43 مليون سطر من الكود مقابل 15 ألف صفحة من النص المصدر، أي نحو 2900 سطر لكل صفحة من النص. وعلى مدى 24 يومًا من العمل، يعني ذلك نحو 1.8 مليون سطر يوميًا، أو قرابة 75 ألف سطر في الساعة بشكل متواصل. وللمقارنة، فإن صوغ نظريات رياضية أكثر تواضعًا بكثير يستغرق عادة أشهرًا من العمل عند المتخصصين البشريين — وهو حجم عمل كان من المستحيل أن ينجزه فريق من علماء الرياضيات يدويًا.

لماذا عثرت الآلة على الثغرة ولم يعثر عليها البشر

نجت الثغرة في الاستدلال التي اكتشفها الوكلاء من أعين عشرات المراجعين الدقيقين لقرب 40 عامًا. وهذا لا يعني إهمالًا من جانب هؤلاء الأشخاص — فالأمر يتعلق بطبيعة التحقق اليدوي نفسها. فقراءة 15 ألف صفحة من البداية إلى النهاية وإعادة فحص كل انتقال منطقي أمر مستحيل عمليًا. ويستند المراجع لا محالة إلى سمعة المؤلفين وإلى شعور حدسي بأن خطوة وسيطة معينة "تبدو صحيحة".

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

ما الذي يمثله ذلك من حيث "الرموز" (tokens)

هذا تقدير من تحرير "حميدون نيوز"، وليس بيانات رسمية للمشروع. فإذا اعتمدنا تقدير 10 إلى 12 رمزًا لكل سطر من الكود النهائي، فإن 43 مليون سطر تعني نحو نصف مليار رمز للمخرجات النهائية وحدها. والتكلفة الفعلية أعلى من ذلك بكثير، إذ يكتب الوكلاء نسخًا أولية، ويحصلون على أخطاء من برنامج التحقق، ثم يعيدون كتابة أجزاء منها ويعيدون التحقق من جديد. ومع حساب كل هذه التكرارات، فإن العدد الإجمالي يُقدَّر على الأرجح بالمليارات من الرموز.

وقد أصبح هذا الإنجاز في 24 يومًا ممكنًا بفضل العمل المتوازي. فالبرهان الضخم ينقسم بطبيعته إلى شبكة من اللِّمات (lemmas) المتداخلة، ويمكن توزيع الفروع المستقلة من هذه الشبكة على وكلاء مختلفين في نفس الوقت. ويعمل برنامج التحقق كحكم محايد يُصدر إجابة ثنائية — "مقبول" أو "مرفوض" — وهو ما يعني أن الوكلاء لا يحتاجون إلى الثقة بنتائج بعضهم بعضًا على الكلام: فكل قطعة من الكود تمر بالتحقق أو لا تمر.

ما يمكن لفرق المهندسين الاستفادة منه

الدرس الرئيسي لا يتعلق بالرياضيات الصرفة وحدها. فالأنظمة الوكيلية تتوسع على أفضل نحو حيث يوجد حكم آلي لا لبس فيه: مترجم (compiler)، أو مجموعة اختبارات، أو محرك إثبات. وفي ظل هذه الشروط، لا حاجة لمراجعة مئات آلاف الأسطر من الكود المولَّد يدويًا — فالآلة نفسها تقوم بعملية الفحص والاستبعاد.

وينطبق النمط نفسه على التحقق الرسمي من المكتبات التشفيرية، والمترجمات، وبروتوكولات التوافق (consensus)، والوحدات العتادية (hardware). والشروط متماثلة في كل مكان: مواصفة تفصيلية للمهمة، وبرنامج تحقق آلي صارم، وإمكانية تقسيم العمل إلى وحدات مستقلة. وعلى الفرق التي تخطط لبناء خطوط أنابيب وكيلية مماثلة أن تستثمر في المقام الأول في برنامج التحقق نفسه وفي تفكيك المهمة إلى وحدات مستقلة — فعدد الوكلاء وحجم النموذج عاملان ثانويان. وهناك استنتاج عملي آخر يتعلق بالمراجعة: فالبرهان المصاغ رسميًا يوفر ضمانة قابلة للتكرار بالصحة، وهو أمر لا يمكن لنص مكتوب بخط اليد من 15 ألف صفحة أن يوفره بطبيعته أبدًا.