דיפסיק הציגה את DeepSeek-Prover-V2, מודל שפה גדול (LLM) בקוד פתוח פורץ דרך שנבנה בקפידה עבור התחום המורכב של הוכחת משפטים פורמלית במסגרת Lean 4. מודל חדשני זה ממנף צינור הוכחת משפטים רקורסיבי, תוך רתימת העוצמה של מודל הבסיס DeepSeek-V3 המתקדם של DeepSeek. Lean 4, האיטרציה האחרונה של מוכיח המשפטים Lean, עומד כעוזר הוכחה אינטראקטיבי שפותח על ידי מיקרוסופט ריסרץ’. שפת תכנות פונקציונלית מתוחכמת זו ומערכת הוכחת משפטים אינטראקטיבית מעצימות מתמטיקאים ומדעני מחשב לבנות הוכחות פורמליות עם אימות מכונה ללא תחרות.
הפרויקט מסמל צעד מונומנטלי לקראת גישור הפער בין חשיבה מתמטית פורמלית ובלתי פורמלית. על ידי מינוף היכולות הטמונות של מודלי LLM למטרות כלליות, הוא מבקש לתת מענה יעיל לתחום המובנה מאוד של הוכחת משפטים פורמלית. צוות המחקר של DeepSeek משער שהגישה החדשנית שלהם משקפת את התהליכים הקוגניטיביים המועסקים על ידי מתמטיקאים אנושיים בעת בניית הוכחות, מנתחים בקפידה משפטים מורכבים לרכיבים ניתנים לניהול ומובנים יותר.
הרחבת מסגרת ההערכה: הצגת ProverBench
במהלך משמעותי להגברת קפדנות המחקר שלהם, צוות DeepSeek הרחיב משמעותית את מסגרת ההערכה שלהם עם הצגת ProverBench, אוסף מדדים חדש לגמרי שתוכנן בקפידה במיוחד להערכה מקיפה של יכולות הוכחת משפטים פורמלית. אוסף מקיף זה משמש משאב רב ערך להערכת הביצועים של מודלי LLM בהקשר של מתמטיקה פורמלית.
"מעבר למדדים המקובלים, אנו מציגים בגאווה את ProverBench, אוסף שנאסף בקפידה של 325 בעיות פורמליות, כדי להעשיר את תהליך ההערכה שלנו. אוסף זה כולל 15 בעיות שנבחרו בקפידה שמקורן ישירות מתחרויות הבחינה המתמטית האמריקאית המוזמנת האחרונה (AIME), במיוחד מהשנים 24-25", הסבירו החוקרים.
הכללת בעיות AIME במערך הנתונים ProverBench ראויה לציון במיוחד, שכן היא מציגה קבוצה של בעיות מתמטיות מאתגרות ומבוססות היטב המוכרות באופן נרחב בקהילה המתמטית. זה מספק בסיס סטנדרטי וקפדני להערכת הביצועים של DeepSeek-Prover-V2 ולהשוותו לגישות אחרות.
תוצאות התחלתיות מבטיחות: התמודדות עם בעיות AIME
התוצאות ההתחלתיות הנובעות מבדיקות קפדניות על בעיות AIME מאתגרות אלו גילו ביצועים מבטיחים במיוחד מהמודל המיוחד להוכחת משפטים שתוכנן בקפידה. צוות DeepSeek מדווח בגאווה ש-DeepSeek-Prover-V2 הדגים את יכולתו על ידי פתרון מוצלח של 6 בעיות AIME מרשימות מתוך 15 שהוצגו לו. לשם השוואה, מודל DeepSeek-V3 למטרות כלליות, כאשר הוא משתמש בטכניקות הצבעה ברוב, הצליח לפתור בהצלחה 8 בעיות.
ממצאים אלה מדגישים את הפוטנציאל של מודלי LLM מיוחדים וגם למטרות כלליות בהתמודדות עם בעיות מתמטיות מורכבות. בעוד שהמודל למטרות כלליות הציג שיעור הצלחה מעט גבוה יותר במדד ספציפי זה, מודל הוכחת המשפטים המיוחד הדגים את מיומנותו בחשיבה מתמטית פורמלית.
חיקוי בניית הוכחה אנושית: גישת שרשרת מחשבות
"בהתחשב באתגרים המתועדים היטב שמודלים למטרות כלליות נתקלים בהם לעתים קרובות כאשר הם מנסים להפיק הוכחות Lean שלמות, הדרכנו באופן אסטרטגי את DeepSeek-V3 ליצור רק שרטוט הוכחה ברמה גבוהה, תוך השמטת הפרטים המורכבים בכוונה. שרשרת המחשבות המתקבלת מגיעה לשיאה במשפט Lean המורכב מסדרה של הצהרות, שכל אחת מהן הסתיימה בקפידה עם מציין מיקום מצטער, המציין למעשה מטרה משנית שיש לפתור. גישה חדשנית זו משקפת באלגנטיות את הסגנון האנושי של בניית הוכחות, שבה משפט מורכב מצטמצם בהדרגה לרצף של למות ניתנות לניהול יותר", הסביר צוות DeepSeek.
גישה חדשנית זו של יצירת שרטוטי הוכחה ברמה גבוהה מתיישרת עם האופן שבו מתמטיקאים ניגשים לעתים קרובות להוכחות מורכבות. על ידי התמקדות במבנה הכללי ובשלבי המפתח, המודל יכול להנחות ביעילות את העידון וההשלמה הבאים של ההוכחה.
אסטרטגיה מתודולוגית: טיפול בכל מרכיב הוכחה בנפרד
לאחר מכן המערכת מעסיקה בקפידה אסטרטגיה מתודולוגית ומובנית לטיפול בכל מרכיב בודד של ההוכחה. גישה שיטתית זו מבטיחה שכל היבט של ההוכחה נשקל בקפידה ומטופל בצורה הגיונית ועקבית. המערכת יוצרת גישה מובנית מאוד להוכחת משפטים, תוך הסתמכות על תוצאות שנקבעו בעבר כדי להבטיח בסיס איתן לכל צעד עוקב.
"תוך מינוף המטרות המשניות שנוצרו על ידי DeepSeek-V3, אנו מאמצים אסטרטגיית פתרון רקורסיבית כדי לפתור באופן שיטתי כל שלב הוכחה ביניים. אנו מחלצים ביטויי מטרה משנית מהצהרות שיש להחליף אותם במטרות המקוריות בבעיות הנתונות ולאחר מכן לשלב את המטרות המשניות הקודמות כהנחות. מבנה זה מאפשר לפתור מטרות משניות עוקבות באמצעות תוצאות הביניים של שלבים מוקדמים יותר, ובכך לקדם מבנה תלות מקומית יותר ולהקל על פיתוח למות פשוטות יותר", פירטו החוקרים.
אסטרטגיית הפתרון הרקורסיבית היא היבט מרכזי ביכולת של המערכת להתמודד עם הוכחות מורכבות. על ידי פירוט הבעיה למטרות משניות קטנות וניהוליות יותר, המערכת יכולה ליישם ביעילות את יכולות החשיבה שלה על כל רכיב בודד.
אופטימיזציה של משאבי מחשוב: מודל 7B פרמטרים מיוחד
כדי לייעל ביעילות את משאבי המחשוב ולהבטיח עיבוד יעיל, המערכת מעסיקה באופן אסטרטגי מודל 7B פרמטרים קטן יותר ומיוחד מאוד לעיבוד הלמות המפורקות. גישה זו חיונית לניהול יעיל של דרישות המחשוב הכרוכות בחיפושי הוכחה נרחבים, ומבטיחה שהמערכת תוכל לפעול ביעילות מבלי להיות מוצפת מהמורכבות של מרחב החיפוש. הגישה מגיעה בסופו של דבר להוכחה שלמה שמקורה אוטומטית כאשר כל השלבים המפורקים נפתרים בהצלחה.
"מסגרת האלגוריתמית פועלת בשני שלבים נפרדים, תוך מינוף שני מודלים משלימים: DeepSeek-V3 לפירוק Lemma ומודל מוכיח 7B להשלמת פרטי ההוכחה הפורמלית המתאימים", תיארו החוקרים.
גישה דו-שלבית זו מאפשרת למערכת למנף את החוזקות של מודל גדול למטרות כלליות ומודל מתמחה קטן יותר. המודל הגדול משמש להפקת שרטוטי הוכחה ברמה גבוהה, בעוד שהמודל הקטן יותר משמש למילוי הפרטים ולהשלמת ההוכחה הפורמלית.
סינתזה של נתוני חשיבה פורמלית: מסלול טבעי
ארכיטקטורה זו מעוצבת בקפידה מבססת למעשה מסלול טבעי ואינטואיטיבי לסינתזה של נתוני חשיבה פורמליים, תוך מיזוג חלק של חשיבה מתמטית ברמה גבוהה עם הדרישות המחמירות והקפדניות של אימות פורמלי. שילוב זה חיוני להבטחת האמינות והמהימנות של תוצאות המערכת.
"אנו אוצרים תת-קבוצה של בעיות מאתגרות שנותרו בלתי פתורות על ידי מודל המוכיח 7B מקצה לקצה, אך שעבורן כל מטרות המשנה המפורקות נפתרו בהצלחה. על ידי הרכבת ההוכחות של כל מטרות המשנה, אנו בונים הוכחה פורמלית שלמה לבעיה המקורית", הסבירו החוקרים.
גישה זו מאפשרת למערכת ללמוד מטעויותיה ולשפר את יכולתה לפתור בעיות מורכבות. על ידי זיהוי מטרות המשנה הספציפיות שגורמות לקשיים, המערכת יכולה למקד את מאמציה בשיפור הביצועים שלה בתחומים אלה.
חששות ואתגרים: פרטי יישום תחת בדיקה
למרות ההישגים הטכניים הבלתי ניתנים לערעור שהודגמו על ידי DeepSeek-Prover-V2, כמה מומחים בתחום העלו חששות רלוונטיים לגבי פרטי יישום מסוימים. אליוט גלזר, מתמטיקאי מוביל נערץ מאוד ב-Epoch AI, הצביע על בעיות פוטנציאליות המצדיקות חקירה נוספת.
כמה חששות לגבי מאמר DeepSeek-Prover-V2. דוגמאות שגויות פוטנציאליות, ודיון על ה-Lean zulip מצביע על כך שהוכחות ה-PutnamBench הן שטויות ומשתמשות במצטער מרומז (אולי מוסתר בטקטיקה apply?) שלא דווחו בלולאת הקריאה-הערכה-הדפסה שלהם.
חששות אלה ממחישים בבירור את האתגרים המתמשכים הטמונים בחלל האימות הפורמלי, שבו אפילו פרטי היישום הקטנים והכאורה חסרי המשמעות ביותר יכולים להפעיל השפעה גדולה באופן לא פרופורציונלי על התוקף והאמינות הכוללים של התוצאות. תהליך האימות הפורמלי דורש תשומת לב בלתי מעורערת לפרטים והקפדה קפדנית על סטנדרטים מבוססים.
הפוטנציאל לדוגמאות שגויות והאפשרות לטקטיקות "מצטערות" נסתרות בהוכחות PutnamBench מעלים שאלות חשובות לגבי הקפדנות והשלמות של תהליך האימות. חששות אלה מדגישים את הצורך בבדיקה מתמשכת ואימות עצמאי של התוצאות.
זמינות ומשאבים: דמוקרטיזציה של גישה להוכחת משפטים פורמלית
DeepSeek הפכה את Prover-V2 שלה לזמינה בשני גדלי מודל שונים, העונים על מגוון רחב של משאבי מחשוב ומטרות מחקר. הגרסה הראשונה היא מודל 7B פרמטרים שנבנה על Prover-V1.5-Base הקודם שלהם, הכולל אורך הקשר מורחב של עד 32K אסימונים. הגרסה השנייה היא מודל 671B פרמטרים גדול משמעותית שאומן על DeepSeek-V3-Base. שני המודלים נגישים כעת בקלות ב-HuggingFace, פלטפורמה מובילה לשיתוף ושיתוף פעולה במודלים של למידת מכונה.
בנוסף למודלים עצמם, DeepSeek גם הפכה את מערך הנתונים המלא של ProverBench, המכיל 325 בעיות פורמליות בקפידה למטרות הערכה, לזמין ב-HuggingFace. מערך נתונים מקיף זה מספק לחוקרים ומפתחים משאב רב ערך להערכת הביצועים של המודלים שלהם ולהשוואתם ל-DeepSeek-Prover-V2.
על ידי הפיכת משאבים אלה לזמינים בחינם, DeepSeek מבצעת דמוקרטיזציה של הגישה לטכנולוגיית הוכחת משפטים פורמלית ומטפחת שיתוף פעולה בתוך קהילת המחקר. גישת קוד פתוח זו עשויה להאיץ את ההתקדמות בתחום ולהוביל לפריצת דרך חדשה בחשיבה אוטומטית ואימות.
מהדורה זו מעצימה חוקרים ומפתחים עם המשאבים הדרושים כדי להתעמק ביכולות ובמגבלות של טכנולוגיה זו. על ידי מתן גישה פתוחה למודלים ולמערך הנתונים ProverBench, DeepSeek מעודדת חקירה נוספת ומאמצים שיתופיים להתייחס לחששות שהועלו על ידי מומחים בתחום. גישה שיתופית זו מחזיקה במפתח לפענוח המורכבויות של הוכחת משפטים פורמלית ולגיבוש המהימנות של ההתקדמות פורצת הדרך הזו.