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

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

صفحة بثلاثة آلاف سطر

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

وتُظهر الحسابات حجم العمل. 43 مليون سطر موزعة على 15 000 صفحة تعني نحو 2 900 سطر للصفحة الواحدة. وخلال 24 يومًا يعادل ذلك قرابة 1,8 مليون سطر يوميًا، أو نحو 75 ألف سطر في الساعة دون توقف. ولم يكن بوسع فريق بشري أن ينجز مثل هذه الأحجام، إذ تستغرق formalization حتى للنظريات الصغيرة عادةً أشهرًا من المختصين.

لماذا اكتشفت الآلة الثغرة تحديدًا؟

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

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

الاقتصاد: كم توكن يكلّف بناء كهذا؟

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

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

أبرز أرقام المشروع:

• نحو 15 000 صفحة من البرهان الأصلي الذي تراكم عبر عقود؛
• 24 يومًا من عمل النظام؛
• عشرات الوكلاء الذين عملوا بالتوازي؛
• أكثر من 43 مليون سطر من الشيفرة القابلة للتحقق؛
• نحو 1,8 مليون سطر يوميًا في المتوسط؛
• نحو 2 900 سطر من الشيفرة لكل صفحة من النص؛
• ثغرة واحدة في الحجة عمرها نحو 40 عامًا.

ما الذي يمكن نقله إلى الممارسة الهندسية؟

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

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