التنوع يتغلب على القوة الغاشمة: خط أنابيب جديد يضاعف نسبة نجاح التحقق البرمجي الآلي

عندما يفوز التنوع على العدد

73 مهمة تحقق شكلي (Formal Verification)، و292 نسخة برمجية مرشحة، ونتيجة واحدة لافتة: توليد عدة نسخ متكافئة وظيفيًا من البرنامج نفسه يرفع بشكل كبير احتمال أن تنجح واحدة منها على الأقل في إثبات صحتها إثباتًا شكليًا. هذه هي الخلاصة المحورية لنظام "Diversify2Verify"، خط أنابيب (Pipeline) جديد متعدد المراحل، ورد وصفه في ورقة بحثية قُدّمت إلى أرشيف arXiv يوم الجمعة الموافق 10 يوليو 2026، وتعالج واحدة من أعنَد العقبات في المناهج الشكلية: كيف تجعل النماذج اللغوية الكبيرة (LLMs) تكتب كودًا يمكن لأدوات التحقق أن تؤكد صحته فعليًا.

يعمل النظام فوق منصة Why3، وهي بيئة مخصصة للتحقق الاستنباطي من البرامج (Deductive Program Verification)، ويعالج مشكلة كانت تحد بصمت من الفائدة العملية للتحقق المدعوم بالنماذج اللغوية. فقد تتصرف نسختان من الدالة نفسها، مثل دالة عكس قائمة مكتوبة بأسلوب تكراري ذاتي (Recursive) مقابل أسلوب حَلَقي (Iterative)، بالطريقة نفسها تمامًا عند التشغيل، بينما تختلفان اختلافًا جوهريًا في سهولة إثبات صحتهما أمام أداة التحقق. وبدل الرهان على نسخة واحدة مولّدة وانتظار نجاحها، يقوم Diversify2Verify بتوليد نسخ متعددة دفعة واحدة.

كيف يعمل خط الأنابيب

تمر العملية بمراحل متتابعة. في البداية، يستنتج النظام عقودًا برمجية (Contracts) مصممة خصيصًا لطبيعة تمثيل البيانات المستخدم، سواء كانت مصفوفة (Array) أو قائمة مرتبطة (Linked List). بعد ذلك، يوجّه النظام نموذجًا لغويًا كبيرًا لتوليد مجموعة متنوعة من التنفيذات، تمزج بين الأساليب التكرارية الذاتية والإجرائية عبر مهام تتعلق بالأعداد الصحيحة والمصفوفات والقوائم. تُختبر كل نسخة مرشحة على حدة، ثم يحاول خط الأنابيب تنفيذ عملية التحقق الشكلي على المجموعة الناتجة. وحين تفشل نسخة معينة، تُفعَّل حلقة إصلاح محدودة موجَّهة بملاحظات أداة التحقق (Verifier-Guided Repair)، تستخدم استجابة الأداة نفسها لتصحيح الشروح التوضيحية (Annotations) وإعادة المحاولة، بدل التخلص من النسخة الفاشلة كليًا.

الأرقام تتحدث

عند تطبيق النظام على مجموعة اختبار (Benchmark) تضم 73 مهمة تحقق أنتجت مجتمعة 292 نسخة تنفيذية، أكدت الجولة الأولى من التحقق صحة 96 نسخة فقط. لكن جولتين من الإصلاح الآلي رفعتا هذا الرقم إلى 154 نسخة، أي أن نسبة التحقق على مستوى النسخ المفردة (Artifact-Level) قفزت من 32.9% إلى 52.7%. تُعد هذه قفزة معتبرة في خطوة غالبًا ما تتطلب عملاً يدويًا شاقًا في كتابة الشروح التوضيحية.

الرقم الأكثر دلالة يظهر عند النظر إلى مستوى المهمة ككل. فبما أن خط الأنابيب يولّد عدة نسخ مرشحة لكل مهمة، يكفي نجاح نسخة واحدة فقط لاعتبار المهمة محلولة. وبهذا المقياس، نجحت 49 مهمة من أصل 73، بمعدل نجاح بلغ 67.1%، وهو رقم يتجاوز بوضوح ما حققته أي استراتيجية تعتمد على نسخة تنفيذية واحدة في نفس مجموعة الاختبار.

لماذا يهم هذا الأمر

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