تلاش استارتاپ‌ها برای مهار باگ‌های نرم‌افزاری؛ وقتی هوش مصنوعی درستی کدها را با ریاضی اثبات می‌کند

تیمی از دانشمندان علوم کامپیوتر در دانشگاه استنفورد موفق به ساخت ابزاری مبتنی بر هوش مصنوعی شده‌اند که توانسته یک پروژه مهندسی را در کمتر از نصف روز و با هزینه‌ای زیر ۵۰۰ دلار به سرانجام برساند؛ در حالی که انجام دستی همین کار پیش‌تر به پنج ماه زمان و تلاش سه کارشناس زبده نیاز داشت. این کاهش چشمگیر در زمان و هزینه‌ها که نتایج آن در یک مقاله پژوهشی تازه منتشر شده است، از نخستین دستاوردهایی به شمار می‌رود که یکی از شاخه‌های ناشناخته پیوند ریاضیات و کدنویسی موسوم به «اثبات درستی صوری» (Formal Verification) را کانون توجه قرار داده است.

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

اکنون موجی از استارتاپ‌ها روی این ایده شرط بسته‌اند که هوش مصنوعی مولد می‌تواند فرایند اثبات صوری نرم‌افزار را کاربردی، سریع و ضروری کند. از جمله این شرکت‌ها استارتاپ &Truth است که پژوهشگران استنفورد نیز به آن پیوسته‌اند و فعالیت عمومی خود را به‌تازگی آغاز کرده است. پژوهش‌های اخیر پتانسیل بالای این فناوری را نشان داده‌اند، جایی که از هوش مصنوعی برای اعتبارسنجی و اثبات درستی بخشی از کدهای رمزنگاری پیام‌رسان Signal استفاده شد.

ایلیا سرگی (Ilya Sergey)، مدیر ارشد علمی استارتاپ &Truth، می‌گوید: «پل‌ها و ساختمان‌ها به این دلیل فرو نمی‌ریزند که مهندسان پیش از ساخت، محاسبات دقیق ریاضی انجام می‌دهند. چرا نباید همین کار را برای کدهای نرم‌افزاری انجام دهیم؟ فناوری استدلال ریاضی همواره وجود داشته، اما مقیاس‌پذیر کردن آن بسیار دشوار بوده است.»

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

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

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

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

ویل ویلسون (Will Wilson)، مدیر استارتاپ Antithesis که در زمینه کشف باگ با هوش مصنوعی فعالیت می‌کند، اثبات صوری را «تله‌ای» برای علاقه‌مندان شیفته ریاضیات مانند خودش می‌داند. استارتاپ Antithesis میلیون‌ها دلار صرف اثبات صوری برخی از سیستم‌های دفاع سایبری خود کرد؛ فرایندی که ویلسون آن را بی‌اندازه خسته‌کننده و طاقت‌فرسا توصیف می‌کند. با وجود این، استارتاپ مذکور باز هم با ابزار اختصاصی خود خطاهای دیگری کشف کرد؛ همچنین در نرم‌افزارهای مشتریانی که کدهایشان از پیش به روش صوری تأیید شده بود نیز باگ‌هایی پیدا شد. ویلسون می‌گوید: «این روش مقداری اطمینان به شما می‌دهد، اما تنها آزمون‌های همه‌جانبه و جامع می‌توانند درستی این اطمینان را ثابت کنند.»

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

امنیت هسته‌ای نرم‌افزارها

بر اساس گزارش‌های رسمی شرکت‌ها، هواپیماهای بوئینگ، سرورهای آمازون و بیش از ۲.۵ میلیارد دستگاه فعال اپل، دست‌کم بخشی از نرم‌افزارهای خود را با روش اثبات صوری تأیید کرده‌اند. این کدها معمولاً بخش‌های امنیتی را شامل می‌شوند؛ بخش‌هایی که آسیب‌پذیری در آن‌ها می‌تواند در صورت سوءاستفاده، خسارات جبران‌ناپذیری به‌همراه داشته باشد.

بایرون کوک (Byron Cook)، دانشمند برجسته و معاون ارشد بخش خدمات ابری آمازون (AWS)، معتقد است اثبات صوری نگرانی مشتریان پیرامون امنیت ابری را کاهش داده و با برطرف کردن سریع باگ‌های بزرگ در همان مراحل اولیه، سرعت عمل تیم‌های داخلی را بالا برده است.

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

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

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

توسعه‌دهندگان پروژه‌های نرم‌افزاری متن‌باز، که ستون فقرات بسیاری از برنامه‌ها هستند، به‌شکل روزافزونی در حال آزمایش اعتبارسنجی به کمک هوش مصنوعی هستند. بنیاد غیرانتفاعی Beneficial AI امسال با استفاده از کمک مالی ارائه‌شده توسط Anthropic، همان کدهای رمزنگاری بررسی‌شده در دانشگاه استنفورد را تأیید کرد. مایکل روزنبرگ (Michael Rosenberg)، یکی از نگهدارندگان کتابخانه curve25519-dalek، امیدوار است بودجه‌های پایداری برای تداوم این اعتبارسنجی‌ها فراهم شود. او می‌گوید: «البته هیچ تصوری ندارم که این اتفاق چگونه خواهد افتاد و قطعاً نباید صرفاً به حسن نیت شرکت‌های هوش مصنوعی متکی باشیم.»

برخی از استارتاپ‌هایی که به دنبال توسعه دامنه اعتبارسنجی هستند، هنوز مطمئن نیستند که ابزارهای خود را مستقیماً در اختیار مشتریان قرار دهند یا از طریق واسطه‌هایی نظیر Anthropic عمل کنند. برنامه کلی آن‌ها استفاده از هوش مصنوعی برای خودکارسازی بخش عمده فرایند تعریف رفتار مورد انتظار از یک برنامه است. برای نمونه، مشخصات تعریف‌شده برای یک جدول داده ممکن است ایجاب کند که اقلام پیش و پس از مرتب‌سازی یکسان بمانند و فقط ترتیب آن‌ها تغییر کند. در گام‌های بعدی خودکارسازی، کدهای برنامه به قالبی ترجمه می‌شوند تا ابزارهای ریاضی معروفی مانند Lean، Rocq و Isabelle بتوانند انطباق دقیق عملکرد کد با اهداف تعیین‌شده را بسنجند.

یکی دیگر از تازه‌واردان به عرصه اثبات صوری، مادان موسووتی (Madan Musuvathi) است که پس از بیش از ۲۰ سال فعالیت در مایکروسافت، این شرکت را برای تأسیس استارتاپ Truidic ترک کرد. او پس از رخدادهایی مانند هک پلتفرم Hugging Face احساس کرد نیازی فوری به تجاری‌سازی مطالعات خود وجود دارد. او تأکید می‌کند: «هوش مصنوعی در دستان مهاجمان می‌تواند بسیار قدرتمند و مخرب باشد؛ اما اثبات صوری این پتانسیل را دارد که هوش مصنوعی را برای همگان در هر نقطه‌ای ایمن و غیرقابل نفوذ کند.»

شرکت Proofcraft، از معدود مجموعه‌هایی که سال‌هاست خدمات سنتی اثبات صوری ارائه می‌دهد، اعلام کرده که افزایش توجه به این حوزه به سیل تقاضا از سوی مشتریان بالقوه انجامیده است. جون آندرونیک (June Andronick)، مدیرعامل و گِروین کلاین (Gerwin Klein)، دانشمند ارشد این شرکت، می‌گویند میزان تقاضا بسیار فراتر از ظرفیت پاسخگویی آن‌ها و رقبایشان در این حوزه است.

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