From categorized neural architectures to subexponential proof theory

فيما يلي ملخص تقني مفصل لورقة البحث بعنوان "من البنى العصبية المصنفة إلى نظرية الإثبات تحت-الأسية" (From Categorized Neural Architectures to Subexponential Proof Theory) للكاتب كارلوس راميريز أوفال.

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

تعالج الورقة فجوة جوهرية في التقاطع بين نظرية الفئات (Category Theory)، والتعلم الآلي، والمنطق. بينما نجح التعلم العميق الفئوي في توفير دلالات للبنى العصبية (عبر اعتبارها بنى تركيبية)، ونجحت المنطق الفئوي في إثبات كيفية توليد الفئات لأنظمة الإثبات، إلا أن الاتجاه العكسي لا يزال غير مستكشف إلى حد كبير: هل يمكن اشتقاق نظام منطقي محدد مباشرة من السلوك الحساس للموارد في بنية عصبية؟

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

2. المنهجية

يقترح المؤلف مسار بناء يتكون من أربع مراحل:
$$\text{Architecture Family} \longrightarrow \text{Categorized Architecture} \longrightarrow \text{Subexponential Signature} \longrightarrow \text{Proof Theory}$$

أ. الصياغة الفئوية للبنى (Categorical Formalization of Architectures)

• سياقات الموارد المحددة بالأنواع (Typed Resource Contexts): يعرّف المؤلف السياقات كقوائم منتهية من الأزواج $(z, A)$، حيث $z$ هو "تسمية المنطقة" (تمثل الذاكرة أو نوع السياق) و $A$ هو نوع من فئة أساسية $\mathcal{C}$ (مثل الفضاءات المتجهة).
• كتل الموارد المعلمة (Parametrisied Resource Blocks): تُنمذج الكتل العصبية كـ مورفزمات (morphisms) $(P, \phi): \Gamma \to \Delta$، حيث $P$ هو كائن المعلمات و $\phi$ هي دالة $P \times [[\Gamma]] \to [[\Delta]]$.
• الفئة المعمارية ($\mathbf{Arch}_Z$): تبني الورقة فئة تكون فيها الكائنات هي السياقات، والمورفزمات هي فئات التكافؤ للكتل المعلمة (مع تحديد الكتل التي تختلف فقط باختلاف إعادة المعلمة المتماثلة). وقد تم إثبات أن $\mathbf{Arch}_Z$ هي فئة مونويدية متناظرة (Symmetric Monoidal Category - SMC).

ب. انضباط المناطق المتسق (Coherent Zone Disciplines)

لالتقاط حساسية الموارد (النسخ، الإهمال، الإكراه)، يقدم المؤلف انضباط منطقة متسق ($\mathcal{L}ic$) على $\mathbf{Arch}_Z$. يتكون هذا الانضباط من:

1. ترتيب مسبق $\preceq$ على المناطق (التكرير/Refinement).
2. إكراهات المنطقة (Zone Coercions): مورفزمات تسمح بانتقال البيانات من منطقة أكثر دقة إلى منطقة أقل دقة.
3. الإهمال المرخص ($W_{\mathcal{L}ic}$): مجموعة فرعية من المناطق حيث يمكن إهمال البيانات (الضعف/Weakening).
4. القطر المرخص ($C_{\mathcal{L}ic}$): مجموعة فرعية من المناطق حيث يمكن تكرار البيانات (التقلص/Contraction).

هذه الأذونات ليست عشوائية؛ بل هي مورفزمات هيكلية موجودة صراحةً في الفئة المعمارية.

ج. استخراج التوقيع تحت-الأسي (Extraction of Subexponential Signature)

من الفئة المنضبطة، يستخرج المؤلف توقيعاً تحت-أسياً $\Sigma_{\mathcal{L}ic} = (Z, \preceq, W, C)$.

• يتم إعادة بناء المجموعات $W$ و $C$ مباشرة من وجود مورفزمات الإهمال والقطر في العائلة المرخصة.
• يثبت النظرية 2.18 أن إعادة البناء هذه أمينة (faithful): التوقيع المستخرج يطابق تماماً المناطق المحددة بواسطة الانضباط المعماري.

د. نظرية الإثبات والصحة (Proof Theory and Soundness)

