أعلنت Anthropic أن نموذج Claude بات قادرًا على إنشاء براهين للتحقق الرسمي من الشيفرة الموجودة تلقائيًا. وفي اختبار شمل 123 مكتبة من مشروع OSS-Fuzz التابع لـGoogle، أنشأ Claude نحو 180 مليون سطر من البراهين خلال بضعة أسابيع. وفحص أداة التحقق Rocq هذه البراهين، وتقول Anthropic إن العملية لم تتطلب تقريبًا أي مراجعين بشريين.
ما الذي فعله النظام فعليًا؟
لم يكتب Claude برامج جديدة، بل حوّل حالات اختبار الأعطال إلى عبارات رياضية، وحلّل الشيفرة الآلية المترجمة، ثم أنشأ براهين رسمية على مطابقة الشيفرة لتلك العبارات. وعندما صادف النموذج خطأً، سُمح له بإصلاح الشيفرة بنفسه. وخلال أسبوع من فحص قارئ PDF شائع، اكتشف Claude عددًا من الثغرات الأمنية يساوي ما يُبلّغ عنه عادةً على مدار عام كامل. وفي مكتبة أخرى، عثر على خطأ منطقي ظل خفيًا لأكثر من عشر سنوات.
القيود والتكاليف
تحذّر Anthropic من أن البراهين لا تصح إلا لبرنامج أحادي الخيط يعمل على بنية معالج محددة، وبمدخلات يقل حجمها عن 64 ميغابايت. كما أن الحوسبة اللازمة مكلفة؛ إذ يتطلب كل برهان مئات الملايين من الرموز، لكن الشركة لم تكشف إجمالي الإنفاق. وأظهر اختبار أصغر أن نموذج Opus 5.5 الأحدث يستطيع إنجاز نصف البراهين باستخدام رموز أقل بنحو 40% من سلفه.
لماذا يهم
إذا استطاع الذكاء الاصطناعي التحقق من الشيفرة تلقائيًا، فقد يقل الوقت الذي يقضيه المطورون في البحث عن الأخطاء ومراجعة التعديلات، ولا سيما في البرمجيات الحساسة للسلامة. لكن النهج الحالي لا يعمل إلا ضمن قيود صارمة على العتاد والمدخلات، لذا تظل معظم التطبيقات اليومية بحاجة إلى الاختبارات التقليدية.
