GPT
הוספת כלי
G

Goedel-Prover-V2-32B

קוד פתוח

Goedel-LMapache-2.02025-07-14

  • transformers
  • safetensors
  • qwen3
  • text-generation
  • conversational

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

  • 33Bפרמטרים
  • 40,960טוקנים בהקשר
  • 61.0 GBמשקל הקבצים
  • 46,423הורדות בחודש

מה זה

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

התוצאות במבחנים מסבירות את העניין סביבו. במבחן MiniF2F הוא מגיע ל־90.4% הצלחה במצב תיקון עצמי, ובמבחן PutnamBench הוא פתר 86 בעיות ב־192 ניסיונות, כשהוא עוקף מודל כמו DeepSeek-Prover-V2-671B שפתר 47 בעיות באלף ניסיונות. המשמעות בפועל היא לא רק דיוק גבוה יותר, אלא חיסכון עצום בזמן ריצה ובמשאבי חישוב כשמחפשים הוכחה עובדת.

מתאים ל

  • הוכחת משפטים ב־Lean 4

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

  • פתרון בעיות אולימפיאדה

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

  • אימות קוד ומתמטיקה

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

איפה זה נופל

זה לא מודל שיחה כללי, הוא לא יודע לענות על שאלות תכנות רגילות, והוא לא מבין עברית. הוא מייצר פלט ספציפי מאוד של קוד Lean 4 עם תוכנית הוכחה מקדימה, וכל שימוש מחוץ למתמטיקה פורמלית פשוט ייכשל. מעבר לזה, הביצועים הגבוהים שנמדדו תלויים לחלוטין ביכולת שלכם לדגום ממנו עשרות ניסיונות שונים (Pass@32 ומעלה) ולחבר אותו לקומפיילר אמיתי שמחזיר לו שגיאות, בלי המעטפת הזו אחוזי ההצלחה יורדים משמעותית.

שאלות
נפוצות

האם המודל יודע לפתור בעיות שנכתבו בשפה חופשית?

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

כמה זמן לוקח לו לייצר הוכחה?

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

איך מריצים

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

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

from transformers import pipeline

pipe = pipeline("text-generation", model="Goedel-LM/Goedel-Prover-V2-32B")
print(pipe("שלום"))

הקבצים

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

הרישיון

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

  • שימוש מסחרי
  • שינוי הקוד
  • הפצה מחדש
  • שימוש בפטנטים

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