المشكلة في كيفية عمل علماء الرياضيات
البحث الرياضي هو أحد أكثر المساعي الفكرية الشاقة في النشاط البشري — وبطرق كثيرة، أحد أقل الأنشطة أتمتة. بينما حول الذكاء الاصطناعي البرمجة والكتابة وتحليل البيانات، ظلت الهياكل الرسمية للرياضيات العليا إلى حد كبير خارج متناولها. يجب التحقق من الإثباتات من خلال المنطق الصارم؛ الأنماط في الهياكل المجردة لا تستسلم لمطابقة الأنماط الإحصائية التي تجعل نماذج اللغة الكبيرة مفيدة للنصوص. تعتقد شركة ناشئة تسمى Axiom Math أنها وجدت طريقة لتغيير ذلك، وهذا الأسبوع أطلقت أداة مجانية لعلماء الرياضيات تضع قدرة اكتشاف أنماط كبيرة على جهاز كمبيوتر محمول واحد.
الأداة، التي تسمى Axplorer، هي نسخة ديمقراطية من PatternBoost — وهي خوارزمية طورها Francois Charton، عالم بحث يعمل الآن في Axiom وعمل سابقًا في Meta. في عام 2024، استخدم Charton PatternBoost يعمل على آلاف عقد أجهزة الكمبيوتر العملاقة على مدى ثلاثة أسابيع لحل مشكلة عمرها قرن واحد في نظرية الرسوم البيانية تسمى مشكلة Turan الأربع دورات. يمكن لـ Axplorer أن تحقق النتيجة نفسها في ساعتين ونصف على Mac Pro.
ما يفعله Axplorer
تعمل الخوارزمية الكامنة وراء Axplorer من خلال دورة تكرارية من البحث الكلاسيكي وتعلم الشبكة العصبية. يبدأ بإنشاء عدد كبير من الحلول المرشحة العشوائية لمشكلة رياضية والاحتفاظ بأفضل ما يؤدي أداء. يتم بعد ذلك تدريب شبكة عصبية محول على تلك الأمثلة الناجحة لتعلم الخصائص التي تميز الحل الجيد. في الجولة التالية، تنتج الشبكة المدربة مرشحين محسنين يخدمان بذورًا لمرحلة بحث كلاسيكية أخرى. تتناوب المرحلتان، مع كل جولة تنتج حلولاً أفضل تدريجياً.
الرؤية الرئيسية هي أن الشبكة العصبية لا تحتاج إلى فهم الرياضيات بأي معنى عميق. إنها تحتاج فقط إلى التعرف على الأنماط الهيكلية في الحلول التي تم العثور عليها حتى الآن واستخدام تلك الأنماط لتوجيه توليد مرشحين أفضل. على مدار العديد من التكرارات، ينتج عن هذا حلول لن يكون البحث الكلاسيكي وحده مرجحًا أن يجدها — خاصة في المشاكل ذات مساحات البحث الضخمة حيث يكون الاستكشاف العشوائي غير قابل للتتبع من الناحية الحسابية.
