מהו MathForm-8B? ההשקה השקטה של OpenBMB לאוטופורמליזציה הופכת מתמטיקה ל-Lean 4

openbmb/MathForm-8B הוא מודל אוטופורמליזציה חדש מבית OpenBMB, המתרגם הצהרות מתמטיות בשפה טבעית ל-Lean 4, והוא הושק כמעט ללא הודעה מוקדמת: המשקולות, מערך הנתונים והמאמר הופיעו כולם ב-Hugging Face וב-arXiv באותו יום, 2026-08-14, תחת הכותרת "MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement." ההשקה השקטה הזו מסתירה תוצאה יוצאת דופן — מודל עם 8B פרמטרים המדווח על ציוני Pass@8 ממוצעים של 88.06% בבדיקת תחביר ו-72.37% בבדיקת עקביות מחמירה יותר, על פני שישה מדדי השוואה, ולפי המאמר הוא מנצח כמה מודלי אוטופורמליזציה ייעודיים בגודל 32B. זהו מאמר "מה שאנחנו יודעים עד כה": כל מה שמסומן למטה כ"מהמאגר" מגיע ישירות מכרטיס המודל, מכרטיס מערך הנתונים ומהמאמר, וכל מה שעדיין לא אושר באופן בלתי תלוי מסומן ככזה.

נקודות עיקריות

• MathForm-8B הוא מודל אוטופורמליזציה בגודל 8B, ברישיון Apache-2.0: הוא קורא בעיית מתמטיקה בלתי פורמלית וכותב הצהרת משפט ב-Lean 4 עם כותרת בעלת שם, מוכן להוכחה מאוחר יותר.

• הוא תוצר של כוונון עדין של Qwen3-8B על FormalVerse, ערכת נתונים מאומתת של Lean 4 עם כ-367,000 דוגמאות, שבנתה OpenBMB באמצעות אחזור ידע ועידון שנבדק על ידי מהדר, ולאחר מכן אומן עם למידת חיזוקים תוך שימוש בהידור Lean ובמשוב עקביות סמנטית.

• מספרים מדווחים (מדווחי ספק, לא משוכפלים): 88.06% ממוצע Pass@8 תחת בדיקת תחביר, 72.37% תחת בדיקת עקביות, כשהם גוברים על אוטופורמליזרים ייעודיים בגודל 7B-32B בטבלת המאמר עצמו.

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

• הגשת המודל מתבצעת באירוח עצמי: Transformers, vLLM, או SGLang, כולם חושפים נקודת קצה תואמת OpenAI.

מה המהדורה מכילה בפועל

שלושה ארטיפקטים עלו תוך דקות זה מזה ב-2026-08-14, וזה איך שנראה שחרור מתואם אך לא מוכרז:

• מאגר המודל, openbmb/MathForm-8B — מודל שפה סיבתי בגודל 8B ב-BF16 עם תבנית צ'אט, ארבעה חלקי safetensors, רישיון Apache 2.0.

• מאגר הנתונים, openbmb/FormalVerse — מערך נתונים של פורמליזציה אוטומטית ב‑Lean 4, הכולל כ‑367,000 דוגמאות מאומתות, גם תחת רישיון Apache 2.0.

• המאמר, arXiv 2608.14221 — 25 עמודים המתארים את צינור בניית הנתונים, את מתכון ההכשרה, ואת ההערכה על ששת מדדי ההשוואה.

בזמן כתיבת שורות אלה, קישור הקוד של GitHub בקובץ ה-README הוא עדיין מציין מיקום, כך שצינור ההערכה וסקריפטי ה-Pass@k מובטחים אך טרם פורסמו. ה-README אכן מציין שבדיקות ההידור דורשות שרת Kimina Lean פעיל, ושהניסויים משתמשים ב-Lean 4.21.0.

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

מה MathForm-8B עושה — ולמה זו משימה מצומצמת

