حدسية عمرها ثلاثون عامًا، ونموذج صيني، وبرهان يتحقق منه الحاسوب

حدسية عمرها ثلاثون عامًا، ونموذج صيني، وبرهان يتحقق منه الحاسوب

في 15 أكتوبر، أعلن Shanghai AI Laboratory (上海人工智能实验室) أن فريقًا بحثيًا أثبت الحالة ثلاثية الأبعاد من حدسية Ghys، وهي مسألة مفتوحة في الأنظمة الديناميكية قائمة منذ عام 1995. طُوّر العمل باستخدام نموذج المختبر الخاص Intern-S2، وقد جرى التحقق الشكلي من البرهان النهائي في Lean على يد فريق من Peking University (北京大学).

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

ما الذي تسأل عنه الحدسية

طرح Étienne Ghys المسألة عام 1995. وبشكل عام، تسأل عمّا إذا كان سلوك الأنظمة الديناميكية الفوضوية قادرًا على تحديد تصنيفها الهندسي، وهو ما يكافئ السؤال عمّا إذا كانت الحركة تكشف شكل الفضاء الذي تحدث فيه.

لم يُحلّ السؤال العام. أثبت الفريق حالة التبعد المشترك واحد، أي الإطار ثلاثي الأبعاد، الذي ظل مفتوحًا ثلاثة عقود. هذه التفرقة مهمة لقراءة الادعاء بأمانة: الحدسية الكاملة تبقى أوسع، لكن الحالة المحددة التي قاومت الجميع حتى الآن قد حُسمت.

الجولة الأولى أنتجت أربعمائة صفحة

آلية التعاون أكثر إثارة من النتيجة نفسها، لأنها تُظهر كيف يبدو البحث بين الإنسان والذكاء الاصطناعي دقيقة بدقيقة.

أنتجت أول عملية استكشاف للمسألة من Intern-S2 تقرير اشتقاق يبلغ نحو 400 صفحة. هذا ليس جوابًا. بل كومة من الاستدلالات المرشحة، بعضها مفيد وبعضها لا، وهو تحديدًا شكل المخرجات الذي تحصل عليه حين تطلب من نموذج أن يفكر في شيء غير محلول فعلًا بدل أن يستدعي شيئًا معروفًا.

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

قدّم هذا الحكم Xu Disheng، وهو باحث زائر في المختبر وأستاذ في Greater Bay University، و Zhang Jiesong، وهو باحث ما بعد الدكتوراه يتابع الحدسية منذ دراسته للدكتوراه. وورقة Zhang، المنشورة على arXiv في 29 سبتمبر والمنقّحة في 13 أكتوبر، عمل بمؤلف واحد مع إفصاح عن استخدام الذكاء الاصطناعي: ساعد النموذج في تطوير الأفكار والحجج عبر جولات متعددة من الحوار، وقد تحقق هو من الرياضيات بشكل مستقل.

الجزء الذي يجعله أكثر من مجرد قصة

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

استخدم فريق Peking University، بقيادة Bin Dong و Ruochuan Liu، إطار SHEAF الخاص به لصياغة المبرهنات الرئيسية الأربع جميعها، إضافة إلى النتائج المساندة لـ Ghys التي تعتمد عليها الحجج. الصياغة الشكلية تعني ترجمة التعريفات والافتراضات والاستدلال إلى لغة يستطيع الحاسوب التحقق منها، حيث يجب كتابة كل خطوة من حجة الكاتب صراحة بدل تركها لقارئ مدرّب ليكملها.

استغرق الجهد نحو خمسة أيام، بمشاركة تصل إلى 100 وكيل يعملون بالتوازي، وأنتج نحو 550 ألف سطر من كود Lean. و Lean برنامج تفاعلي لإثبات المبرهنات. لا يهمّه مقدار ثقة أي أحد. إنه يفحص المنطق، فإما يقبل البرهان أو لا يقبله.

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

الإنسان والنموذج، مهام مختلفة

يستحق تقسيم العمل الذي وصفه المختبر أن يُؤخذ على ظاهره، لأنه ليس النسخة المُطرية لأي من الطرفين.

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

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

هناك طرفة مرتبطة بذلك جعلت الصحافة الصينية تضخّمها كثيرًا. يُقال إن خبيرًا في الأنظمة الديناميكية طرح المسألة نفسها على GPT-6 بدافع الفضول بعد أن سمع أن نموذجًا محليًا حلّها، فلم يصل إلى الحل. وقراءة ضيقة تجعل هذا مجرد مقارنة بين نظامين في مسألة واحدة، وهو ما يثبت قليلًا جدًا. أما قراءته كإشارة عن الديناميكية التنافسية فيجعله من نوع التفاصيل التي تحرّك الاستثمار.

لماذا يغيّر التحقق الشكلي حجم الرهان

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

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

يقول المختبر إنه سيجعل سير العمل وحدة قابلة لإعادة الاستخدام للتحقق الرياضي على منصته للاكتشاف العلمي، تربط النموذج والوكلاء والبيانات والمعدات التجريبية. ويستشهد كذلك بنتيجة أسبق، استخدم فيها فريق من Wuhan University (武汉大学) المنصة لتقليص دورة تطوير تخليق كهروكيميائي من خمس إلى عشر سنوات إلى سنة أو سنتين.

ما الذي نستخلصه

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

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

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