AlphaProof Code מול AesCode 32B: האחד מוכיח שהקוד נכון, והאחר מצייר אותו

שימו את AlphaProof Code ואת AesCode 32B באותו משפט, והדבר היחיד המשותף להם הוא המילה "code". AlphaProof Code הוא מסגרת סוכנית של Google DeepMind שהוכרזה ב-10 בנובמבר 2026 והפיקה כ-6.5 מיליון שורות Lean שנבדקו על ידי מכונה ומוכיחות שהבינארי המקומפל של libsignal מתנהג כפי שמצוין. AesCode 32B הוא צ'קפוינט חזותי-לשוני בעל 33 מיליארד פרמטרים, שאותו העלתה Microsoft ל-Hugging Face בתחילת אוקטובר 2026 ללא הכרזה, והוא כותב פרומפט לתוך מסמך HTML יחיד ועצמאי — שקף, פוסטר, לוח בקרה — שאדם מסתכל עליו לאחר מכן. אף אחד מהם אינו שירות שאפשר לפנות אליו. אחד מהם אפילו אינו מודל. אם הגעתם לכאן בחיפוש אחר החלטת החלפה ישירה, התשובה הכנה היא שהחלטה כזו אינה קיימת, והמשך הקטע הזה מסביר מדוע ההשוואה עדיין שווה לעשות.

הטעות הקטגוריאלית, כשהיא מנוסחת כראוי

AesCode 32B הוא מחולל. אתה נותן לו תיאור; הוא מחזיר תוצר שאיכותו נשפטת מבחינה אסתטית ולפי האם המספרים בעמוד הם במקרה המספרים שביקשת. ההצגה של כרטיס המודל עצמו היא שמחוללי תמונות מרכיבים עמוד יפה ומשבשים את המספרים שעליו, בעוד מודלי קוד מציגים את המספרים נכון ואינם יכולים לראות איך העמוד נראה — AesCode מצמיד להנחיה שלך תמונה שנוצרה מאותה הנחיה ומשתמש בתמונה כהפניה אסתטית תוך היצמדות לטקסט לצורך התוכן.

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

ההבחנה הזו קובעת למה כל אחד מהם נועד. AesCode 32B עונה ל"תכין לי דבר". AlphaProof Code עונה ל"האם הדבר הזה הוא מה שהוא מתיימר להיות". את הראשון הייתם משתמשים ביום שלישי אחר הצהריים בשביל מצגת, ואת השני, אילו הייתם Signal, לאורך ארבעה שבועות עם חמישה חוקרים וצוותים של 40 עד 80 סוכנים.

מה כל אחד מהם מספק בפועל

• פרמטרים — AesCode 32B: כ-33.4 מיליארד ב-BF16 על פני ארבעה־עשר שברי safetensors בסך כולל של 66,714,912,704 בתים. AlphaProof Code: אין. זהו מסגרת בתוספת מאגר ארטיפקטים, ואין משקלים להורדה.

• {{1}}בסיס{{/1}} — AesCode 32B: כוונון עדין של Qwen3-VL-32B-Instruct, כשהארכיטקטורה מוצהרת כ-{{2}}Qwen3VLForConditionalGeneration{{/2}}, ולכן הוא נטען עם transformers 4.57 ואילך. AlphaProof Code: אינו תלוי במודל מעצם בנייתו; המאמר של {{3}}DeepMind{{/3}} מציין את {{4}}G​emini 4 Carbon{{/4}} עבור סוכני ההוכחה ואומר ש{{5}}Claude Opus 5.5{{/5}} היה אחד מהמודלים שניסחו וסקרו מפרטים.

• רישיון — AesCode 32B: Apache 2.0, ב-Hugging Face היום. AlphaProof Code: פיתוח ה-Lean, הסמנטיקה של AArch64 וכריכת libsignal מפורסמים ב-github.com/google-deepmind/code-verification, ודף הנחיתה מציין שאין רישיון, ויש לפתור זאת לפני שמבנים עליו משהו.

• זמינות — AesCode 32B: אירוח עצמי בלבד. כ-65 GB של זיכרון מאיץ עבור המשקלים, פקודת vLLM על ארבע דרגות tensor-parallel, ללא נקודת קצה מנוהלת וללא מיפוי ספק-הסקה מאחורי עמוד המאגר. AlphaProof Code: פריט מחקר, ללא נקודת קצה, ללא רשימת המתנה, ללא תמחור.

• פלט — AesCode 32B: מסמך HTML אחד, שניתן לבדוק על ידי פתיחתו. AlphaProof Code: מונח הוכחה ב-Lean, שניתן לבדוק באמצעות Lean.

• מה פירוש "נכון" — AesCode 32B: הדף נראה תקין והנתונים תואמים להנחיה, כפי שנקבע על ידי אדם. AlphaProof Code: המשפט מתקיים עבור כל הקלטים במודל, כפי שנקבע על ידי קרנל.

החפיפה היחידה שמעניינת באמת: שני הפלטים הם ארטיפקטים.

