2025-11-21T04:31:15.286585

Lecture Notes on Verifying Graph Neural Networks

Schwarzentruber
In these lecture notes, we first recall the connection between graph neural networks, Weisfeiler-Lehman tests and logics such as first-order logic and graded modal logic. We then present a modal logic in which counting modalities appear in linear inequalities in order to solve verification tasks on graph neural networks. We describe an algorithm for the satisfiability problem of that logic. It is inspired from the tableau method of vanilla modal logic, extended with reasoning in quantifier-free fragment Boolean algebra with Presburger arithmetic.
academic

محاضرات حول التحقق من شبكات الرسوم البيانية العصبية

المعلومات الأساسية

  • معرّف الورقة: 2510.11617
  • العنوان: Lecture Notes on Verifying Graph Neural Networks
  • المؤلف: François Schwarzentruber (ENS de Lyon)
  • التصنيف: cs.LO (المنطق في علوم الحاسوب)، cs.LG (التعلم الآلي)
  • تاريخ النشر: 14 أكتوبر 2025
  • رابط الورقة: https://arxiv.org/abs/2510.11617

الملخص

تستعرض هذه المحاضرات أولاً الروابط بين شبكات الرسوم البيانية العصبية واختبار Weisfeiler-Lehman والأنظمة المنطقية مثل المنطق من الدرجة الأولى والمنطق الموجه المتدرج. ثم تقدم منطقاً موجهاً حيث تظهر الوسائط العددية في عدم المساواة الخطية، لحل مشاكل التحقق من شبكات الرسوم البيانية العصبية. يتم وصف خوارزمية لمشكلة الرضا عن هذا المنطق، مستوحاة من طرق الجداول التقليدية للمنطق الموجه، وتوسع الاستدلال على الأجزاء الخالية من المحددات من الجبر البوليني وحسابات Presburger.

خلفية البحث والدافع

خلفية المشكلة

لقد تم تطبيق شبكات الرسوم البيانية العصبية (GNNs) على نطاق واسع في التوصيات على الشبكات الاجتماعية والرسوم البيانية للمعرفة وتحليل الجزيئات الكيميائية واكتشاف الأدوية. ومع ذلك، تواجه مشاكل التحقق من GNNs تحديات كبيرة:

  1. قيود القدرة التعبيرية: تقتصر القدرة التعبيرية للـ GNNs على اختبار 1-WL (Weisfeiler-Lehman)، وغير قادرة على التمييز بين بعض الرسوم البيانية غير المتشاكلة
  2. تعقيد مهام التحقق: الحاجة إلى التحقق من امتثال GNN لمواصفات محددة، مثل خصائص الأمان والصحة
  3. نقص الأساس النظري: غياب إطار منطقي منهجي لوصف والتحقق من سلوك GNN

دافع البحث

  • الاحتياجات العملية: في التطبيقات الحرجة من حيث السلامة، يجب ضمان موثوقية وصحة GNN
  • الفجوات النظرية: تفتقر طرق التحقق الحالية إلى أساس نظري منطقي موحد
  • التحديات التقنية: الحاجة إلى التعامل مع عمليات التجميع والقيود العددية في GNN

المساهمات الأساسية

  1. إنشاء الروابط النظرية: شرح منهجي للروابط العميقة بين GNNs واختبار Weisfeiler-Lehman والأنظمة المنطقية (FO و FOC و GML)
  2. اقتراح منطق K#: تصميم منطق موجه جديد K# قادر على التعبير عن عمليات العد والتجميع في GNN
  3. تصميم الخوارزمية: تطوير خوارزمية PSPACE لمشكلة الرضا عن منطق K#، بناءً على طرق الجداول واستدلال QFBAPA
  4. تحليل التعقيد: إثبات حدود التعقيد الحسابي لمشاكل التحقق من GNN تحت وظائف تفعيل مختلفة
  5. إطار عملي: توفير إطار عمل شامل لاختزال مهام التحقق من GNN إلى مشاكل الرضا المنطقية

شرح الطريقة

تعريف المهام

تشمل مهام التحقق الأساسية من GNN:

  • الرضا: بالنظر إلى GNN N، هل يوجد مدخل يجعل مخرجاته موجبة؟
  • التحقق من المواصفات: هل يفي GNN بمواصفة منطقية معينة φ؟
  • فحص التكافؤ: هل يكون GNNs متكافئين على جميع المدخلات؟

معمارية منطق K#

تعريف بناء الجملة

φ ::= p | ¬φ | φ ∨ φ | ξ ≥ 0
ξ ::= c | 1φ | #φ | ξ + ξ | c × ξ

تعريف الدلالات

  • 1φ: القيمة 1 إذا كانت φ صحيحة، وإلا 0
  • #φ: حساب عدد العقد اللاحقة التي تحقق φ
  • التعبيرات الخطية: تدعم الجمع والضرب القياسي

