Learning GR(1) Specifications from Traces

تخيل أنك تحاول تعليم روبوت كيف يتصرف، لكن لا يمكنك كتابة القواعد لأنك لا تعرف ما هي. بدلاً من ذلك، لديك كاميرا فيديو تسجل الروبوت. تعرض على الكاميرا مجموعة من المقاطع حيث قام الروبوت بعمل رائع (المسارات "الجيدة") ومجموعة من المقاطع حيث اصطدم أو تصرف بغرابة (المسارات "السيئة"). هدفك هو كتابة كتاب قواعد يفصل تماماً بين المقاطع الجيدة والمقاطع السيئة. هذا هو عالم استخراج المواصفات (specification mining): التنقيب في البيانات للعثور على القوانين الخفية التي تحكم نظاماً ما.

ولكن هناك عقبة. في العالم الحقيقي، الأنظمة مثل السيارات ذاتية القيادة أو روبوتات المصانع لا تتبع القواعد فحسب؛ بل تتفاعل مع بيئتها. إذا فعلت البيئة (مثل طريق ممطر أو إنسان يضغط على زر) شيئاً ما، يجب على النظام أن يستجيب. يُسمى هذا نظاماً تفاعلياً (reactive system). ولجعل هذه الأنظمة آمنة، يستخدم علماء الكمبيوتر نوعاً خاصاً من المنطق يسمى GR(1). فكر في GR(1) كعقد صارم: "إذا وعدت البيئة بالتصرف بشكل جيد (الافتراضات)، فإن النظام يعد بالقيام بمهمته (الضمانات)". إذا ضبطت هذا العقد بشكل صحيح، يمكنك تلقائياً بناء روبوت مضمون رياضياً أنه سيعمل. وإذا أخطأت فيه، فقد يفشل الروبوت، أو الأسوأ من ذلك، قد تقول الرياضيات إن الروبوت مستحيل البناء بينما هو في الواقع يمكن بناؤه.

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

هنا يأتي دور الورقة البحثية. لقد بنى الباحثون، بقيادة سام نيكولاس كوتيلي وفريقه، أداة جديدة تسمى GR1MINE. بدلاً من التخمين العشوائي، تعرف GR1MINE شكل العقد مسبقاً. فهي تعرف الهيكل العظمي لقاعدة GR(1): "إذا فعلت البيئة X، فعلى النظام أن يفعل Y". عليها فقط اكتشاف ما هو X وما هو Y.

وللقيام بذلك، استخدموا حيلة ذكية تتضمن "محلل SAT" (SAT solver)، وهو يشبه حلّال الألغاز فائق السرعة. تخيل أنك تحاول بناء قلعة من قطع الليغو، لكنك لا تعرف أي القطع ستستخدم. بدلاً من بناء قلعة كاملة، واختبارها، ثم هدمها لتجربة غيرها، تقوم GR1MINE ببناء إطار القلعة مرة واحدة. ثم تحاول تجربة تركيبات مختلفة من القطع داخل هذا الإطار. إذا فشلت تركيبة ما، يتذكر المحلل لماذا فشلت ويستخدم تلك الذاكرة لتجاوز آلاف التركيبات السيئة الأخرى فوراً. وهذا ما يسمى "الحل التدريجي" (incremental solving).

اختبر الفريق أداتهم على 120 لغزاً مختلفاً (اختبارات معيارية) مأخوذة من تحديات واقعية في الأجهزة والروبوتات. كانت النتائج مذهلة. عندما كانت الألغاز مكونة من قواعد GR(1) قياسية، حلت GR1MINE جميع الـ 60 منها. وفي المقابل، لم تحل أفضل الأدوات السابقة سوى نصفها أو ثلثها تقريباً. والأكثر إثارة للإعجاب هو أن GR1MINE كانت أسرع بأكثر من 30 مرة من الأدوات العامة في هذه الألغاز المحددة.

لكن السحر الحقيقي حدث عندما اختبروها على ألغاز لم تكن قواعد GR(1) مثالية. حتى عندما كانت القواعد الأصلية فوضوية ولم تتناسب مع النموذج المنظم، نجحت GR1MINE في إيجاد قاعدة عاملة وقابلة للتحقيق لـ 38 من أصل 60 حالة فوضوية. أما الأدوات الأخرى فقد عانت، ووجدت القليل جداً من القواعد العاملة، وكانت تلك التي وجدتها غالباً "غير قابلة للتحقيق" (unrealizable)—أي أنها مستحيلة رياضياً لكي يتبعها روبوت.

باختصار، لا تجد GR1MINE مجرد قاعدة تفصل بين الجيد والسيئ؛ بل تجد قاعدة يمكن للروبوت أن يعيش وفقاً لها. من خلال الالتزام بالهيكل المعروف لـ GR(1) واستخدام حيل الذاكرة الذكية لتجنب إعادة العمل، أثبت الفريق أننا نستطيع اكتشاف عقود معقدة وآمنة للروبوتات بشكل أسرع وأكثر موثوقية من ذي قبل. لم يكتفوا بالعثور على إبرة في كومة قش؛ بل صنعوا مغناطيساً يجذب فقط أنواع الإبر الصحيحة.