ملخص تقني: BODHI: استنتاج دقيق لمواصفات نواة نظام التشغيل

بيان المشكلة

يعد التحقق الرسمي من نوى أنظمة التشغيل (OS kernels) أمراً بالغ الأهمية للأنظمة الحرجة للسلامة، ولكنه يواجه عقبة تتمثل في الجهد اليدوي المطلوب لبناء مواصفات رسمية دقيقة. وبينما أظهرت النماذج اللغوية الكبيرة (LLMs) كفاءة في توليد الأكواد البرمجية العامة، إلا أن قدرتها على تخليق المواصفات الرسمية لنوى أنظمة التشغيل لا تزال محدودة. وقد كشف معيار OSV-Bench، الذي يقيم عملية تحويل تنفيذ استدعاءات النظام بلغة C إلى مواصفات حالة (state-machine) بلغة بايثون وZ3، عن فجوة أداء كبيرة: حيث كانت أفضل درجة Pass@1 مسجلة بين 12 نموذجاً تم تقييمها هي 55.10% فقط.

تنشأ هذه الفجوة من أربعة تحديات رئيسية:

1. تعقيد السياق الطويل: تحتوي المطالبات (prompts) على ما يقرب من 26 ألف رمز (token)، بما في ذلك النماذج البرمجية، والأمثلة، والكود المستهدف.
2. الفجوة الدلالية: تتطلب المهمة ترجمة كود نواة C الإجرائي (imperative) إلى مواصفات بايثون/Z3 التصريحية (declarative)، وهو ما يتضمن نماذج برمجة مختلفة جوهرياً.
3. تداخل الاهتمامات: غالباً ما يخلط كود C بين منطق ما قبل الشرط (التحقق من الأخطاء) ومنطق ما بعد الشرط (تغيير الحالة)، والتي يجب فصلها بصرامة في المواصفات الرسمية.
4. المعرفة المتخصصة بالمجال: تتضمن واجهات برمجة تطبيقات النواة (Kernel APIs) أنماطاً متخصصة (مثل صيغ مدخلات جدول الصفحات، ودلالات عد المراجع، وعمليات إفراغ TLB) التي لا تغطيها تدريبات النماذج اللغوية الكبيرة للأغراض العامة.

المنهجية: BODHI

يقترح المؤلفون BODHI، وهي طريقة لتعزيز المطالبة بالمعرفة بالمجال عبر تعزيز مطالبات "التعلم من أمثلة قليلة" (few-shot) القياسية بـ دليل ترجمة من C إلى بايثون مهيكل. وخلافاً لأساليب سلسلة الأفكام (CoT) أو سلسلة الأفكار المهيكلة (SCoT) التي تركز على توليد خطوات الاستدلال الوسيطة، يقوم BODHI بحقن مواد مرجعية مهيكلة في سياق المدخلات.

هيكل المطالبة

تحتفظ مطالبة BODHI بالمكونات الأربعة لمعيار OSV-Bench الأساسي:

1. المطالبة بالنظام (التعليمات).
2. النموذج البرمجي (تعريفات الفئات، والثوابت، والدوال).
3. خمسة أمثلة قليلة (أزواج من تنفيذ C ومواصفات Z3).
4. المهمة المستهدفة (الوصف الوظيفي وكود C).

يضيف BODHI مكوناً خامساً: وهو دليل ترجمة مكون من 519 سطراً يتم إدراجه بين الأمثلة القليلة والمهمة المستهدفة. يهدف هذا الوضع إلى الاستفادة من "تأثير الحداثة" (recency effect) في انتباه المحولات (transformer attention)، مما يضمن سهولة الوصول إلى الأنماط الخاصة بالمجال أثناء عملية التوليد.

تصميم دليل الترجمة

تم تنظيم الدليل في 15 فئة مستمدة من تحليل تكراري للإخفاقات في نموذج متوسط المستوى (Claude Haiku 4.5). ويتبع الدليل مبدأ فصل الاهتمامات، حيث يميز بين استخراج ما قبل الشرط وتوليد ما بعد الشرط. تم تقسيم الفئات إلى ثلاث طبقات:

