Leanstral-2603

קוד פתוח

mistralaiapache-2.02026-03-11

vllm

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

113 GBמשקל הקבצים
68הורדות בחודש
168לייקים

מה זה

מדובר בארכיטקטורת תערובת מומחים עם 119 מיליארד פרמטרים בסך הכול, כאשר רק 6.5 מיליארד פעילים בכל טוקן דרך 4 מומחים מתוך 128. המבנה הזה נותן מהירות תגובה של מודל קטן עם קיבולת ידע של מודל ענק. חוץ מקוד, יש לו יכולת לקבל תמונות כקלט ולהחזיר טקסט, וחלון הקשר שנמתח עד 256 אלף טוקנים, אם כי המפתחים ממליצים להישאר באזור ה־200 אלף.

הייחוד האמיתי שלו הוא ההתמקדות המוחלטת ב־Lean 4 ובאימות הוכחות, תחום שבו רוב המודלים הכלליים פשוט ממציאים סינטקס שגוי. הוא תומך בהפעלת כלים חיצוניים דרך Mistral Vibe, מקפיד על הנחיות מערכת, ותומך ב־11 שפות שונות, ביניהן אנגלית, ערבית, צרפתית וספרדית.

מתאים ל

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

איפה זה נופל

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

שאלות
נפוצות

האם המודל יפעל טוב על כרטיס מסך ביתי אחד?

לא. גודל הקבצים מגיע ל־113 ג'יגה בייט וההרצה המומלצת דורשת פיצול על פני ארבעה מאיצים גרפיים. מומלץ לגשת אליו דרך ה־API אם אין לכם שרת ייעודי.

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

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

האם יש תמיכה בעבודה עם תמונות?

כן. למרות ההתמקדות בקוד ובמתמטיקה, הוא תומך בקלט מולטימודלי של טקסט ותמונה ומחזיר פלט טקסטואלי.

איך מריצים

המשקל הכולל של הקבצים עומד על 113 ג'יגה בייט, כך שאי אפשר להריץ אותו על חומרה ביתית רגילה. פריסה מקומית מומלצת דרך ספריית vLLM בגרסת nightly ודורשת שרת ייעודי, כאשר ההגדרה הרשמית משתמשת בחלוקה לארבעה כרטיסי מסך במקביל עם מנגנון FLASH_ATTN_MLA.

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

pip install -U huggingface_hub
hf download mistralai/Leanstral-2603

הקבצים

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

הרישיון

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

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

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