درباره مسئله جایزه هزاره ناویر–استوکس

راه‌حلی برای مسئله وجود و همواری ناویر–استوکس، یکی از مسائل جایزه هزاره، منتشر می‌کنیم. این برهان که یک سامانه داخلی OpenAI آن را ارائه کرده است، نشان می‌دهد دینامیک معادلات ناویر–استوکس برای حرکت سیال می‌تواند در زمانی متناهی به تکینگی برسد. هم شرح برهان و هم صورت‌بندی صوری آن در Lean را منتشر می‌کنیم.

مسائل جایزه هزاره⁠(در یک پنجره جدید باز می‌شود) از عمیق‌ترین پرسش‌های ریاضیات پیشرو به شمار می‌روند. این پرسش که آیا حرکت هموار یک سیال سه‌بعدی می‌تواند فروبپاشد، حدود ۹۰ سال بی‌پاسخ مانده است.

یکی از اهداف اصلی کار ما توانمندسازی دانشمندان برای پیشبرد پژوهش و فناوری در جهت منفعت همه بشریت است. برای حل مسئله ناویر–استوکس، از مدلی داخلی استفاده کردیم که توانمندی آن به‌مراتب بیش از GPT‑6 Astra است. به باور ما، آگاه‌کردن جهان از سرعت پیشرفت هوش مصنوعی و آنچه باید از مدل‌های آینده انتظار داشت، مهم است.

معادلات ناویر–استوکس با استفاده از قانون دوم حرکت نیوتن («F=ma») چگونگی حرکت سیالات را توصیف می‌کنند. نکته مهم این است که این معادلات سیال را محیطی پیوسته در نظر می‌گیرند، نه اینکه تک‌تک مولکول‌ها را دنبال کنند. از این معادلات در طراحی هواپیما، پیش‌بینی آب‌وهوا و مطالعه جریان خون استفاده می‌شود.

یکی از پرسش‌های بنیادی و حل‌نشده درباره این معادلات دینامیکی آن بوده است که آیا تقریب پیوستار برای سیال می‌تواند فروبپاشد. به‌طور مشخص، آیا معادلات ناویر–استوکس برای سیالی سه‌بعدی، تراکم‌ناپذیر و با چگالی ثابت می‌توانند حتی با شروع حرکتی هموار به «تکینگی» برسند؟ در اینجا تکینگی یعنی دینامیک سامانه باعث شود سرعت‌های سیال در مدتی متناهی بدون کران افزایش یابند. شکل‌گیری تکینگی باید با وجود گرانروی رخ دهد؛ عاملی که معمولاً حرکت را هموار می‌کند. از آنجا که سیال واقعی نمی‌تواند با سرعت نامتناهی حرکت کند، چنین رخدادی نشان‌دهنده فروپاشی شیوه مدل‌سازی سیال با این معادلات است. برای ادامه مدل‌سازی سامانه، پس از آن باید رفتار هر ذره را جداگانه دنبال کرد.

ریشه این معادلات به آثار قرن نوزدهم کلود-لویی ناویه و جورج گابریل استوکس بازمی‌گردد. ژان لره در سال ۱۹۳۴ وجود جواب‌ها را در معنایی تعمیم‌یافته اثبات کرد، اما اینکه آیا آن‌ها همواره هموار می‌مانند به پرسشی محوری و بی‌پاسخ تبدیل شد. مؤسسه ریاضیات کلی در سال ۲۰۰۰ مسئله وجود و همواری ناویر–استوکس را یکی از هفت مسئله جایزه هزاره نامید.

سامانه ما برهانی تحلیلی و صورت‌بندی‌ای در Lean ارائه کرد که نشان می‌دهد سیالی در ابتدا هموار و ساکن می‌تواند در زمانی متناهی به تکینگی برسد. نیرویی هموار به سیال وارد می‌شود و انرژی آن در سراسر دینامیک، از سکون تا شکل‌گیری تکینگی، متناهی باقی می‌ماند. این راه‌حل با اثبات گزاره «C» (و نیز «D») در صورت‌بندی رسمی جایزه هزاره⁠(در یک پنجره جدید باز می‌شود)، مسئله جایزه هزاره ناویر–استوکس را حل می‌کند.

