Verification of High-Order Control Barrier Functions by Computing Class K Functions

تخيل أنك تقوم ببرمجة أسطول من الطائرات بدون طيار (الدرونز) لتتنقل بسرعة عبر مدينة صاخبة. تريدها أن تكون سريعة وفعالة، ولكن الأهم من ذلك، أنك تحتاج إلى ضمان عدم اصطدامها أبدًا بالمباني، أو بالدرونز الأخرى، أو بالبشر. في عالم الروبوتات والهندسة، هذا هو "الكأس المقدسة" لـ "السلامة". يستخدم العلماء أدوات رياضية تسمى "دوال حاجز التحكم" (Control Barrier Functions - CBFs) لتعمل مثل حقول قوة غير مرئية حول هذه الروبوتات. تخبر هذه الحقول حاسوب الروبوت: "إذا سلكت هذا الطريق، فأنت آمن؛ وإذا سلكت ذاك الطريق، فأنت في ورطة".

ومع ذلك، هناك عقبة صعبة. أحيانًا، تكون فيزياء الروبوت معقدة؛ فقد يستغرق الأمر بضع ثوانٍ حتى يتوقف الروبوت حتى بعد ضغطه على المكابح، أو قد يحتاج إلى الدوران قبل أن يتمكن من التوقف. هنا يأتي دور "دوال حاجز التحكم من الرتب العالية" (High-Order CBFs). إنها تشبه نسخة أكثر تطورًا من حقل القوة الذي يأخذ في الاعتبار هذه التأخيرات والحركات المعقدة. لكن المشكلة تكم-ن في أنه لجعل حقول القوة هذه تعمل، يتعين على المهندسين اختيار منحنيات رياضية محددة، تسمى "دوال الفئة K" (class K functions)، لتحديد مدى صرامة قواعد السلامة. اختيار المنحنى الخاطئ يشبه تحديد حد سرعة إما مرتفع جدًا (فتصطدم) أو منخفض جدًا (فيصبح الروبوت عالقًا). لفترة طويلة، كان على المهندسين التخمين، آملين أن تنجح الأمور، وهي لعبة محفوفة بالمخاطر عندما تكون الأرواح أو المعدات الغالية على المحك.

هذه الورقة البحثية، التي تحمل عنوان "التحقق من دوال حاجز التحكم من الرتب العالية عن طريق حساب دوال الفئة K"، تتصدى للعبة التخمين هذه مباشرة. يقترح المؤلفان، إيلي بوند وماثيو ت. هيل، طريقة جديدة لإثبات أن قواعد سلامة الروبوت ستعمل بالفعل قبل أن يغادر الروبوت المرآب. وبدلاً من تخمين المنحنيات الصحيحة، يستخدمون نوعًا قويًا من الرياضيات يسمى "برمجة مجموع المربعات" (Sum-of-Squares programming) لحساب منحنيات السلامة المثالية تلقائيًا. فكر في الأمر كمهندس معماري رئيسي لا يكتفي برسم المخططات فحسب، بل يقوم بتشغيل ألف محاكاة حاسوبية ليثبت أن المبنى لن ينهار قبل وضع لبنة واحدة.

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

حقول القوة غير المرئية

لفهم سبب أهمية هذا الأمر، دعونا ننظر إلى الأدوات التي تستخدمها الورقة. تخيل روبوتًا مثل سيارة تسير على طريق سريع. قد تكون قاعدة السلامة القياسية هي: "ابقَ في مسارك". في الرياضيات، هذا خط بسيط. ولكن ماذا لو كانت السيارة ثقيلة وتستغرق وقتًا طويلاً للتوقف؟ الخط البسيط ليس كافيًا؛ فأنت بحاجة إلى قاعدة تقول: "إذا كنت قريبًا من الحافة، يجب أن تبطئ الآن حتى لا تنزلق لاحقًا". هذا ما تفعله دالة حاجز التحكم من الرتب العالية (HOCBF). إنها قاعدة سلامة تنظر إلى الأمام، وتأخذ في الاعتبار زخم الروبوت والوقت الذي يحتاجه للاستجابة.

