ההוכחות שהגשנו ל-First Proof
אנו משתפים את ניסיונות ההוכחה שלנו ל-First Proof, אתגר מתמטי הבוחן אם בינה מלאכותית יכולה להפיק הוכחות שאפשר לבדוק לבעיות בתחומי התמחות ספציפיים.
הרצנו מודל פנימי על כל 10 הבעיות של First Proof(נפתח בחלון חדש), אתגר מתמטי ברמת מחקר שנועד לבדוק אם מערכות בינה מלאכותית מסוגלות להפיק ניסיונות הוכחה נכונים שאפשר לבדוק. בניגוד לשאלות מתמטיות שהתשובה עליהן קצרה או לבעיות בסגנון תחרותי, הבעיות האלה דורשות בניית טיעונים שלמים בתחומי התמחות ספציפיים, וקשה לקבוע את נכונותם ללא בדיקה של מומחים. מחברי הבעיות של First Proof הם מומחים מובילים בתחומיהם, ולפחות שתיים מהבעיות נותרו פתוחות במשך שנים לפני שהמחברים מצאו להן פתרונות. אפשר להניח שחוג אקדמי שתחומי ההתמחות שלו חופפים במידה רבה לתחומי הבעיות יוכל לפתור רבות מהן בתוך שבוע.
שיתפנו(נפתח בחלון חדש) את ניסיונות ההוכחה שלנו בשבת, 14 בפברואר 2026, בשעה 00:00 לפי שעון החוף המערבי של ארה״ב. על סמך משוב ממומחים, אנו מעריכים שלפחות חמישה מניסיונות ההוכחה של המודל (לבעיות 4, 5, 6, 9 ו-10) נכונים בסבירות גבוהה, וכמה אחרים עדיין נבדקים. בתחילה הערכנו שניסיון ההוכחה שלנו לבעיה 2 ככל הנראה נכון. בעקבות ההתייחסות הרשמית של First Proof וניתוח נוסף של הקהילה, אנו סבורים כעת שהוא שגוי. אנו מודים על המעורבות ומצפים להמשך הבדיקה. אפשר למצוא את כל ניסיונות ההוכחה שלנו כאן(נפתח בחלון חדש). המאמר בגרסתו המוקדמת כולל את כל עשרת ניסיונות ההוכחה, וכן נספח חדש עם תבניות פרומפטים ודוגמאות שנועדו לדמות את האינטראקציות הידניות שלנו עם המודלים לאורך התהליך.
אנו סבורים שמחקר חדשני בחזית הידע הוא אולי הדרך החשובה ביותר להעריך את יכולותיהם של מודלי הבינה המלאכותית מהדור הבא. מבחני ביצועים הם כלי שימושי, אך הם עלולים להחמיץ כמה מההיבטים הקשים ביותר במחקר: שמירה על רצף ארוך של reasoning, בחירת ההפשטות הנכונות, התמודדות עם עמימות בניסוח הבעיות ובניית טיעונים שעומדים בבחינה מדוקדקת של מומחים. אתגרים בחזית הידע כמו First Proof עוזרים לנו לבחון את גבולות היכולות האלה במצבים שבהם אימות הנכונות אינו פשוט, ואפשר ללמוד מאופני הכשל.
״אנחנו מאמנים כעת מודל חדש, שאחד הדגשים המרכזיים באימון שלו הוא הגברת הקפדנות בחשיבה, במטרה לאפשר לו לחשוב ברציפות במשך שעות רבות ולשמור על רמת ביטחון גבוהה במסקנותיו. כשהוכרזו הבעיות של First Proof, זה נראה כמו הזדמנות מושלמת להעמיד אותו במבחן, אז ניסיתי אותו במהלך סוף השבוע. כבר אז הוא הצליח לפתור שתיים מהבעיות (9 ו-10). ככל שהאימון התקדם, היכולות שלו השתפרו, ולבסוף הוא פתר — להערכתנו — לפחות שלוש נוספות. שמחנו במיוחד כשהוא פתר את בעיה 6, ואז, יומיים לאחר מכן, את בעיה 4, כי הבעיות האלה היו מתחומים שמוכרים לרבים מאיתנו. מדהים לראות מודל נעשה חכם יותר מיום ליום באופן כל כך מוחשי.״
– ג׳יימס ר׳ לי (חוקר ב-OpenAI, בתחום ה-reasoning)
הרצנו את המודל בפיקוח אנושי מוגבל. כשנתנו הנחיות לגרסאות של המודל בשלבים שונים של האימון, הצענו לפעמים לחזור לאסטרטגיות שנראו מבטיחות בניסיונות קודמים. בחלק מהניסיונות, לאחר שקיבלנו משוב ממומחים, ביקשנו מהמודל להרחיב או להבהיר חלקים מההוכחה כדי להקל על בדיקת ה-reasoning. תיווכנו גם בחילופי דברים בין המודל הזה לבין ChatGPT לצורך אימות, עיצוב וסגנון. בחלק מהבעיות אנו מציגים את הניסיון הטוב ביותר מבין כמה ניסיונות, שנבחר לפי שיקול דעת אנושי. זה היה מאמץ קצר ואינטנסיבי, והתהליך שלנו לא היה מוקפד כפי שהיינו רוצים שיהיה בהערכה מבוקרת כהלכה. אנו מצפים לדון עם מארגני First Proof במסגרת ניסוי והערכה קפדנית יותר לסבבים עתידיים.
עבודה זו מתבססת על תוצאות קודמות של מודלי reasoning בחזית הטכנולוגיה במתמטיקה ובמדע. ביולי 2025 הגענו לביצועים ברמת מדליית זהב(נפתח בחלון חדש) באולימפיאדה הבין-לאומית למתמטיקה באמצעות מודל reasoning לשימוש כללי (35 מתוך 42 נקודות). בנובמבר 2025 פרסמנו את ״ניסויים ראשוניים בהאצת המדע בעזרת GPT‑5״, אוסף מקרי בוחן שבהם GPT‑5 עזר לחוקרים להתקדם באופן ממשי במתמטיקה, בפיזיקה, בביולוגיה ובתחומים נוספים, לצד המגבלות שזיהינו. ולאחרונה דיווחנו על שיתוף פעולה בפיזיקה שבו GPT‑5.2 הציע ביטוי אפשרי לנוסחה של אמפליטודת גלואונים. לאחר מכן מודל פנימי הוכיח את הנוסחה באופן פורמלי, והמחברים אימתו אותה.
אנו מצפים להעמיק את השיח עם הקהילה על דרכים להערכת reasoning ברמת מחקר, ולקבל בתוך כך משוב ממומחים על הניסיונות האלה. אנו נרגשים לקראת הנגשת היכולות החדשות האלה במודלים עתידיים שיהיו זמינים לציבור.
