Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral

ملخص تقني: الصياغة الرسمية لـ "حد الخطأ في التعميم" عبر تعقيد رادماخرر وتكامل ددلي للإنتروبيا

بيان المشكلة

يتمثل التحدي المركزي الذي يعالجه هذا العمل في التحقق الرسمي من أداء التعميم في تعلم الآلة. وتحديداً، يسعى المؤلفون إلى اشتقاق تقديرات نظرية لخطأ الاختبار (المخاطرة السكانية) من خطأ التدريب (المخاطرة التجريبية) باستخدام إطار عمل نظري للقياس. وبينما تعتمد النهج الكلاسيكية على بُعد فابنيك-تشيرفونينك (VC dimension)، إلا أنها غالباً ما تكون غير معتمدة على البيانات ومصممة للتصنيف الثنائي فقط. أما نظرية التعلم الحديثة، فتستخدم بشكل متزايد تعقيد رادماخرر (Rademacher complexity)، الذي يوفر حدوداً دقيقة تعتمد على البيانات وقابلة للتطبيق على الخسائر ذات القيم الحقيقية وفئات الدوال المتنوعة (مثل التعلم العميق وطرق النواة). ومع ذلك، فإن صياغة هذه الحجج في مساعدات الإثبات (proof assistants) أمر صعب بسبب الحاجة إلى التعامل الصارم مع القابلية للقياس (خاصة بالنسبة للقيم العليا - suprema - فوق فئات فرضيات غير قابلة للعد)، وتدابير الضرب، وتفاوتات التركيز.

المنهجية

قام المؤلفون بصياغة حد خطأ التعميم في لغة Lean 4، مستفيدين من البنية التحتية الواسعة لنظرية القياس والاحتمالات في مكتبة Mathlib. يتبع التطوير مسار "التماثل + الفروق المحدودة" (symmetrization + bounded differences) القياسي الموجود في الكتب المنهجية (مثل Mohri et al., Wainwright)، ولكنه يكيفه مع قيود التحقق الرسمي:

1. الإعداد النظري للقياس: يصيغ الإطار عملية توليد البيانات عبر فضاء احتمالي $(\Omega, m_\Omega, \mu)$ ومتغير عشوائي $X: \Omega \to \mathcal{X}$. ويتم نمذجة العينات كدوال $\omega: \text{Fin } n \to \Omega$، والتي يتم دفعها للحصول على $S = X \circ \omega$.
2. التعريفات الجوهرية:
   • تعقيد رادماخرر: مُعرَّف لكل من الحالات التجريبية (فوق عينة ثابتة $S$) والحالات المتوقعة (فوق تدبير الضرب $\mu^n$). النسخة التجريبية تحسب المتوسط عبر جميع متجهات الإشارات $\sigma \in \{-1, 1\}^n$.
   • الانحراف الموحد (Uniform Deviation): مُعرَّف كالقيمة العليا للفرق المطلق بين المتوسطات التجريبية والسكانية عبر فئة فرضيات $F = \{f_i\}_{i \in \iota}$.
3. التماثل (Symmetrization): يستبدل مبرهنة رسمية (abs_symmetrization_equation) القيمة العليا للفروق بين عينتين مستقلتين بمتوسط عبر مجموعات معكوسة الإشارة، مما يربط الانحراف الموحد بتعقيد رادماخرر.
4. التركيز (Concentration): يثبت المؤلفون متراجحة مكديرميد (McDiarmid inequality) من الصفر داخل Lean. حيث يثبتون أن دالة الانحراف الموحد تحقق خاصية الفروق المحدودة (تغيير نقطة عينة واحدة يغير القيمة بمقدار لا يتجاوز $2b/n$)، مما يسمح باشتقاق حدود ذيل الاحتمالية العالية.
5. التعامل مع مجموعات المؤشرات غير القابلة للعد: تمثل القابلية للقياس للقيم العليا فوق مجموعات مؤشرات غير قابلة للعد $\iota$ عقبة تقنية حرجة. توفر Mathlib القابلية للقياس للمجموعات القابلة للعد، ولكن ليس تلقائياً للمجموعات غير القابلة للعد. حل المؤلفون ذلك من خلال:
   • أولاً، إثبات مبرهنات للمجموعات القابلة للعد.
   • ثانياً، توسيع النتائج إلى المجموعات الطوبولوجية القابلة للفصل عبر اختزال كثيف قابل للعد. يتضمن ذلك إثبات أن القيمة العليا لدوال مستمرة فوق فضاء قابل للفصل تساوي القيمة العليا لمجموعة جزئية كثيفة قابلة للعد، بشرط الحفاظ على الاستمرارية تحت التكامل (وهو ما يضمنه الهيمنة المنتظمة).

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

يمثل هذا البحث أول صياغة منهجية لتحليل التعميم عبر تعقيد رادماخرر. وتشمل المساهمات المحددة ما يلي:

• بنية تحتية قابلة لإعادة الاستخدام: مسار مدقق آلياً يغطي تعقيد رادماخرر التجريبي/المتوقع، والتماثل، وتحليل الفروق المحدودة، ومتراجحة مكديرميد.
• حل مشكلة القابلية للقياس: آلية قابلة لإعادة الاستخدام لرفع النتائج من فئات الفرضيات القابلة للعد إلى فضاءات المعلمات الطوبولوجية القابلة للفصل. تقوم هذه العملية بتغليف الشروط الكافية (القابلية للفصل، والعد الأول، والهيمنة المنتظمة، والاستمرارية تحت التكامل) اللازمة لجعل القيم العليا غير القابلة للعد قابلة للقياس، وهي خطوة غالباً ما تُذكر ضمنياً في البراهين غير الرسمية.
• أدوات تركيز مصاغة رسمياً: إثبات كامل لمتراجحة مكديرميد مع لزمات داعمة لمتراجحات الحد الأقصى، ولمتراجحة ماسات (Massart's lemma)، وأعداد التغطية.
• تطبيقات عملية:
  • المتنبئات الخطية: صياغة رسمية لحدود $O(1/\sqrt{n})$ للمتنبئات ذات الانتظام $\ell_2$ وحدود $O(\sqrt{\log(d)/n})$ للمتنبئات ذات الانتظام $\ell_1$.
  • تكامل ددلي للإنتروبيا (Dudley's Entropy Integral): صياغة رسمية لحد من نوع "دودلي" يربط تعقيد رادماخرر بأعداد التغطية عبر بناء السلسلة (chaining construction). تطلب هذا تعريف مقاييس شبه مسافة تجريبية والتعامل مع الانتقال من مجموعات السلسلة المنفصلة إلى حدود التكامل.

النتائج

تؤدي الصياغة إلى نسخ مدققة آلياً من حدود نظرية التعلم القياسية:

1. الحد المتوقع: $E[\text{UD}_n(F)] \leq 2 R_n(F)$، حيث $R_n(F)$ هو تعقيد رادماخرر.
2. حد الاحتمالية العالية: لأي $\delta \in (0, 1)$، باحتمال لا يقل عن $1-\delta$:
   $$\text{UD}_n(F) \leq 2 R_n(F) + b \sqrt{\frac{2 \log(1/\delta)}{n}}$$
3. حدود محددة: يوفر المستودع براهين ملموسة لتعقيد رادماخرر التجريبي للمتنبئات الخطية تحت قيود $\ell_2$ و $\ell_1$، بالإضافة إلى حد تكامل إنتروبيا ددلي.

الأهمية والادعاءات

يضع المؤلفون هذا العمل كخطوة تأسيسية نحو تعلم آلي موثوق ومعتمد.

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

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