الذكاء الاصطناعي يعيد إحياء التحقق الشكلي في البرمجيات
في أعقاب تصاعد توليد البرمجيات بالذكاء الاصطناعي في الولايات المتحدة، أعلن مطلع العام ساندار بيتشاي، الرئيس التنفيذي لغوغل، أن نحو ٧٥ في المئة من البرمجيات الجديدة لدى الشركة تُولَّد بواسطة الذكاء الاصطناعي، بينما تشير بيانات داخلية لأنثروبيك إلى أن أكثر من ٨٠ في المئة من الأكواد المقبولة كتبت بواسطة كلود. ومع ذلك، أظهرت دراسة لشركة كود رابيت على ٤٧٠ مشروعًا مفتوح المصدر أن طلبات الإدخال المشتركة بالذكاء الاصطناعي تحمل متوسط أخطاء أعلى مرة ونصف من تلك البشرية. كما أعلنت أزيوم ماث في ٢٦ أكتوبر تحويل أطول برهان في تاريخ الرياضيات إلى ٤٣ مليونًا و١٠٠ ألف سطر قابل لفحص لين خلال ٢٤ يومًا، مع رصد ٣٤ خطأ في المنشور الأصلي، من بينها ثغرة عمرها أربعة عقود. هذه الفجوة الإنتاجية أعادت الاهتمام بالتحقق الشكلي، الذي يعود جذوره إلى ستينيات القرن الماضي في أوروبا عبر نظام أوتومات ومنهجيات توني هور، ثم أدوات مثل روك ومايكروسوفت لين. ويقوم على صياغة مواصفات دقيقة وإنتاج برهان يتحقق منه برنامج صغير. لكنه ظل مكلفًا، فمشروع نواة النظام إس إل ٤ استغرق نحو ٢٠ سنة عمل، وتقول آبل إن التحقق في مكتبات التشفير يكشف أخطاء جسيمة لكنه يبطئ تطوير البرمجيات. غيّر الذكاء الاصطناعي هذه المعادلة. ففي ورقة لباحثة الدكتوراه تشويوي صن من ستانفورد في أغسطس، اكتمل التحقق من مكتبة تشفير في ١١ ساعة و٤ دقائق وبتكلفة نحو ٤٦٧ دولارًا، مقابل ٨ أشهر لخمسة خبراء. وأطلقت أنثروبيك مع ثيوريم مشروعًا لفحص ١٢٣ مكتبة باستخدام كلود، أنتج نحو ١٨٠ مليون سطر إثبات وكشف مئات الأخطاء، بعضها لم تظهره اختبارات ضخمة. فيما توسعت هارمونيك بأداة أرسطو نحو التحقق من برامج لغة سي وتصميم الرقائق، ورصدت خللًا في وحدة لشركة تينسورداين. تسارعت الاستثمارات. فجمعت أربع شركات، من بينها أزيوم ماث التي أسستها كارينا هونغ، وهارمونيك التي شارك في تأسيسها فلاد تينيف، وأند تروث، وبرامانا لابز، أكثر من ٦٥٠ مليون دولار. وقد حصلت أند تروث على ٧٠ مليون دولار في أكتوبر، مستهدفة آلة تحقق عامة مبنية على لين وتزعم تسريعًا بمئة ضعف عبر الذكاء الاصطناعي ومئة ضعف إضافي عبر الأتمتة. أما برامانا فأمنت ٢٧ مليون دولار في يونيو لبناء قواعد شكلية في الضرائب والقانون والرعاية الصحية. وفي الصين، تفتح فرق جامعية وخصوصية نماذج قائمة على لين، مع تقدم لافت في إثباتات رياضية، فيما تزال المنتجات التجارية للحماية البرمجية في مراحلها الأولى. لكن التحقق الشكلي ليس ضمانًا مطلقًا. فهو يثبت التزام الكود بالمواصفات، لا صحة المواصفات ذاتها. ومع تسارع الهجمات المدعومة بالذكاء الاصطناعي، يتحول التحدي إلى من يكتب المواصفات ويحكم بصحتها، خصوصًا إذا تولت نماذج من الشركة نفسها كتابة الكود والإثبات. لذلك يرى خبراء، بينهم فيتاليك بوتيرين، أن الذكاء الاصطناعي المعزَز بالتحقق الشكلي قد يعيد توازن الدفاع، على أن يبقى الحكم النهائي والبشري في تحديد المخاطر والإشراف.
