על בעיית המילניום של נאוויה–סטוקס

אנחנו משתפים פתרון לבעיית הקיום והחלקות של נאוויה–סטוקס, אחת מבעיות המילניום. הוכחה זו, שהפיקה מערכת פנימית של OpenAI, מראה כי הדינמיקה של משוואות נאוויה–סטוקס לתנועת זורמים יכולה לפתח סינגולריות בזמן סופי. אנחנו משתפים הן הסבר כתוב של ההוכחה והן ניסוח פורמלי שלה ב-Lean.

בעיות המילניום⁠(נפתח בחלון חדש) מייצגות כמה מהשאלות העמוקות ביותר בחזית המתמטיקה. השאלה אם תנועה חלקה של זורם תלת-ממדי עלולה לאבד את חלקותה נותרה פתוחה במשך כ-90 שנה.

אחת המטרות המרכזיות בעבודתנו היא להעניק למדענים כלים לקידום מחקר וטכנולוגיה שיועילו לאנושות כולה. כדי לפתור את בעיית נאוויה–סטוקס, השתמשנו במודל פנימי בעל יכולות גבוהות משמעותית מאלו של GPT‑6 Astra. אנחנו מאמינים שחשוב לעדכן את העולם בקצב ההתקדמות של הבינה המלאכותית ובמה שאפשר לצפות מהמודלים הבאים.

משוואות נאוויה–סטוקס משתמשות בחוק התנועה השני של ניוטון (״F=ma״) כדי לתאר כיצד זורמים נעים. חשוב לציין שהן מתייחסות לזורם כתווך רציף, במקום לעקוב אחר מולקולות בודדות. משוואות אלו משמשות לתכנון כלי טיס, לחיזוי מזג האוויר ולחקר זרימת הדם.

שאלה פתוחה ויסודית בנוגע למשוואות דינמיות אלו הייתה אם קירוב הרצף של הזורם עלול לאבד את תוקפו. בפרט, האם משוואות נאוויה–סטוקס לזורם תלת-ממדי בלתי דחיס בעל צפיפות קבועה יכולות לפתח ״סינגולריות״, גם כשהתנועה מתחילה באופן חלק? כאן, סינגולריות פירושה שהדינמיקה גורמת למהירויות בזורם לגדול ללא חסם בתוך פרק זמן סופי. סינגולריות כזו צריכה להתפתח למרות קיומה של צמיגות, שנוטה להחליק את התנועה. מכיוון שזורם אמיתי אינו יכול לנוע במהירות אינסופית, מצב כזה יצביע על כשל בתיאור הזורם באמצעות המשוואות. כדי להמשיך לתאר את המערכת במודל, יהיה צורך לעקוב אחר התנהגותו של כל חלקיק בנפרד.

מקורן של המשוואות בעבודתם של קלוד-לואי נאוויה וג׳ורג׳ גבריאל סטוקס במאה התשע-עשרה. ב-1934 הוכיח ז׳אן לרה שקיימים פתרונות במובן מוכלל, אך השאלה אם הם תמיד נשארים חלקים הפכה לשאלה מרכזית שנותרה ללא מענה. בשנת 2000 כלל מכון קליי למתמטיקה את בעיית הקיום והחלקות של נאוויה–סטוקס בין שבע בעיות המילניום.

המערכת שלנו הפיקה הוכחה אנליטית וניסוח פורמלי ב-Lean לכך שזורם במצב התחלתי חלק ובמנוחה יכול לפתח סינגולריות בזמן סופי. על הזורם מופעל כוח חלק, והאנרגיה שלו נשארת סופית לאורך התהליך הדינמי כולו, ממנוחה ועד להיווצרות הסינגולריות. בכך נפתרת בעיית המילניום של נאוויה–סטוקס באמצעות הוכחת טענה ״C״ (וגם ״D״) בניסוח הרשמי של בעיית המילניום⁠(נפתח בחלון חדש).

