VERINA: معيار جديد لتقييم توليد الشفرات القابلة للتحقق بواسطة نماذج اللغات الكبيرة
تُظهر نماذج اللغات الكبيرة (LLMs) أداءً قويًا في البرمجة، وقد تم تبنيها على نطاق واسع في أدوات مثل Cursor و GitHub Copilot لتعزيز إنتاجية المطورين. ومع ذلك، نظرًا لطبيعتها الاحتمالية، لا تستطيع نماذج اللغات الكبيرة تقديم ضمانات رسمية للشفرات التي يتم توليدها. غالبًا ما تحتوي الشفرات المُولدة على أخطاء، وعندما يتم اعتماد توليد الشفرات القائم على نماذج اللغات الكبيرة، يمكن أن تُصبح هذه المشاكل عائقًا للإنتاجية.
تحديات تطوير معايير قياسية لتوليد الشفرات القابلة للتحقق
يُعد تطوير معايير مناسبة لتتبع التقدم في توليد الشفرات القابلة للتحقق مهمًا ولكنه مُحتملاً، حيث يتضمن ثلاث مهام مترابطة: توليد الشفرة، وتوليد المواصفات، وتوليد البرهان. تفتقر المعايير الحالية إلى الدعم الكامل لهذه المهام الثلاث، بالإضافة إلى التحكم في الجودة، والمقاييس المُوثوقة، والتصميم النمطي.
قصور المعايير الحالية
تحقق معايير مثل HumanEval و MBPP تقدمًا جيدًا في توليد الشفرات القائمة على نماذج اللغات الكبيرة، لكنها لا تتعامل مع المواصفات أو البراهين الرسمية. تركز العديد من الجهود المُوجهة للتحقق على مهمة أو مهمتين فقط، وتفترض أن العناصر الأخرى سيتم توفيرها بواسطة البشر. تم تصميم DafnyBench و miniCodeProps لتوليد البراهين، بينما يقوم AutoSpec و SpecGen باستنتاج المواصفات والبراهين من الشفرات المكتوبة يدويًا.
توفر أنظمة إثبات النظريات التفاعلية، مثل Lean، هدفًا واعدًا لتوليد الشفرات القابلة للتحقق باستخدام نماذج اللغات الكبيرة، حيث تدعم بناء البراهين مع خطوات وسيطة. ومع ذلك، فإن معايير التحقق الحالية في Lean، مثل miniCodeProps و FVAPPS، لديها قيود في تغطية المهام والتحكم في الجودة.
VERINA: معيار شامل لتوليد الشفرة والمواصفات والبرهان
اقترح باحثون من جامعة كاليفورنيا و Meta FAIR معيار VERINA (Verifiable Code Generation Arena)، وهو معيار عالي الجودة لتقييم توليد الشفرات القابلة للتحقق. يتكون من 189 تحديًا برمجيًا مع أوصاف مُفصلة للمشاكل، والشفرات، والمواصفات، والبراهين، وأدوات الاختبار، كلها مُنسقة في Lean. تم بناء VERINA مع ضمان الجودة، حيث تم استخراج المشاكل من مصادر مثل MBPP و LiveCodeBench و LeetCode لتقديم مستويات صعوبة مُختلفة. تم مراجعة جميع العينات يدويًا وتنقيتها لضمان أوصاف واضحة باللغة الطبيعية، ومواصفات رسمية دقيقة، وتنفيذ دقيق للشفرات. تحتوي كل عينة على أدوات اختبار لتغطية السيناريوهات الإيجابية والسلبية، مع تغطية 100% لسطور تنفيذ الشفرة ونجاح مواصفات الحقيقة الأرضية.
بنية وتكوين مجموعة بيانات VERINA
تتكون VERINA من مجموعتين فرعيتين بمستويات صعوبة مُختلفة: VERINA-BASIC و VERINA-ADV. تحتوي VERINA-BASIC على 108 مشكلة مُترجمة من شفرة Dafny المكتوبة يدويًا. يتضمن ذلك 49 مشكلة من MBPP-DFY50 و 59 مثيلًا إضافيًا من CloverBench، تم ترجمتها باستخدام OpenAI o3-mini مع مطالبات قليلة اللقطات، متبوعة بالفحص. تحتوي VERINA-ADV على 81 مشكلة ترميز أكثر تقدمًا من مشاركات الطلاب في دورة إثبات النظريات، حيث قام الطلاب باستخراج المشاكل من منصات مثل LeetCode و LiveCodeBench، ثم قاموا بتشكيل الحلول في Lean. علاوة على ذلك، تستخدم VERINA ضمانًا صارمًا للجودة، بما في ذلك أوصاف مُفصلة للمشاكل، وتغطية كاملة للشفرات باختبارات إيجابية، ومعدلات نجاح اختبار كاملة على مواصفات الحقيقة الأرضية، إلخ.
نتائج الأداء: تقييم نماذج اللغات الكبيرة على VERINA
يكشف تقييم تسع نماذج من أحدث نماذج اللغات الكبيرة على VERINA عن تسلسل هرمي صعب واضح. يحقق توليد الشفرة أعلى معدلات النجاح، يليها توليد المواصفات، بينما يبقى توليد البرهان هو الأكثر تحديًا، مع معدلات نجاح أقل من 3.6% لجميع النماذج. تُعد VERINA-ADV أكثر صعوبة مقارنةً بـ VERINA-BASIC في جميع المهام الثلاث، مما يُبرز أن زيادة تعقيد المشكلة يؤثر بشكل كبير على أداء توليد الشفرات القابلة للتحقق. يُظهر التحسين التدريجي للبرهان مع o4-mini تحسنًا من 7.41% إلى 22.22% للمشاكل الأبسط على VERINA-BASIC بعد 64 تكرارًا، على الرغم من أن المكاسب محدودة على VERINA-ADV. يُعزز توفير مواصفات الحقيقة الأرضية توليد الشفرة، مما يُشير إلى أن المواصفات الرسمية يمكن أن تحدد وتوجه عملية التوليف بشكل فعال.
الخلاصة: VERINA يُحدد معيارًا جديدًا في تقييم الشفرات القابلة للتحقق
في الختام، قدم الباحثون VERINA، وهو تقدم في معيار تقييم توليد الشفرات القابلة للتحقق. يوفر 189 مثالًا مُنتقًى بعناية مع أوصاف مُفصلة للمهام، وشفرة عالية الجودة، ومواصفات في Lean، وأدوات اختبار واسعة النطاق مع تغطية كاملة للسطور. ومع ذلك، لا تزال مجموعة البيانات صغيرة نسبيًا لمهام ضبط النموذج الدقيق، مما يتطلب التوسيع من خلال التسمية التلقائية بمساعدة نماذج اللغات الكبيرة. يُركز VERINA على المهام البسيطة والمنفصلة المناسبة لمعيار القياس، ولكنها لا تمثل بشكل كامل مشاريع التحقق المعقدة في العالم الحقيقي. يمكن تحسين مقياس توليد المواصفات في المستقبل من خلال دمج مُثبتات أكثر قدرة، بما في ذلك تلك القائمة على نماذج اللغات الكبيرة أو حلالات SMT، للتعامل مع علاقات الصحة والاكتمال المعقدة بشكل فعال.
اترك تعليقاً