ریاضی "درد در الاغ" که می تواند کدنویسی Vibe را از خودش نجات دهد

برای دهه‌ها، توسعه‌دهندگان تصور می‌کردند از ریاضیات استفاده کنند تا ثابت کنند نرم‌افزارشان بدون اشکال است. این فرآیند طولانی و پرزحمت است و مهندسان را ملزم می کند تا عبارات دقیقی در مورد اهداف نرم افزار خود بنویسند و کد خود را به فرمول هایی تبدیل کنند که قابل تایید باشد. در حالی که شرکت‌ها در حال حاضر تست‌های پیچیده‌ای را برای شناسایی هر چه بیشتر ایرادات در نرم‌افزار خود انجام می‌دهند، به ندرت برای تأیید رسمی هزینه می‌کنند، که می‌تواند حتی رفتار نامنظم‌تری را نشان دهد. اکنون، موجی از استارت‌آپ‌ها شرط می‌بندند که هوش مصنوعی مولد، تأیید رسمی نرم‌افزار را هم عملی و هم ضروری می‌سازد.

از جمله آنها &Truth است که سان در ماه آگوست به آن ملحق شد و روز پنجشنبه به طور عمومی راه اندازی شد. تحقیقات Sun پتانسیل این فناوری را با استفاده از هوش مصنوعی برای تأیید بخشی از کدی که مکالمات را در برنامه پیام‌رسانی Signal رمزگذاری می‌کند، نشان داد. ایلیا سرگی، و مدیر ارشد علوم حقیقت می‌گوید: «پل‌ها، ساختمان‌ها فرو نمی‌ریزند، زیرا مردم قبل از ساختن آن‌ها، ریاضی را انجام می‌دادند. "چرا ما همین کار را برای کد انجام نمی دهیم؟ فناوری برای استدلال ریاضی همه چیز وجود داشت، فقط مقیاس کردن آن دشوار بود." &Truth 70 میلیون دلار از سرمایه گذاران جمع آوری کرده است و قصد دارد در نهایت هر زبان برنامه نویسی را تأیید کند.

Rival Harmonic که توسط ولاد تنف، مدیر عامل Robinhood تأسیس شد و 295 میلیون دلار بودجه دریافت کرده است، این هفته اعلام کرد که عامل هوش مصنوعی مبتنی بر ریاضیات Aristotle از نرم‌افزار تأییدکننده نوشته شده به زبان C و طراحی‌های سخت‌افزاری در Verilog پشتیبانی می‌کند. این شرکت در حال ارزیابی این فناوری با کاربران بالقوه، از جمله تراشه‌سازان Tensordyne و Nvidia است که بازوی سرمایه‌گذاری خطرپذیر آن‌ها یکی از سرمایه‌گذاران استارت‌آپ است. و همین هفته گذشته، Anthropic و استارت‌آپ راستی‌آزمایی Theorem به طور مشترک اعلام کردند که از هوش مصنوعی برای کمک به یافتن باگ‌هایی در نرم‌افزار متن‌باز استفاده کرده‌اند که تریلیون‌ها آزمایش در شناسایی آن‌ها شکست خورده‌اند.

آنها همچنین یک افزونه برای Claude معرفی کردند تا به توسعه دهندگان دیگر در تأیید کمک کند. هزینه های پروژه اولیه فاش نشده است. وعده بزرگ آینده ای است که در آن نرم افزار با اطمینان بیشتر با سردردهای امنیتی کمتر اجرا می شود. اما اینکه آیا هوش مصنوعی می‌تواند تأیید رسمی را فراتر از حیاتی‌ترین سیستم‌ها در سازمان‌هایی مانند ناسا و اپل و به استفاده گسترده برساند، یک سؤال باز باقی می‌ماند. این فناوری هنوز در مرحله نمونه سازی است. اگرچه تقاضا زیاد است، اما مشخص نیست که مشتریان چقدر مایل به پرداخت هستند و چگونه ترجیح می دهند از این فناوری استفاده کنند.