הפתרון הוא מערבולת — זרם מסתחרר שנע בספירלה פנימה ומתארך יותר ויותר, כמו ספגטי. אזור מרכזי זה מתכווץ תוך כדי האצה, באופן שהאנרגיה שלו עדיין נשארת סופית, כנדרש על פי חוקי הפיזיקה. האתגר הטכני הוא שהכשל יתפתח במשוואות מתוך תנועת הזורם עצמו, ולא, למשל, מכך שנוסיף כוח אינסופי באופן מלאכותי. בניסוח מתמטי יותר, האיברים במשוואות נאוויה–סטוקס שמתארים את התנועה — תאוצה, מפלי לחץ, העברת תנע וצמיגות — צריכים גם לגדול וגם לבטל זה את זה באופן מדויק. איזון מדויק זה מותיר כוח חיצוני חלק, גם כשמהירות הזורם גדלה ללא חסם.

מאז 28 באוגוסט אנחנו מאמנים מודל פנימי חדש שהציג ביצועים חסרי תקדים במבחני ההערכה שלנו, לרבות במתמטיקה. אימון המודל נמשך, וביצועיו ממשיכים להשתפר.

ביום שלישי, 1 בספטמבר, שמענו שמועות על כך ששתיים מבעיות המילניום נפתרו. בהשראת השמועות הללו וקפיצת המדרגה בביצועי המודל הפנימי שלנו, התחלנו לבחון אותו על כל בעיות המילניום הפתוחות ועל כמה בעיות נוספות בעלות חשיבות רבה.

השתמשנו במערכת של סוכנים המתאמים ביניהם את פעולתם, המבוססים על המודל הפנימי שלנו. לסוכנים הייתה גישה לכלים שאפשרו להם, בין היתר, לקרוא מעותק שמור של האינטרנט ולהריץ קוד. הסוכנים חולקו לקבוצות, עם יכולת לתקשר בתוך כל קבוצה. הקבוצות היו בגדלים שונים, והקבוצה שהפיקה את הפתרון לנאוויה–סטוקס כללה כ-10,000 סוכנים שפעלו במקביל. לאורך כל הדרך שמרנו על אותם אמצעי הגנה מחמירים שאנו מיישמים בכל ההערכות של מודלי החזית שלנו, לרבות ניטור ובידוד.

לכל בעיה, נתנו לקבוצות סוכנים שונות הנחיות עם גרסאות שונות של ניסוח הבעיה, כך שיכסו את כל גרסאותיה. בבעיית נאוויה–סטוקס הצענו לקבוצות סוכנים נפרדות את גרסאות ״A״ ו-״B״ (ניסוחים מסוימים של הבעיה שיובילו להוכחה) ואת גרסאות ״C״ ו-״D״ (שיובילו להפרכה).

נוסף על בעיות המילניום במלואן, ביקשנו מהמערכת מרובת הסוכנים שלנו לנסות לפתור אוסף של בעיות ״קלות יותר״. אחת מהן הייתה שאלת התבדרות דומה במקרה הגבולי של בעיית נאוויה–סטוקס, שבו מסירים את איבר הצמיגות. זו ידועה כבעיית הרגולריות של משוואות אוילר, והסוכנים שלנו הפתיעו אותנו כשפתרו אותה. הגרסה המסוימת שהם פתרו הייתה הגרסה ללא כוח חיצוני, שבה לא מופעל על הזורם כוח מבחוץ. קרוב ל-100 סוכנים עבדו יחד במשך כ-50 שעות כדי להפיק את ההפרכה שלנו לרגולריות של משוואות אוילר¹.

לאחר שראינו את הפתרון לבעיית אוילר, חשבנו שנאוויה–סטוקס היא הבעיה בעלת סיכויי ההצלחה הטובים ביותר להמשך העבודה. לכן החלטנו להקדיש את המשאבים שלנו לנאוויה–סטוקס. לשם כך העברנו סוכנים מבעיות המילניום האחרות למשימה זו, וכללנו בהנחיות להם את הפתרון לבעיית אוילר. כשגרסה של המודל הפנימי שעברה אימון נוסף נעשתה זמינה במהלך העבודה, עדכנו את הסוכנים שלנו למודל זה.

עודדנו קבוצות סוכנים שונות לבחון מגוון גישות. לאחר זמן מה יצרנו הפריה הדדית בין קבוצות הסוכנים, בעזרת Codex שריכז את התובנות המועילות ביותר מכל קבוצה. הנחיות ההמשך הללו התבססו על תוצאות הביניים של הסוכנים עצמם. כך הונחתה הקבוצה שמצאה את הפתרון לנאוויה–סטוקס.