ولكن لجعل قاعدة "النظر إلى الأمام" هذه تعمل، يتعين على المهندس اختيار شكل محدد للقاعدة، وهو ما يعرف بـ دالة الفئة K. تخيل أنك تضبط حساسية إنذار الدخان؛ إذا ضبطته بحساسية عالية جدًا، فسيعمل عند تحميص الخبز (سيتوقف الروبوت دون داعٍ). وإذا ضبطته بحساسية منخفضة جدًا، فلن يعمل حتى يحترق المنزل (سيصطدم الروبوت). لفترة طويلة، كان على المهندسين اختيار "مقابض الحساسية" هذه يدويًا، وغالبًا ما كانوا يلجؤون للتخمين والتجربة. وإذا أخطأوا في التخمين، فقد يعلق الروبوت، أو الأسوأ من ذلك، قد يتوقف الحاسوب عن العمل لأنه لم يجد مسارًا آمنًا.

"الآلة الحاسبة السحرية" للسلامة

أدرك مؤلفو هذه الورقة أنه بدلاً من التخمين، يمكنهم استخدام خدعة رياضية لـ حساب المقابض المثالية. لقد استخدموا طريقة تسمى برمجة مجموع المربعات (SOS programming). يمكنك التفكير في برمجة SOS كآلة حاسبة ذكية للغاية تتحقق مما إذا كان الشكل دائمًا "إيجابيًا" (آمنًا) أو "سلبياً" (غير آمن).

اكتشاف الورقة الرئيسي هو وصفة (خوارزمية) خطوة بخطوة تستخدم هذه الآلة الحاسبة لإيجاد دوال الفئة K الصحيحة لروبوت لديه قواعد سلامة متعددة. إليك كيف يعمل الأمر في قصتهم:

1. المشكلة: كان لديهم روبوت لديه سبع قواعد سلامة مختلفة (HOCBFs) يجب اتباعها في نفس الوقت. وكان لكل قاعدة "مقبض حساسية" مجهول خاص بها (دالة الفئة K) يجب اكتشافه. وهذا يعني 14 دالة مجهولة في المجمل (اثنتان لكل قاعدة من القواعد السبع).
2. الحل: قاموا ببناء تسلسل من المسائل الرياضية. أولاً، حلوا للطبقة الأولى من السلامة، ثم استخدموا تلك النتيجة لحل الطبقة التالية، وهكذا. يشبه الأمر بناء برج من الكتل حيث لا يمكنك وضع الكتلة الثانية حتى تثبت استقرار الكتلة الأولى.
3. النتيجة: نجح الحاسوب في إيجاد القيم لجميع الدوال الـ 14 المجهولة.

اختبار المحاكاة

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

• ثلاث مناطق كانت عبارة عن دوائر غير مرئية يجب على الروبوت تجنبها.
• أربع مناطق كانت تمثل جدران الغرفة التي يجب أن يبقى الروبوت داخلها.

كما أضافوا هدفًا: يحتاج الروبوت للقيادة إلى نقطة معينة والتوقف هناك (وهذا يسمى "دالة ليبونوف للتحكم" أو CLF، وهي تشبه المغناطيس الذي يسحب الروبوت نحو وجهته).

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

ما يعنيه هذا (وما لا يعنيه)

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

ومع ذلك، هناك بعض القيود الهامة التي يجب مراعاتها. تنص الورقة صراحة على أن هذه الطريقة تعمل للأنظمة التي يمكن كتابة رياضياتها كمتعددات حدود (polynomials) (نوع معين من المنحنيات الناعمة). وبينما يمكن تقريب معظم الأنظمة الواقعية بهذه الطريقة، إلا أن هذا مطلب رياضي. أيضًا، النتائج المعروضة هنا هي محاكاة. لقد وجد الروبوت وجوده فقط على شاشة الكمبيوتر. لم يختبر المؤلفون هذا على روبوت مادي في مختبر حقيقي أو في الشارع.

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

في المحاكاة، استغرق الحاسوب حوالي 1,053 ثانية (حوالي 17 دقيقة) للتحقق من السلامة لجميع القواعد السبعة مجتمعة. وهذا يوضح أنه رغم ثقل الرياضيات، إلا أنها قابلة للتنفيذ. وجد المؤلفون أنه مع إضافة المزيد من قواعد السلامة، زاد الوقت المستغرق لحل المشكلة بشكل خطي، وهو مؤشر جيد للروبوتات الأكثر تعقيدًا في المستقبل.

الخلاصة

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