انتشار کتابخانه متن باز تأیید فرموله بزرگ Claude توسط Anthropic

شرکت هوش مصنوعی Anthropic، تیم Frontier Red خود را در تاریخ 22 اکتبر منتشر کرد و اعلام کرد که مدل‌های زبانی بزرگ قادر به نوشتن خودکار تأییدات فرموله در مقیاس بزرگ‌تری هستند. این تیم با Theorem همکاری کرده و با استفاده از Claude در سطح اسمبلی RISC-V، بیش از 100 کتابخانه متن باز واقعی را برای تأیید ویژگی‌های امنیتی بررسی کرده است که این اولین بار است که از هوش مصنوعی برای تأیید فرموله در سطح اسمبلی نرم‌افزارهای تولیدی استفاده می‌شود. در طول نوشتن تأییدات، نقص‌هایی که سال‌ها نادیده گرفته شده بودند، کشف شد. این آزمایش تست‌های قابل کامپایل موجود در Google OSS-Fuzz را به مشخصات تبدیل کرد و تحت فرضیات باینری استاتیک تک‌نخی، بودجه حافظه ثابت، CPU RISC-V و Linux، برای هر ورودی کمتر از 64 مگابایت، برنامه باید به‌طور عادی خارج شود و خطاهای امنیتی حافظه یا شکست‌های ادعایی را تحریک نکند. Claude پس از اصلاح مشکلات، ویژگی‌های فوق را برای 239 نقطه ورودی در 123 کتابخانه OSS-Fuzz تأیید کرد، که تأییدات مربوط به دستورالعمل‌های RISC-V کامپایل شده، حدود 1.8 میلیون خط Rocq است و توسط هسته Rocq بررسی شده است. صفحه می‌گوید که این به معنای عدم وجود نقص در این کتابخانه‌ها نیست و مسائل باقی‌مانده ممکن است در اجزای مورد اعتماد یا خارج از دامنه تأیید قرار داشته باشند. تیم همچنین از Claude خواست تا RFC 1950 را فرموله کند و در سطح باینری x86 تأیید کند که پیاده‌سازی zlib در هسته Linux با این مشخصات مطابقت دارد؛ یک مفسر نوشته شده با Rust که پوشش‌دهنده زیرمجموعه بزرگ Python است، نسبت به بیش از 1.7 میلیون برنامه تصادفی تولید شده، 99.95% سازگاری با رفتار CPython را نشان داد. در 36 وظیفه تأیید کوچک، Opus 5.5 تأیید کرد که برای نیمی از آن‌ها به حدود 40% توکن کمتری نسبت به Opus 5 نیاز دارد.