أعلنت أنثروبيك (Anthropic) أنها استخدمت نموذجها كلود (Claude) لإثبات صحة أكواد برمجية موجودة بالفعل بطريقة رياضية، بالتعاون مع شركة ثيورم (Theorem). النتيجة نحو 180 مليون سطر من كود الإثبات لـ 123 مكتبة مفتوحة المصدر خلال أسابيع قليلة، مع اكتشاف مئات الأخطاء التي فاتت الاختبارات التقليدية. الفكرة واعدة للمطورين، لكنها ما زالت بحثًا بشروط صارمة.
لماذا كان التحقق الرسمي نادرًا؟
التحقق الرسمي (Formal Verification) يعني إثبات رياضي بأن البرنامج يعمل بلا أخطاء ضمن ظروف محددة، وليس مجرد تجربته على عدة حالات. كانت هذه الطريقة مكلفة جدًا، فنواة نظام التشغيل الصغيرة seL4 احتاجت ما يعادل 20 سنة عمل لشخص واحد من المتخصصين، لذلك بقي الأسلوب محصورًا في حالات قصوى مثل برمجيات الطيران في إيرباص (Airbus).
كيف عمل Claude؟
تولى فريق Frontier Red Team في أنثروبيك المهمة مع ثيورم، وترك عمل الإثبات للنموذج. لم يكتب Claude كودًا جديدًا، بل حوّل اختبارات الانهيار من مكتبات في مشروع OSS-Fuzz الأمني التابع لجوجل (Google) إلى مسائل رياضية، وحلل الكود الآلي المترجم، ثم أنتج الإثباتات. يفحصها بعد ذلك برنامج مستقل اسمه Rocq تلقائيًا، وبحسب أنثروبيك فالعملية لا تحتاج تقريبًا إلى مراجعين بشريين. ومع ذلك فالأدوات والأسس الرياضية بناها بشر في ثيورم، فعبارة «مستقل تمامًا» لا تُؤخذ على إطلاقها.
ما الأخطاء التي اكتشفها؟
أثناء الإثبات وجد Claude مئات الأخطاء، وسُمح له بإصلاحها بنفسه. كثير منها لا يظهر إلا في ظروف نادرة، مثل ملفات إدخال ضخمة بشكل غير معتاد أو تسلسل معين من عمليات الوصول إلى الذاكرة. وفي محاولة لفحص قارئ PDF واسع الانتشار، وجد الفريق خلال أسبوع واحد ثغرات أمنية بقدر ما يُبلَّغ عنه عادة لهذا البرنامج طوال عام كامل. كما رصد خطأ منطقيًا في تطبيق آخر ظل مخفيًا أكثر من عشر سنوات. وحتى لو فشل الإثبات الكامل، تقول أنثروبيك إن المحاولة نفسها تكشف أخطاء حقيقية.
هل «موثّق رسميًا» تعني خاليًا من الأخطاء؟
لا، وأنثروبيك تقر بذلك. فالإثباتات تصح فقط تحت شروط محددة: معمارية معالج بعينها، وبرامج أحادية المسار (single-threaded)، ومدخلات أقل من 64 ميجابايت، بينما تعمل هذه المكتبات عمليًا على أجهزة وإعدادات مختلفة. والتكلفة الحاسوبية مرتفعة، إذ قد يستهلك الإثبات الواحد مئات الملايين من الرموز (tokens)، ولم تعلن الشركة التكلفة الإجمالية للمشروع. في المقابل تتحسن النماذج، فنموذج Opus 5.5 يحل نصف الإثباتات باستخدام رموز أقل بنحو 40% مقارنة بـ Opus 5. وتتوقع أنثروبيك أن يصبح التحقق الرسمي بالذكاء الاصطناعي عمليًا كالاختبار العادي قريبًا، وتستهدف خارطة طريق ثيورم بنية حرجة مثل glibc، OpenSSL، cURL.
ماذا يعني لك؟
إذا كنت مطورًا أو طالبًا، فالمشروع بحثي، ولم تُطرح بعد أداة أو سعر أو خطة اشتراك تتيح هذه الإمكانية للمطورين. فائدتك الحالية غير مباشرة: المكتبات مفتوحة المصدر التي تعتمد عليها تطبيقاتك قد تصبح أكثر أمانًا. ولمتابعة سلوك Claude في المسائل الحساسة، اقرأ تغطيتنا لسلوك Claude Opus في الأسئلة الأمنية، ولو تتابع تحركات الشركة فلدينا تقرير عن صفقة الحوسبة المرتقبة مع Nscale. وللمزيد من هذا الاتجاه تصفح قسم أدوات الذكاء الاصطناعي.
رأي ترقيتك
أرى أن الإنجاز الحقيقي هو خفض تكلفة الإثبات، وليس الأرقام الضخمة وحدها. لكن الشروط الضيقة تعني أن مراجعة الكود البشرية ستبقى ضرورية حاليًا، وهو ما نناقشه أيضًا في تقريرنا عن توظيف المبتدئين في Anthropic.