این راه‌حل گردابه‌ای است—چرخشی مارپیچی از سیال—که به درون می‌پیچد و مانند اسپاگتی پیوسته کشیده‌تر می‌شود. این ناحیه مرکزی هم‌زمان با افزایش سرعت کوچک می‌شود، به‌گونه‌ای که انرژی آن مطابق قوانین فیزیک همچنان متناهی می‌ماند. چالش فنی این است که فروپاشی باید از حرکت خود سیال در معادلات پدید آید، نه مثلاً با اعمال دستی نیرویی نامتناهی. به بیان دقیق‌تر ریاضی، جمله‌های توصیف‌کننده حرکت در معادلات ناویر–استوکس—شتاب، گرادیان فشار، انتقال تکانه و گرانروی—باید هم بزرگ شوند و هم به‌شکلی دقیق یکدیگر را خنثی کنند. این توازن ظریف باعث می‌شود حتی با افزایش بی‌کران سرعت سیال، نیروی خارجی هموار باقی بماند.

از ۲۸ اوت در حال آموزش مدل داخلی جدیدی بوده‌ایم که در معیارهای ارزیابی ما، از جمله ریاضیات، عملکردی بی‌سابقه نشان داده است. آموزش این مدل همچنان ادامه دارد و عملکردش پیوسته بهتر می‌شود.

سه‌شنبه، ۱ سپتامبر، شایعاتی شنیدیم مبنی بر اینکه دو مسئله جایزه هزاره حل شده‌اند. با الهام از این شایعات و جهش عملکرد مدل داخلی‌مان، تلاش برای ارزیابی آن روی همه مسائل حل‌نشده جایزه هزاره و چند مسئله پراهمیت دیگر را آغاز کردیم.

از سامانه‌ای متشکل از عامل‌های هماهنگ‌شونده و مبتنی بر مدل داخلی خود استفاده کردیم. عامل‌ها به ابزارهایی مانند خواندن نسخه ذخیره‌شده اینترنت و اجرای کد دسترسی داشتند. عامل‌ها به گروه‌هایی تقسیم شدند که اعضای هرکدام می‌توانستند با یکدیگر ارتباط برقرار کنند. اندازه گروه‌ها متفاوت بود و گروهی که مسئله ناویر–استوکس را حل کرد، حدود ۱۰٬۰۰۰ عامل هم‌زمان داشت. در تمام مراحل، همان تدابیر حفاظتی سخت‌گیرانه‌ای را حفظ کردیم که در همه ارزیابی‌های مدل‌های پیشرو خود اعمال می‌کنیم، از جمله نظارت و جداسازی.

برای هر مسئله، گونه‌های متفاوتی از صورت مسئله را به گروه‌های مختلف عامل‌ها ارائه کردیم تا همه حالت‌های مسئله پوشش داده شود. برای مسئله ناویر–استوکس، نسخه‌های «A» و «B» (صورت‌هایی خاص که به اثبات می‌انجامیدند) و نسخه‌های «C» و «D» (که به رد گزاره می‌انجامیدند) را به گروه‌های جداگانه عامل‌ها پیشنهاد کردیم.

علاوه بر مسائل کامل جایزه هزاره، از سامانه چندعاملی خود خواستیم مجموعه‌ای از مسائل «آسان‌تر» را نیز امتحان کند. یکی از آن‌ها پرسشی مشابه درباره انفجار در حدی از مسئله ناویر–استوکس بود که جمله گرانروی از آن حذف شده است. این پرسش به مسئله منظم‌بودن معادلات اویلر معروف است و عامل‌های ما با حل آن غافلگیرمان کردند. گونه مشخصی که آن‌ها حل کردند، نسخه بدون نیروی خارجی بود که در آن هیچ نیروی خارجی به سیال وارد نمی‌شود. نزدیک به ۱۰۰ عامل حدود ۵۰ ساعت با یکدیگر کار کردند تا رد منظم‌بودن اویلر را ارائه کنند¹.

پس از دیدن راه‌حل اویلر، به این نتیجه رسیدیم که ناویر–استوکس امیدبخش‌ترین مسئله برای ادامه کار است. بنابراین تصمیم گرفتیم منابع خود را به ناویر–استوکس اختصاص دهیم. برای این کار، عامل‌ها را از دیگر مسائل هزاره کنار کشیدیم و راه‌حل اویلر را در اختیارشان گذاشتیم. هنگامی که در جریان این تلاش نسخه‌ای با آموزش بیشتر از مدل داخلی‌مان آماده شد، عامل‌ها را به آن مدل ارتقا دادیم.

گروه‌های مختلف عامل‌ها را تشویق کردیم رویکردهای گوناگونی را بررسی کنند. پس از مدتی، با استفاده از Codex برای تجمیع سودمندترین بینش‌های هر گروه، میان گروه‌های عامل‌ها تبادل ایده ایجاد کردیم. این درخواست‌های پیگیری بر نتایج میانی خود عامل‌ها تکیه داشتند. گروهی که راه‌حل ناویر–استوکس را یافت نیز به همین شیوه هدایت شد.

