الذكاء الاصطناعي٢٣ أكتوبر ٢٠٢٦
أنثروبيك: النماذج اللغوية تعزز جدوى التحقق الرسمي من البرمجيات
تعاونت أنثروبيك مع Theorem لاختبار قدرة Claude على التحقق الرسمي من برمجيات مفتوحة المصدر، في تجربة واسعة النطاق على مستوى تعليمات المعالج. وأثبت النموذج خصائص أمنية في ١٢٣ مكتبة، منها أن بعض الملفات التنفيذية لا تتعطل ضمن شروط محددة، كما عثر على أخطاء استعصت على الاختبارات سنوات. ونشرت أنثروبيك مجموعة من البراهين ليتمكن المطورون من فحصها وإعادة استخدامها.
الحقائق الأساسية
شمل التحقق ١٢٣ مكتبة مفتوحة المصدر.
«To demonstrate this, we asked Claude to prove useful security properties across 123 open-source libraries, including showing that some of their executable artifacts can never crash under certain conditions.»
عرض المصدر ←اكتشف Claude أخطاء لم ترصدها الاختبارات لسنوات، رغم تنفيذ تريليونات منها.
«While writing the proofs, Claude also discovered bugs that had eluded detection for years, despite trillions of test runs.»
عرض المصدر ←أتاحت أنثروبيك مجموعة من البراهين للتحقق منها وإعادة استخدامها.
«We’re publishing a subset of these proofs so that anyone can verify and reuse them, along with the RISC-V and OS semantics.»
عرض المصدر ←
المصادر
شفت معلومة تحتاج تصحيح؟ بلّغنا ونتحقق ونصحّح — سياسة التصحيح
صحّح هذا الخبر