2026-11-05 · المصدر：Unite AI p4
أبحاث Anthropic الصادرة في 22 أكتوبر، المنجزة مع Theorem، ترسم مسار عمل تصل فيه الأخطاء التي يجدها الذكاء الاصطناعي مع إثبات رياضي بأنها أُصلحت — لا اجتياز اختبار آخر.
239 نقطة دخول لاختبار الفوضى — كل واحدة منها مدعومة الآن بإثبات رسمي متحقَّق منه آليًا. هذه هي الدعوى الرئيسية في أبحاث نشرتها Anthropic في 22 أكتوبر 2026، تصف عملًا أنتج فيه Claude إثباتات لخصائص أمنية لشيفرة مأخوذة من 123 مكتبة مفتوحة المصدر.
كان الجهد تعاونًا مع Theorem، ونطاقه غير مألوف: تعمل الإثباتات على مستوى شيفرة الأسمبلة لـ RISC-V، وهي الطبقة التي تعيش فيها أخطاء سلامة الذاكرة فعلًا. وبحسب Anthropic، لم يتوقف Claude عند اكتشاف العيوب؛ فقد رقّع النموذج الأخطاء التي كشفها، ثم أنتج إثباتات بأن البرامج المُصلَحة ستخرج دائمًا بشكل طبيعي — دون أن تُطلق خطأ سلامة ذاكرة أو فشل تأكيد — لكل مدخل أقل من 64 MB ولكل حالة Linux منمذجة.
والتمييز بين الاختبار والإثبات هو موضع الدلالة. فاختبار الفوضى يخضِع برنامجًا لمدخلات كثيرة ويبلّغ عما يجده بالصدفة؛ ولا يمكنه أبدًا أن يقول ماذا يفعل البرنامج على مدخلات لم يجربها. أما الإثبات المتحقَّق منه آليًا، فيُدقَّق مقابل مواصفة رسمية، ويغطي فضاء المدخلات بأكمله الذي تصفه المواصفة — هنا، كل المدخلات دون حد الـ 64 MB وبيئة Linux المنمذجة. وإذا صحت الدعوى كما نصّت، فإن كل نقطة من نقاط الدخول الـ 239 تحمل ضمانة أقوى مما يمكن لأي حجم من الاختبار العشوائي أن يوفره.
والعمل على مستوى الأسمبلة يرفع السقف أكثر. فالاستدلال على الشيفرة المصدرية قد يفوّت عيوبًا أُدخلت أثناء الترجمة؛ وإثبات الخصائص على أسمبلة RISC-V يعني أن الضمانة تلتصق بالتعليمات التي سينفذها المعالج فعلًا.
ولصائني المكتبات الـ 123 المعنية، تصف النتائج المنشورة حلقة مغلقة — اكتشاف ورقعة وإثبات متحقَّق منه داخل مسار عمل واحد. وسؤال ما إذا كانت تلك الحلقة قادرة على الاشتغال بوتيرة وتكلفة الصيانة البرمجية الاعتيادية هو ما تتركه أرقام Anthropic مفتوحًا، وهو ما سيقرر ما إذا كانت الإثباتات الأمنية المتحقَّق منها آليًا ستصبح روتينًا لا حدثًا استثنائيًا.
الوسوم: Anthropic · Claude · Theorem · Formal Verification · Memory Safety · RISC-V
萬安算交所 AIXX · AIXX · بورصة الحوسبة الموثقة · قاعة التداول