أنتروبيك تقول إن كلود يولّد proofs رسمية على مستوى التجميع لـ123 مكتبة مفتوحة المصدر

تتعاون شركة Anthropic مع شركة Theorem المتخصصة في التحقق الشكلي لتحويل اختبارات التلويث (fuzzing) الموجودة في المشاريع مفتوحة المصدر إلى مواصفات رياضية، حيث يقوم نموذج Claude بكتابة البراهين، التي يتم بعد ذلك التحقق منها بواسطة فاحص البراهين Rocq. وذكرت Anthropic أن الفريق أكمل خلال أسابيع قليلة إثبات صحة 239 مدخلاً للاختبار عبر 123 مكتبة مفتوحة المصدر، بإجمالي حوالي 180 مليون سطر من شيفرة البرهان. وتتمثل النتيجة الأساسية في أنه، بالنسبة للمدخلات التي تقل عن 64 ميغابايت، وتحت ظروف استجابة نظام لينكس وتخطيط الذاكرة المحددين، لا تنهار مداخل الاختبار، بعد ترقيتها وترجمتها إلى برامج RISC-V محددة، بسبب أخطاء في سلامة الذاكرة أو فشل في تأكيد الشروط. كما اكتشف Claude وأصلح، أثناء كتابة البراهين، مشكلات لم يكشف عنها الاختبار السابق، بما في ذلك قراءة وكتابة خارج الحدود تتطلب مدخلات نادرة الحدوث. وعلى عكس اختبارات التلويث التي تعتمد على أخذ عينات متكررة، تغطي البراهين الشكلية جميع المدخلات ضمن النطاق المحدد؛ إلا أن النتائج تعتمد على دقة المواصفات ونموذج الجهاز وفاحص البراهين. حالياً، تستهدف البراهين الرئيسية بشكل أساسي شروط تشغيل محددة مثل تعدد الخيوط المنفرد والربط الثابت، ولا تغطي الشيفرة الكاملة لكل مكتبة. وقد نشرت Anthropic بعض البراهين ليتسنى للجمهور مراجعتها وإعادة استخدامها. وتُظهر هذه الدراسة إمكانية تقليل عبء عمل التحقق الشكلي باستخدام الذكاء الاصطناعي، ولا يمكن بناءً عليها الادعاء بأن المكتبات الـ123 "خالية من الثغرات".