🤖 استفاده از Claude برای اثبات ریاضی کدهای متن‌باز
شرکت Anthropic با همکاری Theorem از مدل Claude برای تأیید رسمی (Formal Verification) کدهای ۱۲۳ کتابخانه متن‌باز استفاده کرده است. در این پروژه، مدل به جای تکیه بر تست‌های تصادفی، تست‌های موجود در سرویس OSS-Fuzz گوگل را به قضایای ریاضی تبدیل کرده و صحت عملکرد آن‌ها را اثبات کرد.
نتایج این آزمایش شامل موارد زیر است:
* تولید ۱۸۰ میلیون خط کد اثبات برای ۲۳۹ نقطه ورود در کتابخانه‌های مختلف.
* تأیید نهایی توسط نرم‌افزار
* شناسایی و رفع صدها باگ پیچیده، از جمله خطای سرریز بافر در الگوریتم‌های فشرده‌سازی و دسترسی خارج از محدوده آرایه در دیکودرهای تصویر که با تست‌های معمولی قابل کشف نبودند.
اگرچه این روش در گذشته به دلیل هزینه بالای زمانی بسیار دشوار بود، اما اکنون خودکارسازی آن سرعت کار را به شدت افزایش داده است.
🔗 ادامه مطلب در سایت
#Formal_Verification #Rocq
شرکت Anthropic با همکاری Theorem از مدل Claude برای تأیید رسمی (Formal Verification) کدهای ۱۲۳ کتابخانه متن‌باز استفاده کرده است. در این پروژه، مدل به جای تکیه بر تست‌های تصادفی، تست‌های موجود در سرویس OSS-Fuzz گوگل را به قضایای ریاضی تبدیل کرده و صحت عملکرد آن‌ها را اثبات کرد.
نتایج این آزمایش شامل موارد زیر است:
* تولید ۱۸۰ میلیون خط کد اثبات برای ۲۳۹ نقطه ورود در کتابخانه‌های مختلف.
* تأیید نهایی توسط نرم‌افزار
Rocq برای اطمینان از اجرای بدون نقص کد با هر ورودی تا ۶۴ مگابایت.* شناسایی و رفع صدها باگ پیچیده، از جمله خطای سرریز بافر در الگوریتم‌های فشرده‌سازی و دسترسی خارج از محدوده آرایه در دیکودرهای تصویر که با تست‌های معمولی قابل کشف نبودند.
اگرچه این روش در گذشته به دلیل هزینه بالای زمانی بسیار دشوار بود، اما اکنون خودکارسازی آن سرعت کار را به شدت افزایش داده است.
🔗 ادامه مطلب در سایت
🇮🇷 - هوش مصنوعی و علم داده به فارسی
🌐 سایت | تلگرام | بله | ایتا | ارتباط با ما
#Formal_Verification #Rocq