ملخص تقني: قوانين التوسع المشبعة للاكتشاف المتساوي

بيان المشكلة

يتقصى البحث ما إذا كانت أنظمة الاكتشاف الرمزي الحتمية — وتحديداً تلك التي تنمو عن طريق إضافة قواعد إعادة كتابة متساوية — تتبع قوانين توسع تجريبية مماثلة لتلك الموجودة في النماذج اللغوية الكبيرة (LLMs). وبينما تعد قوانين التوسع للنماذج العصبية (Kaplan et al., 2020; Hoffmann et al., 2022) راسخة، يظل السؤال مفتوحاً حول ما إذا كانت الركائز الحتمية، مثل تلك المستخدمة في البرمجة المنطقية الاستقرائية، وإشباع التساوي، وتخليق البرامج، تتبع ديناميكيات نمو مماثلة. يهدف المؤلفون إلى توصيف ظواهر النمو في هذه الأنظمة، واختبار ما إذا كان قانون القوة البسيط أو دالة تشبع أكثر تعقيداً هو الذي يصف تراكم القواعد المكتشفة بمرور الوقت.

المنهجية

تستخدم الدراسة إطار عمل تجريبي مضبوط يتضمن ثلاث ركائز حتمية "لعبة" (toy) تزداد تعقيداً في الأنواع:

1. الحساب (arith): هويات متساوية عبر قواعد نحوية محددة النوع تتضمن الجمع، الضرب، والمتغيرات الحرة.
2. البولياني (bool): هويات عبر المعاملات المنطقية (and, or, not).
3. القائمة من الرتبة العليا (list): مجال مستوحى من DreamCoder يتضمن بدائيات مثل map, fold, و cons.

حلقة الاكتشاف:
ينمو النظام لإنتاج ركيزة $S$ (مجموعة من قواعد إعادة الكتابة) عبر خطوات منفصلة $t$. في كل خطوة:

• يقترح مولد (generator) معادلات مرشحة بناءً على الحالة الحالية لـ $S$ (باستخدام استراتيجيات مثل العشوائية، التركيب، التوزين بالتردد، أو الجشع لـ MDL).
• يتم اختبار المرشحين لسلامة الدلالة عبر التعيين العشوائي.
• يتم تعميم الأزواج المقبولة (استبدال المتغيرات الحرة بمتغيرات نمطية).
• يحدد مرشح قبول قابل للضبط (إما "أي" أو "الجدة") ما إذا كانت القاعدة ستُعتمد في $S$.

جمع البيانات:
قام المؤلفون بتوليد 592 مسار اكتشاف مستقل عبر هذه الركائز، مع تغيير خمس ميزات معمارية: نوع المولد، صرامة المرشح، عمق التكرار، حجم الدفعة، والبذرة العشوائية. وقاسوا العدد الإجمالي للقواعد $|S(t)|$ بمرور الوقت.

نهج النمذجة:
يقترح المؤلفون نموذج إغلاق متوسط المجال (mean-field closure model) استدلالي مشتق من افتراضات التغطية الموحدة والاستقلال التقريبي. ينتج عن ذلك معادلة تفاضلية للنمو:
$$\frac{dN}{dt} = K \cdot N^k \cdot e^{-\mu N}$$
حيث $N$ هو حجم الركيزة، و $k$ يتعلق بعمق إعادة التركيب للمولد، و $\mu$ يمثل كسر التغطية لمساحة المرشحين.

• المدى القصير ($\mu N \ll 1$): تقترب المعادلة من قانون قوة نقي $N(t) \propto t^b$، حيث $b = 1/(1-k)$.
• المدى الطويل ($\mu N \gtrsim 1$): يؤدي الحد الأسي إلى التشبع، ويتم نمذجته بصيغة لوجستية-قوة.

تقوم الدراسة بملاءمة ثلاثة نماذج مرشحة (قانون قوة نقي، أس-أسي ممدد، وقانون قوة مشبع) للبيانات باستخدام معيار AIC لاختيار النموذج، وباستخدام الانحدار المعزز بالتدرج للتنبؤ بالأس $b$ من الميزات المعمارية.

المساهمات الرئيسية والنتائج

1. ديناميكيات قانون القوة في المدى القصير

عبر 592 مساراً، يتبع نمو حجم الركيزة $|S(t)|$ في المدى القصير (حتى 30 حقبة) باستمرار شكل قانون القوة $t^b$. يتراوح الأس $b$ باستمرار بين 0 و 1.15 اعتماداً على المجال والمعمارية.

