AlphaProof Code לעומת MathForm-8B: שני שלבים באותו פייפליין Lean, ולא שני יריבים

קראו היטב את מאמר AlphaProof Code ומספר בולט לעין שההכרזה אינה מדגישה: מבין ארבעת השבועות שחמשת החוקרים של DeepMind הקדישו לאימות Signal, החלק שלא ניתן היה לבצע באופן אוטומטי היה השלב הקדמי. מומחים אנושיים עבדו עם שילוב של מודלים כדי לתרגם את מטרות האבטחה של Signal למפרטים פורמליים ב-Lean, ומומחה סקר כל אחד ואחד מהם לפני שהחלה עבודת הוכחה כלשהי. זהו צוואר הבקבוק. MathForm-8B, מודל האוטופורמליזציה בעל 8 מיליארד פרמטרים של OpenBMB, ששוחרר ב-Hugging Face ב-14 באוגוסט 2026, הוא ניסיון ישיר לבצע אוטומטית בדיוק את השלב הזה — לקבל הצהרה מתמטית בשפה טבעית ולפלוט הצהרת משפט ב-Lean 4 המוכנה לכך שמישהו אחר יוכיח אותה. העמידו אותם זה לצד זה ואינכם משווים שני מוצרים. אתם מביטים בשני שלבים עוקבים של צינור עיבוד אחד, שמפריד ביניהם ההבדל בין מתמטיקה לאבטחת פרוטוקולים.

הצינור, לפי הסדר שבו העבודה מתרחשת

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

MathForm-8B מבצע משימה אחת, עבור מחלקת קלט צרה: טענות מתמטיות בסגנון ספר לימוד. תנו לו "לכל מספר ממשי x, x² אינו שלילי" והוא מחזיר את הייבוא, את הטיפוסים ואת כותרת המשפט ב-Lean 4. מה שהוא אינו מחזיר הוא הוכחה, ומחבריו מצהירים במפורש שחיפוש הוכחה הוא הבעיה של מישהו אחר. המספרים המדווחים שלו, כולם מדווחים על ידי הספק ולא משוחזרים, הם 88.06% בממוצע Pass@8 בבדיקת תחביר ו-72.37% תחת בדיקת העקביות המחמירה יותר על פני שישה מבחנים — הפער בין שני הנתונים הללו הוא המדד הכנה לשאלה באיזו תדירות הצהרה תקינה תחבירית אומרת משהו שונה ממה שהתבקש.

AlphaProof Code מבצע את המשימות השנייה והשלישית, ובנוסף שלב מפרט ש-MathForm-8B לא היה מסוגל לגעת בו. יעדי האבטחה של Signal אינם טענות מתמטיות במובן שבו אומן MathForm; הם הצהרות על פרוטוקול — שהודעות נשארות מוגנות לפני ואחרי שמכשיר נפרץ זמנית, שהיוזם והמגיב הם מי שהם טוענים שהם. הפיכתם ל-Lean דרשה מומחיות בפרוטוקולים שאין לאף אוטומפורמלייזר 8B. לאחר שהמפרט היה קיים, עבודת ההוכחה הועברה כולה לסוכנים, והבדיקה הועברה לגרעין של Lean ובנוסף לסוכן שומר סף המשתמש באמצעות משווה מול עותק מפרט שנשמר בנפרד.

מה העלות האמיתית של השימוש בכל אחד מהם עבורך

• משקלים — MathForm-8B: ניתנים להורדה, Apache 2.0, ארבעה שברי safetensors ב־BF16, מכווננים עדין מ־Qwen3-8B. AlphaProof Code: אין. המהדורה היא פיתוח Lean, סמנטיקה של AArch64 ו־binding ל־libsignal בכתובת github.com/google-deepmind/code-verification.

• הרצה שלו — MathForm-8B: Transformers, vLLM או SGLang, כולם חושפים נקודת קצה תואמת OpenAI, על חומרה שבבעלותך. AlphaProof Code: ללא נקודת קצה, ללא API, ללא רשימת המתנה, ללא מחיר; זוהי מסגרת מחקר ש-DeepMind אומרת שזקוקה ל"מחקר מתמשך" לפני שתתרחב.

• קלט — MathForm-8B: הצהרה מתמטית בשפה טבעית. AlphaProof Code: מפרט פורמלי בתוספת הבינארי שברצונך להוכיח כנגדו.

• פלט — MathForm-8B: הצהרת משפט ב-Lean 4, לא מוכחת. AlphaProof Code: הוכחה שנבדקה במכונה, או הפרכה כאשר הקוד שבור.

• סקירה אנושית — MathForm-8B: אתם סוקרים את ההצהרה שנפלטה, וברמת עקביות של 72.37% תסקרו רבים מהן. AlphaProof Code: מומחים סוקרים כל מפרט לפני שעבודת ההוכחה מתחילה, ואז סוכנים מסמנים כ-1% מבסיס הקוד לבדיקה שנייה.

• מגבלות ידועות — MathForm-8B: הצהרות מתמטיות בלבד, ללא יצירת הוכחות, ומאגר הקוד המקושר ב-README שלו עדיין היה מציין מקום בעת השחרור. AlphaProof Code: ללא הבטחה פוסט-קוונטית לריפוי SPQR, ללא פרטיות מטען, סשן אחד לכל קידום, וחסם זיוף MAC שהופך חסר משמעות בסמוך ל-25,000 הודעות בסשן יחיד.

הפער ש-MathForm-8B יצטרך לסגור

