VeriInteresting: An Empirical Study of Model Prompt Interactions in Verilog Code Generation

إليك ملخص تقني مفصل لورقة البحث بعنوان "VeriInteresting: دراسة تجريبية للتفاعلات بين النموذج والمطالبة (Model–Prompt) في توليد كود Verilog."

1. بيان المشكلة

أحدث التقدم السريع في النماذج اللغوية الكبيرة (LLMs) ثورة في توليد الأكواد البرمجية، لكن تطبيقها على لغات وصف العتاد (HDLs)، وتحديداً لغة Verilog، يواجه تحديات فريدة:

• الدلالات الصارمة (Strict Semantics): على عكس البرمجيات، يتطلب تصميم العتاد دقة في توصيل الإشارات، وقيود التوقيت، وإدارة التزامن. قد يبدو نموذج Verilog منطقياً في ظاهره ويعمل بشكل صحيح في المحاكاة المنعزلة، ولكنه قد يفشل بسبب حالات السباق (race conditions) أو انتهاكات التوقيت أثناء التصنيع أو التوليف (synthesis).
• ندرة البيانات: غالباً ما تكون تصميمات العتاد عالية الجودة مملوكة لجهات خاصة، مما يحد من توفر بيانات مفتوحة المصدر للضبط الدقيق (fine-tuning).
• تعقيد التقييم: لا يمكن التحقق من صحة Verilog بالكامل عبر اختبارات الوحدة (المحاكاة) وحدها؛ إذ يتطلب الأمر غالباً التحقق من التكافؤ الشكلي (formal equivalence checking)، وهو أمر مكلف حاسوبياً.
• الفجوة: من غير الواضح ما إذا كانت استراتيجيات المطالبة (prompting) الفعالة في هندسة البرمجيات (مثل: سلسلة الأفكام/Chain-of-Thought، أو المطالبة المهيكلة/structured prompting) تنتقل بفعالية إلى تصميم العتاد، أم أن الضبط الدقيق المتخصص في المجال ضروري تماماً.

2. المنهجية

أجرى المؤلفون دراسة تجريبية واسعة النطاق ومتحكم بها لتقييم 18 نموذج لغة عبر مجموعتين مختلفتين من معايير Verilog باستخدام تصميم تجريبي عاملي.

النماذج التي تم تقييمها

• النماذج التجارية (Commercial LLMs): 7 نماذج (مثل: GPT-4.1، GPT-5، Gemini 3، Claude Sonnet 4).
• النماذج الصغيرة مفتوحة المصدر (Open-Source SLMs): 11 نموذجاً، تشمل نماذج عامة (Qwen2.5)، ونماذج متخصصة في الكود (Qwen-Coder، DeepSeek Coder)، ونماذج متخصصة في Verilog (VeriReason، VeriThoughts) تم ضبطها بدقة عبر الضبط الدقيق الخاضع للإشراف (SFT) والتعلم التعزيزي (RL).
• النطاق: يتراوح من 3 مليار إلى 16 مليار معلمة (parameters).

معايير التقييم (Benchmarks)

1. Verilog Eval v2: يستخدم المحاكاة الديناميكية (Icarus Verilog) مع لوحات اختبار (testbenches) للتحقق من الصحة الوظيفية مقابل المخرجات المرجعية.
2. VeriThoughts: يستخدم التحقق من التكافؤ الشكلي (Yosys) لإثبات الهوية الوظيفية مقابل مرجع ذهبي لجميع حالات المدخلات.

استراتيجيات المطالبة (التكيف أثناء الاستدلال)

عزلت الدراسة تأثير تقنيات الاستدلال المختلفة:

• الأساس (Base): مطالبات بسيطة تمر بمسار واحد.
• المطالبة المهيكلة (Struct): فرض تواقيع مهام ومكونات نمطية ثابتة (عبر DSPy).
• سلسلة الأفكار (CoT): خطوات استدلال صريحة قبل توليد الكود.
• تحسين المطالبة (Refine): مسار من مرحلتين حيث يقوم نموذج لغوي بإعادة كتابة/توضيح المواصفات قبل توليد الكود.
• التعلم داخل السياق (ICL): إضافة أمثلة قليلة (few-shot) إلى المطالبة.
• النمط الجيني-باريتو (GEPA): طريقة بحث تطورية مؤتمتة لتحسين مطالبات النظام دون إعادة التدريب.

3. المساهمات الرئيسية

• خريطة تجريبية لتفاعلات النموذج والمطالبة: أول تقييم منهجي لكيفية تفاعل حجم النموذج، والتخصص في المجال، واستراتيجيات المطالبة خصيصاً لتوليد Verilog.
• مقارنة المعايير: أظهرت النتائج أن الأداء يختلف بشكل كبير بين المعايير القائمة على المحاكاة (Verilog Eval) والمعايير القائمة على التحقق الشكلي (VeriThoughts)، مما يسلط الض الضوء على خطر الإفراط في التخصيص (overfitting) لبروتوكول تقييم واحد.
• مقايضات الاستدلال مقابل التدريب: قدمت رؤى قائمة على البيانات حول ما إذا كانت "المطالبة القوية" يمكن أن تحل محل الضبط الدقيق المكلف والمتخصص في المجال.
• تحديد الهشاشة: أظهرت أن العديد من التقنيات الناجحة في البرمجيات (مثل تحسين المطالبة) قد تكون ضارة في العتاد بسبب الانحراف الدلالي (semantic drift).