• الحساسية المعمارية: ضمن ركيزة واحدة، يكون الأس $b$ حساساً للغاية للاختيارات المعمارية. يتنبأ نموذج انحدار معزز بالتدرج باستخدام خمس ميزات معمارية بالأس $b$ بمعامل تحديد $R^2 \approx 0.82$ لكل من مجالات الحساب والبولياني والمجال القائم على القوائم.
• فشل الانتقال عبر الركائز: يفشل نموذج تم تدريبه للتنبؤ بـ $b$ على بيانات الحساب والبولياني تماماً عند تطبيقه على مجال القوائم ($R^2 \approx -0.84$). إن المعمارية المثلى للنمو التراكمي في الركائز ذات الأنواع المسطحة (مثل مرشحات الجدة) تثبط النمو في الركائز ذات الرتب العليا. وهذا يشير إلى أن ديناميكيات النمو مشروطة بالركيزة وليست عالمية.

2. فرضية التشبع في المدى الطويل

اختبر المؤلفون ما إذا كان النمو يتشبع في النهاية كما يتنبأ نموذج الإغلاق الخاص بهم.

• البيانات اللعبة (مجال القوائم): تمديد خمسة مسارات لمجال القوائم إلى 500 حقبة، يتفوق نموذج قانون القوة المشبع في مقارنات AIC داخل العينة للمسارات التي تزيد عن 200 حقبة. ومع ذلك، فإن التنبؤ خارج العينة (الملاءمة على أول 100 حقبة والتنبؤ بالـ 400 التالية) يميل لصالح قانون القوة النقي في جميع الحالات الخمس. يستنتج المؤلفون أن المسارات "اللعبة" لا تصل فعلياً إلى نظام التشبع ضمن 500 حقبة؛ ومن المرجح أن تفضيل النموذج المشبع داخل العينة هو نتاج ملاءمة (fitting artifact) يتنبأ بشكل سيئ.
• البيانات الواقعية (Mathlib4): يدعم تحليل الإضافات الشهرية لملفات .lean في مكتبة Mathlib4 (60 شهراً، 9,701 ملفاً) الشكل المشبع. يتفوق النموذج المشبع على نموذج قانون القوة النقي في التنبؤ خارج العينة بمعامل $\sim 7\times$ (RMSE 3,279 مقابل 23,896)، مما يشير إلى أن Mathlib4 قد وصلت إلى نظام التشبع.
• البيانات الواقعية (Coq Mathcomp): تحليل التغييرات (commits) الشهرية في مكتبة Coism Mathcomp (129 شهراً) يفضل قانون القوة النقي. ينهار معامل التشبع $\mu$ إلى الصفر، ويتفوق قانون القوة النقي على النموذج المشبع في التنبؤ خارج العينة بمعامل $\sim 67\times$. هذا يشير إلى أن Mathcomp لم تصل بعد إلى نظام التشبع.

3. التأطير الظاهراتي

يقترح البحث تأطيراً عملياً: "نمو قانون القوة المشبع مع معاملات $(k, \mu)$ مشروطة بالركيزة، والتي يمكن ملاحظتها عندما تصل الركيزة إلى نظام التشبع الخاص بها." الديناميكيات مشروطة على مستويين:

1. المعلمات المعمارية التي تتنبأ بأس النمو لا تنتقل عبر أنواع الركائز المختلفة.
2. عائلة الدوال التي تصف النمو (قانون القوة النقي مقابل المشبع) تعتمد على مرحلة دورة حياة الركيزة المحددة.

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

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

• نطاق متواضع: يذكر المؤلفون صراحة أن الأدلة محدودة بثلاث ركائز "لعبة" وممثلين واقعيين اثنين (وهي تمثيلات خشنة تعتمد على عدد التغييرات/الملفات). كما يقرون بأن نتائج "اللعبة" طويلة المدى "متسقة مع، وليست مؤكدة لـ" النتائج بسبب فشل التنبؤ خارج العينة للنماذج.
• رؤية رئيسية: النتيجة الأساسية هي أن ديناميكيات الاكتشاف الرمزي مشروطة بالركيزة. على عكس القوانين العصبية التي تفترض غالباً العالمية عبر المعماريات، يعتمد سلوك النمو هنا بشدة على "هندسة الإغلاق" (معامل التغطية $\mu$) لنظام الأنواع الخاص بالركيزة.
• الاتجاهات المستقبلية: حدد المؤلفون ثلاثة تحديثات ملموسة مطلوبة لرفع هذا العمل من "ظواهر لعبة" إلى "ظاهرة حقيقية":
  1. التكرار على ركيزة غير "لعبة" مع دقة على مستوى المسار (وليس فقط عدد التغييرات).
  2. التنبؤ الناجح خارج العينة للنموذج المشبع.
  3. الاشتقاق النظري لمعامل التشبع $\mu$ من تركيبات الركيزة (مثل إنتروبيا النوع) لجعل الانتقال عبر الركائز قابلاً للتفنيد.

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