فرق دلالي (semantic diff) لسياسات يولّدها LLM: من 18 سطرًا «معدّلًا» يظهر خطآن فقط

تبدأ مراجعة الكود بـ diff. لا أحد يقارن بالعين ملفين من ثلاثة آلاف سطر. ومع السياسات الرسمية يزداد الأمر سوءًا: يُبرز الـ diff النصي بنية لغوية لا تغيّر المعنى. بُدِّل ترتيب شرطين، وعُكست وسائط المساواة، واستُبدل محمول (predicate) بآخر مكافئ، فيبدو نصف الملف معدّلًا. أما الخطأ الحقيقي، مثل Or في موضع يقول فيه المتطلب «و»، فيضيع بسهولة وسط هذه الضوضاء.

تصف مدونة AWS Machine Learning محركًا مفتوح المصدر يحل هذه المشكلة عبر anti-unification. وهي فكرة كلاسيكية لبلوتكين تعود إلى عام 1970: لكل تعبيرين نجد أكثر القوالب المشتركة تحديدًا.

لماذا يلزم ذلك إذا كان LLM هو من يكتب السياسات

السيناريو الرئيسي هنا هو الصياغة الرسمية التلقائية. تأخذ متطلبات بلغة طبيعية وتطلب من النموذج تحويلها إلى SMT-LIB لأجل Z3 أو cvc5، أو إلى سياسات Cedar أو Dogwood، أو إلى قواعد YAML لبيئة OpenShell المعزولة، أو إلى تعبيرات CEL. يكتب النموذج الناتج، لكنه لا يشارك في المقارنة. ولا يوجد مرجع معياري. شغّل النموذج مرتين تحصل على صياغتين مختلفتين، ولا يُعرف أيهما الصحيحة.

يُظهر الـ diff الدلالي أين تتفق النسخ المرشحة وأين تختلف. يمكن توليد مزيد من النسخ بتغيير النموذج أو الـ prompt أو درجة الحرارة. والأجزاء المشتركة تتكرر من تشغيل إلى آخر، ويمكن فحصها بوتيرة أقل. أما ما يتغير فهو ما ينبغي فحصه أولًا.

وهذا قريب من الإنتروبيا الدلالية في عمل Farquhar وزملائه في Nature (2024). هناك تُجمَّع إجابات كثيرة في عناقيد ويُستخرج رقم واحد. أما anti-unification فتحتفظ بمعلومات أكثر: فهي تُظهر البنية المشتركة وكل اختلاف، لا مجرد تقدير.

كيف يعمل ذلك في مثال

يعمل المحرك فوق e-graph، وهي بنية تخزّن تعبيرات معروف مسبقًا أنها متساوية. المساواة تعلنها أنت بنفسك. فتحدد للمعاملين And وOr الترابطية والتبادلية وخاصية idempotence. أما الحقائق الخاصة بالمجال، مثل «external لا يساوي internal»، فتكتبها كقاعدة rewrite. وكل ما عدا ذلك يعدّه المحرك اختلافًا.

تبدو النتيجة كحد (term) واحد. يظهر المشترك مرة واحدة، ويوضع كل اختلاف في عقدة Variants مع النسختين. إذا اخترت الخيار الأول في كل العقد حصلت على السياسة A، وإذا اخترت الثاني فعلى السياسة B. ويتم الدمج دون فقدان.

في المثال المدروس يوجد متطلب للتكرار بين المناطق في S3: تعدد الإصدارات (versioning)، ومنطقة وجهة معتمدة، وللكائنات confidential الحساب نفسه والتشفير بمفتاح العميل، وللكائنات الكبيرة النسخ بطريقة multipart. تختلف الصياغتان في خمسة مواضع. ثلاثة اختلافات شكلية: ترتيب الشروط، وEq معكوس، وapprovedRegion مفصّلة إلى us-east-1 وeu-west-1. واثنان يغيّران المعنى. ففي إحدى النسختين يتطلب شرط كائنات confidential الحساب والتشفير معًا، وفي الأخرى يكفي أحدهما (تحول And إلى Or). وحد حجم الكائن في نسخة Lte وفي الأخرى Lt.

يعلّم unified diff المعتاد 18 سطرًا من 28 ولا يقول أي التغييرات مهم. أما الـ diff الدلالي فيزيل التبديلات ويختزل النتيجة إلى العقد التي ينبغي قراءتها فعلًا. ولهذه الحالات توجد مقياس cr، أي درجة الضغط. الصفر يعني اتفاقًا كاملًا في ظل المساواة المعلنة، والواحد يعني انعدام المشترك تمامًا. في المثال cr يساوي 0.5862 وحجم النتيجة 42.

القيود وما يجب فعله

ثمة عدة تحفظات. لا يستورد المحرك سياسات Cedar أو Dogwood أو OpenShell أو CEL بصيغتها الأصلية. تقوم بترميز البُنى اللازمة كحدود (terms) يدويًا، وتعلن المساواة يدويًا. وإذا لم تكفِ القواعد أو كان البحث غير مكتمل، فقد يتبين أن الاختلاف المتبقي تكافؤ لم يجده المحرك. كذلك لا يثبت انخفاض cr الصحة: فقد يخطئ مرشحان بالطريقة نفسها. وإضافة إلى ذلك، يجري البحث افتراضيًا بطريقة مونت كارلو، وسيُظهر الحقل :completion القيمة budget بدل exact إذا استُنفد الحد قبل استعراض كل الخيارات.

الخلاصة العملية لمن يبني خطوط معالجة «المتطلبات ← سياسة رسمية»: لا تثق بمخرج واحد من النموذج. ولّد عدة نسخ مرشحة، ودمجها عبر الـ diff الدلالي، ثم أعطِ الإنسان أو محلل SMT عقد Variants فقط. يستطيع المحلل إيجاد مثال مضاد، أي إسناد محدد تكون فيه إحدى الصيغتين صحيحة والأخرى خاطئة، ويبيّن anti-unifier أين تبحث. يمكن تجربة ذلك في خمس دقائق: المستودع yaspar-org/semi-persistent، والبناء عبر cargo build --release، والمثال 12-first-au.egg.