4. النتائج الرئيسية

س1: الحجم مقابل التخصص

• التوسع (Scaling): تعمل النماذج الأكبر بشكل أفضل عموماً، لكن الاتجاه غير رتيب لبعض العائلات (على سبيل المثال، تفوق Qwen-3B على Qwen-7B في VeriThoughts).
• التخصص: تتفوق نماذج Verilog المتخصصة (VeriReason، VeriThoughts) في توزيعات تدريبها الخاصة، ولكنها تظهر تراجعاً في المتانة عند مواجهة تحويلات المطالبة المعقدة (مثل المخرجات المهيكلة أو سلسلة الأفكار).
• ملاحظة: غالباً ما يستبدل التخصص القدرة على اتباع التعليمات العامة بالأداء الذروي في توزيع مهمة ضيقة.

س2: الحساسية لاستراتيجيات المطالبة

• المطالبة المهيكلة: مفيدة بشكل عام للنماذج مفتوحة المصدر الصغيرة والمتخصصة في الكود، ولكن عوائدها تتناقص بالنسبة للنماذج التجارية رفيعة المستوى.
• سلسلة الأفكار (CoT): متغيرة للغاية. تعمل كمثبت للمطالبات المهيكلة في Verilog Eval، ولكن يمكن أن تقدم "افتراضات غير متحقق منها" تؤدي إلى تدهور الأداء في معايير التحقق الشكلي (VeriThoughts).
• تحسين المطالبة (Refine): هي التدخل الأقل استقراراً. إعادة كتابة المواصفات غالباً ما تؤدي إلى انحراف دلالي، مما يسبب انخفاضات كبيرة في الأداء (على سبيل المثال، فشلت نماذج GPT-5m ونماذج VeriThoughts عند طلب إعادة كتابة المواصفات).
• التعلم داخل السياق (ICL): ليس حلاً عالمياً. يساعد النماذج الصغيرة من خلال تثبيت تنسيقات المخرات، ولكنه قد يربك النماذج المتخصصة أو تلك ذات نوافذ السياق المحدودة.
• تحسين GEPA: حققت المطالبات المحسنة أداءً مقارباً للقواعد اليدوية القوية (Struct + CoT) ولكنها لم تحقق تحسينات جذرية، مما يشير إلى أن تطور المطالبة له حدود في هذا المجال.

س3: الضبط الدقيق مقابل المطالبة القوية

• يمكن لطرق وقت الاستدلال (المطالبة القوية) تقليص الفجوة مع النماذج المضبوطة بدقة بالنسبة للنماذج اللغوية العامة.
• ومع ذلك، يظل الضبط الدقيق متفوقاً عندما يتطابق التوزيع المستهدف مع هدف التدريب. على سبيل المثال، تفوقت نماذج VeriReason بشكل كبير على القواعد المعتمدة على المطالبة في Verilog Eval v2، مما يثبت أن التكيف في وقت التدريب لا يمكن استبداله في المهام المحددة وعالية الخطورة.

س 4: استقرار المعايير

• هناك ارتباط إيجابي قوي ($r=0.868$) بين المعيارين، ولكن Verilog Eval v2 أصعب بشكل منهجي من VeriThoughts بالنسبة للعديد من النماذج.
• النماذج التي تؤدي جيداً في المحاكاة (Verilog Eval) لا تترجم دائماً إلى نجاح في التحقق الشكلي، والعكس صحيح. الاعتماد على معيار واحد يمكن أن يؤدي إلى استنتاجات خاطئة حول موثوقية النموذج.

5. الأهمية والآثار المترتبة

• العتاد متميز: توليد Verilog ليس مجرد نوع من أنواع توليد البرمجيات. القيود الصارمة للعتاد (التوقيت، التزامن، الصحة الشاملة) تجعله أكثر حساسية للأخطاء الدلالية التي لا تستطيع تقنيات المطالبة القياسية حلها بسهولة.
• لا توجد استراتيجية "مقاس واحد يناسب الجميع": تعتمد الاستراتيجية المثلى بشدة على فئة النموذج المحدد ومعيار التقييم. الاستراتيجية التي تعزز نموذجاً صغيراً مفتوح المصدر قد تؤدي إلى انهيار نموذج متخصص.
• مقايضة المتانة مقابل الأداء: تحقق النماذج المتخصصة في المجال أداءً ذروياً عالياً ولكنها تفتقر إلى المتانة تجاه تغييرات المطالبة. أما النماذج العامة فهي أكثر قدرة على التكيف ولكنها تتطلب دعامات (scaffolding) أقوى.
• إرشادات النشر:
  • للنشر منخفض التكلفة: تعد المطالبة القوية (Structured + CoT) على نماذج مفتوحة المصدر قادرة خطوة أولى قابلة للتطبيق.
  • للعتاد عالي الضمان: يعد الضبط الدقيق المتخصص في المجال ضرورياً، ويجب أن يشمل التقييم كلاً من المحاكاة والتحقق الشكلي لضمان المتانة.
  • يجب استخدام تحسين المطالبة (Prompt Refinement) بحذر شديد في سياقات العتاد.

يعمل هذا العمل كدليل تأسيسي للباحثين والمهندسين الذين يهدفون إلى دمج النماذج اللغية في تدفقات تصميم العتاد، مع التأكيد على أن التحقق التجريبي عبر معايير متعددة أمر بالغ الأهمية قبل النشر.