הסוכנים הגיעו לפתרון ביום שבת, 5 בספטמבר, כ-88 שעות לאחר הפעלת הסוכנים הראשונים. הניסוח הפורמלי והאימות ב-Lean נמשכו 17 שעות נוספות, באמצעות GPT‑6 Astra.

בכל הבעיות שניסו לפתור, הסוכנים שלחו 4.9 מיליון הודעות והשתמשו בכ-300 מיליארד טוקנים של פלט. בתהליך פתרון בעיית נאוויה–סטוקס, הסוכנים שלחו 2.7 מיליון הודעות והשתמשו בכ-130 מיליארד טוקנים של פלט.

העבודה שלנו החלה ב-1 בספטמבר בעקבות שמועה, שבהמשך התברר לנו שנגעה ללבנט אלפוגה, עובד Anthropic, ולטריסטן בקמאסטר, פרופסור למתמטיקה באוניברסיטת ניו יורק.² לאחר שהשלמנו את הפרויקט כולו ואת האימות ב-Lean (ב-6 בספטמבר), ומתוך אמונה על סמך השמועה שגם להם יש פתרון לנאוויה–סטוקס, פנינו אליהם והצענו לפרסם את התוצאה שלנו במקביל לשלהם ולהכיר בקדימותם בהודעה משותפת. בשלב זה גילינו שבעזרת מודל פנימי של Anthropic, הם הפיקו פתרון לבעיית אוילר עם כוח חיצוני. בשיחות אלו הצענו להם לעיין בכל ההנחיות שבהן השתמשנו, ובהמשך גם לראות את ההוכחה. אנו מכירים בקדימות עבודתם על בעיית אוילר עם כוח חיצוני ומברכים אותם על ההישג המתמטי המרשים.

אנחנו (החוקרים והסוכנים) לא ראינו שום חלק מעבודתם בשום דרך עד שפרסמו אותה לציבור — בפרט, לא הייתה גישה לנתונים של משתמש מסוים לצורך פתרון הבעיה.

בעקבות בדיקה, אישרנו שההנחיות שבקמאסטר הזין ל-Codex בחודשיים שקדמו לפרסום ההודעה והמאמר הללו ב-8 בספטמבר 2026 לא יכלו להשפיע על המערכת בשום דרך, לרבות דרך האימון. המודל הפנימי של OpenAI ששימש להשגת תוצאה זו פותח באמצעות למידת חיזוק בקנה מידה גדול, על בסיס מודל שכבר עבר אימון מקדים. גם ההוכחות שלנו שונות באופן מהותי. במקרה של אוילר, אלפוגה ובקמאסטר הוכיחו תוצאה עם כוח חיצוני, ואילו המערכת של OpenAI הוכיחה תוצאה ללא כוח חיצוני.

מטרתנו בפרסום תוצאה זו היא לדווח על ההתקדמות המשמעותית של מודלי הבינה המלאכותית שלנו. איננו מתכוונים לבקש את פרס המילניום על תוצאה זו.

אבן דרך זו משקפת עבודה רבה של מתמטיקאים וחוקרי בינה מלאכותית. עם זאת, אין זו נקודת שיא מסכמת, אלא תמונת מצב של ההתקדמות בפיתוח בינה מלאכותית.

אנחנו מאמינים שכעת אנו בתקופה הבאה של התקדמות הבינה המלאכותית⁠, והתוצאות של היום מספקות ראיה נוספת לכך. אנו מתמקדים בהבנת המודל הזה ומשתמשים בתובנות שאנו צוברים כדי לכוון את המשך פיתוח היכולות ולקבוע את קצבו. אחת מהמטרות המרכזיות שלנו⁠ היא לבנות מערכות בינה מלאכותית שניתן לכוון, שכפופות לאחריותיות ושמחוברות לאנשים. לשם כך ייתכן שנצטרך לקבל החלטות שקולות יותר בנוגע לקצב ההתקדמות, בעודנו ממשיכים במשימתנו להבטיח ש-AGI תועיל לאנושות כולה.