في خطوة جديدة نحو تعزيز فعالية البرمجة المنطقية، تم تقديم مشروع CAPRI، الذي يُعرف بـ "تصحيح البراهين القائم على العقود" (Contract-Aware Proof Repair). يهدف المشروع إلى استخدام نماذج لغوية ضخمة (Large Language Models - LLMs) للمساعدة في اكتشاف براهين Isabelle بشكل أكثر دقة وأمانًا.

يتمثل التحدي الرئيسي في أنه بالرغم من أن بناء Isabelle يثبت قبول النظرية المقدمة، إلا أنه لا يضمن أن النموذج اللغوي قد قام بتغييرات تفويضها المطور فقط. هنا يأتي دور CAPRI، والذي يتضمن سير عمل تصحيح المدرك للعقود، حيث يتحقق Isabelle من البراهين ويقوم مدقق مستقل بفرض عقد تعديل يمكن قراءته آليًا.

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

ومن بين 144 مرشحًا تم قبولهم من قبل Isabelle، كان هناك ستة نصوص محمية قد تم تعديلها، وكلها نشأت من سير عمل تكرارية يمكنها تعديل نظرية كاملة. كما أظهرت واجهة خاصة بتصحيح جسم البراهين نجاحًا أعلى من حيث عدم انتهاك العقود.

يبرز CAPRI كحل مبتكر في مجال تطوير البرمجيات، حيث يمكن أن يُعيد تعريف كيفية معالجة استخدام نماذج الذكاء الاصطناعي في سياق البرمجة. في ظل تطور عالم الذكاء الاصطناعي، تبقى الأسئلة حول مدى فائدة هذه الابتكارات في تعزيز دقة الكود البرمجي وموثوقيته قائمة.

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