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