כבר לא רק פותר תרגילים: OpenAI טוענת לפריצת דרך ב-10 בעיות מתמטיות פתוחות

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

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

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

מעיגולים על דף לקריפטוגרפיה של העתיד

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

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

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

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

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

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

• המודלים הסיניים מצמצמים את הפער מול OpenAI ואנתרופיק
• OpenAI מסמנת 2027 להנפקה, עם פתח להקדים את המועד

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

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

ומה שונה כאן מהזיה רגילה של מודל?

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

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

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

• עוד יום להתכונן להוריקן: ה-AI של גוגל משפר את התחזית בעשור
• מה שעושים בגיל 50 עשוי להשפיע על הזיכרון בגיל 80 - המחקר שמצא פער של 13 שנים

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

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

העלות: בערך 2,000 דולר של טוקנים

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

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

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

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

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

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