۳۷۲ نتیجه ریاضی OpenAI: تاکنون چه چیزهایی واقعاً تأیید شده است؟
نویسنده: Alius Noreika
نکات کلیدی
- انتشار گیت‌هاب OpenAI در ۶ اکتبر اکنون ۷۱۹ دست‌نوشته را در ۳۷۲ خانواده نتیجه فهرست می‌کند. پس از آنکه در ۷ اکتبر سه مقاله به دلیل یک خطای علامت که یک اثبات و دو مقاله وابسته به آن را مختل کرده بود، حذف شدند.
- طبق به‌روزرسانی OpenAI در ۷ اکتبر، از میان ۷۱۹ نتیجه اصلی، ۳۰۰ نتیجه (حدود ۴۲ درصد) دارای صورت‌بندی رسمی در Lean هستند که رایانه آن‌ها را بررسی کرده است. OpenAI هشدار داده است که بخش باقی‌مانده که رسمی‌سازی نشده ممکن است دارای خطا باشد.
- این ۳۷۲ خانواده نتیجه از حدود ۴ هزار مسئله‌ای به دست آمده‌اند که یک مدل داخلی منتشرنشده با آن‌ها آزمایش شده است؛ هر نتیجه به‌طور میانگین حدود سه ساعت توان محاسباتی در سطح ChatGPT Pro نیاز داشته است.
- ۱۴ دست‌نوشته دیگر نیز در یک روز پس از انتشار با اصلاح اثبات‌ها یا تصحیح گزاره‌ها بازبینی شدند و یک ریاضی‌دان دانشگاه کرنل به Retraction Watch گفت انتظار دارد خطاهای بیشتری آشکار شود.
- انجمن ریاضیات انسانی از ریاضی‌دانان خواست همکاری با OpenAI را متوقف کنند، در حالی که گروه مشورتی‌ای که OpenAI با آن مشورت کرده بود اعلام کرد نقش آن به معنای تأیید نتایج یا فرایند انتشار نبوده است.
عدد اصلی که در تیترها دیده می‌شود، عدد درستی نیست
بخش زیادی از گزارش‌ها درباره انتشار ریاضیات OpenAI در ۶ اکتبر با یکی از دو عدد آغاز می‌شوند: ۷۲۲ مقاله نوشته‌شده توسط هوش مصنوعی یا ۳۷۲ مسئله حل‌شده. اما هیچ‌کدام وضعیت فعلی مخزن را دقیق نشان نمی‌دهد. پس از اصلاحیه ۷ اکتبر، مخزن openai/math در گیت‌هاب شامل ۷۱۹ دست‌نوشته است که در ۳۷۲ خانواده دسته‌بندی شده‌اند. یک خانواده به معنای یک مسئله نیست؛ بلکه مجموعه‌ای از یک نتیجه اصلی، استدلال‌های همراه، پیامدها یا اثبات‌های جایگزین است.
ارقام مربوط به میزان استحکام این نتایج کمتر مورد توجه قرار گرفته‌اند. حدود ۴۲ درصد از نتایج اصلی دارای صورت‌بندی Lean هستند؛ یعنی یک رایانه اثبات را گام‌به‌گام بررسی کرده است. سه دست‌نوشته در یک روز حذف شدند، ۱۴ مورد دیگر اصلاح شدند و ۳۷۲ خانواده نتیجه از حدود ۴ هزار مسئله‌ای به دست آمده‌اند که مدل با آن‌ها مواجه شده بود؛ مخرجی که معمولاً در تیترها دیده نمی‌شود.
این موارد به معنای کوچک بودن این انتشار نیست. برخی پژوهشگران برجسته آن را رویدادی تاریخی خوانده‌اند. اما فهرستی از ۳۷۲ ادعا، فهرستی از ۳۷۲ قضیه اثبات‌شده نیست و فاصله میان این دو، موضوع اصلی بحث‌های این هفته بوده است.
OpenAI می‌گوید چه چیزی منتشر کرده است
OpenAI در اعلام نتایج ریاضی خود گفت این کار از یک مدل داخلی پیشرفته به دست آمده و همراه با پروتکل‌هایی برای اصلاحات و ارجاع‌ها منتشر شده است. این شرکت صورت‌بندی‌های Lean برای بسیاری از اثبات‌ها، ۱۰ خلاصه از فرایند استدلال مدل، برآوردهای محاسباتی و آمار مربوط به مسائل آزمایش‌شده را ارائه کرد. OpenAI هزینه متوسط را حدود سه ساعت تفکر در سطح ChatGPT Pro برای هر نتیجه اعلام کرد.
README مخزن نسبت به بسیاری از تیترهای رسانه‌ای محتاطانه‌تر است. در آن آمده که نتایج در مراحل مختلف تأیید قرار دارند، همه آن‌ها نسخه Lean ندارند و برخی نتایج بدون رسمی‌سازی ممکن است مشکل داشته باشند. این فایل همچنین دو استثنا در روش استاندارد تولید را مشخص می‌کند: کار روی ناحیه بدون صفر تابع زتای ریمان و اثبات حدس هاج برای واریته‌های آبلی CM. یکی از نوشته‌های مربوط به ریمان برای خوانایی توسط انسان‌ها ویرایش شده است.
OpenAI می‌گوید برای نحوه انتشار با گروه مشورتی ریاضیات و هوش مصنوعی که در مؤسسه مطالعات پیشرفته فعالیت می‌کند، مشورت کرده است. این شرکت قصد دارد کارگاه‌ها و کنفرانس‌هایی را برای کمک به پژوهشگران در درک نتایج تولیدشده توسط هوش مصنوعی تأمین مالی کند و می‌گوید در حال کار برای انتشار مسئولانه خود مدل است.
روز دوم: یک خطای علامت، سه مقاله حذف‌شده
اولین اصلاح خیلی سریع انجام شد. در ۷ اکتبر، تاریخچه نسخه‌های مخزن ثبت کرد که یک خطای علامت در مقاله‌ای درباره کلاس‌های ویل در هشت‌بعدی‌های آبلی شکافته، یک استدلال حذف و همچنین ساختاری را که دو مقاله دیگر به آن وابسته بودند، خراب کرده است. OpenAI هر سه مقاله را حذف کرد؛ از جمله مقاله‌ای که ادعا می‌کرد حدس هاج منطقی برای حاصل‌ضرب سطوح K3 را اثبات کرده است.
همان مدخل همچنین اصلاح ۱۴ دست‌نوشته دیگر را ثبت می‌کند؛ از اصلاح اثبات‌ها گرفته تا تصحیح گزاره‌ها و روشن‌تر کردن فرضیه‌ها، به‌علاوه به‌روزرسانی ارجاع‌ها در ۱۳ مقاله دیگر. شش رسمی‌سازی جدید نیز سهم نتایج بررسی‌شده با ماشین را به ۳۰۰ مورد از ۷۱۹ نتیجه اصلی رساند.
از یک دیدگاه، این روند نشان‌دهنده کارکرد درست فرایند علمی است: خطا پیدا شد، به‌صورت عمومی اعلام شد و در کمتر از یک روز ثبت نسخه‌ای شد؛ مقالات حذف‌شده نیز همچنان همراه با توضیح درباره مشکل در دسترس هستند. اما از دیدگاهی دیگر، یک اشتباه واحد پیش از آنکه ریاضی‌دانان بیرونی فرصت بررسی داشته باشند، به سه مقاله راه یافته بود. الکس تاونسند، ریاضی‌دان دانشگاه کرنل، به Retraction Watch که خبر حذف‌ها را منتشر کرد گفت این زنجیره خطا برای او غافلگیرکننده نیست و احتمال می‌دهد خطاهای بیشتری آشکار شوند.
بررسی Lean چه چیزی را ثابت می‌کند و چه چیزی را نه
Lean یک زبان برنامه‌نویسی برای نوشتن اثبات‌هاست. اگر یک اثبات رسمی در آن کامپایل شود، هر گام منطقی از فرض‌های اعلام‌شده تا نتیجه نهایی توسط ماشین بررسی شده است؛ موضوعی که از خواندن دقیق یک داور انسانی نیز قوی‌تر محسوب می‌شود. به همین دلیل، رقم ۴۲ درصد مهم‌ترین عدد این انتشار است.
با این حال، هنوز دو شکاف وجود دارد. نخست مسئله ترجمه است: Lean درستی گزاره رسمی را تأیید می‌کند، نه اینکه این گزاره دقیقاً همان چیزی باشد که مقاله انگلیسی ادعا می‌کند. ممکن است قضیه‌ای با فرضیه‌ای کمی متفاوت رسمی‌سازی شود و بررسی Lean را بگذراند، در حالی که ادعای اصلی مقاله همچنان اثبات نشده باشد. دوم مسئله معناست: بررسی ماشینی چیزی درباره تازه بودن، اهمیت یا ارتباط واقعی یک نتیجه با مسئله باز مورد نظر نمی‌گوید.
برای ۵۸ درصد باقی‌مانده از نتایج اصلی، هیچ بررسی ماشینی وجود ندارد و بررسی انسانی نیز تازه آغاز شده است. اسکات آرونسون، نظریه‌پرداز پیچیدگی، در ۷ اکتبر نوشت که ظاهراً هنوز تقریباً هیچ‌کس بیشتر این اثبات‌ها را درک نکرده است. همسر او، دانا موشکوویتز، که سال‌ها روی حدس بازی‌های یکتا کار کرده، در پیامی به او نوشته بود که اثبات ادعاشده «آن‌قدر بد نوشته شده که بدون کمک هوش مصنوعی خواندن آن غیرممکن است». این اثبات، نکته قابل توجه، یکی از موارد دارای گواهی Lean است.
| عدد مطرح‌شده در گزارش‌ها | آنچه واقعاً شمارش می‌کند | منبع | وضعیت |
|---|---|---|---|
| ۷۲۲ | دست‌نوشته‌های منتشرشده در ۶ اکتبر | مخزن OpenAI هنگام آغاز انتشار | منسوخ |
| ۷۱۹ | دست‌نوشته‌ها پس از حذف سه مورد | تاریخچه مخزن، ۷ اکتبر | فعلی |
| ۳۷۲ | خانواده‌های نتیجه (گروه‌هایی از مقالات مرتبط)، نه مسائل جداگانه | README مخزن | فعلی |
| حدود ۴۰۰۰ | مسائلی که در ارزیابی به مدل داده شد | README مخزن | عدد اعلام‌شده توسط شرکت |
| ۳۰۰ از ۷۱۹ (حدود ۴۲٪) | نتایج اصلی دارای رسمی‌سازی Lean | تاریخچه مخزن، ۷ اکتبر | احتمال افزایش دارد |
| ۳ و ۱۴ | مقالات حذف‌شده و مقالات اصلاح‌شده | تاریخچه مخزن، ۷ اکتبر | ممکن است افزایش یابد |
| حدود ۱۰٪ | نرخ موفقیت در مسائل آزمایش‌شده، اصلاح‌شده از رقم ۵٪ قبلی | وبلاگ اسکات آرونسون | برآورد بیرونی |
| حدود ۳ ساعت | میانگین توان محاسباتی معادل ChatGPT Pro برای هر نتیجه | اعلامیه OpenAI | ادعای شرکت |
استدلال کسانی که آن را تاریخی می‌دانند
نوشته آرونسون درباره چیزی که آن را «Mathocalypse» می‌نامد، به یکی از منابع اصلی بحث درباره این انتشار تبدیل شده است و او منتقد آن نیست. او ۶ اکتبر را یکی از بزرگ‌ترین روزها در تاریخ ریاضیات خواند و به نتایجی اشاره کرد که به گفته او هرکدام می‌توانند در برخی حوزه‌های علوم کامپیوتر نظری، نتیجه سال باشند؛ از جمله الگوریتم‌های سریع‌تر از n log n برای تبدیل فوریه و ضرب اعداد صحیح و پاسخ مثبت به یک مسئله محاسبات کوانتومی که خود او در سال ۲۰۰۷ مطرح کرده بود.
با این حال، نوشته او نشان می‌دهد اعداد چگونه به‌سرعت تغییر می‌کنند. او ابتدا نوشته بود مدل روی حدود ۸ هزار مسئله با نرخ موفقیت ۵ درصد آزمایش شده، اما پس از اشاره خوانندگان، هر دو رقم را به حدود ۴ هزار مسئله و حدود ۱۰ درصد اصلاح کرد. برخی خلاصه‌های اولیه هنوز اعداد قدیمی را دارند. حتی نرخ اصلاح‌شده نیز باید با احتیاط تفسیر شود، زیرا ۳۷۲ خانواده نتیجه دقیقاً یک‌به‌یک با مسائل آزمایش‌شده منطبق نیستند.
دیگران نیز مقیاس این کار را قابل توجه دانستند. نشریه The Decoder با گردآوری واکنش پژوهشگران، از آلوارو لوزانو-رابله‌دو نقل کرد که این رویداد شاید مهم‌ترین روز تاریخ ریاضیات تا امروز باشد، هرچند او هم به محدودیت‌های مدل اشاره کرد. این نشریه همچنین نوشت OpenAI هدف خود را حل خودِ فرضیه ریمان قرار داده بود اما تنها به نسخه‌ای ضعیف‌تر رسید.
استدلال مخالفان: مسئله فقط اثبات‌ها نیست، فرایند هم مهم است
شدیدترین انتقادها متوجه نحوه انتشار این کار است. انجمن ریاضیات انسانی در ۷ اکتبر بیانیه‌ای درباره این انتشار منتشر کرد و آن را بیشتر نمایش قدرت دانست تا پژوهش علمی و از ریاضی‌دانان خواست همکاری با OpenAI را متوقف کنند. ترنس تائو این بیانیه را بازنشر کرد و باعث گسترده‌تر شدن بازتاب آن شد، هرچند درباره میزان تأیید آن اختلاف نظر وجود دارد و او نویسنده بیانیه نیست.
این انجمن به همان گروه مشورتی‌ای استناد کرد که OpenAI می‌گوید با آن مشورت کرده است و به توصیه‌های قبلی این گروه اشاره داشت که شرکت‌های هوش مصنوعی پیشرفته نباید مسائل پیچیده ریاضی را با مدل‌های داخلی خود آزمایش کنند. پاسخ خود گروه مشورتی به انتشار OpenAI با لحنی کاملاً بی‌طرفانه بود. این گروه گفت نقش آن نباید به‌عنوان داوری درباره نتایج یا تأیید شیوه دستیابی OpenAI به آن‌ها تعبیر شود، توصیه‌های خود را تکرار کرد و قضاوت درباره رعایت آن‌ها را به ریاضی‌دانان واگذار کرد.
آرونسون با درخواست تحریم مخالفت کرد. او استدلال کرد مسائل باز برای تلاش هر کسی هستند، از جمله یک شرکت، و اعضای انجمن به نمایندگی از خود سخن می‌گویند نه کل جامعه علمی؛ با این حال همچنان از جامعه ریاضی خواست شرکت‌های هوش مصنوعی را برای رفتار بهتر تحت فشار قرار دهد. Futurism نیز شکایت گسترده‌تری میان منتقدان را مطرح کرد: اینکه اکنون انتظار می‌رود ریاضی‌دانان کار کند و زمان‌بر بررسی صدها دست‌نوشته فشرده و تا حدی ناخوانا را انجام دهند که خودشان درخواست نکرده بودند.
این انتشار همچنین پس از یک ادعای بحث‌برانگیز در سپتامبر انجام شد. OpenAI در ۸ سپتامبر گفت یک مدل داخلی نشان داده است که معادلات سه‌بعدی ناویر–استوکس می‌توانند در زمان محدود منفجر شوند. مؤسسه ریاضی کلی این نتیجه را نپذیرفته و ساختار ارائه‌شده به یک نیروی خارجی هموار متکی است؛ حالتی که بیشتر متخصصان آن را جدا از نسخه اصلی مسئله مورد توجه خود می‌دانند.
چگونه باید تیترهای بعدی را خواند
برای خوانندگان، قاعده عملی ساده است: هر مورد در مخزن را یک ادعای پیش‌چاپ بدانید، نه یک قضیه تثبیت‌شده. گواهی Lean شواهد قدرتمندی است که یک گزاره رسمی درست است، اما هنوز باید مشخص شود همان گزاره‌ای است که در عنوان و متن مقاله معرفی شده است. تاریخچه مخزن بهترین محل پیگیری است، زیرا OpenAI متعهد شده همه نسخه‌ها و اصلاحات را در آن ثبت کند.
تغییر بزرگ‌تر، اقتصادی است. تولید اثبات‌های پیشنهادی ارزان شده و طبق محاسبات OpenAI هرکدام حدود سه ساعت توان محاسباتی نیاز دارد. اما بررسی آن‌ها همچنان پرهزینه است. تا زمانی که مدل منتشر نشود و دیگران نتوانند خروجی آن را بازتولید کنند، یا تا زمانی که داوران مقاله‌ها را یکی‌یکی بررسی نکنند، سهم تأییدشده این انتشار همان ۴۲ درصدی است که رایانه بررسی کرده است؛ منهای خطاهایی که ممکن است در مرحله ترجمه رخ دهد، به‌علاوه آنچه انسان‌ها بتوانند تأیید کنند. این رقم هر هفته تغییر خواهد کرد، اما عدد ۳۷۲ تغییر نمی‌کند.