في عالم التكنولوجيا الحديثة، أصبح دور نماذج اللغات الضخمة (Large Language Models) بارزًا في تسهيل العديد من المهام اللغوية والفنية. ومع ذلك، لا يزال يتطلب كتابة مواصفات TLA+ الصحيحة — تلك اللغة الرسمية المستخدمة في التحقق من الأنظمة — مهارات وخبرات معينة، مما يحد من اعتمادها بشكل واسع في الصناعة.

أجرت دراسة حديثة تقييمًا شاملًا لـ 30 نموذجًا من نماذج اللغات الضخمة عبر ثمانية عائلات، مستخدمةً مجموعة بيانات تتضمن 205 مواصفات TLA+. تم اختبار 25 نموذجًا مفتوح الوزن باستخدام أربع استراتيجيات مختلفة للإشارة، بالإضافة إلى 5 نماذج خاصة تحت نماذج التوجيه القليلة.

أبرزت نتائج الدراسة أن النماذج حققت دقة تركيبية تصل إلى 26.6%، ولكن لم تتجاوز دقتها الدلالية 8.6%، حيث كانت النجاحات مرتبطة بشكل حصري مع طرق الإشارة التقدمية. من المدهش أن حجم النموذج لم يكن مؤشرًا موثوقًا للجودة، فمثلاً تمكّن نموذج DeepSeek r1:8b من التغلب على نسخة 70B في جميع الاستراتيجيات، مما يشير إلى أهمية توافق التفكير عند التعامل مع اللغات الرسمية.

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

بناءً على هذه النتائج، توضح الدراسة أن نماذج اللغات الضخمة الحالية لا تستطيع إنتاج مواصفات TLA+ موثوقة دون إشراف خبراء، مما يفتح المجال لمزيد من الأبحاث والتطور في هذا المجال. للمزيد من المعلومات، تم توفير إطار التقييم، الشيفرة، ومجموعة البيانات لدعم التكرار والبحوث المستقبلية.