DeepSeek-Prover-V2-7B
קוד פתוחdeepseek-aiרישיון לא דווח2025-04-30
הוכחת משפטים פורמליים בשפת Lean 4 באמצעות שילוב של הסברים טקסטואליים וקוד מאומת. הוא מיועד למי שמחפש מודל קומפקטי יחסית שמתמקד בלוגיקה מתמטית מדויקת ולא בשיחה כללית.
- 6.9Bפרמטרים
- 65,536טוקנים בהקשר
- 12.9 GBמשקל הקבצים
- 97,229הורדות בחודש
מה זה
הבסיס כאן הוא מודל שתוכנן מראש לייצר הוכחות מתמטיות בשפת Lean 4. תהליך הבנייה שלו נשען על פירוק מטרות מורכבות לתת מטרות קטנות בעזרת המודל הענק של הסדרה, חיפוש פתרונות מקומי, ואימון עם חיזוקים שמבוסס על משוב בינארי של נכון או לא נכון מול שפת ההוכחה. המטרה היא לגשר על הפער שבין תכנון ההוכחה במלל חופשי לבין כתיבת הקוד הפורמלי שנבדק במחשב.
גרסת ה 7B נבנתה על בסיס DeepSeek-Prover-V1.5-Base, בניגוד לגרסת ה 671B שמבוססת ישירות על DeepSeek-V3-Base. בכרטיס המודל לא מפורסמות תוצאות מדידה מספריות ייעודיות עבור גרסת ה 7B עצמה, אלא רק הנתונים המרשימים של גרסת ה 671B שהשיגה 88.9 אחוז ב MiniF2F ופתרה 49 בעיות מתוך 658 ב PutnamBench. המשמעות היא שגרסת ה 7B משמשת בעיקר כמנוע חיפוש מקומי לתת מטרות, ולא בהכרח מחזיקה באותם אחוזי הצלחה בריצה ישירה מקצה לקצה על בעיות קשות.
מתאים ל
- השלמת צעדי הוכחה ב Lean
חיפוש טקטיקות וסגירת תת יעדים נקודתיים בתוך פרויקטים מתמטיים קיימים.
- אימון צנרת הוכחה מקומית
הרצה בלולאות חיפוש אינטנסיביות שדורשות אלפי דגימות בלי עלויות ענן.
- תרגום מתמטיקה לקוד פורמלי
הפיכת רעיונות הוכחה מופשטים להגדרות תואמות Lean 4 בצורה מובנית.
איפה זה נופל
הוא חסר תועלת כמעט לחלוטין מחוץ ל Lean 4. אל תנסו להשתמש בו לצ'אט, לכתיבת פייתון או לתשובות במתמטיקה מילולית רגילה. מעבר לזה, המפתחים מודים בעקיפין שבמשימות מורכבות מקצה לקצה מודל ה 7B מתקשה לפתור את הבעיה לבד, ולכן הם השתמשו בו רק לפתרון תת מטרות מפורקות. אם לא תבנו סביבו מערכת שמפרקת את הבעיה ובודקת את הפלט בתוך Lean, תקבלו שיעורי שגיאה גבוהים.
אותה משפחה
DeepSeek-Prover יצא ב־3 גרסאות שיש להן עמוד כאן. אלה האחרות, לפי כמה מורידים אותן.
שאלות
נפוצות
האם המודל הזה יודע לתכנת בשפות רגילות כמו פייתון או פייתון למדע נתונים?
לא. הוא אומן וכוונן באופן צר מאוד על הוכחות משפטים מתמטיים בשפת Lean 4. בשביל משימות קוד כלליות עדיף לקחת מודל קוד רגיל.
מה ההבדל בין גרסת ה 7B לגרסת ה 671B?
גרסת ה 7B מבוססת על V1.5-Base ונועדה במקור לתפקד כמנוע מהיר לסגירת תת יעדים, בזמן שגרסת ה 671B היא מודל ענק שמפרק בעיות ומחזיק בתוצאות המבחנים הגבוהות שפורסמו.
איך מריצים
כדי להריץ אותו צריך כרטיס מסך בודד עם 16GB זיכרון לפחות, כמו RTX 4090 או כרטיס שרת מקביל, משום שמשקל הקבצים עומד על 12.9GB בדיוק bfloat16. הקוד רץ ישירות דרך ספריית transformers הרגילה של Hugging Face עם הגדרת device_map אוטומטית.
אם כל מה שאתם צריכים זה לפתור בעיה מתמטית מבודדת פעם ביום, עדיף להשתמש ב API חיצוני של מודלים גדולים יותר. פריסה עצמאית של המודל הזה מתאימה רק אם אתם מריצים חיפוש איטרטיבי כבד שדורש אלפי קריאות מקומיות מול מהדר Lean 4 בלי לשלם על כל טוקן.
pip install -U huggingface_hub hf download deepseek-ai/DeepSeek-Prover-V2-7B
הקבצים
9 קבצים במאגר, 12.9 GB סך הכול. הקישורים מובילים ישירות ל־Hugging Face.
הרישיון
בכרטיס המודל לא דווח רישיון מוגדר, ויש רק הפניה להסכם רישיון מודל בלי פרטים מלאים במטא דאטה. המשמעות היא שאסור להניח שמותר להשתמש בו לצרכים מסחריים או לשלב אותו במוצר סגור לפני שבודקים את נוסח הרישיון המדויק מול המפתחים.