GPT-5.6 סגר בפרומפט פער בן 30 שנה באופטימיזציה קמורה

פוסט בפורום r/math מדווח ש-GPT-5.6 Sol Pro הפיק בפגישה אחת של 148 דקות את החצי החסר של תוצאה בסיבוכיות באופטימיזציה קמורה, שנשארה פתוחה מאז 1996. מחבר המאמר המקדים שמתלווה לתוצאה אומר שהטיעון אומת פורמלית ב-Lean, ושהתוצאה טרם עברה ביקורת עמיתים.

מה בדיוק היה פתוח

מדובר באופטימיזציה קמורה דטרמיניסטית מסדר אפס. האלגוריתם רשאי לשאול על כל נקודה בכדור היחידה ב-R^d ומקבל רק את הערך המדויק של פונקציה קמורה בת 1-ליפשיץ — בלי גרדיאנטים — וזולת זאת אינו מוגבל לא בחישוב ולא בזיכרון. בעיות כאלה, שבהן זמין רק ערך הפונקציה, מופיעות כשמעריכים את פונקציית המטרה באמצעות ניסוי פיזי או סימולטור, והשאלה הטבעית היא כמה הערכות נדרשות באופן עקרוני. ב-1996 הציג פרוטסוב אלגוריתם שמראה שסדר גודל של d² הערכות מספיק. החסם התחתון המתאים חסר: התוצאה החזקה ביותר שעמדה לרשות החוקרים עד אז, Ω(d), ירשה מן המודל החזק יותר מסדר ראשון שבו גרדיאנטים זמינים, וכך נותר פער לינארי ב-d בלי ודאות שגרדיאנטים עוזרים בכלל. ההוכחה שהמודל סיפק סוגרת את הפער: שום אלגוריתם אינו יכול להסתפק בפחות מסדר d² הערכות, כלומר שיטתו של פרוטסוב אופטימלית.

פרומפט של עשרה עמודים ו-148 דקות

המחבר, מרצה בהנדסת תעשייה וחקר ביצועים באוניברסיטת קליפורניה בברקלי, עבד על הבעיה בהפסקות במשך כשנה וניסה את GPT-5.4 ואת GPT-5.5 בלי הצלחה. אחרי ש-OpenAI הודיעה על ההוכחה של השערת כיסוי הגרף הכפול במעגלים, הוא כתב פרומפט באורך של כעשרה עמודים באותו סגנון — הוא מצורף בסוף המאמר המקדים — וביקש את החסם התחתון הריבועי ברמת דיוק מסדר d⁻⁴. אחרי 148 דקות של עבודה רצופה החזיר המודל הוכחה שקובעת תלות ריבועית במימד ברמת דיוק מסדר d⁻³. המחבר בדק את הטיעון בעצמו והוכיח אותו פורמלית ב-Lean. הבנייה — מקסימום של פונקציות אפיניות — קרובה לזו שעומדת מאחורי החסם ההדוק של נמירובסקי ויודין לאופטימיזציה קמורה מסדר ראשון.

מה זה אומר למחקר

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