نظام ذكاء اصطناعي مبتكر يظهر وعوداً في التحقق من البرمجيات الخالية من الأخطاء

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

يظهر Baldur، وهو حل هندسي بدقة، الذي يستغل قوة نماذج اللغات الكبيرة (LLMs) لتوليد الأدلة الرياضية تلقائياً. من خلال ضبط نماذج اللغات الكبيرة (LLMs) على محتوى رياضي واسع ولغة Isabelle/HOL المستخدمة في الأدلة، يخطو Baldur خطوة عملاقة نحو أتمتة ما كان يوماً ما مهمة شاقة. والنتيجة؟ نظام يعمل بالتوازي مع مثبتات النظريات للتحقق من صحة الرمج، مما يقلل بشكل كبير من هامش الخطأ.

في صميم نجاح Baldur تكمن الشراكة مع Thor، الأداة المسؤولة عن إنشاء البراهين تلقائيًا. يتمتع Thor بمعدل نجاح يبلغ 57%، ولكن عند دمجه مع Baldur، يحقق الاثنان دقة مذهلة تبلغ 65.7% في إنشاء البراهين. يوضح هذا الثنائي، المستوحى من الأساطير النوردية، الإمكانات الكبيرة للتحقق من البرمجيات المدعوم بالذكاء الاصطناعي.

التحديات في نماذج اللغات الكبيرة (LLMs)

أحد التحديات الرئيسية التي تواجه العمل مع نماذج اللغات الكبيرة (LLMs)، مثل ChatGPT، هو نقصها أحيانًا في الدقة. بدلاً من تنبيه المستخدمين، قد "تفشل بصمت"، مقدّمة نتائج خاطئة تبدو صحيحة. يعد معالجة هذه القضية أمرًا حاسمًا لضمان موثوقية البراهين التي ينشئها الذكاء الاصطناعي.

لم يكن تطوير Baldur أمراً هيناً، حيث استغرق عدة أشهر وجهداً تعاونياً مع Google. استخدمت Emily First، مؤلفة المشروع الرئيسية، Minerva، وهو نموذج لغوي كبير (LLM) تم تدريبه على مجموعة ضخمة من النصوص ذات اللغة الطبيعية. بعد ذلك، تم ضبط Minerva الدقيق على مجموعة بيانات ضخمة بحجم 118 جيجابايت من الأوراق العلمية والرياضية والمحتوى الويب الذي يحتوي على تعبيرات رياضية. ومع ذلك، كان العامل المميز هو ضبط Isabelle/HOL language الدقيق أكثر، مما مهد الطريق لتوليد أدلة رياضية شاملة.

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

مستقبل واعد للبرمجيات الخالية من الأخطاء

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

صرح يوريي برن، الأستاذ في كلية مانينغ لمعلومات وعلوم الحاسوب في جامعة ماساتشوستس أمهرست: "يركز عملنا على محاولة أتمتة كتابة هذه البراهين. يستخدم Baldur نماذج لغات كبيرة لتوليد برهان تلقائي لنظرية رياضية معينة، يمكن لمثبت النظرية التحقق منه لاحقًا.".

يعزى نجاح Baldur إلى الفريق المخلص الذي عمل بلا كلل على هذا المشروع. إلى جانب إيميلي فيرست، وساهم ماركوس رابي، الذي كان يعمل لدى جوجل في ذلك الوقت، وتاليا رينجر، الأستاذة المساعدة في جامعة إلينوي - أوربانا شامبين، بشكل كبير. وقد دعمت وكالة مشاريع الأبحاث المتقدمة (DARPA) والمؤسسة الوطنية للعلوم (NSF) هذا المشروع.

تقدم الحلول المبتكرة مثل Baldur الأمل بينما تواجه صناعة التكنولوجيا التعقيد المتزايد لأنظمة البرمجيات. ومع استمرار تطور ونضج قدرات الذكاء الاصطناعي، تظل إمكانات Baldur في دفع دقة البرمجيات إلى آفاق جديدة واعدة.