Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI

إليك ملخص تقني مفصل لورقة البحث بعنوان: "عدّ عوالم دلالات الزمن المتشعب لتخفيف التحيز البعدي في الذكاء الاصطناعي التوليدي."

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

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

تواجه الطرق الحالية صعوبة في الإجابة على ثلاثة أسئلة حاسمة بشكل ديناميكي أثناء عملية التوليد:

1. التحقق (Verification): هل سلسلة المخرجات الحالية لا تزال ضمن توزيع احتمالي مقصود وعادل؟
2. التنبؤ (Prediction): ما هي احتمالية بقاء السلسلة ضمن الحدود المقبولة مع توليد مخرجات جديدة؟
3. التدخل (Intervention): إذا انحرف التوزيع، فما هو عدد المخرجات التي يجب إزالتها (التخفيف البعدي) لاستعادة العدالة؟

يرى المؤلفون أن مناهج المنطق الزمني الخطي (مثل LTLF) غير كافية للتفكير في الاحتمالات المتشعبة للمخرجات المستقبلية والأعداد المحددة المطلوبة للحفاظ على العدالة.

2. المنهجية: منطق CTLF ودلالات عدّ العوالم

يقترح المؤلفون CTLF (المنطق الزمني للعدّ من أجل العدالة)، وهو منطق زمن متشعب مصمم للتفكير في سلاسل مخرجات الذكاء الاصطناعي التوليدي. الابتكار الجوهري هو دلالات عدّ العوالم (Counting Worlds Semantics) حيث يتم نمذجة عملية التوليد كشجرة من العوالم الممكنة.

أ. هيكل النموذج

يتم صياغة عملية التوليد كنموذج $M = (W, W^1, W^n, R_e, R_f, V)$:

• العوالم ($W$): يمثل كل عالم مخرجاً ممكناً في خطوة محددة من تسلسل التوليد.
• التشعب (Branching): الهيكل عبارة عن شجرة حيث:
  • $R_e$ (علاقة الطفولة): علاقة خلفية تربط الحالة الحالية بوالدها الفريد (المخرج السابق).
  • $R_f$ (علاقة الأبوة): علاقة أمامية تربط الحالة بجميع النتائج المستقبلية الممكنة (الأبناء).
• المسارات (Paths): يمثل المسار الكامل تسلسلاً كاملاً من $n$ من المخرجات.
• التوزيع الاحتمالي ($\Phi_\Sigma$): دالة تقوم بتصفية مجموعة جميع المسارات الممكنة ($\Pi^*$) لتشمل فقط تلك التي تستوفي توزيعاً احتمالياً مستهدفاً $\Sigma$ (على سبيل المثال، 50% ذكر / 50% أنثى).

ب. بناء المنطق (Syntax)

يوسع CTLF المنطق الجهوي القياسي بإضافة معاملات عدّ مرتبطة بمعامل احتمالي $q \in [0, 1]$:

• صيغ الحالة ($\phi$):
  • $\square_q \phi$: في الحالة الحالية، حدثت $\phi$ على الأقل $q \times m$ من المرات في التاريخ (حيث $m$ هو عدد الخطوات الحالي).
  • $\blacksquare_q \phi$: من الممكن أن تكون $\phi$ قد حدثت $q \times m$ من المرات في بعض المسارات الصالحة المتوافقة مع التوزيع المستهدف.
  • $\bigcirc_q \phi$: يوجد مسار كامل حيث تحدث $\phi$ عدد $q \times n$ من المرات.
  • $\triangleright_q \phi$: احتمال حدوث $\phi$ في الخطوة التالية، بالنظر إلى توزيع صالح، هو $q$ على الأقل.
• صيغ المسار ($\psi$):
  • $\bigtriangledown_q \phi$: في مسار كامل، تحدث $\phi$ على الأقل $q \times n$ من المرات.
  • $\dagger_q \phi$: بدءاً من الحالة الحالية، احتمال إكمال المسار مع استيفاء التوزيع المستهدف هو $q$ على الأقل.

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

1. إطار عمل رسمي للتحيز: تقدم الورقة أول إطار منطقي رسمي مصمم خصيصاً للتحقق من التحيز وتخفيفه في سلاسل المخرجات التوليدية باستخدام دلالات الزمن المتشعب.
2. دلالات عدّ العوالم: على عكس التحقق من النماذج الاحتمالية القياسي، يقوم CTLF صراحةً بعدّ حالات السمات المحمية (مثل الجنس) عبر شجرة العوالم الممكنة لتحديد ما إذا كانت هناك مجموعة فرعية "عادلة" موجودة.
3. استراتيجية التخفيف البعدي: يوفر المنطق آلية لحساب العدد الدقيق للمخرات التي يجب إزالتها لاستعادة العدالة. إذا انحرف المسار الحالي بعيداً جداً عن التوزيع المستهدف، يحدد المنطق ما إذا كان من الممكن تحقيق "إكمال عادل"، وإذا لم يكن كذلك، فإنه يحدد الحد الأدنى من المجموعة الفرعية من التاريخ التي تستوفي قيد العدالة.
4. القدرة التنبؤية: تسمح المعاملات $\triangleright$ و $\dagger$ للنظام بالتنبؤ باحتمالية حدوث انتهاكات للعدالة قبل وقوعها، مما يسمال بالتدخل المبكر.

4. النتائج ومثال توضيحي

يستعرض المؤلفون إطار العمل باستخدام "مثال لعبة" لتوليد الصور:

• السيناريو: نموذج مدرب على مجموعة بيانات منحازة (75% ذكر، 25% أنثى) يولد صوراً لطلب (Prompt) "أعطني صورة لمهندس". الهدف هو تحقيق توزيع 50/50.
• التحقق:
  • عند الخطوة 4، إذا كان المخرج 2 ذكر/2 أنثى، فإن الصيغة $w_4 \models \square_{1/2} M \land \square_{1/2} F$ تتحقق، مما يؤكد أن السلسلة الحالية عادلة.
  • يحسب المنطق أن هناك احتمال 50% ($\dagger_{1/2}$) لإمكانية إكمال السلسلة بشكل عادل من هذه النقطة.
• التخفيف:
  • إذا وصلت السلسلة إلى 12 مخرجاً بنسبة 9 ذكور/3 إناث (مما ينتهك هدف 50/50)، يحدد المنطق أن أقصى عدد مسموح به من الإناث في المجموعة الفرعية العادلة هو 3.
  • وبناءً على ذلك، فإن أقصى حجم للمجموعة الفرعية العادلة هو 6 (3 ذكور/3 إناث).
  • يحدد المنطق أن حصة الذكور الحالية قد استُنفدت ($w_5 \models \bigcirc_{1/2} M$).
  • الإجراء: يوصي النظام بإزالة جميع مخرجات الذكور اللاحقة لتشكيل مجموعة فرعية متوازنة $O'$ بحجم 6.

5. الأهمية والعمل المستقبلي

الأهمية:

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

الاتجاهات المستقبلية:

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

في الختام، يقدم CTLF أساساً منطقياً قوياً لضمان التزام أنظمة الذكاء الاصطناعي التوليدي بقيود العدالة طوال عملية التوليد، مما يوفر مساراً واضحاً للتحقق الرسمي وتخفيف التحيز الآلي.