في عالم البرمجة، يُعتبر التحقق من البرامج (Program Verification) أمرًا بالغ الأهمية لضمان صحة البرمجيات. ولكن، يبقى إنتاج برامج مُعتمدة بالكامل تحديًا في الممارسة العملية. في هذا السياق، يتناول بحث جديد تأثير هيكل التنفيذ على القدرة على التحقق التلقائي عندما يتم إنشاء برامج متعددة تهدف إلى تحقيق نفس المعاني على مستوى المهام.

تحت عنوان "تنوع للتحقق"، قدم الباحثون نظامًا مبتكرًا يسمى Diversify2Verify، وهو عبارة عن خط أنابيب قائم على نماذج اللغات الضخمة (Large Language Models) موجه للتحقق عبر منصة Why3. يقوم هذا النظام باستنتاج عقود محددة وفقًا للتمثيل، ويولد ويختبر تنوعًا من التنفيذات المتكررة والإمبراطورية للقوائم والمصفوفات، ويعمل على محاولة التحقق باستخدام إصلاح التوثيق الموجه بواسطة المُحقق.

تم بناء معيار التحقق مع 73 مهمة معنية بالأعداد الصحيحة والمصفوفات والقوائم، مما أسفر عن 292 نوعًا مختلفًا من التنفيذات. وقد تمكن النظام من التحقق من 96 عنصرًا في البداية و154 بعد عمليتين للإصلاح، مما أدى إلى تحسين مُعدل التحقق من 32.9% إلى 52.7%.

عند تقييم النتائج على مستوى المهام، تمكنت على الأقل نوع واحد من التحقق من 49 من أصل 73 مهمة، مما يدل على نسبة نجاح بلغت 67.1%.

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