Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

ملخص تقني: التحقق الدقيق من نماذج المحولات عبر صقل التجريد المحفز بوظيفة ReLU

بيان المشكلة
أصبح التحقق الرسمي من نماذج المحولات (Transformers) أمراً بالغ الأهمية نظراً لنشرها في تطبيقات حرجة تتعلق بالسلامة مثل القيادة الذاتية والرعاية الصحية. ومع ذلك، فإن التحقق من المحولات يعد أكثر صعوبة بكثير من التحقق من الشبكات العصبية التغذوية الأمامية الكلاسيكية (FFNNs) بسبب التعقيد العالي لحسابات الاستدلال الخاصة بها، ولا سيما عمليات الضرب النقطي (dot products) داخل طبقات الانتباه الذاتي (self-attention). تعتمد طرق التحقق الحالية على التفسير التجريدي لبناء تقريبات عليا محدبة لنطاقات المخرجات. ورغم كفاءتها، إلا أن هذه المقاربات تعاني غالباً من "مشكلة الاكتمال": حيث يؤدي التقريب العلوي إلى أخطاء كبيرة، مما يؤدي إلى حدوث إنذارات خاطئة حيث تنتهك المخرجات المقربة خاصية المتانة (robustness) رغم أن المخرجات الفعلية لا تنتهكها. وتحديداً، تستخدم الطرق الرائدة الحالية (مثل Shi et al. [23]) حدوداً مستوية صلبة لعمليات الضرب النقطي تكون سليمة من الناحية النظرية ولكنها غالباً ما تكون غير مثالية، حيث تفشل في حصر شكل "القطع الزائد المكافئ" (hyperbolic paraboloid) الناتج عن ضرب متغيرين بشكل وثيق.

المنهجية
يقترح المؤلفون BuFFeT (صقل المحولات القائم على دمج الحدود - BoUnd Fusing-based reFinEment for Transformers)، وهو إطار عمل جديد للتحقق يحسن الدقة من خلال دمج حدود مستوية متعددة لعمليات الضرب النقطي وتمثيلها باستخدام وظائف ReLU.

1. بناء الحد المزدوج: حددت الورقة أن الحد المستوي القياسي المستخدم في العمل السابق (المعادلة 4) يغطي جانباً واحداً فقط من القطع الزائد المكافئ الذي يمثل الضرب النقطي ($z=xy$). وقد اشتق المؤلفون حداً مستوياً "مزدوجاً" (المعادلة 5) يغطي الجانب المقابل.
2. التمثيل القائم على ReLU: لتجنب التعقيد الأسي لانتشار دوال الـ min/max غير الخطية (والذي سينتج عن مجرد أخذ الحد الأدنى من الحدين المستويين)، يمثل المؤلفون الحد المدمج باستخدام وظائف ReLU. وتحديداً، يتم صياغة الحد العلوي الأكثر إحكاماً بطرح حد ReLU من الحد الأصلي، بينما يتم صياغة الحد السفلي الأكثر إحكاماً بإضافة حد ReLU إلى الحد الأصلي (المعادلتان 8 و9).
3. استراتيجيات صقل التجريد: يكمن الابتكار الجوهري في تحسين التخفيف الخطي لهذه الحدود الخاصة بـ ReLU. يتم تحديد التخفيف الخطي لـ ReLU بواسطة ميل $\alpha \in [0, 1]$. وقد طور المؤلفون استراتيجيتين من عمليات التحقق من شبكات FFNN الكلاسيكية لتحديد $\alpha$ المثلى:
   • r-BuFFeT (القائم على القواعد): يكيف نهجاً استدلالياً من [24] يختار $\alpha$ (إما 0 أو 1) بناءً على نطاق مدخلات ReLU لتقليل مساحة التقريب العلي. وهذا يعني اختيار الحد المستوي الأفضل لحالة معينة.
   • o-BuFFeT (القائم على التحسين): يعامل $\alpha$ كمتغير قرار في مسألة تحسين. حيث يصيغ مهمة التحقق كعملية تقليل لدالة الخسارة (softplus of the negative margin) مع مراعاة القيود الخطية المشتقة من حدود ReLU. وباستخدام الحلول القائمة على التدرج الحديثة (مثل Adam)، يقوم النموذج بتكرار صقل $\alpha$ لإيجاد حل يضمن المتانة، مما يبحث فعلياً في فضاء الحدود الممكنة.

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

• الاستخدام المبتكر لـ ReLU: تقدم الورقة طريقة لتمثيل حدود غير خطية دقيقة لعمليات الضرب النقطي باستخدام وظائف ReLU، مما يسد الفجوة بين التحقق من المحولات والأدبيات الواسعة المتعلقة بتخفيف ReLU في الشبكات العصبية الكلاسيكية.
• التوحيد النظري: أظهر المؤلفون أن الحدود المستوية المستخدمة في النهج الرائد [23] ونظيره المزدوج هي حالات خاصة من تمثيلهم القائم على ReLU (بما يتوافق مع $\alpha=0$ و $\alpha=1$)، مما يفسر سبب كون هذه الاستراتيجيات الثابتة غير مثالية غالباً.
• إطارا عمل جديدان: يوفر اقتراح r-BuFFeT و o-BuFFeT مسارين متميزين للتحقق عالي الكفاءة والدقة، حيث يقدم النهج القائم على التحسين آلية لصقل التقريبات بشكل تكراري حتى يتم إثبات المتانة.

النتائج التجريبية
قيم المؤلفون BuFFeT على 10 نماذج محولات (بما في ذلك بنيات قياسية تتراŸح من 1 إلى 6 طبقات وTinyBERT) مدربة على مجموعات بيانات تحليل المشاعر (SST و Yelp). تضمنت عملية التقييم 1,400 مهمة تحقق مقابل الخط المرجعي الرائد [23].

• الدقة: أظهر كلا نهجي BuFFeT تحسينات كبيرة في الدقة. بالنسبة للنماذج الأكثر عمقاً (مثل $N=6$)، حسن r-BuFFeT أقصى اضطراب يمكن التحقق منه ($\epsilon$) بمقدار يصل إلى 1.8 مرة، بينما حقق o-BuFFeT تحسيناً يصل إلى 3.6 مرة مقارنة بالخط المرجعي. تفوق o-BuFFeT باستمرار على r-BuFFeT، لا سيما في النماذج المعقدة.
• الكفاءة: لم يتسبب r-BuFFeT في عبء زمني طفيف (1.1 إلى 1.7 ضعف الخط المرجعي) بسبب حساب نطاقات مدخلات ReLU. أما o-BuFFeT فقد فرض عبئاً أعلى (33 إلى 96 ضعف الخط المرجعي) بسبب عملية التحسين التكرارية. ومع ذلك، يشير المؤلفون إلى أنه لا يزال بإمكان التحقق من نماذج 6 طبقات وTinyBERT في غضون دقائق، وأن نسبة العبء الإضافي ظلت مستقرة بغض النظر عن عمق النموذج.
• المتانة: في الحالات التي فشل فيها الخط المرجعي في التحقق من المتانة (الهامش السالب)، نجح o-BuFFeT في صقل التقريب لإثبات الخاصية، مما أظهر قدرته على القضاء على الإنذارات الخاطبة.

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