ב-1 בספטמבר הפעילה OpenAI אלפי סוכני בינה מלאכותית על אחת השאלות הקשות ביותר במתמטיקה. ארבעה ימים אחר כך, לפי החברה, קבוצה של כ-10,000 סוכנים כבר החזיקה בפתרון. עוד 17 שעות הוקדשו להפיכת ההוכחה לקוד מתמטי שניתן לבדיקה אוטומטית.
הבעיה שהם תקפו אינה חידה במובן של תשבץ מתוחכם. משוואות נאוויה-סטוקס מתארות את התנועה של נוזלים וגזים – מים סביב גוף של ספינה, אוויר סביב כנף מטוס, זרמים באוקיינוס ומערכות מזג אוויר. מהנדסים ופיזיקאים משתמשים בהן כבר דורות. השאלה שנשארה פתוחה כמעט מאתיים שנה היא בסיסית יותר: האם במרחב תלת-ממדי המשוואות תמיד ממשיכות להתנהג יפה, או שמצב התחלתי חלק לחלוטין יכול בשלב כלשהו להתפרק מתמטית.
OpenAI הודיעה השבוע שמודל פנימי שלה מצא דוגמה שבה מתרחש פירוק כזה. אם ההוכחה תעמוד בבדיקה של הקהילה המתמטית, היא תפתור אחת משבע בעיות המילניום – רשימת השאלות שהציג מכון קליי בשנת 2000, עם פרס של מיליון דולר לכל פתרון.
המשוואות עובדות. המתמטיקה מאחוריהן עדיין לא סגורה
קל להבין למה הסיפור מבלבל. אם משוואות נאוויה-סטוקס משמשות בפועל לתכנון מטוסים, חיזוי מזג אוויר והדמיות הנדסיות, איך ייתכן שאף אחד עדיין לא יודע אם יש להן פתרון תקין לכל מצב?
ההבדל נמצא בין שימוש לבין הוכחה. מחשבים יודעים לחשב פתרונות מקורבים עבור מצבים מסוימים, ולעיתים עושים זאת בדיוק מרשים. המתמטיקאים מבקשים תשובה כללית: אם מתחילים מזרימה חלקה וסבירה, האם המהירות והלחץ יישארו סופיים וחלקים לכל אורך הזמן, או שיכולה להיווצר נקודה שבה גודל מתמטי כלשהו בפתרון מזנק בלי גבול.
במכון קליי ניסחו את הבעיה כך שאפשר לפתור אותה בשני כיוונים. אפשר להוכיח שכל זרימה מהסוג המותר נשארת חלקה תמיד. אפשר גם למצוא דוגמה נגדית – מצב תקין שמוביל בתוך זמן סופי לסינגולריות, נקודת התפרקות של הפתרון.
המערכת של OpenAI הלכה בכיוון השני. לפי החברה, היא בנתה זרימה שמתחילה ממנוחה ומופעל עליה כוח חיצוני חלק. בתוך הזרימה נוצר מערבולת שמסתחררת פנימה, מתארכת ומאיצה. האנרגיה הכוללת נשארת סופית, אבל הפתרון עצמו מפתח סינגולריות בזמן סופי. OpenAI טוענת שהמבנה הזה מקיים את התנאים של סעיפים C ו-D בניסוח הרשמי של בעיית המילניום.
הדוגמה אינה אומרת שמחר בבוקר כוס מים על השולחן יכולה להגיע למהירות אינסופית. אם מודל מתמטי מנבא מצב כזה, הבעיה היא במודל או בגבולות שבהם מותר להשתמש בו, לא בחוקי הטבע. גם תוצאה מהסוג הזה יכולה לחדד מאוד את ההבנה של זרימה, מערבולות וטורבולנציה.
88 שעות, מיליוני הודעות והוכחה שהמחשב יכול לבדוק
המספרים סביב הניסוי חריגים כמעט כמו המתמטיקה. לפי OpenAI, הסוכנים שעבדו על נאוויה-סטוקס החליפו כ-2.7 מיליון הודעות והפיקו כ-130 מיליארד טוקנים. הקבוצה שהגיעה לפתרון כללה בסדר גודל של 10,000 סוכנים שעבדו במקביל. מן ההפעלה הראשונית ועד הפתרון חלפו כ-88 שעות.
אחר כך הגיעה שכבת בדיקה נוספת. GPT-6 Astra הפך את הטיעון להוכחה פורמלית ב-Lean, מערכת שבה כל צעד מתמטי נכתב בצורה שמחשב יכול לאמת. העבודה הזאת ארכה עוד 17 שעות.
Lean אינו ועדת פרס, והוא גם לא מחליף את עבודתם של מתמטיקאים שקוראים את ההנחות ומחליטים אם ההוכחה אכן עונה לשאלה הנכונה. הוא כן מצמצם מאוד סוג אחד של סיכון: טעות לוגית קטנה שמסתתרת בתוך עשרות או מאות עמודי חישוב.
נכון להבוקר, מכון קליי עדיין מציג את בעיית נאוויה-סטוקס כבעיה לא פתורה. גם אם ההוכחה נכונה, הדרך להכרה רשמית ארוכה. לפי כללי המכון, פתרון חייב להתפרסם בבמה מתאימה, לחלוף לפחות שנתיים מן הפרסום, והוא צריך לקבל קבלה כללית בקהילה המתמטית. OpenAI הודיעה שאינה מתכוונת לבקש את פרס מיליון הדולר.
הפרסום הגיע גם עם ויכוח על קרדיט. המתמטיקאים טריסטן בקמאסטר ולבנט אלפגה עבדו במקביל על בעיות קרובות, בעזרת כלים של Anthropic ושל OpenAI, ופרסמו תוצאה על משוואות אוילר – גרסה ללא צמיגות. OpenAI סיפרה ששמעה על ההתקדמות שלהם ואז ריכזה משאבים בנאוויה-סטוקס. בקמאסטר העלה שאלות על שימוש אפשרי ברעיונות ובעבודה שלא פורסמה; OpenAI טוענת שהפתרון שלה פותח באופן עצמאי. הבדיקה המתמטית של ההוכחה והדיון על כללי הקרדיט במחקר מבוסס AI יתקדמו עכשיו במקביל.
למה מתמטיקאים צריכים חידות בכלל
במתמטיקה קוראים להן בדרך כלל בעיות פתוחות או השערות. לעיתים הן נשמעות כמעט ילדותיות. האם קיימים אינסוף זוגות של מספרים ראשוניים שהמרחק ביניהם הוא 2? האם כל מספר זוגי גדול מ-2 הוא סכום של שני ראשוניים? שאלות אחרות דורשות שנים של לימודים רק כדי להבין את הניסוח שלהן.
הערך שלהן אינו רק בתשובה. בעיה טובה מסמנת מקום שבו הידע הקיים נגמר. ניסיונות לפתור אותה מכריחים מתמטיקאים לבנות כלים חדשים, לחבר בין תחומים שלא נראו קשורים ולעיתים לגלות תיאוריה חשובה יותר מן השאלה המקורית.
דויד הילברט הבין את הכוח הזה כבר בשנת 1900. בכנס המתמטיקאים הבינלאומי בפריז הוא פרסם 23 בעיות שהשפיעו על סדר היום של המתמטיקה במשך רוב המאה ה-20. חלקן נפתרו, אחרות קיבלו תשובות מפתיעות, וכמה נשארו פתוחות. סביב הניסיונות לפתור אותן נולדו שיטות ורעיונות ששינו תחומים שלמים.
מכון קליי חזר על המחווה בשנת 2000 עם שבע בעיות המילניום. המטרה לא הייתה רק לחלק שבעה מיליון דולר. המכון ביקש לסמן את הגבולות הפתוחים של המתמטיקה ולהזכיר לציבור שגם בתחום שנתפס לפעמים כאוסף של תשובות מוחלטות יש שאלות עמוקות שאיש עדיין אינו יודע לפתור.
עד היום רק אחת מן השבע זכתה לפתרון שהתקבל – השערת פואנקרה, שהוכיח גריגורי פרלמן בתחילת שנות ה-2000. אם תוצאת נאוויה-סטוקס של OpenAI תתקבל, היא תהיה השנייה.
גם סוג הפתרון כאן ראוי לתשומת לב. במשך שנים אפשר היה לקוות שהתשובה תהיה חיובית – שהמשוואות תמיד נשארות חלקות. ההוכחה שמציעה OpenAI אומרת להפך: קיימים מצבים שבהם הן נשברות. במתמטיקה, הוכחה לכך שמשהו אינו אפשרי או אינו תמיד נכון סוגרת שאלה בדיוק כמו הוכחה חיובית.
כשהוכחות מפסיקות להיות משאב נדיר
לפני כמה ימים Anthropic הציגה הישג אחר: המערכת Claude הצליחה להפוך את ההוכחה המפורסמת של המשפט האחרון של פרמה להוכחה פורמלית ענקית שהמחשב יכול לבדוק. זו הייתה אוטומציה של עבודה מתמטית שכבר נעשתה בידי בני אדם. נאוויה-סטוקס, אם התוצאה תחזיק, נמצאת מדרגה אחרת – מערכת בינה מלאכותית יצרה טיעון חדש לבעיה פתוחה מן השורה הראשונה.
המתמטיקה לא הופכת בשל כך למקצוע שבו לוחצים על כפתור ומקבלים אמת. מי שבוחר את השאלה, בוחן את ההנחות, מזהה למה תוצאה מעניינת ומחבר אותה לידע הקיים עדיין עושה עבודה מתמטית. אבל היחס בין זמן לחשיבה לבין זמן לחיפוש עשוי להשתנות במהירות. אלפי סוכנים יכולים לבדוק במקביל כיוונים שמתמטיקאי יחיד היה משקיע בהם חודשים.
אם היכולת הזאת תמשיך להשתפר, צוואר הבקבוק יעבור בהדרגה מן השאלה "האם אפשר למצוא הוכחה?" לשאלות אחרות: איזו בעיה כדאי לפתור, אילו רעיונות בתוך ההוכחה באמת חדשים, ואיך הופכים מיליוני צעדים מכניים להבנה שאדם יכול להשתמש בה.
