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

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

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

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

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

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

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

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

הכיוון של הוכחות שעוברות אימות ממוחשב התחיל לצבור תאוצה כבר קודם. גוגל דיפמיינד, שבבעלות אלפאבית, תיארה במחקר על מערכת AlphaProof מערכת שלמדה לכתוב הוכחות ב-Lean בעזרת למידת חיזוק, אחרי אימון על כ-80 מיליון בעיות שתורגמו אוטומטית לשפה הפורמלית. באולימפיאדה הבינלאומית במתמטיקה של 2024 פתרה המערכת שלוש בעיות, כולל הבעיה השישית, שחמישה מתחרים אנושיים בלבד פתרו, ויחד עם מערכת הגאומטריה של החברה צברה 28 מתוך 42 נקודות, ציון ברמת מדליית כסף. ההבדל כאן הוא בקנה המידה: בעיות אולימפיאדה נפתרות בכמה עמודים, וההוכחה של יאנג-מילס נפרסת על פני כ-9,500 קבצי קוד.

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

• יונייטד חוסמת סוכני AI מהזמנת טיסות, ומניית אקספדיה עלתה 3%
• OpenAI קנתה סוכן נסיעות של 8 עובדים, ומניות התיירות ירדו עד 5%