הוכחת ה-Lean של OpenAI עבור Navier-Stokes לא תואמת את גרסת השפה הטבעית, טוענים מתמטיקאים

אי-התאמה בין שתי הוכחות

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

כעת קבוצת מתמטיקאים טוענת ששתי הגרסאות הללו אינן תואמות זו לזו. אנדרס האנסן מאוניברסיטת קיימברידג' ופביאן קירשל, יחד עם אלכסנדר באסטון מ-King's College לונדון, טוענים שהמודל של OpenAI תרגם לא נכון חלק מההוכחה בעת המרתו ל-Lean. החוקרים מדגישים שהדבר לא אומר שההוכחות שגויות או ש-OpenAI לא פתרה את הבעיה, אך מעלה חשד לשאלה אם ניתן להסתמך תמיד על תוצאות מתמטיות שנוצרות על ידי AI.

הלמה המחולשת

הטענה של הקבוצה נוגעת לחלק מההוכחה שנקרא למה 8.6. בהוכחה הכתובה בשפה טבעית, הגבלה זו דורשת שערך מסוים יהיה קטן מ-m + 4, כאשר m הוא מספר שלם. בהוכחת ה-Lean, הערך השקול חייב להיות קטן מ-m + 5, מה שחלש מתמטית יותר. שתי הטענות עשויות להיות נכונות, אך הן אומרות דברים שונים וגרסת ה-Lean מציעה תשובה אפשרית רחבה יותר.

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

נטל האימות של הוכחות AI

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

הבעיה רלוונטית במיוחד כיוון ש-OpenAI פרסמה קבוצה של 722 עבודות מתמטיות, מתוכן רק חלק כולל הוכחות ב-Lean שלא נבדקו ידנית. קווין באזארד מ-Imperial College לונדון אמר שהוא בטוח שבעיית Navier-Stokes נפתרה נכונה, אך בטוח הרבה פחות שההוכחה המתוארת ב-PDF נכונה. האנסן אמר שנדרש עוד עבודה על פיתוח טכניקות אוטופורמליזציה יציבות ושהדרך הסופית לכך שגרה לחלוטין.

מקורות: newscientist.com