وطن – في إنجاز لافت قد يفتح باباً جديداً في علاقة الذكاء الاصطناعي بالرياضيات، أعلنت شركة أنثروبيك أن نموذجها Claude نجح في كتابة ما وصفته بأنه أطول برهان رياضي رسمي تم إنتاجه حتى الآن، مستخدماً إياه لإثبات «مبرهنة فيرما الأخيرة» التي حيّرت علماء الرياضيات لأكثر من ثلاثة قرون ونصف.
وقالت صحيفة Decrypt الرقمية إن نموذج Claude أنجز المهمة خلال 11 يوماً فقط، وبدرجة عالية من الاستقلالية، منتجاً نحو 13 مليون سطر من الشيفرة الرياضية القابلة للتحقق حاسوبياً، بحيث يستطيع الكمبيوتر مراجعة كل خطوة من البرهان سطراً بسطر، بدلاً من الاعتماد على قراءة بشرية طويلة ومعقدة.
وتنص مبرهنة فيرما الأخيرة على أنه لا توجد ثلاثة أعداد صحيحة موجبة يمكن رفع كل منها إلى قوة أكبر من 2 بحيث يكون مجموع العددين الأولين مساوياً للثالث. وكان عالم الرياضيات الفرنسي بيير دي فيرما قد دوّن هذه الفكرة عام 1637 في هامش أحد كتب الرياضيات، مضيفاً أنه يمتلك «برهاناً رائعاً حقاً»، لكن الهامش لا يتسع لكتابته.
وبحسب ما أوردته Decrypt، توفي فيرما دون أن يترك ذلك البرهان المزعوم، لتبدأ رحلة طويلة استمرت 358 عاماً حاول خلالها علماء الرياضيات إعادة بناء ما ظن فيرما أنه توصّل إليه، أو إيجاد برهان مستقل يثبت صحة المبرهنة بشكل قاطع.
اللافت في ما أعلنته أنثروبيك لا يتعلق فقط بإعادة إثبات نتيجة رياضية معروفة، بل بطريقة الإثبات نفسها. فالبرهان الرياضي، في جوهره، سلسلة من الخطوات المنطقية الدقيقة؛ وإذا اختلّت خطوة واحدة، انهار البناء كله. والعثور على خطأ واحد داخل مئات الصفحات من الحجج الرياضية المعقدة قد يستغرق سنوات من عمل المختصين.
وأوضحت الصحيفة أن «إضفاء الطابع الرسمي» على البرهان يعني تحويله إلى لغة دقيقة للغاية يمكن للحاسوب فهمها والتحقق من كل خطوة فيها دون مساحة للتأويل أو الاجتهاد البشري. وهذا النوع من التحقق بات مهماً بشكل متزايد في الرياضيات الحديثة، خصوصاً مع ازدياد حجم البراهين وتعقيدها.
ولم تكن مشكلة التحقق من البراهين جديدة على المجتمع الرياضي. ففي عام 1908، رُصدت جائزة ألمانية تعادل قيمتها اليوم ما بين مليون ومليوني دولار تقريباً لأول برهان صحيح لمبرهنة فيرما الأخيرة. وخلال العام الأول وحده، تلقت الجهة المنظمة 621 محاولة خاطئة، ما يعكس حجم الإغراء والصعوبة معاً.
وقالت Decrypt إن البرهان الحقيقي لم يظهر إلا في عام 1995 على يد عالم الرياضيات البريطاني أندرو وايلز. وكان وايلز قد أعلن عن حله في ثلاث محاضرات خلال يونيو 1993، قبل أن يكتشف أحد المراجعين وجود ثغرة في البرهان.
قضى وايلز بعد ذلك نحو عام في محاولة إصلاح الخلل بمساعدة تلميذه السابق ريتشارد تايلور، وكاد يتخلى عن المشروع، قبل أن ينجح في نشر نسخة مصححة من البرهان في مايو 1995، وجاءت في 129 صفحة. واعتمد برهانه على أدوات رياضية لم تكن موجودة في زمن فيرما، وهو ما يجعل كثيراً من علماء الرياضيات يشككون في أن «البرهان الرائع» الذي تحدث عنه فيرما كان صحيحاً بالفعل.
وفي عام 2024، أطلق عالم الرياضيات كيفن بازارد من إمبريال كوليدج لندن مشروعاً يهدف إلى تنفيذ المهمة نفسها التي أنجزها Claude الآن: ترجمة برهان وايلز إلى لغة Lean، وهي لغة رسمية تتيح للحواسيب التحقق من صحة البراهين الرياضية. ووفقاً لما نقلته الصحيفة، فإن هذا النوع من العمل يحتاج عادة إلى جيش من علماء الرياضيات المتطوعين، إذ يبلغ المخطط العام للمشروع وحده 86 صفحة، كما أن تمويله ممتد حتى عام 2029.
لكن Claude، بحسب إعلان أنثروبيك، أنهى العمل بالكامل خلال 11 يوماً فقط.
وفي شرح أكثر تفصيلاً، قالت أنثروبيك إن تيانيي بينغ، الذي يطوّر أدوات لإضفاء الطابع الرسمي على البراهين الرياضية مع فريق في جامعة كولومبيا، أراد اختبار مدى قدرة Claude على إنجاز هذه المهمة بشكل مستقل. وعملت عشرات النسخ أو «الوكلاء» من Claude بالتوازي، حيث تولت كتابة التعريفات، وإثبات النتائج الصغيرة، ثم بناء نتائج أكبر عليها، مع تدخل بشري محدود للغاية اقتصر أحياناً على توجيهات مثل: «أعطِ الأولوية لهذه المبرهنة التالية».
وأضافت Decrypt أن العمل لم يكن سلساً منذ البداية. ففي المراحل الأولى، فقدت وكلاء Claude القدرة على تتبع ما تم إثباته بالفعل، كما توقفت أحياناً عن التعاون الفعال فيما بينها. ولا تزال تلك البدايات المتعثرة تشكّل نحو 7% من إجمالي أسطر البرهان النهائي.
وجاء الحل عبر أداة تحمل اسم Prove2Me، طورها أيضاً فريق بينغ، ومنحت جميع وكلاء الذكاء الاصطناعي قائمة مهام مباشرة ومشتركة توضّح البراهين الجزئية التي لا تزال بحاجة إلى إنجاز. وبهذه الطريقة، تجنبت النماذج تكرار العمل أو الانحراف عن المسار، كما ساعدت الأداة في تنظيم الملفات بحيث يتمكن نظام Lean من فحصها بسرعة أكبر.
كما احتفظت Prove2Me بملاحظات مكتوبة بلغة إنجليزية عادية حول كل نتيجة، ما سمح للوكلاء بإعادة استخدام أعمال بعضهم البعض بدلاً من البدء من الصفر في كل مرة. وبحسب أنثروبيك، كان هذا التنظيم أحد العوامل الحاسمة التي مكنت Claude من الوصول إلى النتيجة النهائية.
وكشفت الصحيفة أن Claude أثبت في النهاية أكثر من 30 ألف مبرهنة داعمة، واستهلك مليارات الرموز النصية أثناء التشغيل، معتمداً على نموذج بحثي تقول أنثروبيك إنه مقارب تقريباً لإصدار Claude Fable 5.1 الذي أتيح لاحقاً للجمهور.
أما حجم البرهان النهائي فبلغ 13 مليون سطر، أي أكثر من خمسة أضعاف حجم Mathlib، وهي المكتبة المشتركة التي يستخدمها علماء الرياضيات عادة في هذا النوع من أعمال التحقق الرسمي. وللمقارنة، فإن الرواية العادية تضم نحو 80 ألف كلمة، بينما يعادل برهان Claude، من حيث الحجم، ما يقرب من 160 رواية مليئة بالحجج المنطقية الصرفة.
والسؤال الأهم: هل يمثل هذا الإنجاز اكتشافاً رياضياً جديداً؟ بحسب ما أوردته Decrypt، فإن الإجابة ليست بهذه البساطة. فـ Claude لم يكتشف مبرهنة جديدة، ولم يقدم حلاً لمشكلة غير محلولة، إذ إن وايلز أثبت مبرهنة فيرما الأخيرة قبل ثلاثة عقود. لكن ما فعله النموذج هو بناء نسخة قابلة للتحقق آلياً من البرهان، وهو أمر بالغ الأهمية في عصر تتزايد فيه البراهين المعقدة، بما في ذلك البراهين التي تنتجها أنظمة الذكاء الاصطناعي نفسها.
وراجع كيفن بازارد، صاحب المشروع الأصلي الممتد حتى 2029، برهان Claude ومنحه موافقته، قائلاً إنه يثبت المبرهنة «من دون أي افتراضات غير بديهيات الرياضيات». وهذه العبارة تعني أن البرهان الرسمي لا يعتمد على ثقة شخصية أو قراءة بشرية، بل على منظومة منطقية يستطيع الحاسوب التحقق منها بشكل صارم.
وتشير الصحيفة إلى أن أهمية هذا النوع من البراهين تكمن في كونه حتمياً وأقل عرضة للأخطاء البشرية، وهي نقطة جوهرية في الرياضيات. فكل خطوة في البرهان الرسمي يجب أن تمر عبر نظام تحقق، وإذا لم تكن صحيحة منطقياً فلن تُقبل.
وليست هذه المشكلة حديثة العهد. فقد احتاج برهان حدسية كبلر بمساعدة الحاسوب إلى أربع سنوات من المراجعة قبل أن تعلن لجنة التقييم أنها «متأكدة بنسبة 99%» فقط. كما استغرق برهان غريغوري بيرلمان لحدسية بوانكاريه سنوات حتى يستوعبه المجتمع الرياضي بالكامل ويتأكد من صحته.
وبحسب ما ختمت به Decrypt، فإن من لا يرغب في الاكتفاء بإعلان أنثروبيك يمكنه التحقق بنفسه؛ فالبرهان الكامل، المؤلف من 13 مليون سطر، متاح حالياً على منصة GitHub، ويمكن لأي عالم رياضيات يمتلك الوقت والخبرة أن يراجعه سطراً بسطر. وبينما لا يعني ذلك أن الذكاء الاصطناعي أصبح بديلاً كاملاً عن علماء الرياضيات، فإنه يؤكد أن أدوات مثل Claude قد تغيّر جذرياً طريقة بناء البراهين والتحقق منها في السنوات المقبلة.
اقرأ أيضا:
تغير مفاجئ في ردود ChatGPT عند التعامل معه بقسوة.. ماذا كشفت التجارب الجديدة؟
قراءة الأفكار لم تعد خيالاً علمياً: كيف تسعى نيورالينك وميتا لربط الدماغ بالحاسوب؟