Anthropic مع Theorem: Claude كتب براهين رياضية إن أجزاء من 123 مكتبة برمجية مفتوحة ما تنهار، ولقى أخطاء مخفية من سنين

Anthropic نشرت يوم 22 أكتوبر بحث مع شركة Theorem: خلوا Claude يكتب براهين رياضية تثبت إن أجزاء من برامج حقيقية ما تنهار، مو بس يدوّر أخطاء.

النتيجة: 239 نقطة دخول (أماكن اختبار) في 123 مكتبة مفتوحة المصدر من مشروع OSS-Fuzz حق Google. البرهان يقول إنها ما تنهار ولا تسوي أخطاء ذاكرة لأي مدخل أقل من 64 ميغابايت.

وأثناء الشغل، Claude لقى مئات الأخطاء وصلّحها، بعضها ما كانت أدوات الاختبار العادية بتلقاها أبدًا، مثل خطأ ما يطلع إلا مع ملف حجمه حوالي 20 ميغابايت بترتيب نادر.

البراهين ضخمة (حوالي 180 مليون سطر)، بس ما تحتاج أحد يراجعها سطر سطر: برنامج تحقق مستقل اسمه Rocq يتأكد إنها صحيحة.

Anthropic كانت واضحة في الحدود: البرهان يخص نسخة RISC-V بشروط محددة، مو أجهزة x86 أو ARM اللي أغلب الناس يستخدمونها، و«متحقق منه» ما يعني «بدون أي خطأ».

ليش يهمك؟ إذا تبرمج أو تسوي vibe coding، الذكاء الاصطناعي ما بيكتفي يكتب لك كود، بيصير يثبت إنه آمن. وTheorem نشرت مهارة (Skill) لـ Claude تساعد المطورين يبدون يتحققون من كودهم.