ملخص تقني: لماذا تنجح أنظمة إثبات النظريات الوكيلة (Agentic Theorem Provers)

بيان المشكلة

أظهرت أنظمة إثبات النظريات الوكيلة الحديثة، والتي تجمع بين النماذج اللغوية الكبيرة (LLMs) والاسترجاع والبحث والمحققات المساعدة في الإثبات (proof assistant verifiers)، نجاحاً تجريبياً في توليد براهين رياضية موثقة. ومع ذلك، تعجز الأطر النظرية الحالية عن تفسير هذا النجاح. فبينما تعالج نظرية الإثبات الكلاسيكية وجود البراهين، تعالج نظرية التعقيد الأسوأ في حالة الصعوبة (worst-case hardness). ولا يفسر أي منهما بشكل كافٍ سبب نجاح خوارزمية معينة باحتمالية عالية ضمن ميزانية حوسبة محددة لمجموعات توزيع النظريات المحددة والمنحازة التي تواجهها في الممارسة العملية (مثل نظريات المكتبات، وعائلات الاختبارات المرجعية).

تعالج الورقة السؤال التالي: ما هو احتمال أن يقوم مُثبت وكيل محدد بتوليد إثبات مقبول من قِبل المحقق (verifier) ضمن ميزانية ثابتة على تدفق محدد من حالات النظريات؟ يجادل المؤلفون بأن فهم هذا "الإثبات الإحصائي" ضروري لتفسير سبب تحسين مكونات مثل الاسترجاع، وتغذية المحقق الراجعة (verifier feedback)، والتفكيك (decomposition) للأداء دون التعارض مع عدم القابلية للتقرير (undecidability) الكلاسيكية أو الحدود الدنيا للحالة الأسوأ.

المنهجية

1. الصياغة كعملية قرار ماركوف (MDP) للوصول

صاغ المؤلفون البحث عن الإثبات الرسمي كـ عملية قرار ماركوف للوصول (Reachability MDP) ذات أفق زمني محدود بديناميكيات حتمية:

• الحالة ($X$): التزام الإثبات الحالي (على سبيل المثال، قائمة من الأهداف المفتوحة في Lean) بالإضافة إلى تغذية المحقق الراجعة.
• الإجراء ($A$): حركات المُثبت مثل التكتيكات (tactics)، أو قواعد الاستدلال، أو أوامر الاسترجاع.
• الانتقال ($F$): خريطة تحديث المحقق الحتمية $F: X \times A \to X$. الإجراءات غير الصالحة تؤدي إلى حالات الفشل؛ أما الإجراءات الصالحة فتنتقل إلى حالات إثبات جديدة.
• الهدف ($G$): مجموعة الحالات المحلولة (قوائم الأهداف الفارغة).

تعامل هذه الصياغة الدلالات التشغيلية للمحقق كـ "نواة الانتقال" (transition kernel). وقد أثبت المؤلفون أنه تحت تجريد حالة أمين (faithful state abstraction)، فإن احتمالية نجاح الـ MDP المثلى تتطابق تماماً مع الإثبات النحوي العادي ضمن نفس الميزانية، مما يحافظ على السلامة المنطقية مع تمكين التحليل الإحصائي.

2. تعريف الإثبات الإحصائي

المقياس الجوهري هو الإثبات الإحصائي ($SP^\pi_B(q_0)$)، والذي يُعرف بأنه احتمال أن يصل سياسة المُثبت $\pi$ إلى إثبات موثق خلال $B$ من استدعاءات المحقق، بمتوسط توزيع النظريات الأولية $q_0$ والعشوائية الداخلية للمُثبت. ويتم مقارنة هذا بـ $SP^*_B(q_0)$، وهو احتمال النجاح الأمثل.

كما يتتبع المؤلفون متوسط طول الإثبات المبتور ($Len^\pi_B(q_0)$)، والذي يُعرف بأنه العدد المتوقع لاستدعاءات المحقق قبل النجاح أو استنفاد الميزانية. يعمل هذا المقياس كأداة تفسيرية حرجة في حدودهم الرياضية.

3. تحليل خط أنابيب التعلم

تحلل الورقة خط أنابيب متوافق مع الممارسات الحالية:

