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

لملء هذه الفجوة، تم تقديم إطار VCoT-Lift الذي يرفع مستوى التفكير المنطقي من أدوات الحلول إلى خطوات تحققية واضحة للإنسان. من خلال الكشف عن الإسناد المنطقي للأداة كمجموعة من خطوات التفكير التي تعتمد على التحقق، يوفر VCoT-Lift أساسًا حقيقيًا لتقييم دقيق.

بناءً على VCoT-Lift، يتم إدخال VCoT-Bench - معيار شامل يتضمن 1988 مهمة لإتمام عملية VCoT بهدف تقييم قدرة نماذج اللغات الضخمة على فهم عملية التحقق بالكامل. يقيس VCoT-Bench الأداء عبر ثلاثة أبعاد رئيسية: صلابة في مواجهة مستويات مختلفة من الإثباتات المفقودة، وكفاءة عبر أنواع مختلفة من الإثباتات، وحساسية لمواقع الإثباتات.

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