From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications

إليك ملخص تقني مفصل للورقة البحثية بعنوان "من المنفصل إلى المقترن: التحقق من المتانة لكشف النقاط المفتاحية القائم على التعلم باستخدام المواصفات المشتركة."

1. بيان المشكلة

يعد كشف النقاط المفتاحية (Keypoint detection) مهمة حاسمة في الرؤية الحاسوبية تدعم تطبيقات مثل تقدير الوضعية (pose estimation)، وإعادة البناء ثلاثي الأبعاد، والقيادة الذاتية. وبينما تؤدي الشبكات العصبية العميقة (DNNs) الحديثة أداءً جيدًا، إلا أنها عرضة للاضطرابات العدائية وتحولات التوزيع.

التحدي الجوهري:
تعتبر طرق التحقق من المتانة الرسمية الحالية لكشف النقاط المفتاحية منفصلة (decoupled) إلى حد كبير؛ فهي تتحقق من كل نقطة مفتاحية بشكل مستقل، وتتعامل معها كمسائل تصنيف منفصلة. ويؤدي هذا النهج إلى قصورين رئيسيين:

1. التحفظ (Conservatism): يتجاهل الاعتمادات المتبادلة بين النقاط المفتاحية. فقد يكون الانحراف الطفيف في إحدى النقاط مقبولاً إذا قامت النقاط الأخرى بالتعويض عنه، لكن التحقق المستقل غالباً ما يصنف ذلك كفشل.
2. عدم توافق المهام (Task Misalignment): تعتمد المهام اللاحقة (مثل تقدير الوضعية عبر خوارزميات PnP) على التكوين المشترك لجميع النقاط المفتاحية، وليس فقط الإحداثيات الفردية. لذا، تفشل عمليات التحقق المستقلة في التقاط متطلبات السلامة الفعلية لهذه المهام.

تعالج هذه الورقة الحاجة إلى إطار عمل للتحقق من المتانة المقترن (coupled robustness verification framework) الذي يضع حدوداً للانحراف المشترك لجميع النقاط المفتاحية في آن واحد، مما يضمن بقاء النموذج متيناً تحت الاضطرابات التي تحترم القيود الهندسية الجماعية للمهمة.

2. المنهجية

يقترح المؤلفون إطار عمل يصيغ التحقق من المتانة كمسألة إبطال (falsification) باستخدام البرمجة الخطية ذات الأعداد الصحيحة المختلطة (MILP). تدمج هذه الطريقة بين تحليل الوصول (reachability analysis) والترميز متعدد الأوجه (polytope encoding) لقيود الانحراف المشترك.

المكونات الرئيسية:

• البنية (Architecture): تستهدف الطريقة كاشفات النقاط المفتاحية القائمة على الخرائط الحرارية (heatmaps) (على سبيل المثال: العمود الفقري $\to$ توليد الخريطة الحرارية $\to$ استخراج الإحداثيات عبر عملية argmax).
• تمثيل المدخلات: يتم نمذجة الاضطرابات كـ غلاف محدب (convex hull) $\mathcal{X}$ يتكون من صورة بذرية (seed image) و $n$ من الصور المضطربة (لتغطية حالات الحجب المحلي أو تغيرات السطوع/التباين العالمية).
• تحليل الوصول (Reachability Analysis): يتم تقريب مخرجات الشبكة (الخرائط الحرارية) كـ زونوتوب (zonotope) $\mathcal{Z}$. يوفر هذا تمثيلاً محدباً ومدمجاً لجميع مخرجات الخريطة الحرارية الممكنة لمجموعة المدخلات المعطاة.
• المواصفات المقترنة (Coupled Specification): بدلاً من فحص الأخطاء الفردية، تحدد الطريقة متعدد أوجه (polytope) $\delta\mathcal{V} = \{ \delta v \mid P_v \delta v \leq b_v \}$ يمثل متجه الانحراف المشترك المسموح به لجميع النقاط المفتاحية $K$. وهذا يلتقط متطلبات مستوى المهمة (مثل عتبات خطأ الوضعية).

عملية التحقق (الإبطال):

الهدف هو إثبات أن لا يوجد أي خريطة حرارية يمكن الوصول إليها تنتج تكويناً للنقاط المفتاحية خارج متعدد الأوجه المسموح به. يصيغ المؤلفون ذلك كمسألة MILP لإيجاد مثال مضاد (counterexample):

