مقاله‌ای جدید می‌گوید اثبات ناویر–استوکس OpenAI و کد Lean آن با یکدیگر مطابقت ندارند
OpenAI اعلام کرده بود که عامل‌های هوش مصنوعی این شرکت یکی از هفت مسئله جایزه هزاره ریاضیات را در ۸۸ ساعت حل کرده‌اند. اما مقاله‌ای که در ۶ اکتبر منتشر شد می‌گوید اثباتی که با رایانه بررسی شده و این شرکت منتشر کرده، در واقع با استدلال انگلیسی‌ای که قرار بود آن را تأیید کند، مطابقت ندارد.
در ۸ سپتامبر، OpenAI اعلام کرد یک سامانه داخلی متشکل از حدود ۱۰ هزار عامل هوش مصنوعی که به‌صورت موازی برای ۸۸ ساعت کار کرده‌اند، راه‌حلی برای مسئله وجود و همواری ناویر–استوکس ارائه کرده است؛ مسئله‌ای که یکی از هفت مسئله جایزه هزاره مؤسسه ریاضیات کلی است و از سال ۲۰۰۰ جایزه‌ای یک میلیون دلاری برای حل آن تعیین شده است. OpenAI دو نسخه از این نتیجه منتشر کرد: یک اثبات با زبان طبیعی که به شیوه معمول ریاضیدانان نوشته شده بود و نسخه‌ای جداگانه که به Lean، نرم‌افزار بررسی رسمی اثبات‌ها، ترجمه شده بود تا منطق اثبات به‌صورت ماشینی بررسی شود.
مشکل از همین بخش دوم آغاز می‌شود. مقاله‌ای با عنوان «ناویر–استوکس در ترجمه گم شد» که در ۶ اکتبر در arXiv توسط الکساندر باستونیس، فابیان چیرچلی و آندرس سی. هانسن منتشر شد، استدلال می‌کند نسخه تأییدشده در Lean با اثبات زبان طبیعی‌ای که قرار بود آن را رسمی‌سازی کند، یکسان نیست. به گفته نویسندگان، هوش مصنوعی هنگام تبدیل استدلال انگلیسی به کد، ریاضیات را به‌درستی ترجمه نکرده است. Lean منطق یک اثبات را تأیید کرده، اما نه لزوماً همان اثباتی را که OpenAI گفته بود در حال بررسی آن است.
هانسن درباره ادعای مقاله با احتیاط صحبت کرده است. او طبق گزارشی از New Scientist درباره این یافته‌ها گفت: «ما نمی‌گوییم اثبات با زبان طبیعی اشتباه است. همچنین نمی‌گوییم که درست است.» مسئله این نیست که ریاضیات OpenAI نادرست است؛ مسئله این است که بررسی Lean، یعنی بخشی که قرار بود تردید انسانی را از میان بردارد، در این مورد دقیقاً این کار را انجام نداده است.
پیدا کردن این اختلاف نیز سریع نبود. گزارش‌های مربوط به مقاله نشان می‌دهند نویسندگان حدود دو هفته زمان صرف کردند؛ ابتدا از ChatGPT خواستند اختلاف‌های احتمالی را شناسایی کند و سپس موارد را دستی بررسی کردند تا به یک تفاوت واقعی میان چیزی که اثبات انگلیسی ادعا می‌کرد و چیزی که کد Lean بررسی کرده بود، برسند. عامل‌های OpenAI نتیجه اولیه را در ۸۸ ساعت به دست آوردند و سپس ۱۷ ساعت دیگر برای رسمی‌سازی آن در Lean صرف کردند. یافتن این ناسازگاری برای یک تیم انسانی بیش از سه برابر زمان مجموع این فرایند طول کشید.
OpenAI به New Scientist گفت از وجود فاصله میان دو نسخه آگاه است و این اختلاف به معنای نادرست بودن هیچ‌کدام از اثبات‌ها نیست. این شرکت اعلام کرد خطاهای موجود در اثبات زبان طبیعی را هر زمان که شناسایی شوند اصلاح خواهد کرد. چنین واکنشی برای یک گزارش خطا منطقی به نظر می‌رسد، اما پرسش اصلی مطرح‌شده در مقاله را حل نمی‌کند: اگر بررسی Lean تضمین نمی‌کند که اثبات رسمی همان چیزی را می‌گوید که اثبات انگلیسی بیان کرده است، دقیقاً چه چیزی بررسی شده است؟
زمان‌بندی این ماجرا نیز از ابتدا بحث‌برانگیز بود. اعلام OpenAI تنها یک روز پس از آن منتشر شد که تریستان باک‌مستر، ریاضیدان دانشگاه نیویورک، و لِوِنت آلپوگه، پژوهشگر Anthropic، اثباتی رسمی‌شده در Lean درباره انفجار یک معادله مرتبط با سیالات منتشر کردند. باک‌مستر گفته است در ۳ سپتامبر به OpenAI ایمیل زده و اطلاع داده بود که او و آلپوگه نیز پژوهشی مرتبط دارند که به‌زودی منتشر می‌شود؛ این اقدام پس از انتشار شایعاتی درباره پیشرفت آنها انجام شد. به گفته باک‌مستر، OpenAI به او پیشنهاد داد اعتبار نویسندگی انحصاری نتیجه ناویر–استوکس را دریافت کند، به شرط آنکه نام آلپوگه حذف شود.
سباستین بوبک، پژوهشگر OpenAI، این روایت را در شبکه‌های اجتماعی رد کرد. باک‌مستر همچنین ادعا کرده است که وقتی تهدید کرد این گفت‌وگو را عمومی می‌کند، بوبک از او پرسید: «چرا می‌خواهی حرفه‌ات را خراب کنی؟» سم آلتمن نیز کمتر از نیم ساعت پس از انتشار روایت بوبک در شبکه اجتماعی X، از نسخه او از ماجرا حمایت کرد. بیانیه OpenAI اعلام کرد پژوهشگران و عامل‌های این شرکت هرگز آثار منتشرنشده باک‌مستر و آلپوگه را ندیده‌اند، اما پذیرفت که «نمی‌تواند رد کند» داده‌های ناشناس‌شده استفاده از Codex توسط آنها به بهبود مدل‌هایش کمک کرده باشد.
در پس اختلاف درباره اعتبار نویسندگی، یک پرسش فنی محدودتر نیز وجود دارد. اثبات OpenAI نسخه «اجباری» معادلات ناویر–استوکس را بررسی می‌کند؛ حالتی که در آن یک نیروی خارجی بر سیال وارد می‌شود. OpenAI می‌گوید این نتیجه گزاره‌های C و D در صورت‌بندی رسمی مؤسسه کلی را اثبات می‌کند. مؤسسه کلی نیز در ۱۱ سپتامبر اعلام کرد که این مسئله «ظاهراً حل شده است»، هرچند تأکید کرد فرایند بررسی جایزه عمداً با سرعتی آهسته پیش می‌رود.
هیچ‌یک از این موارد ثابت نمی‌کند که ریاضیات اصلی OpenAI اشتباه است. با این حال، مقاله باستونیس، چیرچلی و هانسن فراتر از یک گزارش خطای ساده می‌رود و استدلال می‌کند تضمین ترجمه‌ای با وفاداری معنایی میان زبان طبیعی و Lean از نظر نظری ممکن نیست و حتی در محدوده مسائلی قرار می‌گیرد که علوم رایانه نمی‌تواند در اصل آنها را حل کند؛ مشابه مسئله توقف. اگر این دیدگاه پابرجا بماند، عبارت «این موضوع در Lean تأیید شده است» دیگر برگ برنده قطعی‌ای که آزمایشگاه‌های هوش مصنوعی برای چنین اثبات‌هایی در نظر می‌گیرند نخواهد بود؛ نه برای این اثبات و شاید نه برای موارد دیگری که با روش مشابه ساخته می‌شوند.
پنج هفته پیش، OpenAI با نتیجه‌ای روبه‌رو بود که در نگاه اول یک دستاورد تاریخی در ریاضیات به نظر می‌رسید و هم‌زمان با اختلافی درباره اینکه چه کسی باید اعتبار آن را دریافت کند مواجه شد. اکنون یک پرسش دیگر نیز به این موضوع اضافه شده است: آیا بخشی از این اعلامیه که قرار بود غیرقابل‌بحث‌ترین قسمت باشد، یعنی اثبات بررسی‌شده توسط ماشین، واقعاً همان چیزی را بررسی کرده است که OpenAI ادعا می‌کرد؟