استخدم علماء الرياضيات الذكاء الاصطناعي للعمل على نظرية فيرما الأخيرة

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

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

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

لقد حيرت نظرية فيرما الأخيرة علماء الرياضيات لعدة قرون حتى تم إثباتها في عام 1993 على يد أندرو ويلز. تنص على أنه لا توجد أرقام صحيحة a وb وc تحقق المعادلة aⁿ + bⁿ = cⁿ، حيث n عدد صحيح أكبر من 2. من السهل للغاية ذكر ذلك، ولكن من الصعب للغاية إثباته.

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

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

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

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

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

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

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

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

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

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

هانغ لو سو من إمبريال كوليدج لندن هو أحد الباحثين المشاركين في ورشة العمل. لقد استخدمت ChatGPT لتعليم نفسها اللين منذ ستة أشهر فقط، وهي الآن تعمل هنا في أحدث التقنيات.

لا يزال معظم علماء الرياضيات الذين تعرفهم يستخدمون القلم والورق، لذا فإن استخدام الذكاء الاصطناعي وإضفاء الطابع الرسمي المعروض هنا لا يمثل بأي حال من الأحوال المجال اليوم، لكنها تعتقد أنه يمكن أن يكون لمحة عن مستقبله. “أشعر أن هناك تصنيعًا للعملية الفكرية [occurring]”يقول سو. “إذا كان هناك أي شيء، فإن أدوات الذكاء الاصطناعي تعمل بشكل جيد لدرجة أنها تشبه إلى حد ما: “حسنًا، لقد سمحنا فقط [the AI model] كلود يعمل، وبعد ذلك ماذا نفعل؟

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

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

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

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

“نحن نبني طبقة من المنحدر في الأعلى – دعنا نسميها المنحدر – والسؤال الآن هو، ماذا يحدث عندما نحاول نقل الطبقة التالية؟ هل يمكننا بناء الطبقة التالية في الأعلى أم أنها ستتوقف؟” يسأل بوزارد.

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

“نحن جميعا نفعل [maths] لأننا نحبها، ونعتقد أنها مهمة. ولكن الآن يأتي الذكاء الاصطناعي، وفجأة السؤال هو، في الواقع، لماذا نفعل هذا؟ ما الفائدة من ذلك؟” يقول الصقر. “إذا أثبتت الآلة نظرية ولكن لا يمكن لأي إنسان أن يفهمها، فماذا حققنا إذن؟”

تصبح هذه الأسئلة أكثر وضوحًا عندما تكون الرياضيات المعنية مجردة إلى أقصى الحدود، وتجلس في عالم يشتمل على مجالات ذات 38 بُعدًا أو مسائل معقدة دون تطبيق فوري واضح. “هناك هذا العالم المجرد، ولكن هل هذا العالم المجرد موجود إذا لم يكن البشر موجودين لتقديره؟” يسأل بوزارد.