تاكافومي هوريوتشي

رسالة تخرج حول برمجة القيود

نظرة عامة

يزيد المحاكي من فحص العديد من الشروط كلما زادت الأحداث المحتملة. فهل يمكن التوقف عن هذا الفحص بأمان إذا أمكننا الحكم من التقدم المحرز بأن "هذا الشرط لن يتحقق مرة أخرى"؟ صُممت وطبّقت طريقة لإزالة الشروط غير الضرورية من البحث الجاري باستخدام اتجاه تغير القيم كدليل، وذلك من أجل لغة نمذجة الأنظمة الهجينة HydLa.

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

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


المهمة — كلما زادت الإمكانيات، تباطأت الحسابات

HydLa هي لغة لتوصيف "النظم الهجينة" التي تجمع بين التغيرات المستمرة والأحداث المنفصلة باعتبارها قيودًا رياضية ومنطقية. يمكن محاكاة السلوك الذي يفي بالشروط عن طريق إعلان ما يجب أن يتحقق، دون الحاجة لكتابة ترتيب جميع الإجراءات.

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

الموضوع — نظام يجمع بين التتابع والانفصال

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

للقييم، استخدمنا نموذجًا ترتد فيه الكرة المتحركة أفقيًا على سطح مقسم إلى عدة أقسام. لكل قسم من السطح يوجد قاعدة مشروطة تقول "إذا وصلت الكرة إلى هذا النطاق فسترتد". كلما زاد عدد الأقسام، يزداد ما يمكن التعبير عنه، وفي المقابل يزداد عدد الشروط التي يجب على المحاكي فحصها.

رمز مصدر HydLa الذي يعرف سلوك ارتداد الكرة التي تتحرك أفقيًا عند أي من أقسام N من الأسطح المتجاورة.
نموذج HydLa القصير يصف سطحًا مقسمًا إلى كرة واحدة وN قسم محمي.

الاختناق — عدد الشروط يرفع العبء الحسابي

يُطلق على القاعدة التي تصبح صالحة فقط عند تحقق شرط معين اسم 'قيد محروس'. في نموذج التقييم، تصبح قاعدة الارتداد في القسم معينة صالحة فقط عندما يصل الكرة إلى الأرض ويكون موقعها الأفقي داخل هذا القسم.

عند زيادة عدد الأقسام من 10 إلى 200، أصبح المحاكي التقليدي أبطأ تقريبًا بمقدار يتناسب مع مربع عدد الأقسام. في النماذج الكبيرة، يصبح نفس المشكلة أكبر بسبب زيادة الأجسام، ومناطق الاتصال، والأحداث المحتملة.

التحقيق — أين كانت 96٪ من وقت المعالجة

عند قياس وقت المعالجة، في النموذج ذو 100 قسم، كان 96% من الوقت الكلي يُستخدم في FindMinTime. هذا هو العملية التي تبحث عن "أقرب حدث سيحدث بعد ذلك" من بين الخيارات. لذلك، كانت كل شروط الحماية تُقيّم بشكل متكرر.

تم توضيح الأماكن التي يجب تحسينها. ليس من الضروري إعادة إنشاء طريقة الحساب بأكملها، بل يكفي تقليل المرشحين الذين يُمررون إلى FindMinTime بأمان. كان الهدف هو إزالة الاحتمالات التي لا تحتاج إلى الفحص، دون تغيير نتائج المحاكاة.

النهج — إزالة الشروط التي لن تتحقق مرة أخرى بأمان

أريدك أن تتخيل كرة تتدحرج أسفل الدرج وهي تقفز على الدرجات. إذا تجاوزت الكرة درجة معينة واستمرت في التقدم، فلن تؤثر تلك الدرجة على الكرة بعد الآن. الشخص الذي ينظر إلى الرسم يتجاهل على الفور الدرجات الموجودة خلف الكرة. الخوارزمية الأصلية كانت تواصل فحص كل واحدة منها.

تظهر المسارات الحمراء الكرة التي تنزل بينما ترتد على درجات السلم السوداء. المنطقة المظللة تمثل الدرج الذي تم تجاوزه بالفعل ولم يعد ذا صلة.
كلما تحركت الكرة نحو اليمين، يمكن حذف الحماية من المستوي المزخرف الموجود خلفها.

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

في حال عدم تغير اتجاه التغير

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

الخط الأحمر الذي يرتفع من α عند الزمن 0 إلى β عند الزمن الأقصى يمثل متغيرًا يستمر في الزيادة طوال المحاكاة.
الموحدة الأحادية تعني أن اتجاه التغير يُحافظ عليه طوال الفترة التي يتم فيها محاكاة التغير.

في حال تغير اتجاه التغير في المنتصف

العديد من الأنظمة الواقعية لا تتحرك في اتجاه واحد إلى الأبد. يمكن للمتغيرات أن تزداد، وتغير الاتجاه، ثم تنقص. لذلك أظهرت الورقة البحثية الاستجابة الثانية. أولاً يتم افتراض الاتجاه، ومراقبة هذا الافتراض باستخدام التأكيدات، وإعادة معالجة التقليل عند تغير الاتجاه. الحرس الذي أُزيل من أجل فترة أحادية واحدة يُستعاد عند بدء الفترة التالية.

تُظهر الرسوم الخمسة كيفية تأكيد الفترات المتوالية، والتي أفترض فيها زيادة، وفشل التأكيد، وفترة الانخفاض الجديدة، والفشل للمرة الثانية، ثم الفترة الأحادية التزايد.
فشل التأكيد يقسم السلوك المتغير إلى فترات يمكن التعامل معها كلحظات أحادية.

النتيجة — تقليل زمن تنفيذ نموذج التقييم إلى حوالي النصف

تم تنفيذ التعامل مع التوحّد والاتساق الأحادي وتم تقييمه على نموذج مقسم إلى واجهات. كل من الخوارزمية الأصلية والطريقة المقترحة، مع زيادة عدد الأقسام، يزداد الوقت المستغرق. ومع ذلك، كانت الطريقة المقترحة دائمًا أقل في عبء العمل. عند مقارنة المنحنيات المطبقة، انخفض معامل الدرجة الأعلى من 1.1463 إلى 0.6083، وفي هذا الاختبار، أصبح الوقت الإجمالي للمحاكاة تقريبًا نصفه.

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

رسم بياني لزمن المحاكاة مقابل N. في كل نطاق من عدد تقسيمات السطح من 10 إلى 200، الأسلوب المقترح كان أسرع من الأسلوب الأصلي، وعندما N=200، وصل الزمن تقريبًا إلى 250 ثانية مقارنة بحوالي 470 ثانية.
في النموذج الذي تم تقييمه، تستغرق الطريقة المقترحة (المربع) حوالي نصف الوقت مقارنة بالخوارزمية الأصلية (الدائرة).

وجهة النظر التي تم الحصول عليها من هذا البحث

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

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

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

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