تعتبر أنظمة البرهنة الآلية (Automated Theorem Proving) المعتمدة على Lean 4 من أبرز التطورات في عالم الذكاء الاصطناعي وعلوم الحاسوب. تعتمد هذه الأنظمة في عملها على البحث المتوازي لتقنيات الإثبات على الإثباتات المسبقة المعينة، مثل تلك التي يُنتجها نموذج Draft-Sketch-Prove (DSP).

ومع ذلك، تواجه هذه الأنظمة تحديات كبيرة، فكل فرع من فروع البحث يحتاج إلى إعادة بناء حالة الإثبات عبر تشغيل عمليات التحليل من جديد، مما يؤدي إلى تحميل زائد زمنياً كبيراً. يتكون هذا الحمل من جزئين رئيسيين: الأول هو تحميل المكتبات المستوردة (import loading) التي تستغرق حوالي 60 ثانية لكل فرع، والثاني هو تحليل جسم النظرية (theorem-body elaboration) الذي يعيد فحص سياق النظرية حتى الوصول إلى الهدف المطلوب، وقد يستغرق من 18 إلى 735 ثانية حسب تعقيد الإثبات.

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

لتجاوز هذا التحدي، نقدم تقنية جديدة تُعرف باسم "التقاط حالة الإثبات" (proof-state snapshotting)، التي تسمح بالتقاط حالة الإثبات المحسنة مرة واحدة وإعادة استخدامها عبر الفروع المختلفة، من خلال تعديل بسيط على خادم لغة Lean 4.

من خلال تطبيق هذه التقنية على 48 مشكلة miniF2F-v2 (45 معياراً لمرحلة الإثبات و3 عمليات كاملة من النهاية إلى النهاية)، حصلنا على زيادة في السرعة تراوحت بين 5.6 إلى 50 ضعفاً مقارنةً بالطرق التقليدية، حيث بلغ متوسط الزيادة 14 ضعفاً والوسيط 9.7 ضعف. كما أن زيادة عدد فروع الإثبات تساهم بشكل أكبر في تسريع هذه العمليات.

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