ملخص تقني: BEAVER – مُتحقق من النماذج اللغوية الكبيرة (LLM) يتميز بالكفاءة والحتمية

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

مع انتقال النماذج اللغوية الكبيرة (LLMs) من النماذج الأولية البحثية إلى أنظمة الإنتاج، يواجه الممارسون تحديًا حرجًا يتمثل في توصيف "مخاطر الذيل" (tail risk)—وهي حالات الفشل النادرة ولكن عالية التأثير مثل تسريب المعلومات الخاصة، أو توليد كود غير آمن، أو إنتاج محتوى سام. تعتمد ممارسات النشر الحالية بشكل شبه حصري على طرق تجريبية عشوائية، بما في ذلك الاختبارات المعيارية، واختبارات التحدي (red-teaming)، والتقديرات القائمة على أخذ العينات. وبينما توفر هذه الطرق حدسًا، إلا أنها لا تقدم أي ضمانات متينة فيما يتعلق بسلوك النموذج.

تكمن الصعوبة الجوهرية في التحقق من النماذج اللغبية الكبيرة في طبيعتها كنماذج ذاتية الانحدار (auto-regressive) تستحث توزيعًا احتماليًا على تسلسلات المخرجات بدلاً من إنتاج مخرج حتمي واحد. تستهدف أدوات التحقق من الشبكات العصبية الحالية العلاقات الحتمية بين المدخلات والمخرجات، ولا يمكنها التعامل مع مزيج الاختيار الاحتمالي، والتوسيع المتسلسل (sequential unrolling)، ومنطق فك الترميز (decoding logic) الخاص بالتوليد ذاتي الانحدار. وبناءً على ذلك، اعتُبر التحقق السليم من النماذج اللغبية الكبيرة أمرًا غير ممكن بسبب حجم النماذج والنمو الأسي لفضاء المخرجات.

2. المنهجية

تقدم ورقة BEAVER أول إطار عمل عملي لحساب حدود احتمالية حتمية ومتينة لمدى استيفاء النماذج اللغبية الكبيرة لخصائص السلامة. يستند هذا النهج إلى ملاحظة أن العديد من خصائص السلامة تتبع صيغة المنطق الزمني الخطي (LTL) وهي $G\phi$ (التي تؤكد أن "لا شيء سيئ يحدث أبدًا"). وبالنسبة لهذه الخصائص، يمكن اكتشاف الانتهاكات مبكرًا، مما يسمح بتقليص مساحة التوليد بشكل هجومي.

هياكل البيانات الأساسية

يستخدم BEAVER هيكلين جديدين من البيانات لاستكشاف فضاء المخرجات بشكل منهجي:

