722 עבודות מתמטיקה של מודל סגור של OpenAI. כמה מהן בדקה מכונה?

722 כתבי יד, 372 משפחות תוצאות, commit אחד בשם Initial commit. כך נראה ב-6 באוקטובר שחרור המתמטיקה של OpenAI: תוצרים של כמה שבועות עבודה של מודל פנימי נחתו במאגר פתוח ביום אחד. ב-21 בספטמבר החברה עוד דיברה על «יותר מ-100» בעיות פתוחות שנפתרו.

לפני חודש פירקנו איך נחיל של 10,000 סוכני OpenAI תקף את בעיית נאבייה-סטוקס, והסיפור האמיתי שם התברר כמאמת המכונה: Lean. השאלה לשחרור החדש זהה: איפה עמד המאמת, ואיפה הוא חסר.

מה OpenAI פרסמה ב-6 באוקטובר

לפי ה-README של המאגר, כמעט כל התוצאות עברו אותו תהליך: המודל קיבל בעיות פתוחות, כ-4,000, והשקיע בממוצע שלוש שעות «חשיבה» של ChatGPT Pro לכל תוצאה. אחר כך התשובות קובצו למשפחות וסוננו לפי חשיבות. החריגים נאמרים במפורש: התחום ללא אפסים של פונקציית זטא והשערת הודג' ליריעות אבליות CM לא עברו בתהליך הכללי, ואת הטקסט על Re(s) > 11/12 ערכו בני אדם.

השמות ברשימה גדולים. השערת רימן הכמעט-מלאה: לפונקציית זטא ולכל פונקציות L של דיריכלה אין אפסים כאשר Re s > 7/8. מעריך כפל מטריצות ω ≤ 9/4 מעל המספרים המרוכבים. השערת ברנט על מעגלים המילטוניים. דוגמאות נגדיות לכמה מהשערות קפלנסקי. נוסחת ברץ' וסווינרטון-דייר לחלק מהעקומים האליפטיים. את המודל עצמו OpenAI מבטיחה לשחרר «responsibly», בלי תאריך.

עוד פרט נראה רק בשמות התיקיות. על כל כתב יד מופיע תאריך, ו-564 מתוך 722 מתוארכים ל-23–27 בספטמבר, מתוכם 370 נופלים על יומיים בלבד, 23 ו-24 בספטמבר. עוד 112 מסומנים 5 באוקטובר, יום לפני הפרסום.

«יש Lean» לא אומר «נבדק»

הסיכומים כותבים ש«רבות מההוכחות עברו פורמליזציה». זה נכון, אבל הניסוח מסתיר שלוש הסתייגויות ש-OpenAI עצמה השאירה במאגר.

הראשונה: ל-235 משפחות יש קישור ל-Lean, ו-137 נשענות על טקסט בלבד. ה-README אומר את זה ישירות: «Some of the unformalized results could have issues», ומבטיח לתקן מהר.

השנייה: הפורמליזציה מכסה לעיתים קרובות את המשפט המרכזי, לא את המאמר כולו. בתיאור חלק ה-Lean של השערת רימן הכמעט-מלאה כתוב שהחסם 7/8 הוכח פורמלית, ואילו הנספחים המאוחרים של המאמר לא נכנסו לפורמליזציה.

השלישית: הקטלוג lean/formalization.yaml מונה 162 מאמרים שהתוצאה המרכזית שלהם עברה פורמליזציה. בשדה ההיקף כתוב «Partial progress», ובשדה הביקורת status: unchecked. Lean מבטיח שהגזירה תקינה. האם הניסוח הפורמלי הוא בדיוק הטענה שבכותרת המאמר, את זה בודק אדם, ולפי הסימון של OpenAI עצמה הבדיקה הזו לא נעשתה.

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

ב-21 בספטמבר הוקמה במכון למחקר מתקדם בפרינסטון קבוצת יועצים, AGMAI: תשעה מתמטיקאים. אין לה סמכות לקבוע באיזה קצב OpenAI עוסקת במתמטיקה, רק לייעץ איך לפרסם. ב-29 בספטמבר היא פרסמה המלצות על סמך יותר מ-600 תגובות של עמיתים, ופתחה במשפט שקשה לקרוא אחרת: «we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models».

השחרור הגיע שבוע אחר כך. השווינו סעיף מול סעיף.

הקבוצה עצמה הגיבה ב-7 באוקטובר באיפוק: השחרור הוא «the beginning, not the completion, of the process of human understanding». את ההמלצות שלה היא חזרה ואישרה.

איך לבדוק הוכחה של OpenAI בעצמכם

הצד החזק של השחרור נמצא במקום אחר. לתוצאות שעברו פורמליזציה OpenAI צירפה משימות ל-comparator, כלי של Lean FRO שבודק הוכחה מול ניסוח שנכתב מראש. כל אחד יכול לחזור על הבדיקה. ה-README ממליץ לא לבנות את כל הספרייה בבת אחת: יש בה 122,140 קבצי ‎.lean, והבנייה עלולה להיתקע במגבלת המערכת vm.max_map_count, ולכן בודקים תוצאה אחת בכל פעם.

lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

למחרת עשה את זה משתמש בפורום של OpenAI, davegoldblatt, ואת הבדיקה עצמה הריץ Claude Code. התוצאה: 2,924 מודולים נבנו בלי שגיאות ובלי אזהרות, וההוכחה התקבלה גם ב-comparator וגם בליבה העצמאית nanoda. ההסתייגות שלו מדויקת יותר מכל כותרת: «this checks the Lean proof, not the paper». ריצה אחת, מכונה אחת, ומה שנבדק הוא הטקסט הפורמלי, לא המאמר.

מה לקחת מזה למי שעובד עם סוכנים

הדעה שלנו, ואפשר להתווכח איתה: התוצאה המרכזית של השחרור היא לא 722 כתבי היד, אלא כמה קל נעשה להבדיל בין מה שנבדק למה שנטען. איפה שיש משימת comparator, בדיקת החלק הפורמלי מסתכמת בפקודה אחת, וסוכן יכול להריץ אותה. איפה שאין, נשארים המוניטין של החברה ו-«could have issues». נתברר כטועים אם מתמטיקאים עצמאיים ימצאו בחודשים הקרובים שגיאות רציניות דווקא בחלק שעבר פורמליזציה: אז הגבול עובר במקום אחר.

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