الخصائص الرئيسية

  1. القدرة التعبيرية: يحتوي منطق K# على المنطق الموجه المتدرج (GML) كمجموعة فرعية
  2. علاقة المراسلة: يوجد ترجمة ثنائية الاتجاه في الوقت متعدد الحدود مع truncReLU-GNNs
  3. القيود العددية: القدرة على التعبير عن العلاقات العددية المعقدة وعمليات التجميع

علاقة المراسلة بين GNN و K#

من K# إلى GNN

tr(xi = 1) = xi
tr(¬φ) = 1 - truncReLU(tr(φ))
tr(φ ∧ ψ) = truncReLU(tr(φ) + tr(ψ) - 1)
tr(#φ) = agg(tr(φ))

من GNN إلى K#

tr'(truncReLU(ϑ)) = 1tr'(ϑ)≥1
tr'(agg(ϑ)) = #(tr'(ϑ) ≥ 1)

خوارزمية الرضا

أساس QFBAPA

استخدام الجبر البوليني الخالي من المحددات وحسابات Presburger (QFBAPA) للتعامل مع القيود العددية:

  • تقنية مخطط Venn: تحويل تعبيرات المجموعات إلى متغيرات المناطق
  • حد Carathéodory: إثبات أن النظر في عدد متعدد الحدود من المناطق غير الصفرية كافٍ
  • التعقيد NP: مشكلة الرضا عن QFBAPA موجودة في NP

خوارزمية جدول K#

procedure satK#(Γ)
  معالجة القواعد البوليانية وبناء 1φ
  استخراج قيود عدم المساواة الخطية S
  تخمين المناطق غير الصفرية B ⊆ {0,1}d، |B| ≤ 2d log₂(4d)
  استبدال #ψᵢ بـ ∑ρ∈B|ρᵢ=1 sρ
  فحص رضا QFPA
  التحقق العودي من المناطق المختلفة

الإعدادات التجريبية

التحقق النظري

تركز الورقة بشكل أساسي على التحليل النظري، من خلال إثبات بناء:

  1. الصحة: صحة واكتمال الخوارزمية
  2. التعقيد: حدود التعقيد الزمني والمكاني
  3. القدرة التعبيرية: علاقات القدرة التعبيرية بين الأجزاء المنطقية المختلفة

نتائج التعقيد

وظيفة التفعيلالرسوم البيانية الموجهةالرسوم البيانية غير الموجهة
truncReLUPSPACE-completePSPACE-complete
ReLUNEXPTIME-completeغير قابل للحسم
truncReLU مع القراءة العامةNEXPTIME-completeغير قابل للحسم

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

النتائج النظرية الرئيسية

علاقات القدرة التعبيرية

  • cr(G,u) = cr(G',u') ⟺ G,u و G',u' يحققان نفس صيغ GML
  • GML ⊆ K# ⊆ FOC₂
  • K# أقوى بشكل صارم من FO

حدود التعقيد

  1. رضا K#: PSPACE-complete
  2. التحقق من truncReLU-GNN: PSPACE-complete
  3. التحقق من ReLU-GNN: NEXPTIME-complete
  4. القراءة العامة: تؤدي إلى عدم القابلية للحسم (حالة الرسوم البيانية غير الموجهة)

كفاءة الخوارزمية

  • التعقيد المكاني: فضاء متعدد الحدود
  • عدد المناطق: بحد أقصى 2d log₂(4d) منطقة غير صفرية
  • تكلفة الترجمة: وقت متعدد الحدود (حالة الأوزان الصحيحة)

الرؤى التقنية

اتصال Weisfeiler-Lehman

  • خوارزمية تحسين اللون تلتقط نمط الحساب الأساسي لـ GNN
  • تسلسل k-WL يتوافق مع القدرة التعبيرية لـ GNNs من مراتب مختلفة
  • يوفر المنطق الموجه لغة طبيعية لوصف هذا التسلسل الهرمي

معالجة القيود العددية

  • يوفر QFBAPA إطار عمل فعال للتعامل مع عمليات التجميع
  • تحول تقنية مخطط Venn القيود العددية المعقدة إلى برمجة خطية
  • يضمن حد Carathéodory التعقيد المكاني متعدد الحدود للخوارزمية

الأعمال ذات الصلة

الأساس النظري لـ GNN

  • القدرة التعبيرية: Xu وآخرون (2019)، Morris وآخرون (2019) أنشأوا الروابط بين GNN واختبار WL
  • التوصيف المنطقي: Barceló وآخرون (2020) أنشأوا أول مراسلة بين GNN والمنطق
  • طرق التحقق: Benedikt وآخرون (2024) اقترحوا إجراءات قرار، لكن تفتقر إلى إطار موحد

