ملخص تقني: تركيب والتحقق من برامج المحولات (Transformers)

بيان المشكلة

تُعد المحولات (Transformers)، وهي البنية التأسيسية للنماذج اللغوية الكبيرة (LLMs)، صعبة التحليل رسميًا بشكل ملحوظ. فبينما هي تعبيرية وقابلة للتوازي، فإن التحقق من خصائصها أمر غير قابل للتقرير (undecidable)، كما أن توسيعها باستخدام "سلسلة الأفكار" (Chain of Thoughts) يجعلها كاملة تورينج (Turing-complete). ولمعالجة ذلك، طور الباحثون لغات إعلانية مثل RASP (لغة معالجة التسلسل ذات الوصول المقيد) ومتغيرها C-RASP (Counting RASP) لالتقاط سلوك المحولات بدلالات دقيقة.

ومع ذلك، ورغم العلاقة النظرية بين C-RASP والمحولات، لا تزال هناك فجوتان حرجتان:

1. التحقق (Verification): لا توجد طريقة تلقائية للتحقق من برامج C-RASP. إن التحقق مما إذا كان C-RASP يتعرف على لغة تافهة هو أمر غير قابل للتقرير في الحالة العامة، ولا توجد أداة عملية لتحليل خصائص مثل تكافؤ اللغات أو الاحتواء.
2. التركيب (Synthesis): لا توجد طريقة معروفة لتعلم أو تركيب برنامج C-RASP تلقائيًا من الأمثلة. تعتمد النهج الحالية على تدريب الشبكات العصبية واستخراج القواعد، والتي غالبًا ما تفشل في إنتاج ترجمات قابلة للتنفيذ أو تتطلب افتراضات مثالية.

تعالج هذه الورقة هذه التحديات من خلال تطوير أول تقنيات تلقائية لكل من التحقق من برامج C-RASP وتركيبها.

المنهجية

1. التحقق عبر الاختزال إلى Lustre

يؤسس المؤلفون علاقة رسمية بين C-RASP ولغة Lustre، وهي لغة تدفق بيانات متزامنة تُستخدم في الأنظمة المدمجة.

