OpenAI روز ۲۶ اکتبر ۲۰۲۶ در یادداشتی با عنوان «ساختن فهم علمی همراه با جامعه‌های دانشگاهی» اعلام کرد که مدل‌های داخلی‌اش به سه نتیجه تازه در علوم کامپیوتر، ریاضی و فیزیک رسیده‌اند. یکی از آن‌ها رد کردن فرضیه‌ای است که صدها مقاله علمی بر آن بنا شده و دیگری به یکی از مسائل هزاره مؤسسه ریاضی کلی مربوط می‌شود.
این ادعاها اگر درست باشند، نقطه عطفی در استفاده از هوش مصنوعی در پژوهش‌اند. اما سؤال مهم‌تر برای هر خواننده این است: وقتی یک ماشین اثباتی پیچیده می‌نویسد، چه کسی و چطور می‌فهمد درست است؟ در این مقاله، ادعاها، داوران مستقل و ابزاری به نام Lean را ساده توضیح می‌دهیم.
ادعای اول: رد فرضیه زمان نمایی
فرضیه زمان نمایی یا ETH درباره مسئله «صدق‌پذیری» است؛ یعنی اینکه آیا می‌توان به متغیرهای یک فرمول منطقی طوری درست و غلط داد که کل فرمول درست شود. این فرضیه می‌گوید در بدترین حالت، زمان حل این مسئله با افزایش تعداد متغیرها به‌صورت نمایی بالا می‌رود. به نوشته The Decoder، صدها مقاله در نظریه گراف، زیست‌شناسی محاسباتی، پایگاه داده و هندسه محاسباتی بر این فرض تکیه کرده‌اند.
به گزارش Scientific American، اثبات OpenAI الگوریتمی برای نسخه ۳-SAT ارائه می‌دهد که کمی سریعتر از زمان نمایی است و همین ETH را رد میکند. هر دو منبع تأکید می‌کنند که این نتیجه مسئله معروف P در برابر NP را حل نمیکند. جالب اینکه به نوشته Scientific American، چند ساعت پس از اعلام OpenAI، شرکت Anthropic هم نتیجه مستقلی با یک مدل داخلی خود منتشر کرد که آن هم ETH را رد میکند.
ادعای دوم: حدس هموارسازی موضعی در همه ابعاد
این حدس را کریستوفر سوگ در سال ۱۹۹۱ مطرح کرد و به رفتار موج‌ها در طول زمان مربوط است. گوث، وانگ و ژانگ در ۲۰۱۹ حالت دوبعدی آن را ثابت کردند. OpenAI حالا می‌گوید آن را برای همه ابعاد ثابت کرده و این نتیجه، حدس کاکیا و حدس تحدید اشتاین را هم در پی دارد.
اهمیت ماجرا وقتی روشن می‌شود که بدانیم حدس کاکیا در سه بعد را هونگ وانگ و جاشوا زال در ۲۰۲۵ ثابت کردند و وانگ امسال در کنگره بین‌المللی ریاضی‌دانان در فیلادلفیا مدال فیلدز گرفت. به گزارش Scientific American، مدل داخلی OpenAI ماه گذشته حالت چهاربعدی را حل کرده بود و حالا ادعای حل همه ابعاد را دارد.
ادعای سوم: نیمی از یک مسئله هزاره
مسئله یانگ-میلز یکی از مسائل هزاره است که برای هر کدام یک میلیون دلار جایزه تعیین شده است. این مسئله دو بخش دارد: «وجود» نظریه و «شکاف جرم». OpenAI می‌گوید مدلش فقط بخش وجود را در فضازمان چهاربعدی ثابت کرده و این کار را برای کرومودینامیک کوانتومی و ساده‌ترین نظریه وحدت بزرگ هم ادامه داده است. بخش شکاف جرم همچنان باز است، پس جایزه هنوز در کار نیست.
Scientific American یادآوری میکند که تادئوش بالابان در اواخر دهه ۱۹۸۰ مسیری برای اثبات بخش وجود ترسیم کرده بود و تکمیلش محاسبات بسیار زیادی می‌خواست. اتان ساسمن از دانشگاه نورث‌وسترن همراه با لوان آلپوگه، از کارکنان Anthropic، با کمک مدل‌های زبانی روی همین مسیر کار می‌کردند و فکر می‌کردند به پایان نزدیک‌اند.
چه کسانی این اثبات‌ها را بررسی می‌کنند؟
OpenAI برای هر نتیجه راه متفاوتی انتخاب کرده است. طبق گزارش The Decoder و The Neuron، وضعیت هر سه به این شکل است:
- علوم کامپیوتر: راسل ایمپاگلیاتسو و راماموهان پاتوری از دانشگاه کالیفرنیا سن‌دیگو، که خودشان ETH را مطرح کرده بودند، همراه رایان ویلیامز از MIT بررسی را پیش می‌برند؛ بدون قرارداد محرمانگی و بدون دریافت پول
- ریاضی: متن اثبات و نسخه Lean آن روی GitHub منتشر شده و OpenAI فقط با یک کارشناس بیرونی مشورت کرده است
- فیزیک: گروهی به سرپرستی دیوید گراس، برنده نوبل فیزیک ۲۰۰۴، با حضور مایکل داگلاس، آرتور جفی، ایگور کلبانوف و نیکیتا نکراسوف ابتدا توضیح خودشان را می‌نویسند و فعلاً مواد خام منتشر نشده است
گروه بررسی‌کننده ETH در نامه سرگشاده خود نوشته است که همکاری‌اش با OpenAI به معنای تأیید درستی نتیجه نیست.
Lean چیست و چرا کافی نیست؟
Lean یک زبان و نرم‌افزار وارسی اثبات است. ریاضی‌دان یا هوش مصنوعی اثبات را به زبان دقیق Lean می‌نویسد و نرم‌افزار قدم‌به‌قدم بررسی میکند که هر استدلال طبق قواعد منطق از قبلی نتیجه شده باشد. OpenAI برای اثبات‌های ریاضی و علوم کامپیوتر نسخه Lean منتشر کرده و می‌گوید اثبات یانگ-میلز هم به Lean ترجمه شده است.
اما خود OpenAI هم می‌پذیرد که Lean فقط تطابق اثبات با «صورت‌بندی نوشته‌شده» را می‌سنجد. اگر صورت مسئله در Lean کمی با مسئله واقعی فرق داشته باشد، اثبات بی‌نقص است ولی چیز دیگری را ثابت کرده. The Neuron به پژوهشی اشاره میکند که در مجموعه‌های آزمون Lean مواردی یافته که صورت‌بندی با مسئله اصلی یکی نبوده است. برای همین داوری انسانی هنوز ضروری است.
چرا بعضی دانشمندان ناراضی‌اند؟
به گزارش Scientific American، مدلی که اثبات‌ها را تولید کرده اختصاصی است و پرامپت‌ها، زمان محاسبه و زنجیره استدلال آن منتشر نشده است. گروه مشورتی ریاضیات و هوش مصنوعی (AGMAI) هم که OpenAI پس از انتقاد ریاضی‌دانان تشکیل داده بود، یک روز پیش از اعلام، توصیه‌ای درباره نحوه معرفی نتایج داده بود و حالا خواستار انتشار فوری مقاله یانگ-میلز شده و می‌گوید دلیل علمی برای تأخیر بیشتر وجود ندارد.
OpenAI هم پذیرفته که انتخاب داوران اولیه تعیین میکند چه کسانی زودتر به نتایج دسترسی داشته باشند. این شرکت می‌گوید ادعای اعتبار علمی ندارد و اعتبار را از آنِ گروه‌هایی می‌داند که نتایج را توضیح می‌دهند. به نوشته هر دو منبع، OpenAI همچنین پنج میلیون دلار به بنیاد سایمونز برای کارگاه‌ها و همایش‌های مرتبط با نتایج هوش مصنوعی تعهد داده است.
این خبر برای دانشجوها و پژوهشگران ایرانی چه پیامی دارد؟
آینده پژوهش احتمالاً این شکلی است: هوش مصنوعی ایده و اثبات تولید میکند و ارزش انسان در فهمیدن، وارسی و توضیح دادن آن است. رایان ویلیامز گفته ممکن است ظرف ۱۲ ماه پیشرفت جدی در حل عملی SAT ببینیم، اما بلافاصله افزوده: «یا شاید هیچ‌چیزی از این دست نبینیم. واقعاً نمی‌دانم.» همین صداقت، الگوی خوبی برای خواندن خبرهای علمی است.
- یادگیری مقدماتی Lean یا ابزارهای مشابه برای دانشجوهای ریاضی و کامپیوتر مزیت جدی خواهد بود
- در خبرها فرق «ادعا»، «وارسی ماشینی» و «تأیید داوران» را جدی بگیرید
- خروجی هوش مصنوعی در پروژه و پایان‌نامه را بدون بررسی صورت مسئله و فرض‌ها نپذیرید
- دنبال کنید که مواد خام منتشر شده یا فقط خلاصه‌ای از آن در دسترس است
از این به بعد چه چیزی را دنبال کنیم؟
سه نشانه مهم‌اند: گزارش‌های میانی گروه ویلیامز درباره ETH، انتشار یا عدم انتشار مقاله یانگ-میلز و واکنش ریاضی‌دانان به اثبات منتشرشده هموارسازی موضعی. تا آن زمان، این نتایج را باید ادعاهایی جدی ولی هنوز تأییدنشده دانست.
منابع و مطالعه بیشتر
- Dueling proofs from OpenAI and Anthropic astound scientistsScientific American (Yahoo News)
- OpenAI asks outside experts, including a Nobel laureate, to check proofs its AI produced in math, computer science, and physicsThe Decoder
- OpenAI Reports Three AI Discoveries. How Will Scientists Verify Them?The Neuron
سؤال‌های متداول
آیا OpenAI جایزه یک میلیون دلاری مسئله هزاره را برده است؟+
خیر. OpenAI فقط بخش وجود مسئله یانگ-میلز را ادعا کرده و بخش شکاف جرم که برای جایزه لازم است هنوز حل نشده. مقاله کامل این بخش هم هنوز منتشر نشده است.
رد شدن ETH یعنی نرمافزارها سریعتر میشوند؟+
نه لزوماً. الگوریتم ارائهشده فقط کمی سریعتر از زمان نمایی است و منابع میگویند این نتیجه مسئله P در برابر NP را حل نمیکند. اثر عملی آن هنوز روشن نیست.
Lean به زبان ساده چه میکند؟+
Lean نرمافزاری است که بررسی میکند هر گام یک اثبات طبق قواعد منطق درست باشد. اما نمیتواند تضمین کند صورت مسئلهای که در آن نوشته شده دقیقاً همان مسئله مورد نظر پژوهشگران است.
چه کسانی نتایج را داوری می‌کنند؟+
برای ETH راسل ایمپاگلیاتسو، راماموهان پاتوری و رایان ویلیامز، و برای فیزیک گروهی به سرپرستی دیوید گراس، برنده نوبل فیزیک. اثبات ریاضی هم برای بررسی عمومی روی GitHub منتشر شده است.
