🤖 machine learning

Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

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

المؤلفون الأصليون: Itamar Hadad, Guy Katz, Shahaf Bassan

نُشر 2026-02-20

📖 5 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلفون الأصليون: Itamar Hadad, Guy Katz, Shahaf Bassan

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

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

في عالم الذكاء الاصطناوي، تسمى هذه العملية اكتشاف الدوائر (Circuit Discovery). إنها تشبه محاولة العثور على "الوصفة السرية" داخل صندوق أسود.

ومع ذلك، هناك مشكلة كبيرة في الطريقة التي كان العلماء يتبعونها حتى الآن. فهم عادةً يستخدمون أسلوب "التجربة والخطأ". يقومون بسحب بعض الأسلاك، ويرون ما إذا كان الروبوت لا يزال يعمل، وإذا استمر في العمل، يقولون: "رائع! هذه الأسلاك هي الدائرة!" لكن هذا أمر محفوف بالمخاطر. إنه يشبه اختبار محرك سيارة عن طريق تشغيله مرة واحدة فقط. إذا حركت السيارة حركة بسيطة جداً، أو غيرت الوقود قلي بالقدر نفسه، فقد يتوقف ذلك المحرك الذي "يعمل" فجأة. الطرق القديمة لا تضمن عمل الروبوت إذا تغيرت الأشياء ولو قليلاً.

تقدم هذه الورقة البحثية طريقة جديدة، فائقة الدقة، لإيجال هذه الدوائر. يطلق المؤلفون عليها اسم التفسير الآلي الرسمي (Formal Mechanistic Interpretability). إليك التفصيل البسيط:

1. المشكلة: الدائرة "الهشة"

تخيل أنك تحاول تحديد فريق العمل المحدد في مصنع ضخم مسؤول عن صنع لعبة معينة.

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

2. الحل: آلة "الإثبات"

يستخدم المؤلفون أداة قوية من الرياضيات تسمى التحقق من الشبكة العصبية (Neural Network Verification). فكر في هذا ليس كمجرد اختبار، بل كـ إثبات رياضي.

بدلاً من مجرد مراقبة المصنع لبضع دقائق، يستخدمون "مرآة سحرية" (يسمونها الترميز التوأمي - Siamese Encoding) لمحاكاة كل التغييرات الممكنة الطفيفة في المصنع في وقت واحد.

يسألون المرآة: "إذا غيرنا الإضاءة، أو درجة الحرارة، أو المواد الخام بمقدار ضئيل جداً، هل سيظل الفريق أ يصنع اللعبة بشكل صحيح؟"
إذا قالت المرآة: "نعم، بالتأكيد، مهما حدث"، فقد حصلوا على ضمان مثبت (Provable Guarantee). هم يعرفون يقيناً أن هذه الدائرة متينة.

3. القوى الثلاث الخارقة لطريقتهم الجديدة

يثبت البحث أن دوائرهم الجديدة تمتلك ثلاث صفات خاصة:

القوة الفائقة (متانة المدخلات - Input Robustness): تعمل الدائرة حتى لو كانت الصورة التي يراها الروبوت ضبابية قليلاً أو بها بقعة صغيرة. إنها لا تنكسر تحت تأثير التغييرات الصغيرة.
المرونة الفائقة (متانة الرقعة - Patching Robustness): في الأيام الخوالي، عندما كان العلماء يزيلون أجزاء من الروبوت، كانوا يملؤون المساحة الفارغة بقيم "صفر" أو "متوسط" (مثل وضع طوبة وهمية في جدار). تثبت هذه الورقة أن الدائرة تعمل حتى لو مُلئت تلك المساحة الفارغة بأي قيمة واقعية أخرى. إنه يشبه إثبات أن الجسر يصمد سواء كانت الرياح هادئة أو عاصفة، وليس فقط عندما تكون الرياح ساكنة تماماً.
الكفاءة الفائقة (الحد الأدنى - Minimality): هم لا يجدون فقط أي دائرة؛ بل يجدون أصغر دائرة ممكنة لا تزال تعمل. لديهم سلم رياضي لـ "الصغر":
- شبه أدنى (Quasi-minimal): لا يمكنك إزالة قطعة واحدة فقط دون أن ينكسر النظام.
- أدنى للمجموعات الجزئية (Subset-minimal): لا يمكنك إزالة أي مجموعة من القطع دون أن ينكسر النظام.
- أدنى عددياً (Cardinally-minimal): هذه هي دائرة "الاعتدال المثالي". إنها أصغر مجموعة ممكنة من الأجزاء التي يمكنها القيام بالمهمة. لا توجد مجموعة أصغر منها يمكنها فعل ذلك.