عامل‌ها روز شنبه، ۵ سپتامبر، حدود ۸۸ ساعت پس از آغاز کار نخستین عامل‌ها به راه‌حل رسیدند. صورت‌بندی صوری و راستی‌آزمایی در Lean با GPT‑6 Astra نیز ۱۷ ساعت دیگر زمان برد.

عامل‌ها در مجموعِ همه مسائل بررسی‌شده، ۴٫۹ میلیون پیام فرستادند و حدود ۳۰۰ میلیارد توکن خروجی مصرف کردند. عامل‌ها در فرایند حل مسئله ناویر–استوکس، ۲٫۷ میلیون پیام فرستادند و حدود ۱۳۰ میلیارد توکن خروجی مصرف کردند.

تلاش ما در ۱ سپتامبر و پس از شنیدن شایعه‌ای آغاز شد که بعدها دریافتیم به لونت آلپوگه، کارمند Anthropic، و تریستان باک‌مستر، استاد ریاضی دانشگاه نیویورک، مربوط بوده است.² پس از پایان کامل پروژه و راستی‌آزمایی Lean در ۶ سپتامبر، چون بر اساس آن شایعه تصور می‌کردیم آن‌ها نیز راه‌حلی برای ناویر–استوکس دارند، با ایشان تماس گرفتیم و پیشنهاد کردیم نتایج را هم‌زمان منتشر کنیم و در اطلاعیه‌ای مشترک، تقدم کارشان را به رسمیت بشناسیم. آن زمان دریافتیم که آن‌ها با استفاده از یک مدل داخلی Anthropic، مسئله اویلر با نیروی خارجی را حل کرده‌اند. در این گفت‌وگوها پیشنهاد دادیم همه درخواست‌های استفاده‌شده ما را ببینند و بعداً خود برهان را نیز بررسی کنند. تقدم کار آن‌ها درباره اویلر با نیروی خارجی را به رسمیت می‌شناسیم و این دستاورد چشمگیر ریاضی را به ایشان تبریک می‌گوییم.

ما—پژوهشگران و عامل‌ها—تا زمان انتشار عمومی کارشان، به هیچ طریقی آن را ندیده بودیم؛ به‌ویژه برای حل این مسئله به هیچ داده مشخصی از کاربران دسترسی پیدا نشد.

پس از بررسی، تأیید کرده‌ایم که درخواست‌های Codex باک‌مستر در دو ماه پیش از این اطلاعیه و مقاله مورخ ۸ سپتامبر ۲۰۲۶، به هیچ شکلی، از جمله از راه آموزش، نمی‌توانسته بر سامانه اثر بگذارد. مدل داخلی OpenAI که برای این نتیجه به کار رفت، با یادگیری تقویتی در مقیاس بزرگ بر پایه مدلی از پیش آموزش‌دیده توسعه یافت. برهان‌های ما نیز تفاوت‌های چشمگیری دارند. در مورد اویلر، آلپوگه و باک‌مستر نتیجه‌ای با نیروی خارجی را اثبات کردند، در حالی که سامانه OpenAI نتیجه‌ای بدون نیروی خارجی را اثبات کرد.

هدف ما از انتشار این نتیجه، گزارش پیشرفت چشمگیر مدل‌های هوش مصنوعی‌مان است. قصد نداریم برای این نتیجه مدعی جایزه هزاره شویم.

این نقطه عطف حاصل تلاش گسترده ریاضی‌دانان و پژوهشگران هوش مصنوعی است. بااین‌حال، این نقطه اوج نیست؛ بلکه تصویری لحظه‌ای از پیشرفت توسعه هوش مصنوعی است.

به باور ما، اکنون وارد دوره بعدی پیشرفت هوش مصنوعی شده‌ایم⁠ و نتایج امروز شاهد دیگری بر این مدعاست. تمرکز ما بر شناخت این مدل و استفاده از آموخته‌هایمان برای هدایت و تنظیم سرعت پیشرفت‌های بعدی در توانمندی‌هاست. یکی از اهداف کلیدی⁠ ما ساخت سامانه‌های هوش مصنوعی هدایت‌پذیر، پاسخ‌گو و مرتبط با مردم است؛ هدفی که با ادامه مأموریتمان برای اطمینان از منفعت AGI برای همه بشریت، شاید مستلزم تصمیم‌گیری سنجیده‌تر درباره سرعت پیشرفت باشد.