אוטופורמליזציה היא הצעד שלפני הוכחת משפטים: בהינתן בעיה מתמטית באנגלית פשוטה ("הראה שלכל מספר ממשי x, מתקיים x² ≥ 0"), על המודל לייצר ניסוח נכון פורמלית ב-Lean 4 — ייבואים, טיפוסים וכותרת משפט — שאותו יכול אדם או מוכיח לתקוף. זו מיומנות שונה במהותה מלעשות את המתמטיקה, משום שהמודל צריך למפות מושגי שפה טבעית אל ההיררכיה המדויקת של הגדרות וטיפוסים של Mathlib. ניסוח שעובר בדיקת טיפוסים אך מחליש בשקט את הניסוח המקורי ("(2^5) ∣ (13^4 − 11^4)" במקום טענת ההתחלקות המלאה) הוא מצב הכשל הקלאסי, וזו הסיבה שהמאמר מבחין בין בדיקת תחביר (האם הוא מהדר) לבין בדיקת עקביות (האם הוא אותה טענה מבחינה סמנטית).

כרטיס המודל מציג את דפוס השימוש המיועד: אתה נותן לו הנחיה עם הבעיה הבלתי פורמלית ושם משפט רצוי, והוא מחזיר הצהרת Lean 4 עם code>theorem my_favorite_theorem : ... := by sorry/code> — ה-code>sorry/code> משאיר את חובת ההוכחה פתוחה. חלוקת העבודה הזו חשובה: MathForm-8B הוא מפרמל, לא מוכיח. צוותים שבונים כלי Lean משתמשים בו כדי להמיר מאגרי בעיות לצורה הניתנת לבדיקה ממוחשבת.

איך זה אומן

המתכון של המאמר הוא דו-שלבי. ראשית, OpenBMB בנתה את FormalVerse עם צינור עיבוד ש-(1) מאחזר הגדרות רלוונטיות ופורמליזציות קיימות מ-Mathlib לפני היצירה, (2) מייצר הצהרות מועמדות, (3) משכלל אותן באמצעות אבחוני מהדר Lean ומשוב עקביות סמנטית, ו-(4) שומר רק דגימות שעוברות את שתי הבדיקות. הקורפוס המאומת הזה משמש לאחר מכן לכיוונון עדין מונחה, ואחריו למידת חיזוק עם אותות תגמול מהידור Lean ועקביות סמנטית.

כרטיס מערך הנתונים נותן טעם קונקרטי של הנתונים: כל רשומה מצמידה משפט בלתי פורמלי למשפט פורמלי מאומת, עם תגית מקור (למשל AceReason-Math) ותווית נושא (תורת המספרים, וכן הלאה). מכיוון שכל דוגמה עברה בדיקת מהדר אמיתית לפני שנכנסה לאימון, המודל לומד ממשפטים שידועים כתקינים ולא מהפלט הגולמי של מודל.

טבלת המדדים, המסומנת בכנות

כל המספרים בחלק זה מדווחים על ידי הספק מתוך המאמר (arXiv 2608.14221) ולא שוחזרו באופן בלתי תלוי. Pass@8 פירושו שהמודל מקבל שמונה ניסיונות לכל בעיה, והריצה נספרת אם לפחות אחד מהם מצליח; זהו מדד ידידותי יותר מ-pass@1 ויש לקרוא אותו כ"באיזו תדירות המודל יכול לייצר הצהרה נכונה בהינתן תקציב".

• ממוצעי MathForm-8B — בדיקת תחביר 88.06%, בדיקת עקביות 72.37%.

• לפי benchmark, SC ואז CC: FormalIMATH 100.00 / 95.06, ProverBench 100.00 / 94.83, CombiBench 93.00 / 47.00, FATE-M 99.33 / 97.33, FATE-H 82.00 / 63.00, FATE-X 54.00 / 37.00.

הסטים הקשים הם הכנים: FATE-H CC 63% ו-FATE-X CC 37% מראים את תקרת המודל על תת-הסטים הקשים ביותר, לעומת 95%+ CC על FormalIMATH ו-ProverBench הקלים יותר.

• קווי הבסיס הטובים ביותר של 8B שהמאמר מציג — ReForm-8B 81.76 / 66.21, Goedel-Formalizer-V2-8B 78.24 / 60.08 — וקווי הבסיס הטובים ביותר של 32B — ReForm-32B 81.61 / 68.41, Goedel-Formalizer-V2-32B 78.28 / 63.74, StepFun-Formalizer-32B 63.65 / 44.47 — כולם נופלים מ-MathForm-8B עם 88.06 / 72.37.

