کلود 180 میلیون خط اثبات ریاضی را در اولین تأیید رسمی در مقیاس بزرگ هوش مصنوعی نرم افزار منبع باز می نویسد.

گزارش کامل

Anthropic در 22 اکتبر در صفحه تحقیقاتی رسمی خود اعلام کرد: با همکاری شرکت تأیید نرم افزار Theorem، کلود به طور رسمی ویژگی های امنیتی در سطح مونتاژ RISC-V را در 123 کتابخانه منبع باز دنیای واقعی که از OSS-Fuzz گوگل گرفته شده بودند، تأیید کرد و 239 نقطه ورودی برنامه را پوشش می دهد. این شرکت آن را «اولین تلاش در مقیاس بزرگ برای استفاده از هوش مصنوعی برای اعمال تأیید رسمی بر روی نرم‌افزار تولیدی در سطح کد اسمبلی» می‌نامد.

مقیاس قابل توجه است: حدود 180 میلیون خط اثبات Rocq، با اثبات معمولی تا حدود 600000 خط، باینری هایی با طول متوسط ​​18000 دستورالعمل RISC-V را پوشش می دهد - همه در عرض چند هفته تکمیل می شوند. هسته Rocq به طور مستقل هر اثبات را بررسی می کند، بنابراین نیازی به بررسی خط به خط دستی نیست.

این روش تست‌های فاز موجود را به مشخصات ریاضی تبدیل می‌کند: برای هر ورودی کمتر از 64 مگابایت، یک باینری RISC-V با پیوند استاتیک تک رشته‌ای در لینوکس همیشه باید به‌طور عادی و بدون نقض ایمنی حافظه خارج شود. وقتی کلود مشکوک به وجود یک باگ در اواسط اثبات شد، کد را مستقیماً اصلاح کرد و مشخصات جدید را دوباره اثبات کرد.

صدها اشکال در طول مسیر ظاهر شدند، از جمله یک underflow counter در یک کپی از حالت فشرده‌سازی که منجر به نوشتن خارج از محدوده می‌شود (فقط با ورودی‌های 20 مگابایتی با یک طرح‌بندی نادر فعال می‌شود)، یک خارج از محدوده خوانده شده در رمزگشای تصویر، و یک کشف مجدد CVE-2026-2026-56132 livulvulerk.

Anthropic خود محدودیت‌ها را تأیید می‌کند: تأیید رسمی تأیید شده به معنای بدون اشکال نیست - اثبات‌ها فقط باینری‌های استاتیک RISC-V تک رشته‌ای را پوشش می‌دهند، در حالی که اکثر کدها در واقع روی x86/ARM اجرا می‌شوند. زیرمجموعه ای از اثبات ها را برای تأیید مستقل در GitHub منتشر کرده است و Theorem می گوید که همان خط لوله را برای سایر پروژه های منبع باز اجرا خواهد کرد.

نتایج جانبی نیز قابل توجه است: اجرای zlib هسته لینوکس ثابت شد که با RFC 1950 در سطح باینری x86 مطابقت دارد، و زیرمجموعه بزرگی از یک مفسر پایتون که در Rust نوشته شده است، با رفتار CPython در 99.95٪ از برنامه های تصادفی 1.7 میلیون به اضافه مطابقت دارد.