Anthropic اعلام کرد مدل Claude می‌تواند برای کدهای موجود، اثبات‌های راستی‌آزمایی رسمی را به‌طور خودکار تولید کند. در آزمایشی روی 123 کتابخانه از پروژه OSS‑Fuzz گوگل، Claude طی چند هفته حدود 180 million خط اثبات تولید کرد. اثبات‌ها با راستی‌آزمای Rocq بررسی شدند و به‌گفته Anthropic، این فرایند تقریباً به هیچ بازبینی انسانی نیاز نداشت.
این سیستم دقیقاً چه کرد
Claude برنامه‌های تازه‌ای ننوشت. در عوض، موارد آزمونیِ منجر به کرش را به گزاره‌های ریاضی تبدیل کرد، کد ماشینِ کامپایل‌شده را تحلیل کرد و اثبات‌های رسمی‌ای ارائه داد که نشان می‌دادند کد با آن گزاره‌ها مطابقت دارد. اگر مدل باگی پیدا می‌کرد، اجازه داشت خودش کد را اصلاح کند. Claude طی یک هفته بررسی یک PDFخوان محبوب، به همان اندازه باگ امنیتی پیدا کرد که معمولاً در طول یک سال گزارش می‌شود. در کتابخانه‌ای دیگر نیز خطای منطقی‌ای یافت که بیش از ده سال پنهان مانده بود.
محدودیت‌ها و هزینه‌ها
Anthropic هشدار می‌دهد که این اثبات‌ها فقط برای برنامه‌ای تک‌رشته‌ای، روی معماری پردازنده‌ای مشخص و با ورودی‌های کمتر از 64 MB اعتبار دارند. توان محاسباتی موردنیاز بالاست و تولید هر اثبات به صدها میلیون توکن می‌رسد؛ بااین‌حال، شرکت هزینه کلی را اعلام نکرد. یک آزمایش کوچک‌تر نشان داد مدل جدیدتر Opus 5.5 می‌تواند نیمی از اثبات‌ها را با حدود 40 % توکن کمتر از مدل قبلی تکمیل کند.
چرا مهم است
اگر هوش مصنوعی بتواند کد را خودکار راستی‌آزمایی کند، توسعه‌دهندگان ممکن است زمان کمتری صرف پیدا کردن باگ‌ها و بازبینی وصله‌ها کنند؛ به‌ویژه در نرم‌افزارهای حساس از نظر ایمنی. بااین‌حال، روش فعلی فقط با محدودیت‌های سخت‌گیرانه‌ای در زمینه سخت‌افزار و ورودی کار می‌کند و بنابراین بیشتر برنامه‌های روزمره همچنان به آزمون‌های سنتی نیاز دارند.