1. شجرة الرموز (Token Trie - $T$): شجرة بادئة تتتبع جميع التسلسلات المستكشفة التي تستوفي قيد السلامة $\Phi$. يمثل كل عقدة تسلسل رموز $s$ مع احتماليته المرتبطة $\mu(s)$. تخزن الشجرة فقط التسلسلات التي تستوفي خاصية الإغلاق البادئي (prefix-closed property) لـ $\Phi$.
2. الجبهة (Frontier - $\Psi$): مجموعة من العقد الورقية في شجرة الرموز، مقسمة إلى:
   • $\Psi_c$: التسلسلات الكاملة (التي تنتهي بـ ").
   • $\Psi_i$: التسلسلات غير المكتملة المؤهلة للتوسع.

الخوارزمية: التقسيم والتقييد (Branch-and-Bound)

يستخدم BEAVER خوارزمية التقسيم والتقييد لتضييق حدود الاحتمالية $[P_{LB}, P_{UB}]$ بشكل تكراري للاحتمالية $P$ التي يستوفي فيها الرد الخاصية $\Phi$:

• التهيئة: تبدأ الشجرة بالجذر (التسلسل الفارغ). $P_{LB} = 0$ و $P_{UB} = 1$.
• الاختيار: يتم اختيار عقدة غير مكتملة $n[x]$ من الجبهة (عادةً باستخدام استدلال Max-$\mu$ الجشع لإعطاء الأولوية للتسلسلات ذات الاحتمالية العالية).
• التوسع: يتم استعلام النموذج عن احتمالات الرمز التالي $P_M(\cdot | p \cdot x)$. تُضاف التكملات الصالحة $x \cdot t$ التي تستوفي $\Phi$ إلى الشجرة.
• التحديث: يتم إعادة حساب الحدود:
  • $P_{LB}$ هو مجموع احتمالات جميع التسلسلات الكاملة والمستوفية للشروط في $\Psi_c$.
  • $P_{UB}$ هو مجموع احتمالات جميع التسلسلات في $\Psi_i \cup \Psi_c$، بالإضافة إلى مراكم الكتلة المقتطعة ($M_p$).
• المتانة (Soundness): إذا تم اقتطاع الرموز أو التسلسلات ذات الاحتمالية المنخفضة (على سبيل المثال، عبر مرشحات top-$p$ أو top-$k$) لضمان القابلية للتوسع، فإن كتلتها الاحتمالية التراكمية تُضاف إلى $M_p$. يضمن ذلك بقاء $P_{UB}$ حدًا علويًا صالحًا ($P_{LB} \le P \le P_{UB}$) في كل تكرار، بغض النظر عن الاقتطاع.

تتوقف الخوارزمية عندما يتم الوصول إلى الحد الأقصى لميزانية التمريرات الأمامية أو عندما ينخفض الفارق $P_{UB} - P_{LB}$ عن حد التسامح $\epsilon$.

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

1. الصياغة الرسمية: صاغ المؤلفون تقييم مخاطر الذيل للنماذج اللغبية الكبيرة كمسألة تحقق، حيث يحسبون حدود الاحتمالية لخصائص السلامة من النوع $G\phi$. وقد قدموا هيكلي بيانات "شجرة الرموز" و"الجبهة" لتمكين حساب الحدود المتينة.
2. خوارزمية BEAVER: خوارزمية تحقق جديدة تعتمد على التقسيم والتقييد مع براهين متانة رسمية. وهي تنتج فترات احتمالية صالحة في كل تكرار تتقارب نحو الاحتمالية الحقيقية.
3. التحقق التجريبي: تم تقييم إطار العمل على 12 نموذجًا مفتوح الأوزان وموجهًا بالتعليمات (من عائلات Llama، وQwen، وGemma، وPhi، وOLMo، وMistral) وأربعة خصائص سلامة:
   • تسريب الخصوصية (مجموعة بيانات رسائل Enron الإلكترونية).
   • توليد كود غير آمن (CyberSecEval).
   • تحيز الصور النمطية (DecodingTrust).
   • السمية (RealToxicityPrompts).

4. النتائج

أظهر التقييم أن BEAVER يتفوق بشكل كبير على النماذج المرجعية القائمة على أخذ العينات (sampling-based baselines) من حيث الكفاءة وكشف المخاطر:

• كشف المخاطر: يحدد BEAVER حالات أكثر خطورة بمقدار 2.5 إلى 3.3 مرة من المتحقق القائم على أخذ العينات (SV)، حتى عند العمل بـ 1/10 من ميزانية الحوسبة (100 تمريرة أمامية مقابل ~1000 لـ SV).
• إظهار مخاطر الذيل: يثبت BEAVER وجود مخاطر ذيل غير تافهة (احتمالية انتهاك $\ge 10\%$) في عدد كبير من المطالبات (prompts) التي تعتبرها التقييمات التقليدية آمنة.
• الملفات التعريفية المعتمدة على المهمة: كشفت النتائج أن ملفات تعريف المخاطر تعتمد بشدة على المهمة ولا ترتبط بشكل واضح بحجم النموذج. على سبيل المثال، يظهر Qwen3-4B خطرًا عاليًا في الخصوصية وأمن الكود ولكنه آمن في السمية، بينما يظهر Gemma-3-4B النمط العكسي.
• الكفاءة: يتقارب BEAVER إلى حدود ضيقة ($\epsilon=0.01$) في وقت تشغيل معقول (على سبيل المثال، 9.4 ثانية لـ Enron، و18.8 ثانية لـ Secure Code) مع بصمة ذاكرة أقل من 5 ميجابايت لكل حالة.
• الشهادة التوزيعية: توضح الورقة أن الضمانات لكل مطالبة يمكن دمجها مع التقنيات الإحصائية (Clopper-Pearson) لتوفير ضمانات سلامة توزيعية عبر مساحات مدخلات كبيرة، وهي قدرة لا توفرها طرق التقييم الحالية.

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

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

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

القيود: يستهدف الإطار الحالي خصائص السلامة المغلقة بالبادئة ($G\phi$)، رغم أنه يقبل التوسع لخصائص غير مغلقة بالبادئة. كما يعتمد على الوصول "أبيض الصندوق" (white-box) لتوزيعات احتمالية الرموز الكاملة ويستخدم استدلالات (Max-$\mu$) للاختيار، وهو ما أشار المؤلفون إلى إمكانية تحسينه باستخدام دالات قيمة متعلمة للمواصفات الأكثر صعوبة.