آنتروپیک روشی مبتنی بر هوش مصنوعی برای اثبات ریاضی بدون باگ بودن نرم‌افزار توسعه داد
با پیشرفته‌تر شدن هوش مصنوعی، شمار زیادی از باگ‌های موجود در نرم‌افزارهای مختلف شناسایی شده‌اند. برخی از این آسیب‌پذیری‌ها پیامدهای مهمی داشته‌اند و حتی به اقداماتی مانند انتشار به‌روزرسانی اضطراری برای PHP منجر شده‌اند. در چنین شرایطی، شرکت هوش مصنوعی آنتروپیک (Anthropic) اعلام کرده است که روی روشی برای اثبات بدون باگ بودن نرم‌افزارها با استفاده از راستی‌آزمایی صوری (Formal Verification) کار می‌کند.
مدل‌های زبانی بزرگ، راستی‌آزمایی صوری نرم‌افزار را در مقیاسی بسیار گسترده‌تر امکان‌پذیر می‌کنند | آنتروپیک
https://www.anthropic.com/research/formal-verification
راستی‌آزمایی صوری روشی است که در آن با ارائه یک مدل ریاضی از کد نرم‌افزار، تلاش می‌شود بدون باگ بودن آن به‌صورت ریاضی اثبات شود. این مفهوم تازگی ندارد، اما ازآنجاکه انجام فرایند اثبات در عمل به تلاش و منابع فراوانی نیاز دارد، تاکنون عمدتاً در سامانه‌های بسیار حساس و حیاتی، مانند نرم‌افزارهای اویونیک یا سامانه‌های الکترونیکی هواپیما، به کار گرفته شده است.
آنتروپیک با همکاری سازمان پژوهشی Theorem روشی برای انجام راستی‌آزمایی صوری با استفاده از مدل هوش مصنوعی کلود (Claude) توسعه داده و آن را روی ۱۲۳ کتابخانه نرم‌افزاری متن‌باز آزمایش کرده است. پژوهشگران در جریان فرایند اثبات، باگ‌های شناسایی‌شده را به کمک کلود به‌طور مداوم برطرف کردند. در نهایت توانستند به‌صورت ریاضی اثبات کنند که در شرایط اجرایی مشخص، هیچ خطایی باعث ازکارافتادن برنامه نمی‌شود. این اثبات به حالتی محدود است که برنامه به‌شکل یک فایل اجرایی ایستای تک‌رشته‌ای، با مقدار ثابتی از حافظه در دسترس، روی دستگاهی مجهز به پردازنده‌ای با معماری RISC-V و سیستم‌عامل لینوکس اجرا شود.
انجام راستی‌آزمایی صوری به پردازش بیش از ۱۰۰ میلیون توکن نیاز دارد و همین موضوع هزینه بالایی به همراه می‌آورد. بااین‌حال، آنتروپیک پیش‌بینی می‌کند که این مشکل به‌تدریج کمتر شود. به گفته این شرکت، با بهبود عملکرد مدل‌ها، تعداد توکن‌های موردنیاز برای انجام فرایند اثبات کاهش می‌یابد. همچنین ازآنجاکه ممکن است فرایند اثبات در نرم‌افزارهای مختلف شباهت‌هایی داشته باشد، می‌توان با استفاده مجدد از بخش‌هایی از اثبات‌های قبلی، حجم پردازش را کاهش داد. نمودار زیر میزان مصرف توکن را در ۳۶ مورد راستی‌آزمایی صوری نشان می‌دهد. نتایج حاکی از آن است که Claude Opus 5.5 در مقایسه با Claude Opus 5 برای دستیابی به نتیجه به توکن‌های کمتری نیاز دارد.
آنتروپیک تأکید می‌کند که راستی‌آزمایی صوری همچنان محدودیت‌هایی دارد. برای مثال، حتی اگر بتوان ثابت کرد که یک نرم‌افزار روی معماری RISC-V بدون باگ اجرا می‌شود، ممکن است همان نرم‌افزار روی معماری‌های Arm یا x86 با خطا مواجه شود. همچنین برای اثبات نبود باگ در شرایط استفاده واقعی، لازم است تمام پیکربندی‌های سخت‌افزاری دستگاه‌هایی که قرار است برنامه روی آن‌ها اجرا شود، مدل‌سازی شوند. با وجود این محدودیت‌ها، آنتروپیک معتقد است که با شناخت عمیق‌تر روش‌های انجام راستی‌آزمایی صوری به کمک مدل‌های زبانی بزرگ و پیشرفت این مدل‌ها، می‌توان به‌تدریج بر چنین موانعی غلبه کرد.
مؤسسه Theorem امکان استفاده رایگان از روش راستی‌آزمایی صوری مبتنی بر مدل‌های زبانی بزرگ را برای پروژه‌های متن‌باز فراهم کرده است. اطلاعات بیشتر درباره این خدمات در لینک زیر در دسترس است.
OSS Verify | Theorem
https://theorem.dev/oss-verify/
علاوه بر این، مهارت‌ها و دستورالعمل‌های مورد استفاده برای انجام راستی‌آزمایی صوری نیز به‌صورت عمومی و رایگان منتشر شده‌اند.
فایل SKILL.md مربوط به افزودن پروژه در مخزن oss-verify در گیت‌هاب
https://github.com/theorem-labs/oss-verify/blob/main/.claude/skills/add-project/SKILL.md