קלוד משחזר הוכחה פורמלית של משפט פרמה ב-11 ימים בלבד
אנתרופיק אומרת שמודל הבינה המלאכותית שלה קלוד השלים פרויקט פורמליזציה מתמטי שאפתני מאוד, ושחזר גרסה שניתן לבדוק אותה של משפט פרמה ב-11 ימים בלבד עם התערבות אנושית מוגבלת.
לפי הדיווחים, הפרויקט ייצר כ-13 מיליון שורות קוד בשפת התכנות לין וכמעט 29,500 תיאוריות ביניים. הנפח הזה הוא בערך פי חמישה מגודל מת'ליב, ספרייה פתוחה מרכזית המכילה מתמטיקה מאומתת פורמלית.
משפט פרמה הוצע לראשונה על ידי המתמטיקאי הצרפתי פייר דה פרמה במאה ה-17. הבעיה נותרה לא פתורה במשך יותר מ-300 שנה עד שהמתמטיקאי הבריטי אנדרו ויילס סוף סוף הקים הוכחה ב-1994, עם הגרסה הסופית שפורסמה ב-1995 לאחר שזוהה ותוקן פגם בטיעון המקורי.
פורמליזציה שונה מגילוי הוכחה מתמטית חדשה. היא כרוכה בתרגום טיעון מתמטי קיים לשפה מדויקת של מחשבים כך שעוזר הוכחות יכול לבדוק כל צעד לוגי ולאמת שההיגיון נובע מהאקסיומות הבסיסיות ומהתוצאות שהוקמו קודם לכן.
לפי החשבון של הפרויקט, המתמטיקאי קווין באזארד מהקולג' האימפריאלי בלונדון עבד מספר שנים על מאמצי הפורמליזציה, בעוד שקלוד השלים את המשימה ב-11 ימים. התוצאה תוכננה להסתמך אך ורק על אקסיומות מתמטיות והיגיון שהוקם פורמלית ולא על הנחות לא רשמיות.
המערכת האינטליגנטית דיווחה כי חילקה את העבודה בין מספר סוכנים שקיבלו הוראות רחבות במרווחים קבועים. כלי שנקרא Prove2Me, שפותח במקור כדי לסייע למתמטיקאים אנושיים, סייע לתאם חלקים מהתהליך.
ההישג מדגים את התפקיד הגדל של הבינה המלאכותית במתמטיקה פורמלית, שבה אפילו פער לוגי קטן יכול לפסול הוכחה מתוחכמת אחרת. אימות בעזרת מחשבים מציע דרך לבדוק שרשרות ארוכות של היגיון בצורה שיטתית ולזהות חוסר עקביות שעשוי להיות קשה להבחין בו באמצעות סקירה מתמטית קונבנציונלית.
מת'ליב, מאגר המרכזי שבו משתמשים המתמטיקאים העובדים עם לין, מכיל מיליוני שורות של מתמטיקה פורמלית וממשיך להתרחב ככל שחוקרים ממירים תוצאות שהוקמו לצורת בדיקה על ידי מחשבים.
אם התוצאה של קלוד תוכל להיות משוכפלת באופן עצמאי ולהוכיח את אמינותה, מערכות בינה מלאכותית יכולות להאיץ באופן משמעותי את הפורמליזציה של מתמטיקה מודרנית. כלים כאלה לא יחליפו בהכרח מתמטיקאים, אלא יכולים לסייע בהפיכת טיעונים מורכבים שפותחו על ידי בני אדם למבנים מדויקים שמחשבים יכולים לבדוק.
-
17:31
-
16:30
-
15:30
-
14:30
-
14:00
-
13:30
-
13:15
-
12:15
-
11:45
-
11:30
-
11:15
-
10:45
-
10:30
-
10:15
-
09:25
-
09:10
-
22:40
-
22:37
-
21:30
-
21:00
-
19:30