راستی‌آزمایی رسمی مبتنی بر فرضیاتی درباره نحوه تعامل رایانه‌ها و افراد با نرم‌افزار است، و برخی از کارشناسان در مورد توانایی آن در شناسایی اشکالات ناشی از خطای کاربر و خرابی‌های سخت‌افزاری تردید دارند. ویل ویلسون، که راه‌اندازی نرم‌افزار هوش مصنوعی Antithesis را اداره می‌کند، تأیید رسمی را «تله» برای آدم‌های ریاضی مانند خودش می‌نامد.

آنتی‌تز میلیون‌ها دلار هزینه کرد تا به طور رسمی برخی از دفاع‌های امنیتی سایبری خود را تأیید کند، فرآیندی که ویلسون آن را به‌عنوان «درد سخت» توصیف می‌کند. با این حال، استارت‌آپ هنوز با استفاده از ابزار خود خطاهای دیگری را کشف کرده است، و آنتی‌تز همچنین باگ‌هایی را در نرم‌افزاری پیدا کرده است که چندین مشتری آن را به طور رسمی تأیید کرده بودند.

ویلسون می‌گوید: «این می‌تواند به شما اطمینان دهد، اما فقط آزمایش‌های جامع و کامل می‌تواند صحت اطمینان شما را ثابت کند. یا همانطور که ویتالیک بوترین، مهندس معروف به ایجاد ارز دیجیتال اتریوم در اوایل سال جاری در یک پست وبلاگی آن را بیان کرد، "تأیید رسمی نوشدارویی نیست." اما او و سایر حامیان این رویکرد همچنان معتقدند که این یک دفاع مهم در برابر سیستم‌های هوش مصنوعی خواهد بود که حملات سایبری را راه‌اندازی می‌کنند و ویران می‌کنند. امنیت هسته طبق دیسک شرکت، هواپیماهای بوئینگ، سرورهای آمازون و بیش از 2.5 میلیارد دستگاه فعال اپل حاوی حداقل نرم‌افزار تأیید شده رسمی هستند.

ضررها کد مورد بحث معمولا مربوط به امنیت است و آسیب‌پذیری‌های موجود در آن در صورت سوء استفاده می‌تواند آسیب‌های جدی ایجاد کند. بایرون کوک، دانشمند برجسته و معاون رئیس خدمات وب آمازون، می‌گوید تأیید رسمی نگرانی‌های مشتریان در مورد امنیت ابر را کاهش داده است و به تیم‌های داخلی کمک می‌کند تا با رفع اشکالات بزرگ زودتر سریع‌تر حرکت کنند. اما چندین شرکت فناوری متوسط ​​به WIRED می‌گویند که معمولا فقط یک ویژگی کلیدی محصولات خود را تأیید کرده‌اند، اگر اصلا وجود داشته باشد.

آنها به فقدان مهندسان تأیید، هزینه‌هایی که بیشتر از خطرات احتمالی است و شاید مهم‌تر از همه، نگرانی‌هایی را ذکر می‌کنند که هفته‌ها انتظار برای تأیید رسمی کد می‌تواند نوآوری را کند کند. در اوایل سال جاری، تیم امنیتی اپل اعلام کرد که برخی از مشکلات تأیید رسمی که در کتابخانه «corecrypto» آن کشف شده است، که برای رمزگذاری استفاده می‌شود، به هیچ وجه نمی‌توانست پیدا شود.

