VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
تقدم هذه الورقة VeriContest، وهو معيار شامل يضم 946 مسألة من مسائل البرمجة التنافسية بلغة Rust مع Verus، يربط بين الأوصاف اللغوية الطبيعية والمواصفات الرسمية المعتمدة من قبل الخبراء والبراهين القابلة للتحقق آلياً، مما يكشف عن فجوة كبيرة بين قدرات النماذج الحالية في البرمجة وقدرتها على توليد كود برمجي قابل للتحقق.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك توظف مهندساً معمارياً عبقرياً ولكنه يفتقر للخبرة لبناء منزل.
في عالم معايير البرمجة القياسية، تعطي المهندس وصفاً بسيطاً: "ابنِ منزلاً بثلاث غرف نوم ومطبخ". يقوم المهندس برسم المخططات، ويبني المنزل، ثم تتحقق أنت مما إذا كانت الأبواب تفتح والأضواء تعمل. إذا كانت تعمل، فإنه يحصل على درجة نجاح. هذا يشبه ما تفعله نماذج الذكاء الاصطناعي الحالية عند كتابة الكود: فهي بارعة في صنع أشياء تبدو صحيحة وتعمل بشكل صحيح.
ولكن ماذا لو كنت بحاجة إلى منزل مضمون رياضياً بأنه لن ينهار أبداً، حتى في حالة وجود إعصار؟ لا يمكنك فقط التحقق من الأضواء؛ بل تحتاج إلى برهان رسمي على أن الهيكل سليم. هنا يأتي دور ورقة بحثية بعنوان "VeriContest".
المشكلة: "إنه يعمل، ولكن هل هو حقيقي؟"
نماذج الذكاء الاصطناعي الحالية تشبه أولئك المهندسين المعماريين الموهوبين الذين يمكنهم بناء منزل يجتاز الفحص البصري. ومع ذلك، فإنهم غالباً ما يتجاهلون الرياضيات الهندسية الصارمة. قد يبنون منزلاً يبدو جيداً، ولكن به خلل خفي في الأساس لا يظهر إلا تحت ضغط معين.
يجادل مؤلفو هذه الورقة بأننا بحاجة إلى طريقة جديدة لاختبار الذكاء الاصطناعي. بدلاً من مجرد السؤال، "هل يعمل الكود؟"، نحتاج إلى السؤال: "هل يمكنك إثبات، بيقين رياضي، أن هذا الكود يفعل بالضبط ما يُفترض به فعله، ولا شيء غير ذلك؟"
الحل: VeriContest
أنشأ الفريق "امتحاناً" ضخماً يسمى VeriContest. اعتبره بمثابة مسابقة عالية المخاطر لمهندسي الذكاء الاصطناعي المعماريين، ولكن مع ثلاث قواعد صارمة:
- المخطط (المواصفات - Specification): يجب على الذكاء الاصطناعي أولاً كتابة عقد رياضي. هذا ليس مجرد وصف؛ بل هو مجموعة صارمة من القواعد التي تحدد بدقة ماهية المدخلات وما يجب أن تكون عليه المخرجات.
- البناء (الكود - Code): يجب على الذكاء الاصطناعي كتابة الكود الفعلي (بلغة البرمجة Rust) الذي يتبع تلك القواعد.
- البرهان الهندسي (التحقق - Verification): يجب على الذكاء الاصطناعي تقديم برهان رياضي يثبت أن الكود لا يمكن أن يفشل. إنه يشبه تقديم الرياضيات التي تثبت أن السقف لن يسقط، بدلاً من مجرد الأمل في ذلك.
لقد اختبروا هذا على 946 لغزاً صعباً مأخوذة من مسابقات برمجة شهيرة (LeetCode و Codeforces). هذه ليست مهام بسيطة مثل "Hello World"؛ بل هي مشكلات منطقية معقدة تتضمن أشياء مثل العثور على أنماط في البيانات أو تحسين المسارات.
عملية البناء
كان بناء هذا الامتحان صعباً. لم يكتفِ الفريق بطلب صنع الأسئلة من الذكاء الاصطناعي، بل بنوا العملية عبر ثلاث مراحل:
- المرحلة الأولى (البذرة - The Seed): كتب خبراء بشريون يدوياً 91 مثالاً مثالياً مع براهين خالية من العيوب.
- المرحلة الثانية (التوسع - The Expansion): استخدموا مساعد ذكاء اصطناعي لتوليد المزيد من المشكلات، ولكن عمل الخبراء البشريين كـ "محررين"، حيث قاموا بفحص كل واحدة منها للتأكد من صحة الرياضيات.
- المرحلة الثالثة (اختبار الضغط - The Stress Test): أنشأوا "حالات اختبار سلبية" (negative test cases)—وهي سيناريوهات مصممة لخداع الذكاء الاصطناعي. إذا كان برهان الذكاء الاصطناعي غير مكتمل، فإن هذه الأسئلة الخادعة ستكشف الخلل.
النتائج: فجوة هائلة
عندما مرروا أذكى نماذج الذكاء الاصطناعي في العالم عبر هذا الامتحان، كانت النتائج مفاجئة وصارخة.
- الاختبار "العادي": عندما طُلب منهم فقط كتابة كود من وصف (بدون براهين مطلوبة)، نجح أفضل ذكاء اصطناعي بنسبة 92%. إنه بناء ماهر.
- اختبار "المخطط": عندما طُلب منهم كتابة العقد الرياضي (المواصفات)، انخفضت النسبة إلى 48%. عانى الذكاء الاصطناعي في تحديد القواعد بدقة.
- اختبار "البرهان": عندما طُلب منهم تقديم البرهان الرياضي الذي يثبت عمل الكود، انهارت النسبة إلى 14%. لم يستطع الذكاء الاصطناعي القيام بالعمل الثقيل للرياضيات.
- "الامتحان الكامل" (من البداية للنهاية): عندما طُلب منهم القيام بالخطوات الثلاث معاً (المخطط + الكود + البرهان)، نجح أفضل ذكاء اصطناٍ فقط بنسبة 5.3%.
التشبيه: "المنزل المثالي"
تخيل أن الذكاء الاصطناعي هو طاهٍ (Chef).
- البرمجة القياسية: تطلب منه برجر. يصنع الطاهي برجر مذاقه جيد. تأكله. نجاح!
- البرمجة القابلة للتحقق: تطلب منه برجر، ولكنك تطلب أيضاً شهادة تثبت أن اللحم جاء من مزرعة محددة، وأن الخبز تم خبزه عند درجة حرارة 350 درجة بالضبط، وأن البرجر لا يحتوي على أي مسببات حساسية خفية. يمكن للطاهي صنع البرجر، لكنه سيء جداً في كتابة الشهادة أو إثبات الرياضيات وراء عملية الطهي.
الخلاصة
تخلص الورقة البحثية إلى أنه بينما أصبح الذكاء الاصطناعي جيداً جداً في "تخمين" الكود الصحيح لجعل البرنامج يعمل، إلا أنه لا يزال سيئاً جداً في إثبات صحة الكود. أكبر عقبة ليست كتابة الكود؛ بل هي كتابة القواعد الرسمية والبراهين الرياضية التي تضمن سلامة الكود.
تعد VeriContest الآن أداة للباحثين لقياس مدى المسافة التي يجب أن يقطعها الذكاء الاصطناعي قبل أن يمكن الوثوق به لبناء برمجيات مضمونة رياضياً بأنها خالية من الأخطاء.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.