4. كيف يفعلون ذلك: المحقق "مجموعة الحظر" (Blocking Set)

لإيجاد أصغر دائرة ممكنة، يستخدمون خدعة ذكية تتعلق بـ مجموعات الحظر (Blocking Sets).
تخيل أنك تحاول إيجاد أصغر مجموعة من الأشخاص اللازمين لإدارة شركة.

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

5. النتيجة: أقوى، آمن، وأصغر

اختبر المؤلفون هذه الطريقة على نماذج ذكاء اصطناعي شهيرة (مثل تلك التي تتعرف على إشارات المرور أو الأرق_المكتوبة بخط اليد).

الطريقة القديمة: وجدت دوائر تعمل بنسبة 46% من الوقت عندما تتغير المدخلات قليلاً.
الطريقة الجديدة: وجدت دوائر تعمل بنسبة 100% من الوقت، حتى عندما كانت المدخلات مختلفة قليلاً.
المقايضة: تستغرق عملية الحساب وقتاً أطول (مثل حل لغز ضخم بدلاً من مجرد التخمين)، لكن النتيجة هي دائرة يمكنك الوثوق بها تماماً.

الملخص

هذه الورقة البحثية تشبه الترقية من خريطة تعتمد على "أفضل تخمين" إلى نظام GPS مع ضمان.

قبل: "أعتقد أن هذا المسار يعمل، لكنني لست متأكداً إذا أمطرت".
الآن: "لقد أثبتت رياضياً أن هذا المسار يعمل، حتى لو أمطرت، أو أثلجت، أو تحرك الطريق قليلاً. وقد أثبتت أيضاً أنه أقصر مسار ممكن".

هذه خطوة كبيرة للأمام نحو جعل الذكاء الاصطناعي آمناً ومفهوماً، لأنها تنقلنا من مرحه "يبدو أنه يعمل" إلى مرحلة "نحن نعلم يقيناً أنه يعمل".

إليك ملخص تقني مفصل للورقة البحثية بعنوان "التفسير الآلي الميكانيكي: اكتشاف الدوائر مع ضمانات مثبتة" (ICLR 2026).

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

يهدف التفسير الآلي الميكانيكي (Mechanistic Interpretability - MI) إلى الهندسة العكسية للشبكات العصبية وتحويلها إلى وحدات وظيفية مفهومة بشرياً تسمى الدوائر (circuits). ويتمثل التحدي المركزي في هذا المجال في اكتشاف الدوائر: تحديد المجموعات الفرعية (النيورونات، المرشحات، رؤوس الانتباه) المسؤولة عن سلوك النموذج.

تعتمد الطرق الحالية المتطورة بشكل كبير على الاستدلالات (heuristics) والتقريبات القائمة على أخذ العينات (مثل الـ zero-patching أو الـ mean-patching على عينات مدخلات منفصلة). وتعاني هذه النهج من قيود حرجة:

