N環球 
كلود يكتب 180 مليون سطر من الإثبات الرياضي في أول عملية تحقق رسمية واسعة النطاق باستخدام الذكاء الاصطناعي للبرمجيات مفتوحة المصدر
بحث Anthropic الرسمي: باستخدام Theorem، تحقق كلود رسميًا من خصائص الأمان على مستوى تجميع RISC-V عبر 123 مكتبة مفتوحة المصدر و239 نقطة دخول - واكتشف مئات الأخطاء التي تجنبت تريليونات من الاختبارات الآلية.
لماذا يهم
كان التحقق الرسمي بمثابة ترف لا يستطيع سوى الخبراء تحمله على مدار سنوات - استغرقت كتابة النواة الدقيقة seL4 عامين شخصين و20 عامًا للتحقق منها. لقد أظهرت الأنثروبيك الآن أن النموذج الحدودي يمكنه القيام بذلك لأكثر من مائة مكتبة حقيقية مفتوحة المصدر في أسابيع، بينما يكتشف الأخطاء التي نجت من "تريليونات" من عمليات التشغيل الاختبارية الآلية.
تقرير كامل
أعلنت Anthropic على صفحة البحث الرسمية الخاصة بها في 22 أكتوبر: بالتعاون مع شركة التحقق من البرامج Theorem، قام كلود رسميًا بالتحقق من خصائص الأمان على مستوى تجميع RISC-V عبر 123 مكتبة مفتوحة المصدر في العالم الحقيقي مستمدة من OSS-Fuzz من Google، والتي تغطي 239 نقطة دخول للبرنامج. وتصفه الشركة بأنه "أول جهد واسع النطاق لاستخدام الذكاء الاصطناعي لتطبيق التحقق الرسمي على برامج الإنتاج على مستوى رمز التجميع".
المقياس مذهل: حوالي 180 مليون سطر من بروفات Rocq، مع برهان نموذجي يصل إلى حوالي 600 ألف سطر، يغطي ثنائيات يبلغ متوسط طولها 18000 تعليمات RISC-V - وكلها مكتملة في غضون أسابيع. تقوم نواة Rocq بفحص كل دليل بشكل مستقل، لذلك لا حاجة إلى مراجعة يدوية سطرًا تلو الآخر.
تقوم هذه الطريقة بتحويل اختبارات Fuzz الموجودة إلى مواصفات رياضية: بالنسبة لأي إدخال يقل حجمه عن 64 ميجابايت، يجب دائمًا الخروج من ثنائي RISC-V ثنائي الخيط والمرتبط بشكل ثابت على Linux بشكل طبيعي، دون أي انتهاكات لسلامة الذاكرة. عندما اشتبه كلود في وجود خلل في منتصف الاختبار، قام بتصحيح الكود مباشرة وأعاد إثبات المواصفات الجديدة.
ظهرت المئات من الأخطاء على طول الطريق، بما في ذلك عداد التدفق السفلي في نسخة برنامج إلغاء الضغط مما أدى إلى كتابة خارج الحدود (لا يمكن تشغيلها إلا من خلال مدخلات تبلغ 20 ميجابايت تقريبًا مع تخطيط واحد نادر)، وقراءة خارج الحدود في وحدة فك ترميز الصور، وإعادة اكتشاف CVE-2026-56132 في libexpat - كانت بعض الثغرات الأمنية كامنة لسنوات.
تعترف Anthropic بالحدود نفسها: لا يعني التحقق الرسمي الذي تم اجتيازه خلوه من الأخطاء - فالإثباتات تغطي فقط ثنائيات RISC-V الثابتة ذات الخيط الواحد، في حين أن معظم التعليمات البرمجية تعمل فعليًا على x86/ARM. لقد نشرت مجموعة فرعية من البراهين على GitHub للتحقق منها بشكل مستقل، وتقول Theorem إنها ستقوم بتشغيل نفس المسار لمشاريع أخرى مفتوحة المصدر.
النتائج الجانبية ملحوظة أيضًا: ثبت أن تطبيق zlib الخاص بنواة Linux يتوافق مع RFC 1950 على المستوى الثنائي x86، وتطابقت مجموعة فرعية كبيرة من مترجم Python المكتوب بلغة Rust مع سلوك CPython على 99.95% من أكثر من 1.7 مليون برنامج عشوائي.
💬 Comments
No comments yet. Be the first!