کلود آنتروپیک اکنون می‌تواند کدها را بنویسد و درستی آن‌ها را به‌طور خودکار اثبات کند
نویسنده: ماتیاس باستیان | ۲۳ اکتبر ۲۰۲۶
نکات کلیدی
- آنتروپیک با همکاری شرکت Theorem از کلود برای بررسی ریاضی درستی کدهای نرم‌افزاری موجود و تولید اثبات‌های رسمی صحت آن‌ها استفاده کرده است.
- این مدل تنها طی چند هفته حدود ۱۸۰ میلیون خط کد اثبات ریاضی برای ۱۲۳ کتابخانه متن‌باز تولید کرده و در این فرایند صدها باگ را شناسایی کرده است که آزمایش‌های متداول نتوانسته بودند آن‌ها را کشف کنند.
- اگر هوش مصنوعی بتواند هم کد بنویسد و هم درستی آن را اثبات کند، خودکارسازی توسعه نرم‌افزار ممکن است جهش بزرگی را تجربه کند. آنتروپیک می‌خواهد راستی‌آزمایی رسمی با کمک هوش مصنوعی به فرایندی به‌اندازه آزمایش‌های استاندارد نرم‌افزار رایج تبدیل شود.
آنتروپیک از کلود برای اثبات ریاضی درستی کدهای نرم‌افزاری موجود استفاده کرده است. این روش به یکی از چالش‌های اساسی نرم‌افزارهای تولیدشده با هوش مصنوعی می‌پردازد، اما در عمل محدودیت‌های سخت‌گیرانه‌ای دارد.
اثبات اینکه یک نرم‌افزار در تمام شرایط بدون خطا اجرا می‌شود، همواره چنان پرهزینه بوده که استفاده گسترده از این روش صرفه اقتصادی نداشته است. برای نمونه، گروهی از متخصصان تنها برای راستی‌آزمایی رسمی هسته کوچک سیستم‌عامل seL4 به ۲۰ نفرسال کار نیاز داشتند. به همین دلیل، این روش معمولاً به موارد بسیار حساس، مانند نرم‌افزارهای سامانه‌های الکترونیکی هواپیماهای ایرباس، محدود می‌شد.
اکنون تیم Frontier Red Team آنتروپیک با همکاری شرکت Theorem، وظیفه تولید اثبات‌های ریاضی را به کلود سپرده است. این مدل تنها در چند هفته حدود ۱۸۰ میلیون خط کد اثبات ریاضی تولید کرد. مبنای این کار، برنامه‌های آزمایشی مربوط به ۱۲۳ کتابخانه متن‌باز در پروژه امنیتی OSS-Fuzz گوگل بود.
در این پروژه، کلود به‌جای نوشتن کدهای جدید، درستی نرم‌افزارهای موجود را بررسی کرد. برای این کار، آزمون‌های مربوط به خرابی برنامه را به مسائل ریاضی تبدیل کرد، کد ماشینِ کامپایل‌شده را تحلیل کرد و اثبات‌های مفصلی برای صحت عملکرد آن ارائه داد. سپس برنامه مستقلی به نام Rocq این اثبات‌ها را به‌طور خودکار بررسی می‌کند. به گفته آنتروپیک، این فرایند تقریباً هیچ نیازی به بازبینی انسانی ندارد. پژوهشگران آن را تولید اثبات «کاملاً خودکار» می‌نامند؛ هرچند ابزارها و مبانی رسمی مورد استفاده در این فرایند را متخصصان شرکت Theorem توسعه داده‌اند.
کلود باگ‌هایی را پیدا کرد که سال‌ها آزمایش قادر به شناسایی آن‌ها نبود
کلود هنگام تولید اثبات‌های ریاضی با صدها باگ روبه‌رو شد و اجازه داشت خودش آن‌ها را برطرف کند. به گفته پژوهشگران، بسیاری از این خطاها احتمالاً در آزمایش‌های معمول شناسایی نمی‌شدند، زیرا تنها در شرایطی بسیار خاص بروز می‌کنند؛ برای مثال، هنگام پردازش فایل‌های ورودی غیرمعمول و بسیار بزرگ یا زمانی که دسترسی‌ها به ترتیب مشخصی انجام می‌شوند.
برای نمونه، هنگام تلاش برای راستی‌آزمایی یک نرم‌افزار پرکاربرد نمایش فایل‌های PDF، این گروه تنها در یک هفته به‌اندازه تعداد آسیب‌پذیری‌های امنیتی که معمولاً در طول یک سال برای آن نرم‌افزار گزارش می‌شود، باگ امنیتی پیدا کرد. کلود در نرم‌افزار دیگری نیز خطایی منطقی را شناسایی کرد که بیش از یک دهه از دید توسعه‌دهندگان پنهان مانده بود. آنتروپیک می‌گوید حتی زمانی که تلاش برای ارائه یک اثبات کامل در نهایت شکست می‌خورد، همین فرایند همچنان می‌تواند به کشف باگ‌های واقعی منجر شود.
راستی‌آزمایی رسمی چه توانایی‌ها و محدودیت‌هایی دارد؟
آنتروپیک تأکید می‌کند که «راستی‌آزمایی رسمی» لزوماً به معنای «بدون خطا بودن» نرم‌افزار نیست. اعتبار اثبات‌های تولیدشده به شرایط مشخص و سخت‌گیرانه‌ای محدود می‌شود: استفاده از معماری پردازنده‌ای معین، اجرای برنامه‌ها به‌صورت تک‌رشته‌ای و پردازش ورودی‌هایی با حجم کمتر از ۶۴ مگابایت. این در حالی است که کتابخانه‌های نرم‌افزاری در دنیای واقعی روی سخت‌افزارهای مختلف و با پیکربندی‌های متفاوت اجرا می‌شوند.
هزینه محاسباتی این روش نیز بسیار بالاست؛ به‌طوری‌که تولید هر اثبات ممکن است صدها میلیون توکن مصرف کند. آنتروپیک هزینه کل پروژه را اعلام نکرده است. بااین‌حال، اگر هوش مصنوعی بتواند درستی کدی را که خودش تولید کرده نیز اثبات کند، توسعه‌دهندگان می‌توانند با اطمینان بیشتری از نرم‌افزارهای تولیدشده با هوش مصنوعی استفاده کنند و زمان کمتری را به بازبینی آن‌ها اختصاص دهند. در نتیجه، صرفه‌جویی در هزینه‌ها تنها به مرحله راستی‌آزمایی محدود نخواهد بود و می‌تواند کل فرایند برنامه‌نویسی را دربر بگیرد. یک آزمایش کوچک‌تر نیز نشان داده است که اثبات‌های تولیدشده قابلیت استفاده مجدد دارند و مدل‌های جدیدتر در انجام این کار کارآمدتر شده‌اند. برای مثال، مدل Opus 5.5 می‌تواند نیمی از اثبات‌ها را با مصرف حدود ۴۰ درصد توکن کمتر نسبت به Opus 5 حل کند.
نتایج این پروژه استدلال‌های موافق خودکارسازی توسعه نرم‌افزار را تقویت می‌کند. اگر هوش مصنوعی بتواند کد بنویسد و درستی عملکرد آن را در شرایطی مشخص تضمین کند، پرسش اصلی دیگر این نخواهد بود که «آیا هوش مصنوعی می‌تواند برنامه‌نویسی کند؟» بلکه به این تبدیل می‌شود که «آیا هوش مصنوعی می‌تواند ایمن بودن کدی را که می‌نویسد اثبات کند؟» اگر پاسخ مثبت باشد، پیامدهای این توانایی ممکن است بسیار فراتر از ابزارهای برنامه‌نویسی امروزی باشد.
برای نمونه، آنتروپیک انتظار دارد راستی‌آزمایی رسمی با کمک هوش مصنوعی به‌زودی از نظر کاربردپذیری به سطح آزمایش‌های استاندارد نرم‌افزار برسد. همچنین نقشه راه شرکت Theorem از هم‌اکنون زیرساخت‌های نرم‌افزاری حیاتی، از جمله glibc، OpenSSL و cURL را هدف قرار داده است.
منبع: آنتروپیک