The Machine Proposes. The Proof Disposes: Neuro-Symbolic Synthesis of Formally Verified Markov Usage Models from Natural Language Requirements
تقدم هذه الورقة البحثية إطار عمل "Neuro-Symbolic MBST"، وهو إطار عمل يعمل على أتمتة تخليق نماذج استخدام ماركوف (Markov usage models) المُتحقق منها رسميًا من متطلبات اللغة الطبيعية عبر دمج تعلم L*، والنماذج اللغوية الكبيرة المقيدة بالقواعد (grammar-constrained LLMs)، والتحسين المحدب (convex optimization)، مما يحقق كشفًا عن الأخطاء وتغطية عالية الدقة تتفوق بشكل كبير على النماذج الأساسية العصبية البحتة مع القضاء على اختناقات النمذجة اليدوية للأنظمة الحرجة للسلامة.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تحاول تعليم روبوت كيفية قيادة سيارة أو تصفح موقع إلكتروني. للقيام بذلك بأمان، تحتاج إلى خريطة لكل حركة ممكنة يمكن للروبوت القيام بها. في عالم اختبار البرمجيات، تُسمى هذه الخريطة "نموذج الاستخدام" (usage model). إنها تشبه المخطط الانسيابي الذي يوضح كل حالة يمكن أن يكون النظام فيها (مثل "الضغط على المكابح" أو "سلة التسوق ممتلئة") واحتمالية الانتقال من حالة إلى أخرى (مثل "احتمال 80% أن ينقر المستخدم على 'شراء'").
لعقود من الزمن، استخدم الخبراء هذه الخرائط لتشغيل "اختبارات إحصائية". فبدلاً من مجرد التحقق مما إذا كان الكود يعمل لمرة واحدة، يستخدمون الخريطة لمحاكاة آلاف الرحلات العشوائية عبر النظام. وإذا كانت الخريطة دقيقة، فستجد الاختبارات الأخطاء البرمجية المخفية التي لا تظهر إلا في المواقف النادرة والمعقدة. ومع ذلك، هناك مشكلة كبيرة: رسم هذه الخرائط يدوياً هو أمر بطيء، ممل، وعرضة للخطأ البشري. الأمر يشبه محاولة رسم خريطة مفصلة لمدينة كاملة وأنت معصوب العينين. مؤخراً، امتلكنا أداة جديدة: الذكاء الاصطناعي (AI) الذي يمكنه قراءة النصوص وتخمين شكل الخريطة الذي ينبغي أن يكون عليه. ولكن هنا تكمن المشكلة: الذكاء الاصطناعي بارع في تخمين شكل الخريطة، لكنه سيء جداً في ضبط الأرقام بشكل صحيح. قد يرسم طريقاً غير موجود، أو يقول إن هناك احتمالاً بنسبة 150% لهطول الأمطار (وهو أمر مستحيل). تسأل هذه الورقة البحثية: هل يمكننا دمج إبداع الذكاء الاصطناعي مع "قاعدة قواعد" رياضية صارمة لبناء خريطة مثالية تلقائياً؟
الورقة البحثية، التي تحمل عنوان "الآلة تقترح، والبرهان يحسم" (The Machine Proposes. The Proof Disposes)، تقدم نظاماً جديداً يسمى NeSy-MBST. فكر في الأمر كتعاون بين كاتب مبدع ومعلم رياضيات صارم. "الكاتب" هو نموذج لغوي كبير (LLM)، وهو ذكاء اصطناعي يقرأ المتطلبات باللغة الطبيعية (مثل "يجب أن يتمكن المستخدم من إضافة عناصر إلى السلة") ويقترح مسودة لخريطة النظام. و"معلم الرياضيات" هو برنامج حل رمزي (symbolic solver)، وهو برنامج حاسوبي يتحقق من المسودة مقابل قوانين الرياضيات.
إليك كيف يعمل هذا الفريق معاً:
- الاقتراح: يقرأ الذكاء الاصطناعي المتطلبات ويرسم مخططاً للحالات والانتقالات. إنه سريع ويفهم اللغة البشرية جيداً.
- البرهان: يقوم معلم الرياضيات فوراً بفحص المخطط. هل اخترع الذكاء الاصطناعي انتقالاً مستحيلاً من الناحية الفيزيائية؟ هل نسي خطوة ما؟ يقول المعلم: "لا، هذا الطريق غير موجود"، أو "لقد فاتتك لفة".
- الإصلاح: يتلقى الذكاء الاصطناعي الملاحظات، ويقوم بإصلاح الخريطة، ثم يحاول مرة أخرى.
- الأرقام: بمجرد أن يصبح شكل الخريطة مثالياً، يتولى معلم الرياضيات المهمة لتحديد الاحتمالات. فبدلاً من أن يخمن الذكاء الاصطناعي الأرقام (مما يؤدي غالباً إلى أخطاء)، يستخدم المعلم "محسّناً محدباً" (convex optimizer) لحساب الاحتمالات الدقيقة بحيث تبلغ مجموعها 100% بشكل صحيح وتعكس الاستخدام الواقعي.
اختبر الباحثون هذا النظام في نوعين من التحديات: مركبة ذاتية القيادة (نظام سيارة ذاتية القيادة) وموقعين للتجارة الإلكترونية (صفحة تسوق للمستخدم ولوحة تحكم المسؤول). وقارنوا نظامهم الجديد "المتكامل" مقابل استخدام الذكاء الاصطناعي وحده وضد الطرق التقليدية اليدوية.
كانت النتائج مبهرة. فعند استخدام الذكاء الاصطناعي وحده، فات النظام حوالي نصف المسارات المهمة وارتكب أخطاء في هيكل الخريطة. ولكن مع نظام NeSy-MBST المتكامل، حقق النظام درجة 0.9125 على مقياس يعتبر فيه 0.90 هو عتبة السلامة المطلوبة للأنظمة الحرجة مثل السيارات ذاتية القيادة. وهذا يعني أن الذكاء الاصطناعي وحده لم يكن جيداً بما يكفي، لكن النظام المتكامل اجتاز اختبار السلامة.
على وجه التحديد، تمكن النظام الجديد من تغطية 85.7% من الانتقالات الممكنة (المسارات التي يمكن أن يسلكها النظام)، بينما غطت نسخة الذكاء الاصطناعي المنفردة 50% فقط. هذه زيادة هائلة قدرها 35.7 نقطة مئوية. وباللغة البسيطة، وجد النظام الجديد تنوعاً أكبر بك jauh من الأخطاء البرمجية المحتملة لأنه لم يقع في فخ "النهايات المسدودة" أو "الطرق المستحيلة" التي كان الذكاء الاصطوني وحده يتخيلها.
كما نظرت الورقة البحثية في مدى دقة النظام في ضبط الأرقام. استخدمت مقياساً يسمى "تباعد جينسن-شانون" (Jensen–Shannon divergence) لقياس مدى قرب تخمينات احتمالات الذكاء الاصطناعي من الرياضيات الحقيقية. حقق النظام الجديد درجة 0.012، وهي قريبة جداً من المثالية، بينما كان إصدار الذكاء الاصطناعي المنفرد بعيداً جداً عند 0.157. وهذا يثبت أن معلم الرياضيات قد نجح في إصلاح أخطاء الرياضيات الخاصة بالذكاء الاصطناعي.
أجرى الباحثون تجربة خاصة تسمى "دراسة الاستئصال" (ablation study) لمعرفة أي جزء من الفريق كان يقوم بالعمل الثقيل. ووجدوا أن حلقة التحقق الرمزي (معلم الرياضيات الذي يفحص هيكل الخريطة) كانت السبب الرئيسي في اكتشاف النظام لمزيد من المسارات. أما المحسن المحدب (معلم الرياضيات الذي يقوم بحسابات الاحتمالات) فقد كان السبب الرئيسي في دقة الأرقام. أما التغذية الراجعة في الحلقة المغلقة (حيث يتعلم النظام من إجراء الاختبارات) فقد ساعدت قليلاً، لكن السحر الجوهري كان في التعاون الأولي.
في الختام، تشير هذه الورقة البحثية إلى أنه ليس علينا الاختيار بين سرعة الذكاء الاصطناعي وسلامة الخبراء البشريين. فمن خلال السماي للذكاء الاصطناعي باقتراح الأفكار ولنظام رياضي صارم بالتحقق منها وتصحيحها، يمكننا بناء خرائط اختبار برمجيات سريعة الإنشاء وآمنة بما يكفي للأنظمة الحرجة. ويشير المؤلفون إلى أنه بينما يعمل هذا بشكل جيد جداً للأنظمة التي اختبروها (حتى 42 حالة)، إلا أن هناك حاجة لمزيد من العمل لمعرفة ما إذا كان يمكن توسيع نطاقه ليشمل الأنظمة الصناعية الضخمة والمعقدة. ولكن في الوقت الحالي، فقد أثبتوا أن "الآلة تقترح" هي بداية رائعة، طالما أن "البرهان يحسم" أي أخطاء قبل استخدام الخريطة النهائية.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.