التحقق من المنطق الموجه

  • الطرق التقليدية: إجراءات القرار للمنطق الموجه بناءً على طرق الجداول
  • التوسعات العددية: خوارزميات الرضا للمنطق الموجه المتدرج
  • نظرية التعقيد: تحليل التعقيد لأجزاء مختلفة من المنطق الموجه

التحقق من الشبكات العصبية

  • طرق SMT: استخدام حلالات SMT للتحقق من خصائص الشبكات العصبية
  • التفسير المجرد: تحليل سلوك الشبكة من خلال المجالات المجردة
  • التنفيذ الرمزي: استكشاف مسارات تنفيذ الشبكة بشكل رمزي

الخلاصة والمناقشة

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

  1. التوحيد النظري: إنشاء إطار نظري موحد لـ GNN واختبار WL والأنظمة المنطقية
  2. المساهمات الخوارزمية: توفير خوارزميات فعالة للتحقق من GNN بتعقيد أمثل
  3. القدرة التعبيرية: يلتقط منطق K# بدقة القدرة الحسابية لـ truncReLU-GNNs
  4. فصل التعقيد: تؤدي وظائف التفعيل المختلفة إلى تعقيد تحقق مختلف بشكل كبير

القيود

  1. قيود وظيفة التفعيل: تركز النتائج الرئيسية على truncReLU، وحالة ReLU أكثر تعقيداً
  2. مشاكل التكميم: تتطلب الأوزان النسبية مقام مشترك بحجم أسي
  3. تعقيد التنفيذ: لا يزال التنفيذ العملي للخوارزمية يواجه تحديات الكفاءة
  4. نطاق التطبيق: يركز بشكل أساسي على مهام تصنيف العقد، وتتطلب المهام على مستوى الرسم البياني اعتبارات إضافية

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

  1. توسيع وظائف التفعيل: دراسة طرق التحقق لوظائف تفعيل أكثر عمومية
  2. تحسين الخوارزمية: تحسين الأداء العملية وقابلية التوسع للخوارزمية
  3. تطوير الأدوات: تطوير أدوات عملية للتحقق من GNN
  4. توسيع التطبيقات: التوسع إلى معماريات GNN وأنواع مهام أكثر

التقييم المتعمق

المميزات

  1. العمق النظري: إنشاء روابط نظرية عميقة، ملء فجوة نظرية مهمة
  2. ابتكار الطريقة: تصميم منطق K# يوازن بذكاء بين القدرة التعبيرية والقابلية للحسم
  3. أناقة الخوارزمية: الجمع بين طرق الجداول واستدلال QFBAPA طبيعي وفعال
  4. اكتمال النتائج: توفير تحليل تعقيد شامل وإثبات علاقات المراسلة
  5. القيمة التعليمية: كمحاضرات، الهيكل واضح ومناسب للتعلم والتدريس

أوجه القصور

  1. غياب التحقق التجريبي: نقص التحقق التجريبي الفعلي وتقييم الأداء
  2. تفاصيل التنفيذ: مناقشة غير كافية لتفاصيل التنفيذ واستراتيجيات التحسين
  3. حالات التطبيق: نقص حالات التطبيق المحددة والدراسات الحالة
  4. دعم الأدوات: عدم توفير أدوات تحقق متاحة أو نظام نموذجي

التأثير

  1. المساهمة النظرية: وضع أساس نظري صلب لمجال التحقق من GNN
  2. الإلهام الطريقة: توفير إرشادات منهجية مهمة للبحث اللاحق
  3. القيمة التعليمية: كمادة تعليمية ممتازة، تساعد في تدريب المواهب في المجال
  4. الآفاق العملية: على الرغم من القوة النظرية، إلا أنها توضح الاتجاه لتطوير أدوات عملية

السيناريوهات المناسبة

  1. الأنظمة الحرجة من حيث السلامة: تطبيقات GNN التي تتطلب تحققاً صارماً
  2. البحث النظري: التحليل النظري للقدرة التعبيرية والتعقيد لـ GNN
  3. التدريس والتدريب: تدريس شبكات الرسوم البيانية العصبية والتحقق المنطقي
  4. تطوير الأدوات: الأساس النظري لتطوير أدوات التحقق من GNN

المراجع

تستشهد الورقة بـ 65 مرجعاً مهماً، تغطي:

  • الأساس النظري لـ GNN (Grohe 2021, Barceló et al. 2020)
  • اختبار Weisfeiler-Lehman (Morris et al. 2019, Xu et al. 2019)
  • المنطق الموجه (Blackburn et al. 2001, Tobies 1999)
  • نظرية التعقيد (Grädel et al. 1997, Kuncak and Rinard 2007)
  • التحقق من الشبكات العصبية (Benedikt et al. 2024, Haase and Zetzsche 2019)

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