• الترجمة: يتم ترجمة برنامج C-RASP إلى عقدة Lustre. تقوم الترجمة بربط قواعد C-RASP بمتغيرات Lustre (تدفقات بولية وصحيحة).
  • عوامل العد (Counting Operators): يتم محاكاة عامل العد في C-RASP وهو #φ (عد المواقع التي تتحقق فيها φ) في Lustre باستخدام متغيرات صحيحة مساعدة تراكم القيم عبر تدفق لانهائي.
  • المحدود مقابل اللانهائي: بما أن C-RASP يعمل على كلمات محدودة وLustre على تدفقات لانهائية، يتم ترميز المدخلات كتدفق لانهائي مع علامة نهاية التدفق (#) وعلامة الأبدية (Ω).
• التحقق من النموذج (Model Checking): بمجرد الترجمة، يتم التحقق من الخصائص مثل تكافؤ اللغة، والاحتواء، والفراغ باستخدام أدوات التحقق من النموذج الحديثة (تحديدًا Kind2) مقترنة بمحللات SMT محسنة (CVC5, Z3).
• التعقيد: الترجمة ذات حجم متعدد الحدود، بشرما تم ترميز معاملات النطاق في المعامل #rs,re بصيغة الوحدة (unary).

2. التركيب عبر التلدين المحاكي (Simulated Annealing)

تقترح الورقة خوارزمية بحث محلي تعتمد على التلدين المحاكي لتركيب برامج C-RASP من أمثلة موجبة وسالبة.

• فضاء الحالة: يتم تقييد البحث ضمن "شكل برنامج" ثابت يتم تحديده بعدد القواعد البولية ($N_b$)، وقواعد العد ($N_c$)، وحد للثوابت الرقمية ($K$).
• عوامل الطفرة (Mutation Operators): تستكشف الخوارزمية فضاء الحالة عن طريق تطبيق طفرات تركيبية على البرنامج الحالي. وتشمل هذه:
  • إعادة أخذ العينات (Resampling): استبدال الجانب الأيمن من القاعدة بالكامل.
  • الطفرات الدقيقة (Micro-mutations): تغييرات محلية مثل تبديل الروابط المنطقية، أو عكس النفي، أو قلب صرامة المقارنة.
  • القيود: تُقيد الطفرات في أجزاء تركيبية ضحلة (على سبيل المثال، العمق-2 لتعبيرات العد) لتوجيه البحث نحو نماذج بسيطة وقابلة للتفسير.
• دالة الهدف: تعطي دالة التقييم $E(P)$ الأولوية لتقليل التصنيفات الخاطئة ($\lambda_{mis}$)، يليه معاقبة القواعد غير القابلة للوصول ($\lambda_U$) ثم الحجم الإجمالي لشجرة الإعراب المجردة ($\lambda_S$).
• ديناميكيات التلدين: تقبل الخوارزمية الحلول الأسوأ باحتمالية تعتمد على جدول درجة حرارة التبريد، مما يسمي لها الهروب من النهايات العظمى المحلية.

3. التطبيقات المتكاملة

يدمج المؤلفون هذين المكونين في إطار موحد يدعم تطبيقين:

1. تقليص برنامج المحول (Transformer Program Minimization): بالنظر إلى برنامج C-RASP، يقوم النظام بتركيب برنامج أصغر هيكليًا ومكافئ له؛ حيث يتنقل بين البحث المحلي والتحقق من التكافؤ، حيث توجه الأمثلة المضادة من المتحقق عملية البحث.
2. التعلم المقيد (Constrained Learning): بالنظر إلى مواصفات جزئية (برنامج $P_{spec}$) وأمثلة مصنفة، يقوم النظام بتركيب برنامج يتناسب مع الأمثلة ويكون متضمنًا في لغة $P_{spec}$ ($L(P) \subseteq L(P_{spec})$).

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

1. أول طريقة تحقق تلقائية: تقدم الورقة أول تقنية للتحقق تلقائيًا من برامج C-RASP عن طريق اختزالها إلى Lustre واستخدام التحقق من النموذج. وهذا يتيح التحقق من تكافؤ اللغة، والاحتواء، والفراغ.
2. أول طريقة تركيب تلقائية: يقدم المؤلفون خوارزمية بحث محلي (التلدين المحاكي) قادرة على تركيب برامج C-RASP مباشرة من الأمثلة، متجاوزة الحاجة إلى التدريب الوسيط للشبكات العصبية.
3. التنفيذ والقياس المرجعي: تم تنفيذ سلسلة أدوات Scala موحدة وتقييمها مقابل مجموعة من الاختبارات المرجعية من الأدبيات، بما في ذلك اللغات المنتظمة، والقائمة على العد، واللغات ذات النمط السياقي الحر.

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

قيم المؤلفون أداتهم مقابل مجموعة اختبار مرجعية تشمل لغات مثل Dyck-1، وMajority، ومختلف أوتوماتا Tomita.

• الكفاءة: نجحت الأداة في تركيب برامج C-RASP صحيحة لمعظم الاختبارات المرجعية ضمن مهلة زمنية قدرها 300 ثانية. على سبيل المثال، استغرق تركيب برنامج لـ Dyck-1 حوالي 3.92 ثانية، بينما استغرق AnBnCn حوالي 80.05 ثانية.
• الدقة: حقق التركيب دقة عالية في التدريب والتقييم (غالبًا 100%) في اللغات التي تقع ضمن القدرة التعبيرية لـ C-RASP.
• المقارنة بالمحولات: تشير الورقة إلى أنه بالنسبة لبعض الاختبارات المرجعية، قد يستغرق تدريب محول (مثل GPT-2 عبر HuggingFace) لتحقيق اللغة الصحيحة عدة ساعات، بينما أكملت أداة تركيب C-RASP المهمة في ثوانٍ.
• القيود: كما هو متوقع من نظرية القدرة التعبيرية، لم يكن من الممكن تعلم اللغات التي تتجاوز قدرة C-RASP (مثل Parity، وTomita 3، وTomita 5) بدقة عالية، حيث ظلت أفضل دقة تدريب أقل من 80%.

الأهمية والادعاءات

تضع هذه الورقة C-RASP ليس مجرد أداة نظرية لفهم القدرة التعبيرية للمحولات، بل كـ نموذج بديل قابل للتفسير. ومن خلال توفير طرق تلقائية للتحقق والتركيب، يجادل المؤلفون بأن C-RASP يمكن تحليلها باستخدام الأساليب الرسمية (FXAI)، مما يسد الفجوة بين الطبيعة "الصندوق الأسود" للشبكات العصبية والحاجة إلى القابلية للتفسير.

تكمن الأهمية في:

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

يخلص المؤلفون إلى أن عملهم يضع حجر الأساس للتحليل الرسمي للمحولات، مع توجهات مستقبلية تشمل التحقق من المتانة ودمج آليات "سلسلة الأفكار" (CoT).