מפתה לומר שמערכת אוטומטית לפורמליזציה הייתה יכולה לכתוב את המפרטים של Signal ולחסוך לחוקרים את השבועות האינטנסיביים בתחילת הדרך. אך התיאור של המאמר עצמו אומר אחרת, והסיבה ספציפית. מפרט של פרוטוקול אינו ניסוח מחדש של טענה; הוא בחירה של מודל יריב. עבודת Signal כוללת מסלול סימבולי בדולב–יאו עם תוקף קוונטי ששובר את Diffie–Hellman לאחר לחיצת היד, ומסלול חישובי עם יריבים קלאסיים וחסם קונקרטי. שני המסלולים הללו מציגים משפטים שונים על אותו קוד, והבחירה ביניהם היא החלטה הנדסית עם השלכות אבטחה. שום מודל שאומן להפוך את „הראה ש-x² ≥ 0” ל-Lean לא יקבל את ההחלטה הזאת.

מה שאוטופורמלייזר יכול לעשות באופן סביר הוא החלק המכני של העבודה הזו: בהינתן מטרת אבטחה בפרוזה וספרייה של הגדרות Lean קיימות, להפיק טיוטה ראשונה של ההצהרה באידיום של הפרויקט עצמו, כדי שמומחה יתקן אותה. זהו חיסכון אמיתי, וקטן בהרבה ממה שהכותרת מרמזת. המאמר מדווח על קטלוג סטיות מפרט של יותר מ-200 ערכים חישוביים וכ-35 סמליים — חמישה-עשר מהם פערים או באגים בניתוח Double Ratchet — וזה מה ששלב הביקורת האנושית מצא. מודל שמנסח הצהרות יצטרך להימדד מול הקטלוג הזה, ולא מול ציון Pass@8 במבחני מתמטיקה.

כאשר שני המספרים אינם ברי השוואה כלל

88.06% של MathForm-8B ו-6.5 מיליון השורות של AlphaProof Code מודדים דברים שונים ולעולם אין להציב אותם באותה עמודה. האחד הוא שיעור הצלחות בחבילת בנצ'מרק שהמחברים בנו; האחר הוא כמות הוכחות שהופקה עבור יעד אחד. הספק גלוי לב ש-88.06% משתמשים בבדיקת תחביר, שהיא קריטריון חלש — הצהרה יכולה להתקמפל ועדיין לנסח את הטענה השגויה, ולכן נתון העקביות נמוך ב-16 נקודות.

הדוגמה של AlphaProof Code בעלת נופך דומה היא עבודת האימות: שני באגים ב-Signal שתוקנו בעבר — באג של מצב חלש ובאג של תת-קבוצה קטנה — הוחזרו לתוך עותק מבודד, ובשני המקרים המערכת הפיקה הוכחה מאומתת במכונה לכך שהגרסה הבאגית נכשלת במשפט האבטחה. זהו מבחן שלילי, ומבחן שלילי הוא בדיוק מה שחסר לחלוטין לבנצ'מרק של אוטופורמליזר. MathForm-8B אינו מדווח על תוצאה מהצורה "בהינתן הצהרה שגויה במכוון, המודל אמר כך".

איך בעצם היית משתמש בהם יחד

באופן קונקרטי, וזהו החלק היחיד בהשוואה שיש לו מסלול לטווח הקרוב: השתמשו ב-autoformalizer כדי לנסח טיוטה, במודל כללי חזק כדי לבקר את הטיוטה, ובסוכן הוכחה כדי לנסות להוכיח את ההוכחה. לכל שלב יש אופן כשל שונה, וניתוב כל השלושה דרך מפתח אחד הוא הנוחות המעשית. ב-OrcaRouter, יותר מ-200 מודלים נמצאים מאחורי API יחיד במחיר המחירון של הספק עם 0% תוספת, כך שלולאת ניסוח מפרט ששולחת את אותה הצהרה לשני מודלים ומשווה את ה-Lean שלהן היא קריאת routing-DSL ולא שלושה חוזים ושלושה SDKs. מעבר אוטומטי לכשל מכסה את המקרה שבו המודל שבחרתם חווה אחר צהריים רע.

מה ששום דבר מזה לא מספק הוא הערובה. MathForm-8B נותן לך טענה, המודלים נותנים לך ביקורת, ועדיין משהו צריך להוכיח אותה. נכון להיום, המערכת היחידה שפורסמה וסוגרת את הלולאה הזו על קוד פרוס בפועל היא AlphaProof Code, והיא לא למכירה.

הסיבה לקרוא את שני המאמרים ולא לבחור מנצח

MathForm-8B הוא ארטיפקט שימושי עם תפקיד צר ותקרת דיוק אמיתית ומדודה. AlphaProof Code הוא הדגמת זרימת עבודה שהממצא הניתן להעברה ביותר בו אינו היקף ההוכחות אלא הפיצול: עבודת המפרט דורשת בני אדם ומודל כללי חזק, עבודת ההוכחה דורשת צוותי סוכנים וקרנל, והגבול ביניהם הוא המקום שבו נמצא כל הקושי. כל מי שבונה צינור אימות צריך להתייחס לפיצול ברצינות ולחשוב על אוטופורמליזציה כעל החלק שמפחית את העלות של השלב הראשון — לא החלק שמחליף אותו.

סיכום כן לצוות שמחליט מה להוריד החודש: MathForm-8B — כן, אם אתם עובדים עם Lean ורוצים עזרה בניסוח טיוטות. AlphaProof Code — קראו את מאגר הארטיפקטים ואת קטלוג הסטיות מהמפרט, כי הקטלוג מספר לכם יותר על מה שאימות פורמלי של קוד ייצור עדיין לא מסוגל להגיע אליו מאשר כל הכרזה רשמית.