TLA-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation
يقدم TLA-Bench معياراً اختبارياً قائماً على التنفيذ يتضمن 403 مواصفات تم التحقق منها برمجياً، وهو ما يكشف عن "غلاف صحة" واسع عند تقييم كود TLA الذي تولده النماذج اللغوية الكبيرة، مما يثبت أن النماذج الحالية تنتج مواصفات صالحة من الناحية التركيبية ولكنها غير صحيحة من الناحية الدلالية بشكل أكثر تكراراً مما تنتج مواصفات صحيحة حقاً.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تعلم روبوتاً كيفية كتابة وصفة لكعكة معقدة للغاية. تعطي الروبوت وصفاً مثل: "اصنع كعكة ترتفع، ولا تحترق، وتتكون من ثلاث طبقات بالضبط". يخرج الروبوت قائمة من التعليمات. الآن، كيف تعرف ما إذا كان الروبوت قد أدى عملاً جيداً حقاً؟ إذا اكتفيت بالتحقق مما إذا كانت التعليمات تبدو وكأنها وصفة حقيقية، فقد يخدعك الأمر؛ إذ يمكن للروبوت أن يكتب قصيدة جميلة تبدو كأنها وصفة، لكنها تخبرك أن "تأكل الفرن". وإذا طلبت من إنسان قراءتها فحسب، فقد يغفل عن خطأ صغير يتسبب في انفجار الكعكة.
هذا هو تحدي "التحقق الرسمي" (Formal Verification) في علوم الحاسوب. يتعلق الأمر بالتأكد من أن برامج الحاسوب تفعل بالضبط ما يُفترض بها فعله، دون أي مجال للخطأ. اللغة المستخدمة في هذه الورقة البحثية، والتي تسمى TLA+، تشبه كتاب وصفات رياضياً فائق الدقة للأنظمة المعقدة (مثل إشارات المرور أو خوادم الإنترنت). السؤال الكبير الذي يطرحه الباحثون هو: هل يمكن للذكاء الاصطناعي (AI) كتابة هذه الوصفات الرياضية المثالية بمجرد قراءة وصف باللغة الإنجليزية العادية؟ الإجابة مهمة لأننا إذا لم يستطع الذكاء الاصطناعي ضبط الرياضيات بشكل صحيح، فلن نتمكن من الوثوق به لتصميم أنظمة السلامة لتقنيات المستقبل.
"مقياس الحقيقة" لوصفات الذكاء الاصطناعي
قرر فريق من الباحثين من جامعة لويولا شيكاغو التوقف عن التخمين والبدء في الاختبار. لقد بنوا ملعباً جديداً يسمى TLA+-Bench. فكر فيه كأنه مطبخ ضخم ومؤتمت حيث يمكنهم اختبار ما إذا كانت الوصفات التي كتبها الذكاء الاصطناعي تعمل حقاً.
قبل هذه الورقة البحثية، كان التحقق مما إذا كان الذكاء الاصطناعي قد كتب مواصفات TLA+ جيدة يشبه الحكم على الكعكة من خلال النظر إلى الزينة (Frosting). كان الباحثون يتحققون مما إذا كان مخرج الذكاء الاصطناعي يشبه مثالاً كتبه بشر، أو ما إذا كان بإمكان الكمبيوتر قراءته (Parse). لكن المظهر الجميل لا يعني أن الكعكة لن تنهار. كانت الطرق القديمة سهلة للغاية وجعلت الذكاء الاصطناعي يبدو أذكى مما هو عليه في الواقع.
هذا المعيار الجديد مختلف. فهو يستخدم "مقياس حقيقة" يسمى Model Checker (مدقق النماذج). بدلاً من مجرد النظر إلى الوصفة، يحاول المقياس فعلياً "خبز الكعكة" في محاكاة. إنه يمر عبر كل خطوة ممكنة يمكن أن يتخذها النظام ليرى ما إذا كانت القواعد صامدة. إذا ارتكب الذكاء الاصطناعي خطأً، تنهار المحاكاة، ويقول مقياس الحقيقة: "كلا، هذا خطأ".
الاكتشاف الكبير: "غلاف الصحة" (Correctness Envelope)
أكثر شيء مفاجئ وجده الباحثون هو أنه لا يوجد رقم واحد فقط يخبرك بمدى جودة الذكاء الاصطناعي. الأمر أشبه بنطاق، وهو ما يسمونه Correctness Envelope.
تخيل أنك تطلب من ذكاء اصطناعي كتابة وصفة:
- الدرجة السهلة: إذا سألت فقط، "هل كتب الذكاء الاصطناعي شيئاً يبدو كأنه وصفة؟"، يحصل الذكاء الاصطناعي على نسبة نجاح 10%.
- الدرجة الأصعب: إذا سألت، "هل كتب الذكاء الاصطناعي وصفة تعمل حقاً عند محاولة خبزها؟"، تنخفض نسبة النجاح.
- الدرجة الأشد صعوبة: إذا سألت، "هل كتب الذكاء الاصطناعي وصفة تعمل وتفعل شيئاً مفيداً حقاً (وليس مجرد كعكة مملة وفارغة)؟"، تهبط نسبة النجاح إلى 1.7%.
تظهر الورقة البحثية أنه اعتماداً على مدى صرامتك في التصحيح، يمكن لدرجة الذكاء الاصطناعي أن تتأرجح بشكل كبير. إذا أخبرت الذكال الاصطناعي بالأسماء الدقيقة للمكونات التي يحتاجها، تقفز درجته إلى 18.7%. ولكن إذا جعلت الذكاء الاصطناعي يستنتج الأسماء بنفسه، تنخفض إلى 10%. وإذا طالبت بأن تقوم الوصفة بشيء معقد، تنخفض إلى 1.7%.
هذا يعني أن الدراسات السابقة، التي نظرت فقط إلى "الدرجة السهلة"، كانت كمن يعطي طالباً درجة امتياز (A+) لكتابة جملة تبدو كمسألة رياضية، حتى لو كانت الرياضيات خاطئة. يكشف المعيار الجديد أن الذكاء الاصطناعي يعاني حقاً في إجراء الرياضيات الفعلية.
النتائج: بارع في الكتابة، ضعيف في الحل
اختبر الباحثون عدة نماذج للذكاء الاصطناعي، بما في ذلك النماذج الضخمة والمتطورة (مثل GPT-5 و Claude Opus) وبعض النماذج مفتوحة المصدر. وهذا ما وجدوه:
- مشكلة "التظاهر": كان كل نموذج ذكاء اصطناعي أفضل بكثير في كتابة لغة TLA+ صحيحة نحوياً (Syntax يمكن للكمبيوتر قراءته) من كتابة لغة TLA+ صحيحة منطقياً (Logic يعمل بالفعل). أفضل ذكاء اصطناعي استطاع كتابة كود صحيح نحوياً بنسبة 87% من المرات، لكنه نجح في المنطق بنسبة 16% فقط. أما النماذج مفتوحة المصدر فكانت أسوأ بكثير، حيث حققت صحة منطقية بنسبة تقل عن 1%.
- منحدر الصعوبة: يصبح الذكاء الاصطناعي أسوأ بكثير كلما زادت صعوبة المهام. في المهام البسيطة والأساسية، حقق الذكاء الاصطناعي حوالي 25% من المهام بشكل صحيح. ولكن في المهام المتوسطة والمتقدمة، انهارت نسبة النجاح إلى 2%. الأمر يشبه طالباً يمكنه جمع 2+2 ولكنه يفشل تماماً عندما تطلب منه حل مسألة في التفاضل والتكامل.
- "لعبة الأسماء": حدث جزء كبير من الأخطاء بسبب خطأ الذكاء الاصطناعي في أسماء المتغيرات. إذا أعطيت الذكاء الاصطناعي أسماء المكونات (الواجهة/Interface)، فإنه يؤدي بشكل أفضل بكثير. هذا يشير إلى أن الذكاء الاصطناعي لا يفشل في فهم المنطق بقدر ما يفشل في تذكر الملصقات المحددة التي يحتاجها النظام.
لماذا يهم هذا الأمر
تخلص الورقة البحثية إلى أنه لا يمكننا الوثوق بالذكاء الاصطناعي لكتابة هذه الأنظمة الحساسة للسلامة بعد. يوضح "مقياس الحقيقة" أنه بينما يمكن للذكاء الاصطناعي محاكة مظهر المواصفات المثالية، فإنه غالباً ما يفشل في تجسيد واقع سلوك النظام.
لقد نشر الباحثون مجموعة البيانات الخاصة بهم، وأدوات "مقياس الحقيقة"، وجميع نتائج الاختبارات حتى يتمكن العلماء الآخرون من استخدامها. هم لا يقولون إن الذكاء الاصطناعي عديم الفائدة؛ بل يقولون إننا بحاجة إلى طريقة أفضل لقياسه. تماماً كما لا تسمح لروبوت بقيادة حافلة حتى يجتاز اختبار قيادة حقيقي، وليس مجرد اختبار كتابي، نحتاج إلى التأكد من أن الذكاء الاصطناعي يجتاز "اختبار التنفيذ" قبل أن نتركه يصمم أنظمة مستقبلنا. الفجوة بين "الظهور بمظهر صحيح" و"أن يكون صحيحاً" فجوة هائلة، وTLA+-Bench هو الأداة التي تقيس أخيراً مدى اتساع تلك الفجوة.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.