وكلاء الذكاء الاصطناعي يصممون خوارزميات تحسين بحدود زمن تشغيل يفحصها Lean
تعرض ورقة أولية جديدة مساراً مرحلياً بالذكاء الاصطناعي يقترح خوارزميات تحسين صندوق أسود ثم يستخدم Lean لفحص تحليلات زمن تشغيلها المتوقع.
لا يكفي تصميم الخوارزمية؛ فحجة زمن التشغيل يجب أن تصمد
تصف ورقة أولية نُشرت في 26 أكتوبر سير عمل يقوده الذكاء الاصطناعي لمهمة رياضية أشد تطلباً من حل مبرهنة معطاة: اقتراح خوارزمية تحسين في نموذج الصندوق الأسود وإنتاج حجة يفحصها Lean لزمن تشغيلها المتوقع. وتركز الورقة على مسائل الخوارزميات التطورية، حيث تستعلم الطريقة دالة هدف سعياً إلى القيمة المثلى.
مسار مرحلي من الاقتراح إلى البرهان
يفصل النظام العمل إلى مراحل. يقترح وكيل قائم على نموذج لغوي خوارزمية أولاً، لكن حواجز مبنية على Lean ترفض التصاميم التي لا تجتاز شروطاً صورية أساسية. ثم يقترح الوكيل دالة كمون ويطور حدود الانجراف، وهي طريقة معيارية لتحويل التقدم المقاس نحو الهدف إلى ضمان للزمن المتوقع. وتُعاد المحاولات الصورية استجابةً لملاحظات Lean، لذلك لا يعد التشغيل مكتملاً إلا عندما يفحص النظام الحد المعلن.
يفيد المؤلف بإكمال 12 تشغيلاً من أصل 15 باستخدام نماذج رائدة عبر ثماني فئات من المسائل. ومن الأمثلة أن المسار وجد، بحسب المخطوطة، خوارزمية ذات زمن متوقع متعدد الحدود لمسألة CycleUncover، في حين أن خوارزمية التطور الكلاسيكية (1+1) المذكورة تحتاج زمناً أسياً، وطابق الرتبة المعروفة في LeadingOnes. كما أن تجربة حذف المراحل، وفقاً للورقة، كانت تميل إلى إعادة إنتاج خط أساس البحث العشوائي أو تترك البراهين غير مكتملة. وهذه نتائج يوردها المؤلف في ورقة أولية غير محكمة، وليست تأكيداً مستقلاً للخوارزميات أو البراهين أو ادعاءات الجدة.
ما الذي يشهد عليه Lean، وما الذي ينبغي للقارئ فحصه أيضاً؟
يوفر نجاح فحص Lean دليلاً مهماً على اتساق التعريفات المرمزة وحجة زمن التشغيل. لكنه لا يثبت تلقائياً أن النموذج الصوري يلتقط كل سمة عملية في مُحسِّن واقعي، ولا أن الطريقة المقترحة ستتفوق على البدائل خارج إعداد الصندوق الأسود المحدد. وتذكر الورقة أيضاً أن مستودع مصدرها لم يكن قد نُشر بعد عند ظهورها، مما يحد من إمكان إعادة الإنتاج المستقل فوراً.
ومع ذلك، يشير هذا المسار إلى تحول مثير للاهتمام في الذكاء الاصطناعي الرياضي: فبدلاً من اختيار الاستدلالات المولدة بالتجارب وحدها، يمكن مطالبة الوكيل بحمل حجة تعقيد قابلة للفحص آلياً إلى جانب تصميمه. وعندها ينتقل السؤال الصعب إلى مرحلة أبكر: خيارات النمذجة وترجمة الخوارزمية المقصودة إلى مواصفاتها الصورية.