۷۲۲ مقالهٔ ریاضی از OpenAI و بحران راستیآزمایی
خلاصهٔ کاملتر
OpenAI ۷۲۲ مقالهٔ ریاضی رو که یه مدل داخلی و منتشرنشده نوشته، همراه با ردِ استدلالها و فایلهای راستیآزمایی Lean روی GitHub منتشر کرده. این کارها ۱۷ حوزه رو پوشش میدن، از نظریهٔ اعداد اول تا فیزیک پلاسما و مدارهای کوانتومی. به گفتهٔ نویسنده، داستان اصلی خود نتیجهها نیست، اینه که تقریباً هیچ ریاضیدانی نمیتونه بیشتر از یه تیکهٔ کوچیک از این حجم رو خودش چک کنه.
رشد خروجی خیلی تنده: حدود ۱۰ نتیجه تو اوت، بیش از ۱۰۰ تا تو سپتامبر و ۷۲۲ تا فقط شش روز بعد از شروع اکتبر. یعنی تقریباً ۱۰ برابر در ماه. هر مقاله حدود سه ساعت محاسبه در حد حالت thinking تو ChatGPT Pro خرج داشته. نویسنده میگه نکتهٔ جالب اینه که این یه موتور مخصوص ریاضی نیست، یه مدل زبانی عمومیه که همزمان روی چند زیرشاخهٔ ریاضی کار میکنه.
مدل روی چند مسئلهٔ معروف پیشرفت جزئی داشته، مثلاً یه کران عددی مرتبط با فرضیهٔ ریمان رو از نتیجههای قبلی آدمها جلوتر برده. ولی فرضیهٔ ریمان و حدس Birch و Swinnerton-Dyer هنوز حل نشدن.
Lean یه proof assistant هست، یعنی ابزاری که قدمبهقدم چک میکنه هر مرحلهٔ اثبات منطقاً از قبلی درمیاد. این خیلی کمک میکنه، ولی نویسنده تأکید میکنه درست بودن از نظر فرمال با مهم بودن یکی نیست. یه اثبات میتونه کاملاً معتبر باشه ولی پیشپاافتاده باشه یا یه نسخهٔ عوضشده از مسئله رو حل کرده باشه. برای قضاوت دربارهٔ این، تو بعضی زیرشاخهها فقط چند صد تا حدود هزار نفر تو کل دنیا صلاحیت دارن و بررسی هر مقاله چند روز تا چند هفته طول میکشه.
به گفتهٔ مقاله، ریاضی یه زمین آزمایشه چون حداقل ابزاری مثل Lean داره. زیستشناسی، فیزیک و اقتصاد چنین لایهای ندارن و تأیید یه نتیجه اونجا ممکنه ماهها کار آزمایشگاهی بخواد. پس اگه هوش مصنوعی اونجا هم با همین سرعت نتیجه تولید کنه، گلوگاه بررسی بدتر میشه. اثر نزدیکتر، به نظر نویسنده، روی خود تحقیقات هوش مصنوعیه، چون پیشرفت تو جبر خطی و بهینهسازی دوباره به ساخت مدلهای بعدی برمیگرده.
سؤال باز آخر اینه که آیا آدمها اصلاً میتونن این ریاضیات رو بفهمن. ریاضیدانها دارن میپرسن که آیا نگه داشتن یه جامعهٔ انسانی که بتونه ریاضیات مرزی رو دنبال کنه باید یه هدف آگاهانه باشه. اگه بررسی به تولید نرسه، یه کوه نتیجهٔ چکنشده جمع میشه که اعتبار کل کار رو زیر سؤال میبره.
نکات کلیدی:
- OpenAI ۷۲۲ مقالهٔ ریاضی در ۱۷ حوزه رو همراه با فایلهای Lean روی GitHub منتشر کرده.
- خروجی از حدود ۱۰ نتیجه در اوت به ۷۲۲ تا در اوایل اکتبر رسیده، یعنی تقریباً ۱۰ برابر در ماه.
- روی فرضیهٔ ریمان فقط یه کران عددی جلوتر رفته و هیچ مسئلهٔ جایزهٔ هزارهای حل نشده.
- فقط چند صد تا حدود هزار نفر میتونن این اثباتها رو درست بررسی کنن و هر بررسی روزها تا هفتهها طول میکشه.
- علوم تجربی مثل زیستشناسی ابزاری شبیه Lean ندارن، پس گلوگاه بررسی اونجا سختتره.




