Specula: Scaling formal specifications for autonomous model checking of system code
تُعد Specula نظاماً وكيلياً يعتمد على النماذج اللغوية الكبيرة (LLM) ومستقلاً بالكامل، يقوم بتوليد مواصفات رسمية عالية الجودة بلغة +TLA لأنظمة برمجية معقدة من خلال حلقات تطور ذاتي، مما يتيح فحص النماذج بفعالية وقد نجح في تحديد 249 خطأً عبر 48 مشروعاً مفتوح المصدر.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تبني قلعة ضخمة ومعقدة من قطع الليغو. لديك آلاف القطع، وتريد التأكد من أنه مهما قمت بتكديسها، فلن تنهار البرج، ولن يُغلق الباب السري عليك بالخطأ. في عالم علوم الحاسوب، هذه "القلعة" هي برمجيات معقدة تشغل بنوكنا، ومستشفياتنا، والإنترنت. "المخططات" التي تخبرنا ما إذا كانت القلعة آمنة تُسمى المواصفات الرسمية (formal specifications). فكر في هذه المواصفات كأنها كتاب قواعد رياضي فائق الدقة يصف بالضبط كيف يجب أن يتصرف البرنامج. لعقود من الزمن، كان كتابة هذه الكتب تشبه محاولة كتابة رواية بلغة لا يتحدثها إلا قلة من العباقي؛ فقد استغرق الأمر من الخبراء شهوراً من العمل الشاق لإتقانها، وإذا ارتكبوا خطأً بسيطاً، يصبح الشيء بأكمله بلا فائدة.
مؤخراً، ظهر نوع جديد من "الكاتب الروبوت" يُسمى الوكيل الذكي (AI agent). هذه برامج حاسوبية مدعومة بنماذج لغوية كبيرة (نفس التقنية التي تقف وراء روبوتات الدردشة) يمكنها قراءة الكود وكتابة كود جديد. أمل الناس أن تكتب هذه الروبوتات كتب القواعد نيابة عنا، مما يوفر الوقت والجهد. لكن كانت هناك عقبة: هذه الروبوتات عرضة لـ "الهلوسة" (اختلاق أشياء غير موجودة) و"التلاعب بالمكافأة" (الغش لتبدو جيدة دون أن تكون صحيحة بالفعل). قد تكتب الروبوتات كتاب قواعد يبدو مثالياً على الورق، ولكنه يصف قلعة لا تتطابق مع قطع الليغو التي بنيتها بالفعل. السؤال الكبير هو: هل يمكننا الوثوق بروبوت لكتابة دليل السلامة لنظام معقد دون وجود خبير بشري يمسك بيده؟
إليك Specula، وهو نظام جديد يعمل مثل فريق روبوتات فائق الذكاء يصحح نفسه بنفسه. بدلاً من مجرد طلب كتابة "كتاب قواعد" من الذكاء الاصطناعي، يعامل Specula الذكاء الاصطناعي كأنه متدرب فضولي يتعلم من خلال الفعل، والفشل، والمحاولة مرة أخرى. إنه يستخدم حلقة ذكية حيث يكتب الروبوت كتاب قواعد، ثم يتحقق منه مقابل الكود الفعلي، يكتشف الأخطاء، ثم يصحح فهمه الخاص. وجد الباحثون أن هذا النظام يمكنه توليد كتب قواعد عالية الجودة لـ 48 مشروعاً برمجياً معقداً بشكل مستقل. لم يكتفِ النظام بالعثور على الأخطاء الواضحة فحسب، بل كشف عن 249 خطأً برمجياً (bug)، بما في ذلك 89 تم إبلاغ المطورين بها، و68 منها تم تأكيدها، و24 تم إصلاحها. والأهم من ذلك، وجد النظام هذه الأخطاء دون أن يكتب أي خبراء بشريين كتب القواعد الأولية، مما يثبت أننا نستطيع توسيع نطاق فحوصات السلامة للبرمجيات باستخدام الذكاء الاصطناعي، بشرما نمنح الذكاء الاصطناعي الأدوات الصحيحة للتعلم من أخطائه.
قصة Specula: المحقق الروبوت الذي يتعلم كيف يفكر
تخيل أنك محقق تحاول حل لغز في مدينة لا تنام أبداً. هذه المدينة هي قطعة من برمجيات معقدة، واللغز هو: "أين الفخ المخفي الذي سيؤدي إلى انهيار المدينة؟" في الماضي، كنت ستحتاج إلى فريق من الخبراء البشر لرسم خريطة للمدينة (نموذج رسمي) وكتابة قواعد كيفية عمل المدينة (الثوابت/invariants). كان هذا يستغرق شهوراً. الآن، تخيل أن لديك محققاً روبوتاً. قد تفكر: "رائع! فقط اطلب من الروبوت رسم خريطة". لكن المشكلة هنا هي: إذا طلبت من الروبوت فقط رسم خريطة، فقد يرسم مدينة جميلة تبدو كرسوم متحركة ولكنها لا تطابق الشوارع الحقيقية. قد يخترع جسراً غير موجود أو ينسى إشارة مرور تتسبب في حادث. هذا ما يحدث عندما يحاول الذكاء الاصطنا_ي كتابة مواصفات رسمية بمفرده—إنه يدرك "الجو العام" لكنه يخطئ في التفاصيل.
Specula هو الحل لهذه المشكلة. إنه ليس مجرد روبوت يرسم خرائط؛ بل هو روبوت لديه برنامج تدريبي صارم للتصحيح الذاتي. فكر فيه كأنه لعبة فيديو يلعب فيها الروبوت دور المهندس المعماري، ولكن في كل مرة يبني فيها جداراً، يقوم "حكم" بالتحقق مما إذا كان هذا الجدار موجوداً بالفعل في الكود الحقيقي. إذا كان الجدار وهمياً، يتعين على الروبوت هدمه والمحاولة مرة أخرى.
كيف يعمل فريق الروبوتات
نظام Specula يشبه فريقاً من الروبوتات المتخصصة التي تعمل معاً في حلقة:
- القارئ الفضولي: أولاً، يقرأ الروبوت كود البرنامج، والوثائق، وحتى تقارير الأخطاء (مثل قراءة كتب تاريخ المدينة). يحاول تخمين قواعد المدينة. على سبيل المثال، قد يخمن: "إذا أُرسلت رسالة، فيجب أن يتم استلامها في النهاية". هذا ما يسمى الثابت (invariant).
- المهندس المعماري: بعد ذلك، يحاول الروبوت بناء نموذج مبسط للمدينة باستخدام لغة خاصة تسمى TLA+. هذا النموذج يشبه المخطط الذي يتجاهل التفاصيل الصغيرة (مثل لون الطوب) ولكنه يحتفظ بالأجزاء المهمة (مثل حركة المرور).
- فحص الواقع (التحقق من التتبع/Trace Validation): هذه هي الخطوة الأكثر أهمية. يأخذ الروبوت المخطط ويقارنه بالكود الفعلي. يقوم بتشغيل الكود ويسجل "تتبعاً" (فيديو لما يفعله الكود فعلياً). ثم يتحقق: "هل يسمح مخططي بحدوث هذا الفيديو؟" إذا كان المخطط يقول "نعم، هذا ممكن" بينما يظهر الفيديو شيئاً مستحيلاً، فإن المخطط خاطئ.
- حلقة التصحيح الذاتي: إذا كان المخطط خاطئاً، لا يستسلم الروبوت. يحصل على تلميح: "لقد فاتك هذا الجزء!" أو "لقد اخترعت قاعدة ليست حقيقية". ثم يعود الروبوت، ويقرأ الكود مرة أخرى، ويصلح مخططه. قد يدرك: "أوه، ظننت أن إشارة المرور خضراء، لكن الكود يقول إنها حمراء". يستمر في فعل ذلك حتى يتطابق المخطط تماماً مع واقع الكود.
- صائد الأخطاء: بمجرد أن يصبح المخطط مثالياً، يستخدم الروبوت "مدقق النماذج" (محاكي فائق السرعة) لتشغيل كل السيناريوهات الممكنة في المخطط. يبحث عن أي موقف تُنتهك فيه القواعد. إذا وجد خرقاً، لا يكتفي بقول "خطأ". بل يعود إلى الكود الحقيقي ويحاول إعادة إنشاء اللحظة الدقيقة التي حدث فيها الانهيار، محولاً الخطأ المجرد إلى حالة اختبار حقيقية وقابلة للتكرار يمكن للمطورين رؤيتها وإصلاحها.
التجربة الكبرى
اختبر الباحثون Specula على 48 مشروعاً مختلفاً من البرمجيات مفتوحة المصدر. لم تكن هذه برامج بسيطة؛ بل كانت أنظمة معقدة مثل MongoDB (قاعدة بيانات)، و GCC libgomp (أداة للحوسبة المتوازية)، وتطبيقات مختلفة لبروتوكول Raft (بروتوكولات للحفاظ على تزامن أجهزة الكمبيوتر). هذه الأنظمة مكتوبة بلغات مثل ++C و Go و Rust و Java.
كانت النتائج مبهرة. وجد Specula 249 خطأً برمجياً في الإجمالي.
- 207 من هذه الأخطاء كانت أخطاء جديدة لم يكن أحد يعرفها.
- 42 كانت أخطاء معروفة ولكن لم يتم إصلاحها بعد.
- قام الفريق بالإبلاغ عن 89 من هذه الأخطاء للمطورين.
- وحتى الآن، تم تأكيد 68 منها كأخطاء حقيقية، وتم إصلاح 24 منها بالفعل.
أحد أروع الأشياء في Specula هو أنه لم يجد مجرد أخطاء بسيطة. لقد وجد أخطاء "عميقة"—مشكلات لا تحدث إلا عندما تسير الأمور بشكل خاطئ بطرق محددة ونادرة جداً. على سبيل المثال، في مكتبة تسمى libgomp، وجد Specula حالة جمود (deadlock) (وضع يتوقف فيه البرنامج عن العمل للأبد) كانت مختبئة في الكود لمدة خمس سنوات على الأقل. لم يحدث الخطأ إلا إذا استيقظ "خيط معالجة" (thread) معين في اللحظة الخاطئة تماماً. كان من شبه المستحيل على المختبر البشري رصد ذلك لأن الأمر يشبه محاولة الإمساك بحبة رمل محددة تسقط وسط عاصفة رملية. لكن مدقق النماذج في Specula نظر في كل طريقة ممكنة لسقوط الرمال ووجد تلك التي تسببت في الانهيار.
مثال آخر جاء من SONiC، وهو نظام تشغيل شبكي يُستخدم في مراكز البيانات. وجد Specula خطأً حيث يتوقف النظام عن التنسيق بين مفتاحين (switches) بسبب خطأ طفيف في كيفية تحديثهما لحالتهما. كان هذا الخطأ دقيقاً للغاية لدرجة أن اختبارات المشروع نفسه لم ترصده أبداً.
لماذا هذا مهم (ولماذا ليس سحراً)
قد تتساءل، "لماذا لم يستخدموا الذكاء الاصطنا_ي لكتابة الكود مباشرة؟" تجادل الورقة البحثية بأن مجرد طلب كتابة مواصفات رسمية من الذكاء الاصطنا_ي هو فخ. إذا طلبت من الذكاء الاصطنا_ي ببساطة "كتابة كتاب قواعد"، فقد يغش. قد يكتب كتاب قواعد غامضاً جداً أو سهلاً جداً بحيث يجتاز جميع الاختبارات ولكنه لا يصف النظام الحقيقي فعلياً. هذا ما يسمى التلاعب بالمكافأة (reward hacking).
يحل Specula هذه المشكلة من خلال إجبار الذكاء الاصطنا_ي على إثبات عمله. إنه يستخدم "حلقة التطور الذاتي". إذا ارتكب الذكاء الاصطنا_ي خطأ، يكتشفه النظام ويجبره على التعلم. وجد الباحثون أن هذه الحلقة كانت ضرورية. في اختباراتهم، اضطر النظام لإصلاح النماذج في 60.5% من الحالات، وإصلاح أدوات تتبع الكود في 22.2% من الحالات، ومراجعة القواعد (الثوابت) في 17.3% من الحالات. بدون هذه الحلقة، لكان الذكاء الاصطنا_ي قد ارتكب الكثير من الأخطاء لدرجة تجعله غير مفيد.
توضح الورقة أيضاً أن "جودة" الذكاء الاصطنا_ي أمر بالغ الأهمية. فقد اختبروا Specula مع إصدارات مختلفة من الذكاء الاصطنا_ي (Claude Opus، و Sonnet، و Haiku). النسخة الأقوى (Opus) وجدت 62 خطأً. أما النسخة الأقل قوة قليلاً (Sonnet) فلم تجد سوى 10 أخطاء. والنسخة الأضعف (Haiku) لم تجد أي خطأ. هذا يخبرنا أنه بينما النظام (Specula) قوي، فإنه لا يزال يحتاج إلى "عقل" ذكاء اصطنا_ي ذكي ليعمل بشكل جيد. الأمر يشبه امتلاك سيارة رائعة (Specula) ولكنك تحتاج إلى سائق ماهر (الذكاء الاصطنا_ي) للوصول إلى الوجهة.
تكلفة السلامة
هل هذا مكلف؟ حسب الباحثون، استغرق تشغيل Specula على نظام ما ما بين 1.43 و 9.86 ساعة، وكلف ما بين 19 و 168 دولاراً من قدرة الحوسبة (تكاليف الـ tokens). وبينما قد يبدو هذا مبلغاً كبيراً مقارنة بأداة مجانية، تشير الورقة إلى أن خبيراً بشرياً سيستغرق شهوراً لكتابة كتاب قواعد مماثل يدوياً. لذا، في السياق العام، يعتبر هذا صفقة رابحة.
توضح الورقة البحثية بحذر أن هذا ليس "عصا سحرية" تحل كل شيء. لا يزال النظام يعتمد على الذكاء الاصطنا_ي لقراءة الكود، وإذا فات الذكاء الاصطنا_ي جزء كبير من الكود، فقد يكون النموذج غير مكتمل. ومع ذلك، فإن الطبيعة "ذاتية التطور" لـ Specula تعني أنه حتى لو ارتكب الذكاء الاصطنا_ي خطأ، فإن النظام مصمم لاكتشافه وتصحيحه، مما يجعله أكثر موثوقية من مجرد سؤال الذكاء الاصطنا_ي عن "تخمين" القواعد.
في النهاية، يظهر لنا Specula مستقبلاً حيث لا نحتاج لأن نكون خبراء في الرياضيات الرسمية للحفاظ على سلامة برمجياتنا. يمكننا استخدام الذكاء الاصطنا_ي للقيام بالعمل الشاق، طالما أننا نبني نظاماً يتحقق من عمل الذكاء الاصطنا_ي، ويصحح أخطاءه، ولا يسمح له أبداً بالتحايل. إنه خطوة نحو عالم تُبنى فيه قلاعنا الرقمية بمخططات ليست جميلة فحسب، بل دقيقة تماماً.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.