OpenAI מפרסמת הוכחות מתמטיות של AI: מי בודק שהן נכונות?
OpenAI פרסמה תוצאות מתמטיות של מודל פנימי, כתבי יד ב־GitHub והוכחות רבות ב־Lean. החומרים מאפשרים ביקורת, אך אימות פורמלי אינו מחליף בדיקה של הקהילה.
OpenAI פרסמה ב־6 באוקטובר תוצאות מתמטיות שהפיק מודל פנימי, בצירוף כתבי יד ב־GitHub ופורמליזציות של רבות מההוכחות בשפת Lean. החידוש החשוב לקוראים מחוץ לחברה הוא האפשרות לבחון את התוצרים, במקום להסתפק בתיאור ההישגים. אבל בין הוכחה שמודל מציע לבין תוצאה מתמטית חדשה שהקהילה מקבלת יש כמה בדיקות שונות, ומחשב אינו מחליף את כולן.
מה פורסם: תוצאות לבדיקה, לא מודל להורדה
הפרסום, שכותרתו Sharing AI progress in mathematics, כולל אוסף תוצאות לצד חומרים שנועדו לאפשר עיון וביקורת. OpenAI פרסמה גם עשרה סיכומי תהליכי חשיבה ונתוני משאבי חישוב. אלה מוסיפים מידע על הדרך לתוצאות ועל המשאבים שנדרשו, אך סיכום תהליך אינו תיעוד מלא של כל ניסיון, ופרסום תוצר אינו שקול לשחזור עצמאי של אופן הפקתו.
חשוב להפריד בין שלושה דברים: כתבי היד מציגים את הטענות ואת ההסברים המתמטיים; הפורמליזציות מאפשרות בדיקה ממוחשבת של ניסוחים פורמליים; וסיכומי התהליכים מספקים הקשר נוסף לעבודת המודל. כל שכבה עונה על שאלה אחרת. גם יחד, הן אינן מאפשרות להסיק שכל הטענות כבר עברו אימות עצמאי, או שהמודל שהפיק אותן זמין לשימוש הציבור.
נכון ל־7 באוקטובר 2026, זהו פרסום תוצאות של מודל פנימי. אין לראות בו הכרזה על מודל מתמטי זמין לציבור, וגם לא אישור גורף שכל התוצאות אומתו בידי חוקרים בלתי תלויים.
מה Lean יכולה לאשר, ומה נשאר למתמטיקאים
הוכחה מתמטית רגילה נכתבת עבור בני אדם. היא יכולה להסתמך על ידע מקובל, לדלג על צעדים שגרתיים ולהשתמש בניסוח שמומחה מבין מההקשר. בפורמליזציה צריך לתרגם את הטענה, ההגדרות והצעדים למערכת מפורשת. Lean מאפשרת לבדוק שההוכחה הפורמלית תקפה ביחס להגדרות ולהנחות שבהן השתמשו, במקום להסתמך רק על טקסט שנשמע משכנע.
זו הבחנה מרכזית כשמודל שפה מעורב בתהליך: הסבר שוטף אינו ערובה לטיעון תקף. עם זאת, גם בדיקה פורמלית מוצלחת משאירה שאלות אנושיות. האם המשפט שנוסח בקוד הוא באמת המשפט שבכתב היד? האם ההנחות תואמות את הבעיה המקורית? והאם התוצאה מוסיפה ידע, או מציגה מחדש משהו שכבר ידוע בספרות?
בדיקה פורמלית בוחנת אם ההוכחה תקפה במסגרת שנוסחה. היא לא קובעת לבדה אם נוסחה הבעיה הנכונה, או אם התוצאה חדשה.
לכן אין סתירה בין הערך של Lean לבין הצורך בביקורת מתמטית. דווקא השילוב ביניהם מעניין: המחשב יכול לבדוק פרטים לוגיים בניסוח הפורמלי, והחוקרים יכולים לבחון את ההתאמה לבעיה, את ההקשר ואת החשיבות. בפרסום הנוכחי יש פורמליזציות של רבות מההוכחות, ולכן גם לא נכון להתייחס לכל האוסף כאילו לכל תוצאה מצורפת אותה רמת תיעוד.
איך בוחנים את ההישג בלי להסתפק בכותרת
הדרך המועילה לקרוא את הפרסום היא ברמת התוצאה הבודדת. המילה ״הוכחה״ אינה פוטרת מהשאלה מה בדיוק נבדק, ופרסום קוד אינו מבטיח שמי שמוריד אותו יוכל מיד לשחזר את הבדיקה. לחוקר או למפתח שרוצים להעריך את החומרים, כדאי לבנות מסלול בדיקה שמפריד בין נכונות, יכולת שחזור וחידוש מדעי.
- לזהות את הטענה המדויקת: מה נטען בכתב היד, תחת אילו הנחות ולאיזו בעיה הוא מתייחס.
- לבדוק מה מצורף לתוצאה: האם קיימת פורמליזציה, ואילו חלקים מהטיעון היא מכסה.
- להריץ את הבדיקה בסביבה המתאימה: לתעד תלויות והגדרות, ולוודא שאין רכיבים לא מוכחים שמשנים את משמעות האימות.
- להשוות בין הקוד לטקסט: לבדוק שהניסוח הפורמלי אינו מחליש את הטענה או מוסיף הנחות מהותיות.
- לבחון את הספרות הרלוונטית: להפריד בין הוכחה תקפה לבין תוצאה חדשה ובעלת משמעות.
גם את נתוני החישוב צריך לקרוא בזהירות. הם יכולים לסייע בהערכת המשאבים שתוארו, אבל אין להסיק מהם לבדם כמה יעלה לחוקר אחר להגיע לתוצאה דומה. יצירת הוכחה ובדיקת הוכחה הן משימות שונות. האפשרות לבדוק תוצר שפורסם אינה מעידה בהכרח שאפשר לשחזר את החיפוש שהוביל אליו.
הזווית הישראלית: אפשר לבדוק גם בלי גישה למודל
לקבוצות מחקר בישראל יש כאן הזדמנות מעשית שאינה תלויה בקבלת גישה למודל הפנימי: לבחור תוצאה בתחום ההתמחות שלהן ולבחון אותה לעומק. סמינר משותף למתמטיקאים ולחוקרי מדעי המחשב יכול לחלק את העבודה בין קריאת כתב היד, סקירת הספרות ובדיקת הפורמליזציה. זו הצעה למסלול מחקר מקומי, לא דיווח על בדיקה שכבר בוצעה בישראל.
לסטודנטים, החומרים יכולים לשמש תרגיל ממוקד בקריאה ביקורתית: לא ״האם AI טוב במתמטיקה״, אלא האם טענה מסוימת מנוסחת ומוכחת היטב. תוצר שימושי של עבודה כזו יהיה דוח שמפרט מה נבדק, באיזו סביבה ומה נותר פתוח. גם זיהוי פער בין הניסוח הטבעי לפורמלי יכול להיות תרומה משמעותית, בלי להכריז שהאוסף כולו נכון או שגוי.
למפתחי AI בחברות ישראליות העוסקות באימות תוכנה, הלקח הוא תכנוני: להפריד בין רכיב שמציע פתרון לבין רכיב שבודק אותו לפי כללים מפורשים. עם זאת, הפרסום המתמטי אינו הוכחה שמערכת דומה מוכנה לאמת מוצר מסחרי. במערכת עסקית עדיין צריך להגדיר מה נחשב נכון, אילו הנחות מותרות ואילו תקלות הבודק כלל אינו מכסה.
מה הלאה: המדד החשוב יהיה הביקורת על התוצרים
OpenAI מציינת שתמשיך לשפר את הצגת המאמרים ולהוסיף פורמליזציות. לכן השלב הבא שכדאי לעקוב אחריו אינו רק פרסום תוצאות נוספות, אלא גם בהירות התיעוד ובדיקות עצמאיות של תוצאות מסוימות. אימות חיצוני מועיל יבהיר בדיוק איזו טענה נבדקה, מה כיסתה הבדיקה ואילו שאלות נשארו ללא מענה.
הערך המחקרי המיידי הוא בהפיכת תוצרים של מודל פנימי לחומרים שאפשר לבקר. זה בסיס רציני יותר לדיון מאשר תשובה מרשימה בצ׳אט, אבל עדיין לא סוף תהליך ההערכה. עבור חוקרים בישראל, השאלה המעשית כעת היא איזו תוצאה ראוי לבדוק, ואיך לפרסם בדיקה שאחרים יוכלו לשחזר.
שאלות נפוצות
האם OpenAI הוכיחה שהמודל שלה פתר בעיות מתמטיות חדשות?
OpenAI פרסמה תוצאות מתמטיות שהפיק מודל פנימי ותוצרים שמאפשרים לבדוק אותן. הפרסום אינו מעיד שכל הטענות אומתו באופן עצמאי, ויש להבחין בין נכונות ההוכחה, התאמתה לשאלה ומידת החידוש שלה.
מהי Lean ואיך היא בודקת הוכחות מתמטיות?
Lean היא שפה וסביבה לכתיבת טענות והוכחות פורמליות, המאפשרת למחשב לבדוק את תקפותן ביחס להגדרות ולהנחות שנוסחו. בדיקה מוצלחת אינה קובעת לבדה שהניסוח תואם את הבעיה המקורית או שהתוצאה חדשה וחשובה.
האם אפשר להשתמש במודל המתמטי ש־OpenAI הציגה?
הפרסום המתואר עוסק בתוצאות של מודל פנימי ואינו הכרזה על זמינותו לציבור. אפשר לבחון את כתבי היד ואת הפורמליזציות שפורסמו, אך אין להסיק מכך שניתן להריץ את המודל או לשחזר את תהליך היצירה המלא.
דרגו את הכתבה
הדירוג עוזר לנו לדעת מה שווה לכם.
תגובות