• حساب المتتاليات التنسورية ($T\mathcal{Z}_{\Sigma}$): يتم تعريف نظام إثبات بناءً على التوقيع المستخرج. يتضمن قواعد لضرب التنسور ($\otimes$)، والوحدة ($I$)، وقواعد الضعف والتقلص المفهرسة بالمنطقة ($W_z, C_z$).
• حذف القطع (Cut Elimination): تثبت الورقة أن الحساب المستخرج يقبل حذف القطع (النظرية 3.7)، اعتماداً على حقيقة أن الجزء التنسوري مغلق تحت الاشتقاقات الخالية من القطع في المنطق تحت-الأسي المحيط.
• الصحة (Soundness): توضح النتيجة الدلالية الرئيسية (النظرية 4.8) أن كل اشتقاق في المنطق المستخرج يقابل مورفزم في "فئة المخططات المرخصة" للفئة المعمارية الأصلية. القواعد الهيكلية للمنطق تُفسر بدقة بواسطة مورفزمات الإهمال والقطر المرخصة في المعمارية.

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

1. تعريف الفئة المعمارية: التعريف الرسمي لـ $\mathbf{Arch}_Z$، وهي فئة مونويدية متناظرة من الكتل المعلمة المسماة بالمناطق، مما يوفر دلالات فئوية صارمة للمكونات العصبية الحساسة للموارد.
2. آلية الاستخراج: طريقة مبتكرة لـ "قراءة" توقيع تحت-أسي من البيانات الفئوية. بخلاف النهج التقليدي حيث يكون المنطق ثابتاً، هنا يكون المنطق ثابتاً (invariant) لسياسة موارد المعمارية.
3. إعادة البناء الأمينة: إثبات أن مناطق الضعف والتقلص المستخرجة ($W, C$) هي بالضبط المناطق التي تسمح فيها المعمارية بالإهمال والتكرار، مما يضمن عدم إدخال أي قواعد هيكلية "عرضية".
4. نظرية الصحة: إثبات صارم بأن نظرية الإثبات المستخرجة صحيحة بالنسبة للفئة المعمارية الأصلية. القواعد المنطقية ليست فقط صالحة دلالياً، بل هي مُنفذة بواسطة المورفزمات الهيكلية المحددة (الإهمال/القطر) للمعمارية.
5. التجسيد الملموس: تطبيق هذا الإطار على شبكة عصبية بسيطة مكونة من كتلتين (تتضمن ذاكرة مستمرة، سياق مسترجع، وملاحظة خطية)، مما يوضح كيف تؤدي أدوار المدخلات المختلفة (المستمرة مقابل الخطية) إلى قواعد منطقية تحت-بنيوية محددة.

4. النتائج

• النظرية 2.10: $\mathbf{Arch}_Z$ هي فئة مونويدية متناظرة.
• النظرية 2.18: الفئات الهيكلية المعاد بناؤها ($W_{\mathcal{L}ic}, C_{\mathcal{L}ic}$) مطابقة تماماً للمناطق المحددة ($W_{\mathcal{L}ic}, C_{\mathcal{L}ic}$) في الانضباط، مما يثبت أن الاستخراج أمين.
• النظرية 3.7: الحساب التنسوري المستخرج $T\mathcal{Z}_{\Sigma}$ يقبل حذف القطع.
• النظرية 4.8 (الصحة): لكل اشتقاق $\pi$ في الحساب المستخرج، يوجد مورفزم $[[\pi]]$ في فئة المخططات المرخصة للمعمارية. وتحديداً، يستخدم تفسير الضعف الإهمال المرخص، ويستخدم التقلص القطر المرخص.
• المثال 4.11: عرض ملموس يوضح كيف تؤدي معمارية عصبية ذات أنواع ذاكرة متميزة (مستمرة، ذات صلة، خطية) بشكل طبيعي إلى منطق ذي قواعد تحت-أسية مقابلة (النسخ/الإهمال مسموح للمستمرة، النسخ فقط للذات صلة، والخطية للملاحظة).

5. الأهمية

تمثل هذه الورقة تحولاً تأسيسياً في برنامج "المعمارية العصبية $\leftarrow$ الفئة $\leftarrow$ المنطق".

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

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