1. انحدار قيمة الإجراء خارج الخط (Offline Action-Value Regression): تعلم دالات قيمة الإجراء حسب العمق ($Q^*_t$) من عمليات التدحرج المدعومة بالمحقق (الإثباتات المحاكية) على توزيع تدريبي.
2. الإثبات عند وقت الاختبار الجشع (Greedy Test-Time Proving): استخدام الدرجات المتعلمة لاختيار أفضل إجراء بشكل جشع عند وقت الاختبار.

يعتمد التحليل على الافتراض 3.1، الذي يفترض:

• مجموعات تركيز مدمجة ($C_t$) حيث يحدث التدريب والاختبار.
• استمرارية ليبشيتز (Lipschitz continuity) لدالة القيمة المثلى وفئة الفرضيات.
• تغطية كافية لفضاء الحالة-الإجراء بواسطة توزيع الاستكشاف.
• توفر تسميات (labels) متعددة ومستقلة لكل استعلام لتقليل الضجيج.

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

1. المبرهنة الرئيسية (حد الإثبات الإحصائي)

النتيجة المركزية (المبرهنة 3.1) تضع حداً للفجوة بين احتمالية نجاح المُثبت المتعلم واحتمالية نجاح المُثبت الأمثل. الحد هو عبارة عن مجموع موزون بالانشغال (occupancy-weighted sum) لأخطاء قيمة الإجراء الموحدة:

$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \leq 2 \sum_{s=1}^B P^{\hat{\pi}}_{q_0}(T_G \geq s) \cdot \epsilon_{B-s+1}$$

حيث أن:

• $P^{\hat{\pi}}_{q_0}(T_G \geq s)$ هو احتمال أن المُثبت المتعلم لم يحل المشكلة بعد في الخطوة $s$ (منحنى الكتلة غير المحلولة).
• $\epsilon_t$ هو حد الخطأ الموحد لمقدر قيمة الإجراء المتعلم عند العمق $t$.

تفسير حد الخطأ ($\epsilon_t$):
ينقسم الخطأ إلى ثلاثة مكونات:

1. خطأ التقريب (Approximation Error): عدم قدرة فئة الفرضيات على تمثيل دالة القيمة الحقيقية.
2. خطأ التغطية/الهندسة (Coverage/Geometry Error): يعتمد على البعد المحلي الفعال ($d_t$) وثابت التغطية ($c_t$) لتوزيع التدريب.
3. ضجيج التدحرج (Rollout Noise): التباين الناتج عن العدد المحدود من تسميات مونت كارلو ($m_t$) المستخدمة في الانحدار.

2. دور متوسط طول الإثبات

تتمثل الرؤية الأساسية في أن المضاعف المعقد الرئيسي في الحد هو متوسط طول الإثبات المبتور للمُثبت المتعلم ($Len^{\hat{\pi}}_B(q_0)$).
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim \bar{\epsilon}_B \cdot Len^{\hat{\pi}}_B(q_0)$$
وهذا يعني أن الآليات التي تقصر البراهين (مثل التفكيد الفعال، أو إدخال التمهيدات/Lemmas) تقلل مباشرة من الخسارة الشاملة، حتى لو ظل خطأ تقدير القيمة المحلي ($\bar{\epsilon}_B$) ثابتاً.

3. شروط الهامش والمعدلات السريعة

تحت شرط الهامش (حيث تكون الفجوة بين أفضل ثاني أفضل قيم للإجراء كبيرة بما يكفي باحتمالية عالية)، يتحسن الحد ليصل إلى معدل سريع:
$$SP^*_B(q_0) - SP^{\hat{\pi}}_B(q_0) \lesssim Len^{\hat{\pi}}_B(q_0) \cdot \bar{\epsilon}_B^{\beta+1}$$
يشير هذا إلى أن تحسين فجوات الإجراءات (جعل الحركات الصحيحة متفوقة بوضوح على الحركات غير الصحيحة) يسرع عملية التقارب بشكل كبير.

4. قوانين القياس (Scaling Laws)

تستنتج الورقة استدلالات حول تعقيد العينات. بتجاهل العوامل اللوغاريتمية، يتناسب الخطأ مع $n^{-1/(d+2)}$، حيث $n$ هي ميزانية تسميات المحقق و $d$ هو البعد الهندسي المحلي الفعال. وهذا يوضح أن مكاسب "القياس في وقت الاختبار" يمكن أن تأتي من:

• تقليل الأفق الفعال (براهين أقصر).
• تقليل البعد الهندسي الفعال (استرجاع/تمثيل أفضل).
• زيادة هامش الفجوة في الإجراءات.

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

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

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

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