במרוץ להוכיח ש־AI מסוגל לגלות ידע חדש, השאלה מי בודק את ההוכחות הופכת חשובה כמעט כמו הפתרון עצמו.
כשחברת AI מודיעה שהמערכת שלה פתרה בעיה שמתמטיקאים התקשו לפצח במשך עשרות שנים, התגובה המתבקשת היא התפעלות. התגובה הבאה צריכה להיות: מי בדק? במקרה של AlphaProof Nexus מבית Google DeepMind, יש תשובה מעבר להודעה לעיתונות: המחקר פורסם ב־8 באוקטובר בכתב העת Science, לאחר ביקורת עמיתים. לפי הודעת AAAS, המוציאה לאור של כתב העת, המערכת פתרה תשע מתוך 353 שאלות שניסתה מקטלוג בעיות ארדש, ובהן שתי שאלות שנותרו פתוחות במשך יותר מחצי מאה. החוקרים מציינים תקופה מדויקת של 56 שנה. הסיפור, שעליו דיווח גם The Decoder, מגיע ברגע שבו הקהילה המתמטית מתווכחת לא רק על יכולות הבינה המלאכותית, אלא גם על הדרך שבה חברות הטכנולוגיה מבקשות לקבל הכרה בהן.
תשע השאלות הן רק חלק מהתוצאות: המערכת הוכיחה גם 44 מתוך 492 השערות פתוחות שנבדקו מתוך OEIS, האנציקלופדיה המקוונת לסדרות מספרים שלמים. המחקר מתאר שימושים נוספים בגאומטריה אלגברית, באופטימיזציה, בתורת הגרפים ובאופטיקה קוונטית. עם זאת, המספרים דורשים קריאה מפוכחת: תשע מתוך 353 הן כ־2.5%, ו־44 מתוך 492 הן כ־8.9%. אלו שיעורי הצלחה בקבוצות שנבדקו, ולא מדד ליכולת לפתור כל שאלה מתמטית. הקורא יכול להחזיק בשתי מחשבות במקביל: פתרון של שאלה ותיקה הוא הישג משמעותי, ורשימת ההצלחות עדיין אינה רישיון להכריז שהמחקר המתמטי עבר לאוטומט. גם הכותרת המרשימה ביותר צריכה להשאיר מקום למכנה.
המערכת משלבת סוכני AI שמציעים הוכחות עם Lean, כלי לבדיקת הוכחות פורמליות. במקום להסתפק בטקסט משכנע, היא נדרשת לייצר הוכחה שהמחשב יכול לאמת, ומשתמשת במשוב שלו כדי לתקן ניסיונות כושלים. אבל גם כאן יש אחריות אנושית: צריך לוודא שהטענה שנכתבה בשפה הפורמלית אכן מייצגת את השאלה המקורית. החוקרים מתארים במאמר בדיקות מומחים ותיקונים של ניסוחים פורמליים, ומבהירים שרוב בעיות ארדש עדיין מחוץ להישג ידם של הסוכנים. לכן אימות ממוחשב וביקורת עמיתים הם שכבות בדיקה משלימות. האחד בוחן את ההוכחה בתוך המסגרת שהוגדרה; האחר מאפשר לבחון את העבודה כמחקר. עבור מי שקורא הכרזות על פריצות דרך, ההבחנה הזאת חשובה יותר מעוד תואר כמו ״מהפכני״.
במקביל, OpenAI בחרה לפרסם אוסף רחב של תוצאות מתמטיות במאגר GitHub. בהודעתה מ־6 באוקטובר הסבירה החברה שהתוצאות נוצרו במודל פנימי, ושחלק מההוכחות מלוות בניסוח ב־Lean. היא גם תיארה התייעצות עם קבוצת ייעוץ עצמאית והתחייבות לשפר את איכות ההצגה וההפניות. מנגד, Association for Human Mathematics פרסם הצהרה שהופיעה גם בבלוג של טרנס טאו, ובה התנגדות להפצת יותר מ־700 קבצים בבת אחת וקריאה למתמטיקאים להפסיק לעבוד עם החברה. זו קריאה של ארגון מסוים, ולא עמדה מוסכמת של כלל המתמטיקאים. ההצהרה גם אינה בדיקה שמפריכה את ההוכחות; היא מבטאת מחלוקת על כללי העבודה, הלגיטימציה לפרסום והמקום של הבנה אנושית במחקר.
לקורא הישראלי שמתעניין בכלכלת AI, יש כאן שיעור שימושי מעבר למתמטיקה. בניתוח שלנו, השאלה העסקית היא כמה עולה להגיע לתוצאה שאפשר להשתמש בה בביטחון. החוקרים מדווחים על עלות הרצה של כמה מאות דולרים לבעיה שנפתרה, אך מדגישים שהנתון אינו כולל את מלוא עלות החיפוש אחר בעיות שניתן לפתור, ואינו השוואה לעלות עבודתו של מתמטיקאי. עבור צוות מחקר או חברת טכנולוגיה בישראל, המשמעות היא שכדאי לחשב גם את הכנת הקלט, הניסיונות שנכשלו וזמן הבדיקה של מומחים. תוצאה זולה לייצור עלולה להיות יקרה לאישור. מנגד, מערכת שמחזירה תוצר שניתן לבדיקה עשויה להפוך השקעה בחישוב לכלי עבודה מועיל, גם אם אינה מצליחה בכל ניסיון. זו אפשרות כלכלית מעניינת, שעדיין צריך למדוד בכל שימוש בנפרד.
הלקח הרחב יותר, לטעמנו, נוגע לתכנון מערכות AI: כדאי לשאול מראש איך תיראה בדיקה אמינה של התוצאה, ומי יישא בעלותה. במתמטיקה קיימת אפשרות לנסח הוכחה שהמחשב בודק; בתחומים אחרים, מסמך רהוט או תחזית משכנעת אינם מספקים מנגנון דומה. לכן אי אפשר להסיק מההישג הזה שכל עבודת מחקר, ניתוח כלכלי או החלטה עסקית מוכנים למסירה לסוכן אוטונומי. אפשר בהחלט להסיק שיש ערך בהצמדת יכולת היצירה למסלול בדיקה ברור. הפרסום ב־Science הוא צעד חשוב בכיוון הזה, והוויכוח סביב OpenAI מחדד את מה שנותר פתוח: כיצד מגדילים את קצב הגילוי בלי להפוך את האימות לצוואר הבקבוק הבא. ה־AI יכול לכתוב מהר; האמון עדיין צריך להרוויח את מקומו.
