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