في عالم الرياضيات المتقدمة وهندسة البرمجيات، تظل الطرق الرسمية (Formal Methods) أداة حيوية لضمان موثوقية الأنظمة الحرجة. ومع ذلك، تبقى هذه الأساليب بعيدة عن الاستخدام واسع النطاق، وذلك بسبب التحديات المرتبطة ببناء إثباتات يدوية تتطلب جهدًا كبيرًا.

نظرًا للتقدم الأخير في نماذج اللغات الضخمة (Large Language Models - LLMs)، ظهرت فرص جديدة لإثبات النظريات بشكل آلي. وقد اتضح أن هناك مدرستين رئيسيتين قد برزتا في هذا المجال: توليد البرهنة بناءً على استراتيجيات خطوة بخطوة، وتوليد الإثباتات الكاملة.

في هذا السياق، تقدمنا بإطار عمل مبتكر يعرف باسم HybridProver، والذي يدمج بين الطريقتين السابقتين من خلال استخدام «رسومات الإثبات» (Proof Sketches) كتمثيل وسيط. يمكّن هذا التصميم من إعادة استخدام الهياكل الجزئية الصحيحة، مما يجعل الجمع بين التخطيط عالي المستوى والاستدلال الدقيق أمرًا ممكنًا.

قمنا بتنفيذ HybridProver في بيئة Isabelle/HOL، وقمنا بإعادة تدريب نماذج LLM بحجم 7B على مجموعات بيانات محسنّة لموديل Isabelle. وأظهرت التجارب على معيار miniF2F أن هناك معدل نجاح بلغ 73.8%، متفوقًا على المعدل السابق الذي بلغ 61.9%. وهذا يدل على أن الموديلات الخفيفة الوزن عند استخدامها مع منهجيتنا يمكنها توليد إثباتات Isabelle/HOL بكفاءة، دون الاعتماد على نماذج LLM الكبيرة جدًا.

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

ما رأيكم في هذا التطور؟ شاركونا في التعليقات.