דיפמיינד מוכיחה שבינה מלאכותית צריכה מהדר צמוד

מתמטיקה היא המקום שבו מודלי שפה אוהבים לשקר בביטחון עצמי מוחלט. עכשיו מתברר שכדי לגרום לבינה מלאכותית להוכיח טענות מדעיות בלי להמציא שטויות בדרך, אי אפשר פשוט לתת לה לפטפט במילים יפות. לפי מחקר חדש של Google DeepMind שפורסם בכתב העת Science, מערכת בשם AlphaProof Nexus הצליחה להוכיח תשע בעיות פתוחות של המתמטיקאי פול ארדש מתוך 353 בעיות שנבדקו. שתיים מהן עמדו ללא מענה במשך 56 שנה. השיטה הזו לא מתבססת על עוד מודל ענק שמקליד טקסט, אלא על חיבור קשיח למהדר תוכנה אמיתי.

זה לא טריק שיווקי רגיל.

מהדר במקום מנחש

הרעיון ההנדסי שמאחורי AlphaProof Nexus שונה מהותית ממה שראינו במערכות צ׳אט רגילות שמנסות לייצר תשובות אינטואיטיביות. בליבת המערכת יושב Gemini 3.1 Pro, אך במקום לייצר הוכחות מתמטיות בשפה טבעית, הוא מנסח טיוטות קוד בשפת ההוכחה הפורמלית Lean 4. המהדר של Lean בודק כל שורה וכל צעד לוגי באופן דטרמיניסטי מוחלט מיד אחרי כל עריכה. אם ההיסק שגוי, הודעת השגיאה המדויקת חוזרת ישירות למודל השפה כדי שיכוון את הניסיון הבא בלולאת היזון סגורה. במקרים שבהם מתגלות תתי-בעיות קשות במיוחד, הסוכן יכול להפעיל ברקע את כלי ההוכחה הייעודי AlphaProof.

נוסף לתשע הבעיות של ארדש, המערכת הוכיחה 44 מתוך 492 השערות ממאגר הסדרות On-Line Encyclopedia of Integer Sequences, הידוע כ-OEIS. היא גם הכריעה שאלה פתוחה בגיאומטריה אלגברית ושיפרה חסם מוכר באופטימיזציית מינימקס, תחום שמשמש בעצמו לאימון מודלים. בדיווח של DeepMind בדף המאמר הרשמי נכתב שאפילו סוכן בסיסי שפשוט החליף לסירוגין בין יצירת טיוטות ב-Gemini לבין אימות ב-Lean הצליח לשחזר לבדו את ההצלחות בבעיות של ארדש, גם בלי להפעיל את AlphaProof המורכב. המהדר של Lean פשוט לא מעביר אף שורה שלא יושבת במדויק על חוקי הלוגיקה הפורמלית.

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

מדע אמיתי מול יחסי ציבור

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

איגוד המתמטיקאים Association for Human Mathematics, בהובלת המתמטיקאי הנודע טרנס טאו (Terence Tao), יצא בקריאה לחרם על OpenAI בשל הצפת הקהילה בחומרים מרושלים ולא מפוקחים שדורשים שעות רבות של בדיקה וסינון ידני. ב-DeepMind נקטו גישה הפוכה לחלוטין. במקום לשפוך הוכחות חצי אפויות לרשת ולחכות שחוקרים אנושיים יעשו עבורם את העבודה השחורה, הם העבירו את העבודה ביקורת עמיתים מקיפה ופירסמו את הממצאים בכתב העת Science.

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

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

המחיר שמחביאים מתחת לשטיח

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

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

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

מה לקחת לפיתוח הבא

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

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