ریاضیدانان و هوش مصنوعی در پشت صحنه بر سر حقیقت با هم می جنگند

به سختی می توان مطمئن بود که هوش مصنوعی حدس های ریاضی را حل کرده است

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

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

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

نرم افزار پیشرو برای انجام این کار، Lean، در دنیای هوش مصنوعی به عنوان راهی مناسب برای غول های فناوری برای اثبات سریع و قاطع خروجی مدل های خود شناخته شده است. با استفاده از Lean است که شرکت ها می توانند اعلامیه های جسورانه ای در مورد حل پازل های پیچیده ارائه دهند. بدون آن، آنها فقط می توانستند ادعا کنند که راه حل ممکنی برای معماها پیدا کرده اند و سپس ریاضیدانان انسانی را برای ارزیابی راه حل ها دعوت کنند - کاری که ممکن است هفته ها یا ماه ها طول بکشد.

لئوناردو دی مورا Lean را در دهه 2010 و در حین کار در Microsoft Research ایجاد کرد. او می‌گوید که این نرم‌افزار در ابتدا یک ابزار تخصصی بود که فقط توسط ریاضیدانان انسانی مورد استفاده قرار می‌گرفت و هرگز هیچ تلاشی برای فریب یا دستکاری صورت نگرفت.

همه چیز در ژوئیه امسال تغییر کرد، زمانی که مهندس نرم افزار رامانا کومار اعلام کرد که حدس کولاتز - یکی از مشهورترین مسائل باز در تمام ریاضیات - را رد کرده است و برای تایید ادعای خود یک رسمی سازی ناب را منتشر کرد.

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

کد رسمی‌شده‌ای که توسط دو هسته بررسی می‌شود، به همان اندازه که همه چیز در برابر آب قرار نمی‌گیرد، بود.

اما بعد معلوم شد که رد کومار آنطور که به نظر می رسید نبود. او از هوش مصنوعی برای کشف و بهره برداری از دو باگ جداگانه در دو هسته مجزا در کد Lean استفاده کرده بود.

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

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

صرف نظر از انگیزه های کومار، مطمئنا به د مورا، 20 توسعه دهنده تمام وقت که روی Lean و ریاضیدانان کار می کنند، مربوط می شود. آنها می ترسیدند که بازیگران بدخواه بتوانند از هوش مصنوعی برای انجام چنین بدلکاری استفاده کنند، همانطور که کومار انجام داده بود.

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

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

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

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

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

توسعه دهندگان اکنون بر این باورند که رویکرد کومار دیگر موفق نخواهد بود. دی مورا می‌گوید: «ما می‌خواهیم به ایده ضدگلوله بودن خیلی نزدیک‌تر شویم. "می توانم به شما بگویم که اکنون بسیار بهتر می خوابیم. ما باور نداریم که هوش مصنوعی موجود بتواند تمام این لایه های دفاعی را بشکند."

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

به عنوان مثال، هنگام کار با مهندسان OpenAI، تیم Lean یک اشکال در زمان اجرای برنامه خود پیدا کرد - کد کامپایل شده که در واقع توسط یک کامپیوتر اجرا می شود و از کد منبع با استفاده از ابزاری به نام کامپایلر ساخته شده است. آنها با سوء استفاده از این باگ موفق شدند حدسی نادرست را به اشتباه ثابت کنند. این خطا به این دلیل ظاهر شد که کامپایلر کامل نبود، نه به این دلیل که کد Lean دارای خطا بود.

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

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

کوین بازارد در امپریال کالج لندن می گوید: «می توانید جمع را دوباره تعریف کنید. و سپس می توانید آخرین قضیه فرما را که جمع را ذکر می کند، اثبات کنید، و می توانید بگویید که آن را انجام داده اید. اما وقتی مردم واقعا به آنچه واقعا انجام داده‌اید نگاه می‌کنند، شما آن را انجام نداده‌اید.»

این حفره ها هم اکنون در Lean در حال بسته شدن هستند. تلاش دیگر مربوط به Google DeepMind است که فهرستی از مسائل ریاضی باز را که به صراحت در Lean تعریف شده و سپس توسط ریاضیدانان به دقت بررسی شده اند، نگهداری می کند. هرکسی که ادعا می‌کند یکی از این مشکلات را حل کرده است، می‌تواند تعریف مناسب را از قفسه برداشته و از آن به شکلی تغییر نیافته برای آزمایش اثبات پیشنهادی خود در Lean استفاده کند. انجام این کار نشان می دهد که آنها سعی نمی کنند با تغییر نامحسوس تعریف مشکل به تقلب بپردازند تا حل آن بسیار آسان تر شود.

برای مثال، وقتی OpenAI پازل Navier-Stokes را در اوایل این ماه حل کرد، می‌دانستیم که در زمینی پایدار است زیرا بیانیه ارائه شده به Lean مستقیما از فهرست حدس‌های رسمی گرفته شده بود.

اما برای برخی، هیچ یک از این تلاش ها هرگز کافی نخواهد بود.

بازارد می گوید: «دانشمندان کامپیوتر، به طور کلی، افراد بسیار پارانوئیدی هستند و احتمالا دلیل خوبی دارند، زیرا آنها همه چیز را دیده اند. "شما می توانید افرادی را پیدا کنید که هرگز چیزی را باور نخواهند کرد. شما می گویید "من میلیون ها بار آن را بررسی کرده ام" و آنها می گویند "خب، در مورد اشعه گاما [تغییر بیت ها در حافظه] چطور، آیا آنها را بررسی کردید؟" برخی از افراد هستند که شما هرگز نمی توانید آنها را متقاعد کنید."