הנה השוואה ששווה לעשות. שתי המערכות מייצרות קובץ שמאריך ימים יותר מהמודל שיצר אותו. ה-HTML של AesCode 32B הוא מסמך גמור; אפשר לשחרר אותו, לערוך אותו, להפיק לו diff, ואף אחד כבר לא צריך את המודל. ההוכחה ב-Lean של AlphaProof Code היא גזירה גמורה; אפשר לבדוק אותה מחדש על מחשב נייד בכמה דקות חישוב, ואם המפרט לא השתנה, התוצאה עדיין עומדת בעינה בעוד חמש שנים.

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

המקום שבו האנלוגיה נשברת הוא יכולת הביקורת. כל אחד יכול לפתוח את ה-HTML ולראות אם הכותרת שגויה. כמעט אף אחד לא יכול לפתוח 6.5 מיליון שורות של Lean ולראות אם המשפט אומר את מה שההודעה לעיתונות טוענת שהוא אומר — וזו בדיוק הסיבה שהמאמר של DeepMind מקדיש עמודים לפירוט הבסיס המהימן שלו, 37 הפרימיטיבים החוזיים שלו והתכונות שהוא לא מוכיח. אפשר לבדוק את הארטיפקט; הקריאה בו אינה בחינם.

כמה שווים המספרים בכל צד

הכותרת של AesCode 32B היא ציון כולל של 85.89 לעומת GPT-5.5 עם 81.28 — מדידה של מיקרוסופט של מודל מתחרה, לפי רובריקה שמיקרוסופט כתבה, על גבי הארנס שמיקרוסופט בנתה. Boundary עומד על 97.27 עם גלישה חמורה ב-4.3% מהדגימות, ו-style על 55.99, שורה שבה אף מודל בטבלה לא עובר 60. לפי המונים של המאגר עצמו, איש מחוץ למיקרוסופט לא פרסם מספר עבור המודל. כל נתון לעיל דווח על ידי הספק ולא שוחזר.

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

מספר אחד אכן עובר בצורה מועילה. האימות של AlphaProof Code ארך ארבעה שבועות, בעוד שעבודה דומה נמשכה היסטורית שנים אצל צוותי מומחים, לעומת קווי הבסיס שהמאמר עצמו מצטט: כ-20 שנות אדם עבור seL4 וכ-6 עבור CompCert. היחס הזה הוא הטענה שיש להחזיק בה, והיא טענה בנוגע לתהליך עבודה, לא לאיכות המודל.

איזה מהם אתה באמת יכול להריץ השבוע

AesCode 32B: כן, אם יש לך את החומרה. הורד את השברים, הרץ שירות עם vLLM על ארבעה רנקים, שמור על פרומפטים מתחת לתקרת 24,576 הטוקנים של הכרטיס, וקבל את זה ששלב הסקירה שלך הוא אדם שמצמצם עיניים מול HTML מרונדר. זה לא יגיד לך אם העמוד נכון; זה יגיד לך אם העמוד נראה נכון.

AlphaProof Code: לא. הארטיפקטים שפורסמו הם פיתוח ב-Lean, לא צינור עיבוד שאתם מפעילים. אפילו המודלים שבתוכו אינם התוצר — המסגרת היא מבנה מחקרי, והניסוח של DeepMind עצמה הוא שהרחבתו "דורשת מחקר מתמשך". CodeMender הוא הפרויקט האח לתיקון אוטומטי; אימות ותיקון הם שני מוצרים שונים במפת הדרכים של אותה מעבדה.

אם מה שאתם רוצים הוא מודל שינסח את המפרטים — השלב שבו מומחים אנושיים תרגמו את יעדי האבטחה של Signal ל-Lean, ונסקרו אחד אחד — זו עבודה רגילה של מודל, ו-Claude Opus 5.5 נמצא בקטלוג של OrcaRouter במחיר 4 דולרים למיליון טוקני קלט ו-20 דולרים למיליון טוקני פלט, כאשר מחיר המחירון של הספק מועבר ללא תוספת של 0%. ניתוב לולאת ניסוח מפרטים בין שניים או שלושה מודלים והשוואת פלט ה-Lean שלהם הוא קריאת routing-DSL, לא פרויקט מחקר. מה ששום דבר מזה לא נותן לכם הוא הוכחה; שלב ההוכחה הוא המקום שממנו הגיעו ששת מיליון השורות.

למה בכל זאת שווה לפרסם את הזיווג

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

אם אתם מעריכים את AesCode 32B עבור צינור עיצוב, הדבר שצריך לבדוק אינו הציון הכולל שלו אלא התנהגות הגבול שלו — שיעור הגלישה החמורה של 4.3% הוא המקום שבו מצגת הופכת בשקט לשגויה ולא למכוערת. אם אתם מעריכים את AlphaProof Code, הדבר שצריך לקרוא הוא קטלוג הסטיות מהמפרט במאגר הארטיפקטים: למעלה מ-200 רשומות חישוביות וכ-35 רשומות סימבוליות, חמש-עשרה מהן פערים או באגים בניתוח Double Ratchet. הקטלוג הזה הוא המסמך הכנה ביותר במהדורה, משום שהוא רשימה של כל מה שההוכחות לא סגרו.