GPT
הוספת כלי
Q

QED-Nano

קוד פתוח

lm-proversapache-2.02026-02-12

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

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

  • 4Bפרמטרים
  • 262,144טוקנים בהקשר
  • 7.5 GBמשקל הקבצים
  • 3,487הורדות בחודש

מה זה

הבסיס כאן הוא Qwen3-4B-Thinking-2507, אבל עבר כוונון עמוק שכלל supervised fine-tuning ולמידת חיזוק עם זיכרון חישובי מובנה, על גבי מאגר FineProofs-RL שמכיל 5,227 שאלות מתמטיקה תחרותית. המטרה הבלעדית שלו היא לפתור ולכתוב הוכחות פורמליות ומורכבות ברמת אולימפיאדה.

במבחן IMO-ProofBench הוא מגיע לציון של 40%, בדיוק כפול ממודל הבסיס שממנו הוא נבנה, ותוצאה שמשתווה לביצועים של GPT-OSS-120B. כשמריצים אותו במבנה סוכן שמשקיע מעל מיליון טוקנים בפתרון בעיה אחת, הציון קופץ ל־54%, קרוב לביצועים של Gemini 3 Pro שמוביל את הטבלה עם 58.7%. זה מראה שאפשר לסחוט חשיבה עמוקה גם ממשקל קל, אם מכוונים את תהליך ההסקה נכון.

מתאים ל

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

    הוא מיועד לכתיבת הוכחות מתמטיות שלמות ברמה תחרותית ומגיע ל־40% הצלחה ב־IMO-ProofBench.

  • מחקר באופטימיזציית הסקה

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

  • אימות טענות מתמטיות

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

איפה זה נופל

זה כלי צר מאוד. היוצרים מצהירים במפורש שהוא נועד להוכחת משפטים מתמטיים בלבד, ושכל ניסיון להשתמש בו כעוזר כללי יוביל להזיות ולתשובות חסרות משמעות. מעבר לזה, המודל אומן ותומך רשמית באנגלית בלבד, כך שאין מה לבנות עליו לניתוח טקסטים בעברית. גם במתמטיקה עצמה התוצאות שלו אינן חפות מטעויות ודורשות בדיקה אנושית, כפי שמעיד ציון של 67.5% בלבד ב־IMO-AnswerBench.

שאלות
נפוצות

האם אפשר להשתמש במודל הזה כעוזר פיתוח או צ'אט כללי?

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

כמה משאבים דרושים כדי להגיע לביצועים הדומים ל־Gemini 3 Pro?

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

איך מריצים

המשקל הכולל עומד על 7.5 גיגה בייט בדיוק bfloat16, מה שאומר שהוא נכנס בקלות לכרטיס מסך בודד עם 16 גיגה זיכרון, כמו כרטיס ביתי חזק. כדי להרים אותו משתמשים ישירות בספריות כמו vLLM או SGLang לפריסה מקומית בתאימות מלאה לממשק של OpenAI, כשהיוצרים ממליצים על temperature=0.6 ו־top_p=0.95.

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

from transformers import pipeline

pipe = pipeline("text-generation", model="lm-provers/QED-Nano")
print(pipe("שלום"))

הקבצים

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

הרישיון

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

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

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