Anthropic: Claude كتب براهين قابلة للتحقق آلياً للشيفرة المترجمة لـ123 مكتبة مفتوحة المصدر
استخدم فريق Frontier Red Team في Anthropic وشركة الأساليب الشكلية Theorem نموذج Claude لإثبات أن 239 نقطة دخول لاختبارات التشويش في 123 مكتبة من OSS-Fuzz لا يمكن أن تنهار مع مدخلات أقل من 64 ميغابايت في بيئة نمذجة. وكشف العمل أخطاء فاتت سنوات من اختبارات التشويش، لكن البراهين تحمل تحفظات مهمة.
نشرت Anthropic بحثاً استخدم فيه فريق Frontier Red Team التابع لها، بالتعاون مع شركة الأساليب الشكلية Theorem، نموذج Claude للتحقق رسمياً من خصائص أمنية في 123 مكتبة مفتوحة المصدر من مشروع OSS-Fuzz التابع لغوغل، تشمل 239 نقطة دخول لاختبارات التشويش. واللافت أن البراهين تتعلق بـشيفرة آلة RISC-V المترجمة وليس بالشيفرة المصدرية.
آلية العمل
حُوّل كل اختبار تشويش قائم إلى مواصفة رسمية: يجب ألا ينهار الاختبار المترجم (مثلاً بسبب خطأ ذاكرة يرصده AddressSanitizer أو فشل تأكيد) مع أي مدخل أقل من 64 ميغابايت في بيئة نمذجة. وفّرت Theorem نماذج رسمية لمجموعة تعليمات RISC-V وسلوك عمليات لينكس، وكتب Claude البراهين، وتحقق منها مدقق البراهين Rocq. ووفق DevOps.com أنتج Claude نحو 180 مليون سطر من البراهين خلال بضعة أسابيع.
أخطاء فاتت اختبارات التشويش
سُمح لـClaude بإصلاح الأخطاء التي صادفها، فظهرت المئات منها. ومن الأمثلة خطأ في عدّاد داخل أداة فك ضغط يؤدي إلى كتابة خارج حدود الذاكرة فقط مع مدخلات بحجم نحو 20 ميغابايت، وخطأ قراءة في مفكك صور يتطلب مدخلاً بحجم 64 ميغابايت. وتقول Anthropic إنها عاقبت التعديلات الكبيرة وراجعتها كي لا يعيد النموذج كتابة البرامج بطريقة تجعلها “لا تنهار أبداً” بشكل شكلي.
الحدود
تشدد Anthropic على أن “التحقق الرسمي” لا يعني “الخلو من الأخطاء”. فالبراهين تفترض ملفات RISC-V أحادية الخيط ومربوطة ستاتيكياً بمكتبة musl libc، بينما تعمل معظم برمجيات لينكس على x86 أو ARM مع glibc؛ كما أن AddressSanitizer لا يرصد كل أخطاء الذاكرة، ولم يُتحقق من كل نقاط الدخول. والتكلفة قيد آخر: قد تستهلك البراهين مئات الملايين من الرموز. وبيانات تحسّن كفاءة نماذج Claude الأحدث مصدرها اختبارات Anthropic الداخلية. ونُشر جزء من البراهين على GitHub.