‏اثبات ریاضی برای کدی که هوش مصنوعی نوشته

مقاله با یه تشبیه شروع می‌شه: به کدی که هوش مصنوعی نوشته باید همون‌قدر اعتماد کنی که به کد یه برنامه‌نویس تازه‌کار ساعت ۲ شب، یعنی هیچی، تا وقتی یه چیزی چکش کنه. formal verification (یعنی اثبات ریاضی اینکه برنامه دقیقاً طبق مشخصاتش رفتار می‌کنه) همون ابزاریه که نویسنده برای این کار پیشنهاد می‌ده. به‌جای اینکه برنامه رو با چند تا ورودی نمونه تست کنی، تعریف «درست» رو به یه جمله‌ی منطقی تبدیل می‌کنی و یه solver یا proof assistant چک می‌کنه که کد برای همه‌ی ورودی‌های ممکن درسته یا نه.

این روش جدید نیست و خیلی قبل از مدل‌های زبانی بزرگ وجود داشته. توی جاهایی که خطا فاجعه‌ست ازش استفاده می‌شه، مثل سیستم‌های جلوگیری از برخورد هواپیما، طراحی چیپ و سیستم‌های embedded حساس. ابزارهاش هم شناخته‌شده‌ان: SAT/SMT solverها، model checkerها و proof assistantها.

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

نویسنده می‌گه این روش واقع‌بینانه‌ست، ولی برای یه بخش محدود از مشکل. formal verification وقتی خوب کار می‌کنه که بشه ویژگی رو دقیق تعریف کرد، مثلاً «این تابع هیچ‌وقت تقسیم بر صفر نمی‌کنه» یا «این parser هیچ‌وقت بیرون از buffer خودش نمی‌نویسه». ولی کد روزمره‌ای که هوش مصنوعی تولید می‌کنه معمولاً مشخصات رسمی نداره، و چیزی که مشخصات نداره رو نمی‌شه خودکار تأیید کرد. برای همین بخشی از پژوهش‌ها روی تولید مشخصات کنار خود کد، یا وصل کردن verification به حلقه‌ی تولید کد کار می‌کنن.

پژوهشگرهای Stanford که روی automated reasoning کار می‌کنن هم توی یه کنفرانس اخیر درباره‌ی ایمنی هوش مصنوعی همین موضوع رو بررسی کردن. نگاهشون مهندسیه: امن کردن کد هوش مصنوعی مثل امن کردن هواپیما یا چیپه، یه مشکل سخت ولی قابل حل با ابزارهای شناخته‌شده. به گفته‌ی مقاله، ریسک واقعی کوتاه‌مدت اینه که مدل‌ها کار مهاجم‌های انسانی رو برای پیدا کردن ضعف‌های سیستم‌های قدیمی مثل بیمارستان‌ها و بانک‌ها راحت‌تر کنن، نه اینکه خودشون تصمیم به حمله بگیرن.

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

نکات کلیدی:

• تست فقط باگ‌هایی رو پیدا می‌کنه که بهشون فکر کردی، formal verification ویژگی رو برای همه‌ی ورودی‌ها اثبات می‌کنه.
• ابزارهای اصلی: SAT/SMT solverها، model checkerها و proof assistantها.
• این روش قبلاً توی سیستم ضدبرخورد هواپیما و طراحی چیپ امتحانش رو پس داده.
• بیشترین کارایی روی ویژگی‌های دقیق مثل memory safety یا نبود تقسیم بر صفره.
• بیشتر دستیارهای کدنویسی فعلاً به هیچ ابزار verification وصل نیستن.