نقص المتانة (Lack of Robustness): الدائرة التي تُوجد كدائرة "أمينة" (faithful) لمجموعة منفصلة من العينات قد تفشل عند حدوث اضطرابات مستمرة متناهية الصغر في المدخلات أو في القيم المنقولة (patched activations).
غياب الضمانات المثبتة: لا يوجد ضمان رسمي بأن الدائرة المكتشفة ستتصرف بشكل مطابق تماماً للنموذج الكامل عبر نطاق مدخلات مستمر.
الغموض في الحد الأدنى (Minimality): تختلف التعريفات الحالية لـ "الحد الأدنى" للدوائر (مثل quasi-minimal أو local-minimal)، وغالباً ما تتقارب الخوارزميات نحو حلول دون المستوى الأمثل دون دعم نظري صارم.

تعالج الورقة الحاجة إلى إطار عمل يكتشف دوائر بـ ضمانات مثبتة عبر النطاقات المستمرة، مما يضمن الأمانة (faithfulness)، والمتانة، والحد الأدنى.

2. المنهجية

يقترح المؤلفون إطار عمل مبتكر يدمج التحقق من الشبكات العصبية (Neural Network Verification - NNV) مع اكتشاف الدوائر. فبدلاً من أخذ العينات، يستخدمون أدوات التحقق الرسمي لإثبات أن الدائرة تحقق خصائص محددة رياضياً.

أ. تعريفات الضمانات المثبتة

تُصنف الورقة ثلاثة أنواع من الضمانات:

متانة نطاق المدخلات (Input-Domain Robustness): يجب أن تطابق الدائرة مخرجات النموذج الكامل ضمن حد سماح $\delta$ لـ جميع المدخلات في منطقة مستمرة (على سبيل المثال، كرة $\ell_p$ حول نقطة بيانات)، وليس فقط النقاط التي تم أخذ عينات منها.
متانة نطاق النقل (Patching-Domain Robustness): يجب أن تظل الدائرة أمينة حتى عندما يتم استبدال المكونات غير التابعة للدائرة بقيم تنشيط (activation values) ممكنة مشتقة من نطاق مدخلات مستمر، بدلاً من الثوابت الثابتة (صفر أو المتوسط).
الحد الأدنى (Minimality): صياغة مفاهيم مختلفة للإيجاز، تتراوح من الحد الأدنى شبه (Quasi-minimality) (حيث يؤدي حذف عنصر واحد إلى كسر الأمانة) إلى الحد الأدنى الكاردينالي (Cardinally-minimality) (أصغر دائرة أمينة عالمياً).

ب. الابتكار التقني: الترميز السيامي (Siamese Encoding)

للتحقق من هذه الخصائص، يقدم المؤلفون ترميز شبكة سيامية:

لمتانة المدخلات: يقومون بتكرار الدائرة و"رصّها" مع النموذج الكامل بحيث يتشاركان في طبقة المدخلات. يتحقق المُحقِّق (verifier) مما إذا كانت المسافة بين مخرجات (logits) النموذج الكامل والدائرة (مع تثبيت الأجزاء غير التابعة للدائرة) تظل أقل من $\delta$ لجميع المدخلات في النطاق.
لمتانة النقل: يستخدمون شبكة سيامية مزدوجة المدخلات. يعالج أحد الفروع المدخل $x$ عبر الدائرة، بينما يعالج الفرع الآخر مدخلاً مضطرباً $z$ عبر النموذج الكامل لتوليد قيم النقل (patching values). يضمن المُحقِّق أن مخرجات الدائرة على $x$ تطابق مخرجات النموذج الكامل على $x$ حتى عند استبدال الأجزاء غير التابعة للدائرة بالتنشيطات القادمة من $z$ .

ج. الخوارزميات والروابط النظرية

تؤسس الورقة روابط نظرية عميقة بين الرتابة (monotonicity) والحد الأدنى:

