في عالم الذكاء الاصطناعي، تتطلب طرق إثبات النظريات (Theorem Proving) بنية تحتية قوية للتواصل مع إثباتات النظريات التفاعلية (Interactive Theorem Provers - ITPs)، واستخراج البيانات المثبتة المنظمة، وتنفيذ عمليات البحث عن الإثبات على نطاق واسع. ولكن، غالباً ما تكون الأدوات المتاحة حالياً مخصصة للمساعدات (Assistants) فقط وموجهة نحو التنفيذ على مستوى الملفات، مما يجعل التحليل على مستوى المستودعات والتجارب المتوازية أمراً صعباً.

هنا يتدخل ProofWala، وهو إطار عمل مبتكر لهندسة الإثباتات متعددة اللغات. يعتمد ProofWala على مكتبة exttt{itp-interface} القابلة لإعادة الاستخدام، التي تسهل التفاعل البرمجي مع ITPs. لقد تم تنفيذ طبقة تفاعلية برمجة فرعية لـ Lean 4، مما يُمكّن من تتبع دقيق لمستوى التكتيك (Tactic-Level) واستخراج البيانات المرتبطة بالإعلانات (Declarations) والاعتماديات (Dependencies) عبر مستودعات كاملة.

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

اعتمدت ProofWala على هذه البنية التحتية لتوفير مجموعات بيانات إثبات متعددة اللغات، وأدوات تدريب النماذج، وخوارزميات بحث إثبات متوازية. تم إثبات من خلال هذا الإطار أن التدريب متعدد اللغات بين Lean وRocq يمكّن من النقل عبر اللغات والمجالات. لوحظت تحسينات ذات دلالة إحصائية على Lean Mathlib وفي التكيف بالمجالات (Category Theory)، بينما أظهرت إعدادات أخرى اتجاهات تصاعدية متسقة.

الأكثر إثارة هو أننا نفتح مصدر الإطار بالكامل، بما في ذلك وحدة البحث عن الإثبات المتوازي، والمجموعات البيانية، والنماذج عبر مستودعين: ProofWala (ProofWala Repository) ومكتبة itp-interface (itp-interface Repository).

هل أنتم متحمسون لمستقبل الإثباتات متعددة اللغات؟ شاركونا آراءكم في التعليقات!