טענת ההוכחה של OpenAI לנאוויה–סטוקס, מוסברת

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

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

טענת OpenAI, כפי שדווחה על ידי Quanta Magazine, היא שסוכני AI אוטונומיים שרצו על מודל פנימי מצאו סינגולריות במשוואות נאוויה–סטוקס התלת-ממדיות. Quanta מדווחת שהעבודה השתמשה בכ-10,000 סוכנים, שהסוכנים מצאו הוכחה לאחר 88 שעות, ושמודל AI אחר פורמל את התוצאה ב-Lean לאחר 17 שעות נוספות. הסוכנים החליפו כמעט 5 מיליון הודעות, וסבסטיאן בובק מ-OpenAI העריך את עלות החישוב בכמה מיליוני דולרים, לפי Quanta.

MIT Technology Review מדווח ש-OpenAI אומרת כי אינה מתכננת לתבוע את פרס מיליון הדולר. לפי Wikipedia, הדוגמה הנגדית עדיין לא אומתה על ידי מתמטיקאים חיצוניים או על ידי מכון Clay למתמטיקה.

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

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

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

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

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

המחלוקת מתמקדת בקשר בין עבודתה של OpenAI לבין עבודתם של באקמאסטר ואלפגה.

Quanta מדווחת שההכרזה של OpenAI הגיעה כ-12 שעות לאחר שבאקמאסטר הכריז על תוצאות עם אלפגה בבעיות קרובות מאוד. עבודתם השתמשה במגוון מודלי AI, כולל מודלים של OpenAI. MIT Technology Review מדווח שבאקמאסטר ואלפגה עבדו כמעט שנה על הבעיה, ושבאקמאסטר פרסם הוכחה שמראה שגרסה מפושטת של משוואות נאוויה–סטוקס יכולה לקרוס.

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

OpenAI הכירה בכך, לפי MIT Technology Review, שהצוות קיבל השראה לרדוף אחרי הבעיה לאחר ששמע שמועה על מאמציהם של באקמאסטר ואלפגה. המחלוקת היא אם המודלים או העובדים של OpenAI קיבלו גישה לעבודתם של באקמאסטר ואלפגה, אומנו עליה, או נהנו ממנה בדרך אחרת.

MIT Technology Review מדווח שבאקמאסטר פרסם מסמך המתאר אינטראקציות עם עובדי OpenAI. לפי גרסתו של באקמאסטר, עובדי OpenAI הציגו שתי אפשרויות. באקמאסטר ואלפגה יוכלו לפרסם את עבודתם ו-OpenAI תפרסם את פתרון נאוויה–סטוקס שלה ביום הבא, או שבאקמאסטר יוכל לעבוד עם OpenAI על מאמר נאוויה–סטוקס שלא יכלול את אלפגה כמחבר בגלל השתייכותו ל-Anthropic. MIT Technology Review מדווח גם ש-OpenAI הכחישה שעובדיה או הסוכנים שלה ניגשו לתמלילים של באקמאסטר ואלפגה.

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

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

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

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

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

זו אחת הסיבות שעבודה מרובת-סוכנים היא בעיה הנדסית, לא רק טריק prompting. בין שאתם מתכננים סוכני מחקר ובין שאתם בונים תהליכי עבודה עסקיים, השאלות המעשיות דומות: אילו סוכנים יכולים לראות איזה הקשר, לאילו כלים הם יכולים לקרוא, איפה מתרחשות העברות, ומה מתועד בלוגים? בחירות התכנון האלה חשובות בסוכני AI הרבה לפני שההימור מגיע לשטח של פרס מילניום.

הפרט התפעולי הבולט ביותר הוא קנה המידה. Quanta מדווחת על כ-10,000 סוכנים, 88 שעות חיפוש, 17 שעות נוספות לפורמליזציה וכמעט 5 מיליון הודעות בין סוכנים. MIT Technology Review מדווח ש-OpenAI אמרה שההרצה עלתה מיליוני דולרים.

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

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

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

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

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

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

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

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

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

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

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

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

OpenAI אומרת שיש לה פתרון שנוצר על ידי AI, אבל הטענה עדיין זקוקה לביקורת מתמטית חיצונית ולהערכה של מכון Clay למתמטיקה.

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

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

המחלוקת נוגעת לשאלה אם עבודתה של OpenAI נהנתה ממחקר בסיוע AI של טריסטן באקמאסטר ולבנט אלפגה ללא קרדיט ראוי. לפי MIT Technology Review, OpenAI הכחישה שעובדיה או הסוכנים שלה ניגשו לתמלילים שלהם.

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