رتابة الدائرة (Circuit Monotonicity): يكون المحمول (predicate) $\Phi$ رتيباً إذا كان إضافة مكونات إلى دائرة أمينة يحافظ على الأمانة. يثبت المؤلفون أنه إذا حققت نطاقات المدخلات والنقل خصائص إغلاق معينة، فإن محمول المتانة يكون رتيباً.
التقارب الخوارزمي:
- البحث الجشع (Greedy Search - Alg 1): في ظل وجود الرتابة، تتقارب خوارزمية حذف جشعة بسيطة نحو دائرة أدنى فرعياً (Subset-Minimal) (لا توجد مجموعة فرعية أمينة).
- ثنائية المجموعة الحاجزة (Blocking-Set Duality): لتحقيق دوائر أدنى كاردينالياً (Cardinally-Minimal) (الأمثل عالمياً)، يستفيد المؤلفون من الثنائية بين الدوائر و"المجموعات الحاجزة" (الرسوم البيانية الفرعية التي يؤدي حذفها إلى كسر الأمانة). يصيغون المشكلة كإيجاد أصغر مجموعة ضاربة (Minimum Hitting Set - MHS) لهذه المجموعات الحاجزة، وهي مسألة يمكن حلها عبر حلول MaxSAT/MILP.

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

إطار عمل رسمي لاكتشاف الدوائر: أول إطار عمل يشتق دوائر بـ ضمانات مثبتة عبر نطاقات المدخلات والنقل المستمرة، متجاوزاً الاستدلالات القائمة على أخذ العينات.
التوحيد النظري: اكتشاف روابط نظرية جديدة بين متانة المدخلات، ومتانة النقل، والحد الأدنى. وتحديداً، إثبات أنه تحت ظروف معينة، تكون محمولات المتانة رتيبة، مما يضمن أن الخوارزميات الجشعة تجد دوائر أدنى فرعياً.
خوارزميات مبتكرة:
- تقنية الترميز السيامي لاعتماد المتانة باستخدام أدوات NNV الحالية (مثل $\alpha$ - $\beta$ -CROWN).
- خوارزمية قائمة على MHS (الخوارزمية 2) تقرب أو تستعيد بدقة الدوائر الدنيا كاردينالياً، مما يسد الفجوة بين الحد الأدنى المحلي والعالمي.
تعريفات شاملة: صياغة تسلسل هرمي للحد الأدنى (Quasi $\to$ Local $\to$ Subset $\to$ Cardinal) والظروف التي تتقارب عندها الخوارزميات لكل منها.

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

قيم المؤلفون إطار عملهم على معايير الرؤية القياسية (MNIST, CIFIA-10, GTSRB, TaxiNet) باستخدام المُحقِّق المتطور $\alpha$ - $\beta$ -CROWN.

المتانة:
- متانة المدخلات: حققت الطريقة المثبتة متانة بنسبة 100% عبر جوارات المدخلات المستمرة، بينما حققت الخطوط المرجعية القائمة على أخذ العينات متانة تتراوح بين 9.5% إلى 46.5% فقط. حتى الاضطرابات الصغيرة كسرت أمانة الدوائر القائمة على أخذ العينات.
- متانة النقل: وبالمثل، حافظت الطريقة المثبتة على متانة بنسبة 100% ضد اضطرابات النقل المستمرة، بينما انخفضت خطوط الأساس القائمة على النقل الصفري أو المتوسط إلى 0–63% من المتانة.
حجم الدائرة: رغم القيود الصارمة، كانت الدوائر المثبتة ذات أحجام مقاربة للدوائر القائمة على أخذ العينات (مثلاً 15.8 مقابل 12.5 نيورون في MNIST)، مما يثبت أن المتانة لا تتطلب بالضرورة دوائر أكبر بكثير.
الحد الأدنى: نجحت الطريقة القائمة على MHS في تحديد دوائر أدنى كاردينالياً أو توفير حدود دنيا وثيقة للحجم الأدنى، متفوقة على البحث الجشع في إيجاد التفسيرات الأكثر إيجازاً.
المقايضات: الطريقة المثبتة أكثر تكلفة حوسبياً (دقائق مقابل ثوانٍ لكل دائرة) بسبب استعلامات التحقق، لكن المقايضة توفر موثوقية مضمونة رياضياً.

5. الأهمية

يمثل هذا العمل تحولاً نوعياً في التفسير الآلي الميكانيكي:

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

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