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