GPT
הוספת כלי
D

DeepSeek-Prover-V2-671B

קוד פתוח

deepseek-aiרישיון לא דווח2025-04-30

  • transformers
  • safetensors
  • deepseek_v3
  • text-generation
  • conversational

זה מודל ענק שנועד ספציפית להוכחת משפטים מתמטיים בשפת Lean 4. תרצו אותו אם אתם מחפשים אוטומציה של הוכחות ברמה אקדמית ותחרותית גבוהה במיוחד.

  • 685Bפרמטרים
  • 163,840טוקנים בהקשר
  • 641 GBמשקל הקבצים
  • 774הורדות בחודש

מה זה

הוא מבוסס על הארכיטקטורה של DeepSeek-V3 ומכיל 685 מיליארד פרמטרים, אבל אומן למטרה אחת ברורה: לקחת ניסוח מתמטי ולייצר לו הוכחה פורמלית מלאה ב־Lean 4. תהליך האימון שלו שילב פירוק תתי מטרות בעזרת DeepSeek-V3, פתרון שלהן במודל 7B קטן יותר, ואז אימון בחיזוקים עם משוב בינארי של נכון או לא נכון.

התוצאה של התהליך הזה היא יכולת ייחודית לחבר בין הסבר אינטואיטיבי בטקסט חופשי לקוד הוכחה קפדני. במבחן MiniF2F-test הוא הגיע לשיעור הצלחה של 88.9 אחוזים, וב־PutnamBench הוא פתר 49 מתוך 658 בעיות, מספרים שמעמידים אותו בשורה הראשונה של הוכחת משפטים נוירונית בעולם.

מתאים ל

  • אימות הוכחות ב־Lean 4

    יצירת קוד פורמלי מלא למשפטים מורכבים ב־Lean 4 תוך שילוב הסבר שלבי ההוכחה.

  • פתרון בעיות תחרותיות

    התמודדות עם שאלות אלגברה ותורת המספרים ברמת תחרויות AIME ומבחני מתמטיקה אקדמיים.

  • מחקר בהוכחת משפטים נוירונית

    שימוש כבסיס השוואה או ככלי עבודה במעבדות שחוקרות שילוב בין מודלי שפה למערכות הוכחה.

איפה זה נופל

הוא לא מיועד לשיחה רגילה, כתיבת קוד כללי או מענה על שאלות יומיומיות. כל הכוח שלו ממוקד ב־Lean 4, וגם שם הוא פתר רק 49 מתוך 658 בעיות ב־PutnamBench, מה שמראה שמתמטיקה ברמה אולימפית עדיין מפילה אותו לעיתים קרובות. בנוסף, חלון ההקשר העצום של 163,840 טוקנים וזמני הריצה הארוכים דורשים משאבים שקשה להצדיק במערכות ייצור רגילות.

אותה משפחה

DeepSeek-Prover יצא ב־3 גרסאות שיש להן עמוד כאן. אלה האחרות, לפי כמה מורידים אותן.

DeepSeek-Prover-V2-7B97,229 DeepSeek-Prover-V1.5-RL738

שאלות
נפוצות

אפשר להשתמש בו כעוזר פיתוח רגיל לקוד פייתון או ווב?

לא. למרות שהוא מבוסס על DeepSeek-V3, המודל הזה כוונן ספציפית למתמטיקה פורמלית ב־Lean 4. למשימות פיתוח כלליות עדיף להשתמש במודלי קוד ייעודיים.

מה ההבדל בינו לבין גרסת ה־7B של אותו מודל?

גרסת ה־671B מציגה יכולות פירוק והוכחה עמוקות בהרבה על בעיות קשות כמו אלו שב־PutnamBench. עם זאת, גרסת ה־7B שוקלת שבריר ממנו ויכולה לרוץ על כרטיס גרפי יחיד.

איך מריצים

כדי להריץ אותו מקומית צריך מערך חומרה רציני מאוד. מדובר על 641 גיגה בייט של משקלים בפורמט bfloat16 שמתפרסים על 172 קבצים, כך שתצטרכו אשכול של מספר כרטיסי H100 או A100 עם מאות גיגה בייט של זיכרון גרפי רק כדי לטעון אותו לזיכרון באמצעות ספריית transformers.

אם אין לכם תשתית כזאת, עדיף להשתמש בגרסת ה־7B הקטנה יותר שפורסמה במקביל, או לחכות לשירותי ענן שיציעו גישה אליו דרך API. ריצה מקומית של מפלצת כזו שווה את המאמץ רק אם אתם עוסקים במחקר מתמטי מתקדם שדורש פרטיות מלאה או שאתם מריצים אצוות הוכחה כבדות.

from transformers import pipeline

pipe = pipeline("text-generation", model="deepseek-ai/DeepSeek-Prover-V2-671B")
print(pipe("שלום"))

הקבצים

172 קבצים במאגר, 641 GB סך הכול. הקישורים מובילים ישירות ל־Hugging Face.

הרישיון

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

הרישיון המלא בעמוד המודל ↗