• الطبقة الأولى (بنيوية/Syntax): تغطي قوالب المواصفات، وترجمة ما قبل الشرط (نفي عمليات التحقق من أخطاء C)، وأنماط ما بعد الشرط، وبنية حقول الخرائط (التمييز بين القراءة () والكتابة [])، وقواعد المعاملات، وبادئات الثوابت.
• الطبقة الثانية (دلالات المجال): تغطي صيغ مدخلات جدول الصفحات (PTE) (التمييز بين x86 وIOMMU)، والبيانات الوصفية الظلية (shadow metadata)، وعد المراجع، وعمليات إفراغ TLB، وأسماء مؤشرات الحالة، وتعيين أسماء الحقول.
• الطبقة الثالثة (الاكتمال): تعالج توسيع الدوال المساعدة في C، وجرد المساعدات المتاحة، وأنماط آلة الحالة المعقدة لـ IPC.

من الأهمية بمكان أن الدليل يعمل كـ "كتاب مدرسي للمجال" يحتوي على قواعد ترجمة عامة وأنماط توضيحية، وليس حلولاً خاصة بالمهمة أو أكواداً كاملة.

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

1. دليل ترجمة متخصص بالمجال: دليل مهيكل من 15 فئة يغطي أنماط الترجمة من C إلى Python/Z3 مستمدة من مواصفات حقيقية موثقة.
2. تقييم شامل: الاختبار عبر تسعة نماذج من ستة مزودين (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba)، تغطي البنى الكثيفة، وبنى خليط الخبراء (MoE)، وبنى الاستدلال.
3. تحليل الأخطاء: تفصيل دقيق يوضح أن BODHI يقلل من الأخطاء البنيوية والدلالية، مع التأثير الأكبر على النماذج متوسطة المستوى التي تمتلك قدرات اتباع التعليمات ولكنها تفتقر إلى المعرفة المحددة بالمجال.
4. رقم قياسي جديد: تحقيق درجة Pass@1 تبلغ 96.73% على OSV-Bench، متجاوزاً بشكل كبير أفضل نتيجة سابقة بلغت 55.10%.

النتائج

• مكاسب الأداء: حقق BODHI تحسينات في درجات Pass@1 لـ كل نموذج تم اختباره، حيث تراوحت الزيادات بين +11.0% (Qwen3) و +31.8% (Devstral 2).
• الأداء الأعلى: حققت تهيئة Claude Opus 4.6 + BODHI نسبة 96.73%، حيث فشلت في 8 مهام فقط من أصل 245 مهمة.
• تقليل الأخطاء:
  • الأخطاء البنيوية (Syntax Errors): قلل BODHI بشكل كبير من الأخطاء البنيوية، لا سيما عدم تطابق الأنواع/الأنواع (type/sort mismages) وإساء استخدام الواجهة البرمجية (مثل استخدام الأقواس للخرائط الكتابية). بالنسبة لـ Devstral 2، انخفضت الأخطاء البنيوية من 31.0% إلى 8.2%.
  • الأخطاء الدلالية (Semantic Errors): عالج الدليل بفعالية أخطاء الأنماط الدلالية (مثل صيغ PTE غير الصحيحة) وأخطاء منطق الترجمة. بالنسبة لـ Claude Opus 4.6، كانت إخفاقات المعيار الأساسي تنحصر تقريباً في أخطاء الأنماط الدلالية؛ وقد خفضها BODHI إلى 2.4%.
• استقلالية النموذج: كانت التحسينات متسقة عبر مختلف البنى والمزودين، مما يشير إلى أن التقنية ليست مرتبطة بعائلة محددة من النماذج.
• تحسين النماذج متوسطة المستوى: لوحظت أكبر المكاسب النسبية في النماذج متوسطة المستوى (مثل Devstral 2 و Claude Haiku 4.5)، والتي تمتلك قدرة كافية على اتباع التعليمات لاستخدام الدليل ولكنها تفتقر إلى المعرفة الجوهرية بالمجال التي تمتلكها النماذج رفيعة المستوى.

الأهمية والادعاءات

يزعم البحث أن حقن المعرفة بالمجال هو تقنية مستقلة عن النموذج تعمل بفعالية على سد الفجوة بين توليد الكود العام وتخليق المواصفات الرسمية. ويرى المؤلفون أن العائق في التحقق من نواة نظام التشغيل ليس قدرة النموذج اللغوي على الاستدلال (حيث إن النماذج المحسنة للاستدلال مثل o1 و DeepSeek-R1 لم تتفوق على النماذج القياسية المتبعة للتعليمات)، بل هو نقص معرفة الترجمة المحددة.

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