Microsoft: סוכני AI סייעו לפריצת דרך בהשערת KLS

Microsoft Research פרסמה ב-21 באוקטובר תיאור מפורט של עבודה שהובילה לטענה לפתרון השערת Kannan–Lovász–Simonovits, המוכרת כהשערת KLS. המאמר של Zhao Song ושל Xinzhi Zhang הועלה ל-arXiv ב-1 באוקטובר ועודכן ב-4 באוקטובר. הוא משתרע על 140 עמודים וטוען לחסם קבוע על קבוע KLS, התוצאה שההשערה דורשת.

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

איך שולבו הסוכנים במחקר

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

התוצאה אינה נשענת רק על הודעת Microsoft. ב-4 באוקטובר העלו Pierre Bizeul, Boaz Klartag ו-Joseph Lehec מאמר נפרד בן 32 עמודים שמציג הוכחה אחרת ומשתמש בקריטריון החדש של Song ו-Zhang כשלב מרכזי. נוסף לכך פורסמה פורמליזציה ב-Lean של גרסה של הטיעון, שמאפשרת למחשב לבדוק את שרשרת ההיסקים בתוך מערכת הוכחה פורמלית.

מה כבר מבוסס ומה עוד פתוח

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

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

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