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

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

מה ביקשו המתמטיקאים

הקבוצה נקראת Advisory Group on Mathematics and Artificial Intelligence ‏(AGMAI). היא פועלת במסגרת Institute for Advanced Study שבפרינסטון וחברים בה תשעה חוקרים בולטים ממוסדות שונים בעולם. בסוף ספטמבר היא פרסמה הנחיות למעבדות AI שעוסקות בפתרון בעיות מתמטיות.

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

לפי TechCrunch, חלק מהעקרונות OpenAI כן יישמה: היא פרסמה את התוצאות מהר ככל האפשר וצירפה מידע על הדרך שבה המודלים הגיעו למסקנות. אבל רק 10 מתוך 719 כתבי היד כללו את ה-chain of thought, כלומר את שרשרת ההסקה של המודל. גם הפורמליזציה, הכתיבה מחדש של ההוכחה בשפה שמחשב יכול לבדוק, לא בוצעה בכל המקרים שבהם המתמטיקאים המליצו עליה.

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

"אבודים בתרגום"

השבוע פרסמו מתמטיקאים מאוניברסיטת קיימברידג' ומ-King's College London מאמר שמחדד את הבעיה. כשמודל פותר בעיה מתמטית, הוא כותב קודם הסבר ב"שפה טבעית" ואחר כך מנסה לנסח את התוצאה ב-Lean. ‏Lean היא שפת תכנות שבה הוכחה שעוברת קומפילציה אמורה להיות נכונה.

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

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

למה זה חשוב

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

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

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