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