OpenAI سه دست‌نوشته را پس از یک روز پس گرفت و «پیمان ریاضی» را زیر سؤال برد
نویسنده: انریکو بوچی
۱۴ اکتبر ۲۰۲۶
روز سه‌شنبه ۶ اکتبر، یک مخزن گیت‌هاب متعلق به OpenAI با نام ساده «math» منتشر شد. این مخزن شامل ۷۲۲ مقاله ریاضی بود که در ۳۷۲ خانواده از نتایج دسته‌بندی شده بودند و حوزه‌هایی از هندسه جبری تا علوم کامپیوتر نظری را پوشش می‌دادند. همه این نتایج توسط یک مدل داخلی شرکت تولید شده بود؛ مدلی که OpenAI آن را عرضه نکرده و حتی نامش را نیز اعلام نکرده است.
کمتر از ۲۴ ساعت بعد، سه مقاله از این مجموعه به دلیل یک خطا پس گرفته شدند؛ اتفاقی که در تاریخ اصلاح و پس‌گرفتن مقالات علمی بسیار غیرمعمول است، زیرا معمولاً این یک پژوهشگر منفرد است که در برابر اتهام خطا قرار می‌گیرد و مجبور به عقب‌نشینی می‌شود، نه یکی از بزرگ‌ترین شرکت‌های هوش مصنوعی جهان. طبق داده‌هایی که خود OpenAI منتشر کرده، این مدل با حدود چهار هزار مسئله باز روبه‌رو شده و ChatGPT Pro برای هر نتیجه به‌طور میانگین سه ساعت محاسبه انجام داده است. این پروژه پس از آن آغاز شد که آزمون‌های ریاضی معمول شرکت دیگر معیار مفیدی محسوب نمی‌شدند، زیرا مدل همه آن‌ها را حل می‌کرد.
در میان ادعاهای مطرح‌شده در این دست‌نوشته‌ها، اثبات «حدس بازی‌های یکتا» (Unique Games Conjecture) قرار داشت؛ مسئله‌ای که بیش از ۲۰ سال جایگاه مهمی در علوم کامپیوتر نظری داشته است. همچنین ادعایی درباره وجود ناحیه‌ای بدون صفر برای همه توابع L دیریکله مطرح شده بود. با این حال، هیچ‌یک از این مقالات به پنج مسئله حل‌نشده هزاره نمی‌پرداختند. به گفته یک سخنگوی شرکت، تقریباً همه نتایج از یک دستور واحد به یک عامل واحد هوش مصنوعی به دست آمده‌اند و بسیاری از آن‌ها هنوز حتی برای ریاضی‌دانان خود شرکت نیز به‌طور کامل درک نشده‌اند.
از آنجا که این مدل در دسترس عموم نیست، هیچ فردی خارج از OpenAI نمی‌تواند این ادعاها را به‌طور مستقل بررسی کند. به همین دلیل، در ۲۹ سپتامبر، گروه مشورتی ریاضیات و هوش مصنوعی وابسته به مؤسسه مطالعات پیشرفته پرینستون از آزمایشگاه‌های هوش مصنوعی خواسته بود هر نتیجه را همراه با دستورهای ورودی تولیدکننده آن و هزینه محاسباتی مرتبط منتشر کنند. OpenAI در پاسخ تنها میانگین میزان محاسبات موردنیاز را ارائه داد و ده خلاصه کوتاه‌شده از روند استدلال مدل منتشر کرد، اما دستورهای ورودی را منتشر نکرد.
خطایی که در ۷ اکتبر در گزارش تغییرات مخزن اعلام شد، مربوط به یک علامت اشتباه در دست‌نوشته‌ای درباره جبری‌بودن کلاس‌های ویل برای برخی واریته‌های آبلی هشت‌بعدی بود. این اشتباه یک استدلال حذف و خنثی‌سازی را بی‌اعتبار می‌کرد و در نتیجه ساختاری را که دو مقاله دیگر بر آن بنا شده بودند، از جمله مقاله‌ای که حدس هاج منطقی برای حاصل‌ضرب سطوح K3 را اثبات می‌کرد، زیر سؤال می‌برد. هر سه دست‌نوشته به خانواده نتایج مرتبط با حدس هاج تعلق داشتند؛ بخشی که بیشترین توجه را در کل این مجموعه به خود جلب کرده بود. مقاله دارای خطا که تاریخ آن ۱۸ سپتامبر بود، نیز یکی از قدیمی‌ترین نوشته‌های این مجموعه محسوب می‌شد.
در همان روز، OpenAI چهارده دست‌نوشته دیگر را اصلاح کرد و اثبات‌ها، اظهارات و فرضیات آن‌ها را بهبود داد. همچنین منابع کتاب‌شناختی سیزده مقاله دیگر را به‌روزرسانی کرد. در نتیجه، تعداد عناوین فهرست از ۷۲۲ به ۷۱۹ کاهش یافت و نسخه‌های پس‌گرفته‌شده همچنان همراه با توضیحی درباره حذف مورد نظر در دسترس باقی ماندند.
یک سخنگوی شرکت اعلام کرد که این خطا در جریان یک بررسی داخلی کشف شده است، اما مشخص نکرد چه کسی آن را شناسایی کرده است. او همچنین گفت روند بازبینی، مانند هر دست‌نوشته پژوهشی دیگر، ادامه خواهد داشت و مقالاتی که اصلاح آن‌ها ممکن نباشد، پس گرفته خواهند شد. OpenAI معمولاً در پاسخ به نگرانی‌ها به زبان برنامه‌نویسی بازمتن Lean اشاره می‌کند؛ زبانی که در آن یک اثبات به شکلی دقیق بازنویسی می‌شود تا برنامه بتواند همه مراحل آن را بررسی کند.
با این حال، هنگام انتشار مقاله تنها ۱۶۲ مورد از ۷۲۲ دست‌نوشته دارای نتیجه اصلی رسمی‌شده در Lean بودند. پس از اصلاحات ۷ اکتبر، این رقم به ۳۰۰ نتیجه اصلی از ۷۱۹ مقاله رسید؛ یعنی کمی بیش از ۴۲ درصد. این نسبت از آن زمان تغییر نکرده است، زیرا گزارش تغییرات تنها همان یک مورد را ثبت کرده و فایل README نیز همان درصد را تکرار می‌کند. شرکت می‌پذیرد که برخی نتایج غیررسمی‌شده ممکن است دارای خطا باشند و توضیح می‌دهد که بنا بر توصیه گروه مشورتی، آن‌ها را پیش از رسمی‌سازی کامل منتشر کرده است؛ هرچند مقایسه با فهرست مخزن نشان می‌دهد تقریباً همه موارد پس‌گرفته‌شده یا به‌طور اساسی اصلاح‌شده خارج از بخش تأییدشده توسط Lean قرار داشته‌اند.
اینکه حتی بخش تأییدشده نیز نیازمند احتیاط است، با نمونه‌ای که در ۸ سپتامبر رخ داد روشن می‌شود. در آن زمان OpenAI اعلام کرد اثباتی ۱۶۶ صفحه‌ای درباره شکل‌گیری تکینگی در زمان محدود در معادلات سیالات تولید کرده است؛ اثباتی که حاصل کار حدود ۱۰ هزار عامل هوش مصنوعی در ۸۸ ساعت بود و ۱۷ ساعت دیگر نیز برای رسمی‌سازی آن در Lean صرف شد. با این حال، این نتیجه مربوط به معادلاتی با نیروی خارجی بود، در حالی که مسئله هزاره به حالت بدون نیروی خارجی مربوط می‌شود و به همین دلیل مؤسسه کلی آن را حل‌شده نمی‌داند.
در ۶ اکتبر، هم‌زمان با انتشار ۷۲۲ دست‌نوشته، الکساندر باستونیس، فابیان چیرچلی و آندرس سی. هانسن پیش‌چاپی در arXiv با عنوان «Navier-Stokes lost in translation» منتشر کردند. آن‌ها در این مقاله استدلال می‌کنند که اثبات رسمی‌شده در Lean با اثبات نوشته‌شده به زبان طبیعی یکسان نیست و متن طبیعی ادعایی بیش از آنچه کد تأیید می‌کند مطرح می‌کند. آن‌ها همچنین نمونه‌های دیگری از ترجمه‌های نادرست تولیدشده توسط سامانه‌های هوش مصنوعی ارائه کرده و در سطح نظری مدعی شده‌اند که تضمین وفاداری یک رسمی‌سازی، مسئله‌ای ذاتاً دشوارتر از مسئله توقف تورینگ است.
از آنجا که این مقاله یک پیش‌چاپ است، OpenAI ظاهراً آن را بازتولید نکرده و چکیده آن نیز نسخه‌ها یا فایل‌های مشخصی را معرفی نمی‌کند، نتیجه‌گیری‌های آن باید با دقت بررسی شود. یک اثبات رسمی که مسیر متفاوتی از نسخه نوشته‌شده طی کند، همچنان معتبر است، مشروط بر اینکه گزاره رسمی‌شده همان قضیه مورد نظر باشد؛ مشکل زمانی ایجاد می‌شود که خود گزاره‌ها متفاوت باشند.
با این حال، مسئله به هر ۷۱۹ دست‌نوشته مربوط می‌شود، زیرا Lean تضمین می‌کند کدی که ارائه شده، همان چیزی را اثبات می‌کند که در کد نوشته شده است؛ اما اینکه آنچه در کد آمده با قضیه‌ای که ریاضی‌دانان قصد اثبات آن را دارند یکسان است یا نه، همچنان وظیفه انسان‌ها باقی می‌ماند و میان‌بری برای آن وجود ندارد. بنابراین رقم ۴۲ درصد تنها نشان می‌دهد چه بخشی از مجموعه توسط ماشین بررسی شده است، نه اینکه چه مقدار از آن واقعاً درست است.
پس‌گرفتن این مقالات در پایان یک ماه پرتنش رخ داد؛ ماهی که با اختلاف بر سر اولویت علمی در اعلام نتیجه مربوط به معادلات ناویر–استوکس آغاز شد، زمانی که مشخص شد دو ریاضی‌دان، آلپوگه و باک‌مستر، روی یک مسئله مشابه کار می‌کردند. این تنش‌ها در ۱۱ سپتامبر با بیانیه‌ای ادامه یافت که در آن ۲۵ برنده مدال فیلدز، از جمله ترنس تائو، از استفاده صنعت هوش مصنوعی از مسائل ریاضی به‌عنوان میدان آزمایش انتقاد کردند.
اورسولا مارتین، ریاضی‌دان دانشگاه آکسفورد، انتشار انبوه ۷۲۲ دست‌نوشته را به ارائه یک پیش‌نویس آشفته تشبیه کرد که جامعه علمی باید آن را مرتب کند. اعداد نیز این مقایسه را تأیید می‌کنند؛ زیرا هر دست‌نوشته برای OpenAI به‌طور میانگین سه ساعت محاسبه هزینه داشته، در حالی که بررسی آن‌ها هفته‌ها یا ماه‌ها کار تخصصی پژوهشگرانی را می‌طلبد که خود این وظیفه را درخواست نکرده‌اند.
این شرکت وعده داده است برای کمک به ریاضی‌دانان در فهم نتایج، کارگاه‌ها و کنفرانس‌هایی تأمین مالی کند و می‌گوید در حال کار روی انتشار مدل است. گروه مشورتی نیز این انتشار را آغاز فهم انسانی دانسته، نه پایان آن؛ به این معنا که بخش عمده کار تازه شروع شده و انجام آن بر عهده دیگران خواهد بود.
خطای علامت شاید انسانی‌ترین نوع خطا باشد؛ خطایی که هم برای دانشجویی در نخستین آزمون و هم برای برندگان مدال فیلدز ممکن است رخ دهد. اما آنچه این رویداد زیر سؤال می‌برد، نه امکان اشتباه، بلکه نحوه تقسیم مسئولیت است. ریاضیات بر پیمانی استوار است که در آن کسی که یک اثبات را امضا می‌کند، آن را می‌فهمد و از آن دفاع می‌کند و جامعه علمی نیز آن را بررسی می‌کند.
این پیمان زمانی دچار مشکل می‌شود که نویسنده یک مدل باشد که کسی نمی‌تواند از آن سؤال کند و بررسی‌کنندگان، ریاضی‌دانانی باشند که چنین مسئولیتی را نخواسته‌اند. قرار بود Lean راهی برای حل این مشکل باشد و بررسی را به نرم‌افزار بسپارد، اما ماجرای ناویر–استوکس یادآوری می‌کند که نرم‌افزار تنها چیزی را بررسی می‌کند که به آن داده شده است. تا زمانی که OpenAI قضیه‌های جدید را سریع‌تر از آنچه جهان می‌تواند بخواند تولید کند، واژه «اثبات‌شده» باید با احتیاط به کار رود؛ حتی زمانی که یک رایانه آن را تأیید کرده باشد.