رسالة تخرج حول برمجة القيود
يونيو 2019
نظرة عامة
يزيد المحاكي من فحص العديد من الشروط كلما زادت الأحداث المحتملة. فهل يمكن التوقف عن هذا الفحص بأمان إذا أمكننا الحكم من التقدم المحرز بأن "هذا الشرط لن يتحقق مرة أخرى"؟ صُممت وطبّقت طريقة لإزالة الشروط غير الضرورية من البحث الجاري باستخدام اتجاه تغير القيم كدليل، وذلك من أجل لغة نمذجة الأنظمة الهجينة HydLa.
في نموذج التقييم، تم تقليل وقت التنفيذ إلى نحو نصف الوقت التقليدي دون تغيير نتائج المحاكاة. المهم ليس تسريع جميع الحسابات بشكل متساوٍ، بل استخدام بنية المشكلة لتقليل الاحتمالات نفسها التي يجب أخذها في الاعتبار.
النهج الذي تعلمته في هذا البحث حول برمجة القيود أصبح أساس فلسفة التصميم الخاصة بي الحالي. بدلاً من تحديد كل نتيجة مباشرة، يتم تعريف القواعد والأولوية والحدود، ومن خلال ذلك يتم استنتاج الحلول التي تتحقق داخل هذه الحدود.
المهمة — كلما زادت الإمكانيات، تباطأت الحسابات
HydLa هي لغة لتوصيف "النظم الهجينة" التي تجمع بين التغيرات المستمرة والأحداث المنفصلة باعتبارها قيودًا رياضية ومنطقية. يمكن محاكاة السلوك الذي يفي بالشروط عن طريق إعلان ما يجب أن يتحقق، دون الحاجة لكتابة ترتيب جميع الإجراءات.
من ناحية أخرى، في النماذج التي تحتوي على العديد من القواعد التي تصبح فعالة وفقًا للشروط، يقوم المحاكي بفحص العديد من المرشحين بشكل متكرر. وبما أن المرشحين يبقون حتى للشروط التي قد تجاوزت بالفعل ولن تتحقق في المستقبل، تتراكم الحسابات غير الضرورية كلما كبر النموذج.
الموضوع — نظام يجمع بين التتابع والانفصال
كرة ترتد هي مثال واضح على النظام الهجين. في الهواء، تتغير الموضع والسرعة بشكل مستمر، وعند اللحظة التي تضرب فيها الأرض، يحدث حدث منفصل وهو الارتداد. منظمات الحرارة، السيارات، والروبوتات، رغم اختلاف المقاييس، تمتلك نفس النوعين من التغيرات داخليًا.
للقييم، استخدمنا نموذجًا ترتد فيه الكرة المتحركة أفقيًا على سطح مقسم إلى عدة أقسام. لكل قسم من السطح يوجد قاعدة مشروطة تقول "إذا وصلت الكرة إلى هذا النطاق فسترتد". كلما زاد عدد الأقسام، يزداد ما يمكن التعبير عنه، وفي المقابل يزداد عدد الشروط التي يجب على المحاكي فحصها.
الاختناق — عدد الشروط يرفع العبء الحسابي
يُطلق على القاعدة التي تصبح صالحة فقط عند تحقق شرط معين اسم 'قيد محروس'. في نموذج التقييم، تصبح قاعدة الارتداد في القسم معينة صالحة فقط عندما يصل الكرة إلى الأرض ويكون موقعها الأفقي داخل هذا القسم.
عند زيادة عدد الأقسام من 10 إلى 200، أصبح المحاكي التقليدي أبطأ تقريبًا بمقدار يتناسب مع مربع عدد الأقسام. في النماذج الكبيرة، يصبح نفس المشكلة أكبر بسبب زيادة الأجسام، ومناطق الاتصال، والأحداث المحتملة.
التحقيق — أين كانت 96٪ من وقت المعالجة
عند قياس وقت المعالجة، في النموذج ذو 100 قسم، كان 96% من الوقت الكلي يُستخدم في FindMinTime. هذا هو العملية التي تبحث عن "أقرب حدث سيحدث بعد ذلك" من بين الخيارات. لذلك، كانت كل شروط الحماية تُقيّم بشكل متكرر.
تم توضيح الأماكن التي يجب تحسينها. ليس من الضروري إعادة إنشاء طريقة الحساب بأكملها، بل يكفي تقليل المرشحين الذين يُمررون إلى FindMinTime بأمان. كان الهدف هو إزالة الاحتمالات التي لا تحتاج إلى الفحص، دون تغيير نتائج المحاكاة.
النهج — إزالة الشروط التي لن تتحقق مرة أخرى بأمان
أريدك أن تتخيل كرة تتدحرج أسفل الدرج وهي تقفز على الدرجات. إذا تجاوزت الكرة درجة معينة واستمرت في التقدم، فلن تؤثر تلك الدرجة على الكرة بعد الآن. الشخص الذي ينظر إلى الرسم يتجاهل على الفور الدرجات الموجودة خلف الكرة. الخوارزمية الأصلية كانت تواصل فحص كل واحدة منها.
الصعب هو الجانب الذي يوضح أن الحماية التي أُزيلت لاحقًا لن تكون ضرورية. إذا تمت الإزالة فقط لأنها كانت زائفة في الوقت الحالي، فقد تُعيد نتيجة خاطئة بصمت عندما تصبح صحيحة مرة أخرى. لذلك، تستخدم الطريقة المقترحة خاصية التوحيد — أي ما إذا كان يمكن ضمان أن متغيرًا ما سيستمر في الزيادة أو النقصان على مدى فترة زمنية معينة.
في حال عدم تغير اتجاه التغير
التعامل الأول ينطبق عندما تتحرك المتغيرات في اتجاه واحد طوال فترة المحاكاة. في النموذج الذي تم تقسيم السطح فيه، يزداد الموضع الأفقي للكرة دائمًا. بمجرد تجاوز قسم معين، لن يتم استيفاء شروط هذا القسم مرة أخرى. يمكن التحقق من هذه الخاصية قبل المحاكاة باستخدام تقنيات فحص النماذج، لذا يمكن إزالة الحراسة غير الضرورية بأمان مع تقدم التنفيذ.
في حال تغير اتجاه التغير في المنتصف
العديد من الأنظمة الواقعية لا تتحرك في اتجاه واحد إلى الأبد. يمكن للمتغيرات أن تزداد، وتغير الاتجاه، ثم تنقص. لذلك أظهرت الورقة البحثية الاستجابة الثانية. أولاً يتم افتراض الاتجاه، ومراقبة هذا الافتراض باستخدام التأكيدات، وإعادة معالجة التقليل عند تغير الاتجاه. الحرس الذي أُزيل من أجل فترة أحادية واحدة يُستعاد عند بدء الفترة التالية.
النتيجة — تقليل زمن تنفيذ نموذج التقييم إلى حوالي النصف
تم تنفيذ التعامل مع التوحّد والاتساق الأحادي وتم تقييمه على نموذج مقسم إلى واجهات. كل من الخوارزمية الأصلية والطريقة المقترحة، مع زيادة عدد الأقسام، يزداد الوقت المستغرق. ومع ذلك، كانت الطريقة المقترحة دائمًا أقل في عبء العمل. عند مقارنة المنحنيات المطبقة، انخفض معامل الدرجة الأعلى من 1.1463 إلى 0.6083، وفي هذا الاختبار، أصبح الوقت الإجمالي للمحاكاة تقريبًا نصفه.
هذا لا يعني أن جميع نماذج HydLa ستصبح أسرع بمرتين. ما يُظهره هو الأماكن التي تكون فيها هذه الطريقة فعّالة — النماذج التي تحتوي على العديد من الحراس، والتي يمكن إثبات اتجاه التغيير فيها، والتي يصبح الحارس فيها غير ذي صلة بشكل دائم أثناء التنفيذ.
وجهة النظر التي تم الحصول عليها من هذا البحث
ما قمنا به في هذا البحث لم يكن تسريع الحسابات الفردية خطوة بخطوة. بل كان استخدام ما نعرفه عن سلوك النظام لتقليص مجموعة الاحتمالات التي يجب أخذها بعين الاعتبار. فكرة تضييق فضاء البحث دون تغيير النتائج هي قوة البرمجة القائمة على القيود.
ما تم تنفيذه وتقييمه هو الحالة التي تستمر فيها المتغيرات في التحرك في اتجاه واحد. أما في حالة تغير اتجاه التغير في منتصف الطريق، فتم الاكتفاء بالتصميم، وبقي التقييم كموضوع للتحدي المستقبلي. هناك مجال لاستخدام خصائص أخرى غير التوحيدية واكتشاف قيود غير ضرورية بشكل أكبر.
إن سبب محاولتي حالياً تصميم الشروط والحدود التي يمكن للذكاء الاصطناعي استكشافها بدلاً من تصميم مخرجاته مباشرة، يعود إلى هذه التجربة. عند التعامل مع نتائج معقدة، من المهم بنفس قدر أهمية تحديد ما يجب حسابه، تحديد ما لا يحتاج إلى التفكير فيه.
Takafumi Horiuchi, Kazunori Ueda, “Dynamic Reduction of Guarded Constraints for the Hybrid Systems Modeling Language HydLa,” 2019 Annual Conference of the Japanese Society for Artificial Intelligence (33rd), 2019. DOI: 10.11517/pjsai.JSAI2019.0_1E3OS3b02