اما این شرکت اضافه کرد که هنگام افزودن کد جدید به corecrypto باید محافظه کارانه عمل کند تا اطمینان حاصل شود که می تواند با بررسی آن همگام شود. دو مدیر امنیت سایبری در شرکت‌های بزرگ که هیچ کدی را به طور رسمی تأیید نکرده‌اند، می‌گویند مطمئن نیستند که آیا اتوماسیون آن را ارزشمند می‌کند یا خیر. اما مدیرانی که مجاز به صحبت علنی نبودند، می‌گویند می‌توانند تصور کنند که برای کد تولید شده توسط هوش مصنوعی «تأیید شده» به آزمایشگاه‌های اصلی هوش مصنوعی پول پرداخت کنند. توسعه‌دهندگان پروژه‌های نرم‌افزار متن‌باز، که بستر بسیاری از اپلیکیشن‌ها هستند، به طور فزاینده‌ای در حال آزمایش تأیید با کمک هوش مصنوعی هستند.

بنیاد غیرانتفاعی هوش مصنوعی سودمند از کمک مالی آنتروپیک برای اعتبارسنجی همان کد رمزگذاری امسال استفاده کرد که Sun در استنفورد انجام داد. مایکل روزنبرگ، نگهدار کتابخانه معروف به curve25519-dalek، امیدوار است که بودجه پایدار برای تلاش‌های راستی‌آزمایی مداوم پدیدار شود. او می‌گوید: «من هیچ ایده‌ای در مورد چگونگی این اتفاق ندارم، و مطمئنا نباید به حسن نیت شرکت‌های هوش مصنوعی تکیه کنیم.» برخی از استارت‌آپ‌هایی که مشتاق گسترش راستی‌آزمایی هستند نیز مطمئن نیستند که ابزارهای خود را مستقیما برای مشتریان یا از طریق واسطه‌هایی مانند آنتروپیک مستقر کنند.

برنامه کلی آنها این است که از هوش مصنوعی برای خودکارسازی بیشتر کارهای مربوط به تعریف نحوه عملکرد یک برنامه استفاده کنند. برای مثال، مشخصات یک جدول داده ممکن است مستلزم آن باشد که موارد مشابه قبل و بعد از مرتب‌سازی، فقط به ترتیبی متفاوت باشد. تلاش‌های اتوماسیون بیشتر، که ممکن است شامل هوش مصنوعی نباشد، آن کد را به قالبی ترجمه می‌کند که ابزارهای ریاضی مانند Lean، Rocq و Isabelle می‌توانند از آن برای بررسی اینکه آیا کد به‌طور مورد نظر کار می‌کند یا خیر، ترجمه می‌کنند. یکی دیگر از افرادی که اخیرا وارد حوزه تأیید رسمی شده است، مادان موسوواتی است که پس از بیش از 20 سال مایکروسافت ریسرچ را ترک کرد تا sta را تأسیس کند.

rtup Truidic. پس از حوادثی مانند هک OpenAI در Hugging Face، او احساس کرد که نیاز فوری به تجاری سازی مطالعاتش وجود دارد. Musuvathi می‌گوید: «هوش مصنوعی در دست مهاجمان می‌تواند بسیار قدرتمند باشد، اما تأیید می‌تواند هوش مصنوعی را برای همه و در همه جا ایمن و امن کند». Proofcraft، یکی از معدود شرکت‌هایی که مدت‌هاست تاییدیه سنتی را ارائه کرده است، می‌گوید که افزایش هیجان در مورد این فرآیند به سیل سوالات مشتریان بالقوه تبدیل می‌شود.

جون آندرونیک، مدیر عامل شرکت، و گروین کلاین، دانشمند ارشد آن، می‌گویند که علاقه به راحتی از آنچه آنها و رقبایشان می‌توانند ارائه کنند، پیشی می‌گیرد. اما هر دو نگران هستند که مشخصات تولید شده توسط هوش مصنوعی می تواند "اعتماد ناموجه" را به نتایج القا کند. تأییدکنندگان همچنین مشتاق هستند تا لذتی را که کارشان برای آنها به ارمغان می آورد حفظ کنند. کلاین آن را "بسیار اعتیاد آور، مانند یک بازی پازل" می نامد. اگر همه چیز به خوبی پیش برود، او بیش از هر زمان دیگری حل می کند.