الذكاء الاصطناعي يحل مسألة رياضيات حيرت العلماء لمدة 10 سنوات

تمكن نظام ذكاء اصطناعي صيني من حل مسألة رياضيات معقدة ظل العلماء عاجزين عن حلها لمدة 10 سنوات، وكان قد طرحها عالم رياضيات أمريكي في عام 2014.

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

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

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

يعتمد النظام الجديد على آلية ذكية تبدأ بنظام استدلال اسمه "ريثلاس" (Rethlas) يستخدم محرك بحث للنظريات الرياضية يسمى Matlas لاستكشاف استراتيجيات الحل. وعندما يصل هذا النظام إلى برهان محتمل، يتولى نظام ثان اسمه "آرتشون" (Archon) باستخدام محرك بحث آخر يسمى LeanSearch، تحويل ذلك البرهان إلى مشروع يمكن لمثبت نظريات تفاعلي يدعى "لين 4" (Lean B4) التحقق منه ، وهذا المثبت ليس مجرد أداة، بل هو لغة برمجة متكاملة تحتوي مكتبتها على مئات الآلاف من النظريات والتعريفات الرياضية.

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