OpenAI הוציאה מאות מיליוני דולרים על מתמטיקה, ואלטמן מודה: יש עוד הוכחות במגירה
OpenAI הוציאה על מתמטיקה סכום בסדר גודל של מאות מיליוני דולרים, ולפי מנכ"ל החברה סם אלטמן, היא מחזיקה בהוכחות נוספות שטרם פורסמו, מעבר ליותר מ-700 שכבר שוחררו. הוכחה אחת, של בעיית נאוויה-סטוקס, עלתה לבדה כ-10 מיליון דולר ואולי מעט יותר. המספרים האלה, שאלטמן מסר בפודקאסט של ג'ון קוליסון, נשיא סטרייפ, ממחישים עד כמה התחרות בין מעבדות ה-AI עברה מצ'טבוטים ומבחני ביצועים למחקר בסיסי. ובמקביל הם מסבירים את החשש בקהילת המתמטיקאים: גוף מסחרי אחד יכול להשקיע בבעיה בודדת יותר ממה שמחלקה אוניברסיטאית שלמה מוציאה בשנים.
- אלטמן: הזכות של העולם לידע בסיסי גוברת על הפגיעה בקריירה של מדענים
- חוקרים מקיימברידג' ומקינגס קולג' לונדון מצאו פערים בין ההוכחה הכתובה לגרסה הממוחשבת שלה
- גוגל דיפמיינד פתרה 9 בעיות ארדש פתוחות בעלות של כמה מאות דולרים לבעיה
אלטמן אמר שהוא מבין את המתמטיקאים, ושבשבוע אחד מאמץ המתמטיקה של החברה אכן "יצא משליטה", בכוונה. לדבריו, בפרדיגמה חדשה נותנים לחוקרים לבדוק את גבולות היכולת ומייעלים בהמשך. כשעבדו על נאוויה-סטוקס, הצוותים הבינו מעט על האופן שבו קבוצות של סוכני AI משתפרות עם תוספת משאבים, והוא מעריך שבתוך שנה אפשר יהיה לחזור על אותה הוכחה באחוז אחד מהעלות.
הוא גם סיפר על ערוץ פנימי בשם "Model Name-Hold My Beer", שנפתח כשהגיע מודל חדש. עובדים זרקו לתוכו את הבעיות הקשות ביותר מהקריירה האקדמית שלהם, והמודל פתר אותן אחת אחרי השנייה. אלטמן תיאר שני לילות כמעט בלי שינה מרוב התרגשות, לצד עצב ותחושה שמשהו מסתיים. ועדיין, מבחינתו זה הצעד הנכון ואיש איננו יכול או צריך לעצור אותו.
הידעת?מה היא בעיית נאוויה-סטוקס?
הוויכוח כבר יצא מגבולות האקדמיה. מתמטיקאים מתחו ביקורת על הדרך שבה OpenAI מפרסמת את התוצאות: מאות תוצאות בחודש, עם תיאורים קצרים וקשים למעקב, ומעט הקשר וייחוס. את עבודת הבדיקה הם נאלצים לעשות בעצמם. החברה אף פרשה מ"האקתון מתמטיקה" במכון קאלטק, אחרי שמתמטיקאים מהמכון ומחוצה לו טענו שהאירוע עלול לפגוע בקהילה.
בספטמבר הציגה OpenAI פתרון לבעיית נאוויה-סטוקס, אחת מבעיות המילניום. לפי החברה, הסוכנים הגיעו לתוצאה כ-88 שעות אחרי שהופעלו, והאימות הפורמלי בשפת Lean נמשך עוד 17 שעות. אבל שלושה חוקרים, אנדרס הנסן ופביאן צ'רצ'לי מקיימברידג' ואלכסנדר בסטוניס מקינגס קולג' לונדון, עברו על ההוכחה הממוחשבת, שאורכה כ-180 עמודים, ומצאו כבר בשני עמודים שני מקרים שבהם הקוד מוכיח טענה חלשה מזו שבגרסה הכתובה. זה עדיין אומר שההוכחה שגויה? לא בהכרח, ו-OpenAI הבהירה שהיא מודעת לפער ותתקן טעויות כשיימצאו. במקביל, מתמטיקאים אחרים הראו שהפתרון נשען על כוח חיצוני מלאכותי, שמותר בנוסח המקורי של מכון קליי, ולכן הוא עונה על הבעיה כפי שנוסחה, ופחות על השאלה שמעניינת את חוקרי הזרימה.
הידעת?מה זה Lean?
בסוף אוקטובר הכריזה החברה על תגליות נוספות: הוכחת השערת ה-local smoothing בכל מספר ממדים, ובעקבותיה השערת קאקיה, והוכחת קיום של תורות שדה קוונטיות, כולל תורת יאנג-מילס הטהורה, שהיא חלק מבעיית מילניום נוספת. את התוצאה בפיזיקה העבירה OpenAI לקבוצה בראשות זוכה פרס נובל דייוויד גרוס, שתחליט איך ומתי לפרסם. היא גם תרמה 5 מיליון דולר ליוזמה של קרן סיימונס שתעזור למתמטיקאים לבחון תוצאות של בינה מלאכותית.
OpenAI איננה לבד במרוץ. גוגל דיפמיינד, שבבעלות אלפאבית, פרסמה מערכת בשם AlphaProof Nexus שפתרה 9 מתוך 353 בעיות ארדש פתוחות, בהן שתיים שהמתינו לפתרון 56 שנה, וגם 44 מתוך 492 השערות מאנציקלופדיית סדרות המספרים. העלות שם הייתה כמה מאות דולרים לבעיה, ומומחים מהצוות בדקו שהניסוח הפורמלי תואם את הבעיה המקורית. כלומר, השאלה כבר איננה אם מודלים יכולים לפתור בעיות פתוחות, אלא כמה זה עולה ומי מאמת את התוצאה.
לשאלת העלות יש משמעות עסקית. OpenAI, שבה מיקרוסופט מחזיקה נתח מהותי, צורכת כמויות חישוב אדירות, ואלטמן מעדיף לשרוף אותן עכשיו ולסמוך על ירידת מחירים בהמשך. המתמטיקה משמשת לה חלון ראווה ליכולות המודלים מול משקיעים ומתחרים. להרחבה: שווי של 1.25 טריליון דולר: מי עומד מאחורי גיוס הענק של OpenAI ולמה השווי ירד?
להרחבה: שלושה משפטים פתוחים במתמטיקה, במחשבים ובפיזיקה: OpenAI טוענת שהמודלים שלה פתרו אותם
