وكيل الذكاء الاصطناعي LongTails يثبت أكثر من 30 نظرية جديدة في التحسين الرياضي

تحقق رسمي عبر Lean 4

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

وتمكن الباحثون من الوصول إلى نحو 100 نظرية وصياغتها رسميًا، بينها 50 نظرية تحسّن ضمانات معروفة في دراسات سابقة. ويعتزم الفريق نشر 35 نظرية أخرى بوصفها نتائج رياضية مستقلة تستحق النشر الدولي. ويستغرق البرنامج في المتوسط بين 3 و7 ساعات لإثبات نظرية واحدة.

أهمية التطبيقات

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

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