1. قيود مجموعة الوصول: ترميز الزونوتوب $\mathcal{Z}$ باستخدام قيود خطية تتضمن معاملات المولد $\alpha_k \in [-1, 1]$.
2. الفهرسة الديناميكية: بما أن موقع النقطة المفتاحية يتحدد عبر عملية argmax للخريطة الحرارية، يجب على الطريقة اختيار قيم البكسلات ديناميكياً بناءً على الإحداثيات المضطربة ($v^* + \delta v$). يتم التعامل مع ذلك باستخدام متغيرات مؤشر ثنائية وقيود Big-M لاستخراج قيم البكسلات الصحيحة من مصفوفة الخريطة الحرارية.
3. التحقق من العظمى (Maximality Check): تتحقق MILP مما إذا كانت قيم البكسلات المستخرجة عند المواقع المضطربة هي بالفعل القيم القصوى في قنواتها الخاصة (للتحقق من عملية argmax).
4. ترميز الانتهاك: تقوم الطريقة بترميز الشرط الذي ينص على أن الانحراف الناتج $\delta v$ يقع خارج متعدد الأوجه المسموح به $\delta\mathcal{V}$.
   • عدم القابلية للحل (Infeasibility): إذا لم تجد MILP أي حل، فهذا يثبت أنه لا توجد خريطة حرارية يمكن الوصول إليها تنتج انحرافاً مشتركاً خارج الحدود. وبذلك يتم اعتماد النموذج كـ متين (robust).
   • القابلية للحل (Feasibility): إذا وجد حل، يتم تحديد مثال مضاد (اضطراب محدد تسبب في الفشل).

التحسين (Optimization):

لتحسين الكفاءة الحسابية، قدم المؤلفون استراتيجية تقليم (pruning strategy)؛ حيث يتم استبعاد الفهارس "داخل الحدود" (مواقع البكسلات) التي لا يمكن أن تكون هي القصوى مقارنة بالمرشحين الآخرين، مما يقلل بشكل كبير من عدد المتغيرات والقيود في MILP.

3. المساهمات الرئيسية

1. أول إطار عمل للتحقق المقترن: تقدم الورقة أول طريقة تحقق رسمية لكاشفات النقاط المفتاحية التي تتحقق من السلوك المشترك بدلاً من النقاط المفتاحية المستقلة، مما يعالج مباشرة قصور الطرق المنفصلة السابقة.
2. صياغة MILP للمخرجات المستمرة: نجحت الطريقة في سد الفجوة بين مخرجات الإحداثيات المستمرة والتحقق المنفصل عبر نمذجة عملية argmax والقيود المشتركة ضمن MILP واحدة.
3. ضمان السلامة (Soundness Guarantee): أثبت المؤلفون أن الطريقة سليمة (sound): إذا كانت MILP غير قابلة للحل، فإن النموذج مضمون رياضياً بأنه متين ضد الاضطرابات المحددة.
4. التعامل مع الاضطرابات الدلالية: يدعم إطار العمل الاضطرابات الدلالية الواقعية (مثل الحجب المحلي للأشياء/المركبات) والتي يتم نمذجتها عبر الأغلفة المحدبة، بدلاً من مجرد ضوضاء مستوى البكسل.

4. النتائج التجريبية

تم تقييم الطريقة في مهمة تقدير وضعية طائرة قائمة على النقاط المفتاحية (7,320 صورة، 23 نقطة مفتاحية) تحت اضطرابات متنوعة:

• الحجب المحلي: رقع عشوائية من الأجسام (متداخلة وغير متداخلة مع الطائرة).
• الاضطرابات العالمية: تغيرات السطوع والتباين.
• النماذج المرجعية (Baselines): تمت المقارنة مع طريقة تحقق منفصلة حديثة (Luo et al., 2025).

النتائج الرئيسية:

• معدلات تحقق متفوقة: حقق النهج المقترن معدلات تحقق أعلى بكثير من النموذج المرجعي المنفصل.
  • تحت عتبات الخطأ الصارمة ($\alpha = 0.1$)، فشل النموذج المرجعي في التحقق من 0% من الصور، بينما حافظت الطريقة المقترحة على معدلات تحقق تتراوح بين 5% و10% (وتصل إلى أكثر من 70%+ للعتبات الأكثر تساهلاً).
  • في حالات الحجب غير المتداخل، حققت الطريقة المقترحة معدلات تحقق قريبة من الحد الأعلى للاختبار التجريبي (مثلاً ~99% مقابل 100% تجريبياً)، بينما انخفض النموذج المرجعي إلى ~47%.
• المتانة تجاه أنواع الاضطرابات: أظهرت الطريقة أداءً ثابتاً عبر حالات الحجب المحلي وتغيرات السطوع والتباين العالمية.
• القابلية للتوسع والكفاءة:
  • قللت استراتيجية التقليم من حجم MILP بعدة مراتب (تصل إلى $10^3$ في حالات عدم التداخل).
  • كان وقت التحقق تنافسياً بشكل عام، رغم أنه يزدادة مع تعقيد الاضطرابات المتداخلة بسبب اتساع مجموعات الوصول.
  • من المثير للاهتمام، بالنسبة للطريقة المقترحة، كان وقت التحقق ينخفض كلما أصبحت عتبات الخطأ أكثر صرامة (أي $\alpha$ أصغر) في حالات عدم التداخل، لأن المشكلة تصبح أسهل في الإثبات كغير قابلة للحل (إيجاد مثال مضاد يصبح أصعب).

5. الأهمية والخاتمة

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

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

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