ذكاء اصطناعي صيني يحل مسألة رياضية حيّرت العلماء لعقد من الزمن
الثورة نت /..
تمكن نظام ذكاء اصطناعي صيني من حل مسألة رياضيات معقدة ظل العلماء عاجزين عنها لعشرة أعوام، كانت قد طرحها عالم رياضيات أمريكي عام 2014.
وطور فريق من جامعة بكين نظاما يعمل بشكل شبه مستقل، حيث استعرض عقودا من الأبحاث الرياضية ليصل إلى الحل، ثم تحقق من صحة النتائج التي توصل إليها بنفسه دون أي تدخل بشري تقريبا.
والمسألة المحلولة هي “تخمين جبري” كان قد وضعه الأستاذ دان أندرسون من جامعة آيوا قبل وفاته عام 2022.
وأوضح الباحثون، بقيادة عالم الرياضيات دونغ بن، أن نظامهم نجح في حل هذه المسألة المفتوحة في مجال الجبر التبادلي (Commutative Algebra – وهو فرع من فروع الجبر التجريدي يركز على دراسة الحلقات التبادلية ومثالياتها)، وأثبت النتيجة بشكل تلقائي، وهو إنجاز يعتبر مثالا ملموسا على إمكانية أتمتة البحث الرياضي باستخدام الذكاء الاصطناعي.
وما يميز هذا النظام هو سرعته الفائقة مقارنة بالبشر، إذ يمكنه القيام بمهام رياضية معقدة كانت تتطلب في السابق تعاون خبراء من تخصصات متعددة. لكن التحدي الأكبر الذي واجهه الباحثون هو أن البراهين الرياضية تحتاج إلى دقة مطلقة، بينما البراهين التي تنتجها النماذج اللغوية الكبيرة غالبا ما تكون غير موثوقة بسبب ميلها إلى “الهلوسة” أو اختلاق معلومات غير صحيحة. لذلك، صمم الفريق الصيني نظاما مبتكرا يجمع بين وكيلين: الأول يعمل على الاستدلال باللغة الطبيعية، والثاني يتولى إضفاء الطابع الرسمي على النتائج والتحقق منها.
ويعتمد النظام الجديد على آلية ذكية تبدأ بنظام استدلال اسمه “ريثلاس” (Rethlas)، يستخدم محرك بحث للنظريات الرياضية يسمى Matlas لاستكشاف استراتيجيات الحل. وعندما يصل هذا النظام إلى برهان محتمل، يتولى نظام ثان اسمه “آرخون” (Archon) باستخدام محرك بحث آخر يسمى LeanSearch، تحويل ذلك البرهان إلى مشروع يمكن لمثبت نظريات تفاعلي يدعى “لين 4” (Lean B4) التحقق منه. وهذا المثبت ليس مجرد أداة، بل هو لغة برمجة متكاملة تحتوي مكتبتها على مئات الآلاف من النظريات والتعريفات الرياضية.
واستغرق النظام الصيني 80 ساعة فقط من وقت التشغيل لحل تخمين أندرسون، دون حاجة إلى أي حكم رياضي من المشغل البشري. لكن الباحثين لاحظوا أنه يمكن تسريع العملية إذا قام عالم رياضيات حقيقي بتوجيه نظام “آرخون”.
ويؤكد الفريق أن هذا العمل يمثل نموذجا واعدا للمستقبل، حيث تعمل أنظمة الاستدلال غير الرسمي والرسمي جنبا إلى جنب لإنتاج نتائج قابلة للتحقق، مع تقليل الجهد البشري بشكل كبير.
