توسعه ابزارهای هوش مصنوعی برای تایید رسمی نرم‌افزارها

استارتاپ &Truth با جذب ۷۰ میلیون دلار سرمایه، فعالیت خود را برای توسعه ابزارهای هوش مصنوعی جهت تایید رسمی نرم‌افزارها آغاز کرده است. همچنین استارتاپ Harmonic با جذب ۲۹۵ میلیون دلار سرمایه، ابزار هوش مصنوعی Aristotle را برای تایید نرم‌افزارهای نوشته شده با زبان C و طراحی‌های سخت‌افزاری Verilog معرفی کرد.

در همین حال، شرکت‌های Anthropic و Theorem با استفاده از هوش مصنوعی موفق به شناسایی باگ‌هایی در نرم‌افزارهای متن‌باز شدند که تریلیون‌ها تست قبلی قادر به تشخیص آن‌ها نبودند. یک پژوهشگر استنفورد به نام Chuyue Sun نیز پروژه‌ای مهندسی را با هوش مصنوعی در کمتر از نیم روز و با هزینه‌ای کمتر از ۵۰۰ دلار تکمیل کرد که پیش‌تر توسط سه متخصص در ۵ ماه انجام شده بود.

در حال حاضر بیش از ۲.۵ میلیارد دستگاه فعال اپل، سرورهای آمازون و هواپیماهای بوئینگ حاوی بخش‌هایی از نرم‌افزارهای تایید شده به صورت رسمی هستند.

درباره کارایی این فناوری، ایلیا سرگی، مدیر ارشد علمی &Truth، معتقد است که فناوری لازم برای تایید ریاضی کدها وجود دارد اما مقیاس‌پذیری آن دشوار است. در مقابل، ویل ویلسون، مدیر استارتاپ Antithesis، تایید رسمی نرم‌افزار را تله‌ای برای علاقه‌مندان به ریاضی می‌داند و معتقد است تنها تست‌های جامع و سخت‌گیرانه می‌توانند امنیت را اثبات کنند. ویتالیک بوترین، خالق اتریوم، نیز بر این باور است که تایید رسمی نرم‌افزار یک راه‌حل قطعی و همه‌جانبه برای مشکلات امنیتی نیست.