• נקודת הבידוק של SFT בלבד (לפני שלב ה-RL) מגיעה ל-84.38 / 66.53, כך שמעבר הלמידה עם חיזוק מוסיף בערך +3.7 SC ו-+5.8 CC בממוצע, כשהרווחים הגדולים ביותר הם בסטים הקשים.

הטענות החזקות ביותר שכדאי להטיל בהן ספק: ציוני ה-SC של 100.00 ב-FormalIMATH וב-ProverBench (100% קומפילציה בסטים הקלים היא דגל אדום לכך שסטים אלה התכנסו), וההשוואה מול מודלים של 32B שלא הורצו מחדש בתנאים זהים. מספרי בדיקת העקביות ב-FATE-H וב-FATE-X הם הנתונים שסביר להניח שישרדו בדיקות עצמאיות.

מה שלא אושר

• לא קיימת הערכה בלתי תלויה. נכון לכתיבת שורות אלה, אף צד שלישי לא הריץ את MathForm-8B במסגרת בדיקה פומבית, וקוד ההערכה טרם פורסם.

• אין הכרזת שירות. OpenBMB לא פרסמה בלוג השקה, דף תמחור או נקודת קצה API. המסגור "quietly shipped" הוא מילולי.

• משקלי התגמול של RL, תקציב האימון והחומרה אינם בכרטיס המודל; הם נמצאים רק במאמר.

• לא נבדק האם מודל ה-8B מכליל ל-Lean 4.21.1+ או לייבוא שאינו Mathlib.

איך להריץ את זה

אירוח עצמי הוא הדרך היחידה כיום. ה-README מתעד שלוש דרכים, כולן עם נקודת קצה צ'אט תואמת OpenAI ב-code>localhost:8000/v1/chat/completions/code>:

• טרנספורמרים — code>AutoModelForCausalLM.from_pretrained("openbmb/MathForm-8B", torch_dtype=torch.bfloat16)/code>, ולאחר מכן צור/י באמצעות תבנית הצ'אט.

• vLLM — code>vllm serve openbmb/MathForm-8B --served-model-name MathForm-8B --dtype bfloat16 --max-model-len 16384/code>.

• SGLang — code>python -m sglang.launch_server --model-path openbmb/MathForm-8B --served-model-name MathForm-8B --dtype bfloat16 --context-length 16384/code>.

ה-README ממליץ על temperature 0.6, top_p 0.95, ועד 16384 טוקנים חדשים — הצהרות פורמליות נוטות להיות ארוכות, כך שחלון היצירה הנדיב הוא דרישת המערכת האמיתית שיש לתקצב עבורה.

למה החלק של "8B מנצח את 32B" חשוב

אם המספרים יחזיקו מעמד, MathForm-8B הוא הטיעון החזק ביותר עד כה לכך שהצוואר בקבוק של האוטופורמליזציה הוא איכות הנתונים ואימות, לא מספר הפרמטרים הגולמי. הטבלה של המאמר עצמו מראה שמודלים מתמחים של 32B (ReForm-32B, Goedel-Formalizer-V2-32B, StepFun-Formalizer-32B) נמצאים מתחת למודל 8B שאומן על קורפוס שנבדק על ידי מהדר. לצוותים שמפעילים כיום פורמליזר 32B, זה שינוי עלות מהותי — מודל 8B ב-BF16 נכנס ל-GPU יחיד שרוב מודלי ה-32B לא נכנסים אליו, והוא משרת מהר יותר לכל טוקן.

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

מה לצפות בהמשך

שלושת הדברים שיהפכו את זה מ"מאגר מעניין" ל"כלי מהימן": קוד ההערכה של GitHub שיופיע בפועל; מעבר עצמאי ראשון על FATE-H ו-FATE-X תחת pass@1 במקום pass@8; וכל הכרזה של OpenBMB שמוסיפה מסלול מתארח או גרסת מאמר שנייה עם מספרי אבלציה. עד שלפחות אחד מאלה ינחת, התייחסו לציונים בכותרת כאל כיווניים — הארכיטקטורה ורעיון נתוני האימון הם החדשות העמידות, לא האחוז המדויק.