AlphaProof Code — סוכני AI שמוכיחים מתמטית שקוד עומד בדרישות אבטחה

מה הודיעה Google DeepMind ב-10 בנובמבר 2026

ב-10 בנובמבר 2026 הציגה Google DeepMind את AlphaProof Code, מערכת שבה בני אדם וצוות של סוכני AI עובדים יחד כדי להוכיח מתמטית שתוכנה עומדת בדרישות שהוגדרו לה. את ההודעה בבלוג של החברה כתבו פושמיט קוהלי (Pushmeet Kohli) וסוורט צ'אודהורי (Swarat Chaudhuri), ולצידה פורסם מאמר טכני של חוקרים מ-Google DeepMind ומגוגל. כמקרה בוחן הם בחרו ב-libsignal, ספריית הקוד שמממשת את פרוטוקול Signal. זה הפרוטוקול שמצפין הודעות מקצה לקצה באפליקציית Signal, ולפי המאמר גרסאות שלו פועלות גם ב-WhatsApp, ב-Messenger של Meta וב-Google Messages. לפי החברה, הסוכנים הוכיחו תכונות אבטחה מרכזיות של הקוד הזה, והעבודה כולה נמשכה ארבעה שבועות, משימה שלדבריה דרשה בעבר שנים של עבודת צוותי מומחים. החברה מתארת את ההישג כפעם הראשונה ש-AI שימש לאימות פורמלי של פרוטוקול הצפנה בשימוש רחב, בעומק כזה. המפרטים וההוכחות פורסמו לציבור באתר הפרויקט וב-GitHub.

מה זה אימות פורמלי, במילים פשוטות

רוב התוכנה בעולם נבדקת בבדיקות: מריצים אותה על הרבה מקרים ומחפשים תקלות. בדיקה כזו יכולה למצוא באג, אבל לא להבטיח שאין באג אחר שלא נבדק. אימות פורמלי עובד אחרת. קודם כותבים בשפה מתמטית מדויקת מה התוכנה חייבת לקיים, למשל "אף אחד מלבד הנמען לא יכול לקרוא את ההודעה". המסמך הזה נקרא מפרט. אחר כך מוכיחים, כמו שמוכיחים משפט בגיאומטריה, שהקוד מקיים את המפרט בכל ריצה אפשרית ולא רק במקרים שנוסו. לפי המאמר, הוכחה כזו פוסלת כל באג או מתקפה שהיו מפרים את התכונות שבמפרט. את ההוכחות כאן כתבו בשפה Lean, שבה מחשב בודק כל צעד לוגי. הבעיה היא המחיר: המאמר מזכיר שאימות ליבת מערכת ההפעלה seL4, אחת ההצלחות הגדולות בתחום, דרש עשרים שנות אדם, ואימות המהדר CompCert דרש שש. לכן אימות פורמלי שמור בדרך כלל למערכות הקריטיות ביותר. הטענה של DeepMind היא ש-AI יכול להוזיל את כתיבת ההוכחות עד כדי כך שהשיטה תתאים לתוכנה רגילה.

מה בדיוק הוכח

ההוכחות עוסקות בשני חלקים של Signal. הראשון הוא PQXDH, לחיצת היד שבה שני הצדדים מסכמים על סוד משותף בתחילת שיחה, ושנועדה להחזיק גם מול מחשב קוונטי עתידי. השני הוא ה-Triple Ratchet, המנגנון שמחליף מפתח בכל הודעה. לפי המאמר, הוכחו סודיות קדימה (Forward Secrecy: מי שגונב את המפתחות היום לא יכול לקרוא הודעות ישנות), אבטחה אחרי פריצה (Post-Compromise Security: אחרי שהתוקף מאבד גישה, השיחה חוזרת להיות מוגנת), אימות של הצד השני וסודיות של לחיצת היד. מה שמייחד את העבודה הוא הרמה שבה נעשתה. ההוכחות לא נכתבו על תיאור של הפרוטוקול על הנייר וגם לא על קוד המקור בשפה Rust, אלא על קוד המכונה עצמו: libsignal בגרסה 0.105.4, בלי שינויים, אחרי שהמהדר הרגיל של Rust הפך אותו לתוכנה שרצה על מעבדי Arm של 64 ביט. כך גם באג שהמהדר עצמו היה מכניס ושפוגע בתכונות האלה היה מפיל את ההוכחה. לפי החוקרים, אלה ההוכחות הראשונות שמחברות תכונות אבטחה של פרוטוקול הצפנה לקוד הלא משונה של מימוש שנמצא בשימוש רחב. לפי Let's Data Science, שמסתמך על WIRED, הניתוח לא מצא חולשות חדשות בחלקים שנבדקו.

איך זה עבד: אדם קובע מה להוכיח, הסוכנים מוכיחים

החלוקה בין בני האדם למכונה היא לב השיטה. לפי המאמר, החוקרים בחרו מה להוכיח, הכריעו בשאלות פתוחות ואישרו כל מפרט, וסוכן AI ייעודי עזר להם לנסח אותו. המפרטים נבנו על מודלים של אבטחת Signal שכבר פורסמו בספרות המחקר, וסוכנים אחרים בדקו כל טיוטה בעין ביקורתית. את ההוכחות עצמן כתב צוות של סוכנים אוטונומיים: מתזמר שמחלק את העבודה, ראשי צוותים, סוכנים שכותבים הוכחות, וסוכן שמשלב את התוצרים לספרייה אחת. לפי המאמר, צוות כזה מנה בדרך כלל 40 עד 80 סוכנים ורץ על מחשב אחד במשך 24 עד 72 שעות. ההוכחות נכתבו כולן בידי סוכנים שפעלו על Gemini 4 Carbon, ואיש מהחוקרים לא כתב קוד הוכחה. בכתיבת המפרטים השתתפו גם סוכנים שפעלו על Claude Opus 5.5. לפי המאמר, את עבודת ההוכחה עשה צוות של חמישה חוקרים במשך ארבעה שבועות. התוצר: כ-6.5 מיליון שורות של הוכחות ב-Lean. כדי לסמוך על התוצאה, קורא צריך לבדוק בעיקר את מה שנקרא הבסיס המהימן, כ-26 אלף שורות של מפרטים ושל תיאור התנהגות המעבד, ובנוסף לסמוך על Lean עצמה ועל ההנחות לגבי אבני הבניין של ההצפנה. את ההוכחות עצמן אין צורך לקרוא: סוכן שומר סף מקבל הוכחה רק אם הליבה של Lean אישרה אותה, ורק אם כלי השוואה מאשר שהיא מוכיחה בדיוק את המפרט שהחוקרים אישרו ולא גרסה מוחלשת שלו.

מבחן הבאגים הישנים

הוכחה טובה רק כמו המפרט שהיא מוכיחה. מפרט חלש מדי יכול להתקיים גם בקוד פגום, ואז ההוכחה מרגיעה בלי סיבה. כדי לבדוק שהמפרט שלהם חזק מספיק, החוקרים החזירו לקוד שני באגים אמיתיים שנמצאו בעבר ב-libsignal ותוקנו מאז. את שניהם חשפו קודם לכן החוקרים וינסן שבאל, שרלי ז'קום וג'סיקה ריצ'רדס במחקר על ה-Double Ratchet. באחד, הקוד לא בדק כראוי מפתח שנשלח בתחילת שיחה, ותוקף יכול היה לשלוח גרסה משובשת שלו וליצור שיחה נוספת עם אותו סוד. בשני, מצב השיחה נשמר בתנאים שבהם לא היה צריך להישמר, יחד עם עותק של מפתח סודי. לפי המאמר, בשני המקרים הפיקה המערכת הוכחה שנבדקה במחשב לכך שהגרסה הפגומה מפרה את תנאי האבטחה. לפי Let's Data Science, שמסתמך על דיווח של WIRED, המערכת גם סימנה גרסאות ישנות של Signal, שבהן היו חולשות שתוקנו מזמן, כגרסאות שאי אפשר לאמת. החוקרים כותבים שבדרך מצאו גם טעויות במאמרים שעליהם נשענו: חמש עשרה בעיות בניתוח החישובי של ה-Double Ratchet שפורסם בעבר, ושגיאות בניסוח של חלק מטענות האבטחה במחקר של שבאל ושותפיו.

מה לא הוכח

הכותרות על "אימות Signal" רחבות מהעבודה עצמה, והמאמר מפרט את הגבולות. ההוכחות חלות על תוכנת בדיקה קטנה שהחוקרים בנו סביב libsignal ורצה על Linux, ולא על אפליקציות Signal לאייפון, לאנדרואיד או למחשב. לפי המאמר, הן עוסקות בשיחה בין שני אנשים בלבד, ולא בקבוצות או בכמה מכשירים של אותו משתמש. הן מניחות שאבני הבניין של ההצפנה, כמו פונקציות הגיבוב וההצפנה עצמה, עושות את עבודתן, ולא מוכיחות זאת. מתקפות ערוץ צד, למשל מדידה של זמן החישוב, לא נבדקו. ההוכחה החישובית אינה מכסה תוקף בעל מחשב קוונטי, והתכונה של SPQR שאמורה להחזיר את האבטחה גם מול תוקף כזה לא הוכחה. חלק מההנחות על הסביבה שבה התוכנה רצה נומקו בלי הוכחה פורמלית. לפי Let's Data Science, גוגל סירבה לחשוף כמה עלה הניתוח, והבלוג של DeepMind כותב שכדי להרחיב את השיטה נדרש עוד מחקר. החוקרים מציינים גם שחלק העבודה שתבע הכי הרבה מאמץ אנושי היה דווקא כתיבת המפרטים, ולא ההוכחות.

הקשר ל-AlphaProof ולמאמץ לאמת את Signal

השם מזכיר את AlphaProof, המערכת ש-Google DeepMind הציגה ב-25 ביולי 2024. היא כתבה הוכחות מתמטיות ב-Lean, ויחד עם AlphaGeometry 2 הגיעה לרמת מדליית כסף באולימפיאדה הבינלאומית למתמטיקה. ב-12 בנובמבר 2025 פורסמה שיטת העבודה שלה בכתב העת Nature: מערכת שלמדה להוכיח בלמידת חיזוק, כלומר בניסוי וטעייה מול משוב. שתי המערכות כותבות הוכחות ב-Lean, אבל ההודעה על AlphaProof Code אינה מתארת אותה כגרסה של AlphaProof. לפי המאמר, כל הסוכנים בה הם סוכני תכנות כלליים שמבוססים על מודלי שפה, והתנהגותם מוגדרת במסמכי הנחיות בשפה רגילה. למאמץ לאמת את Signal יש גם הקשר רחב יותר. באפריל 2026 השיקו Beneficial AI Foundation, ‏Signal ו-Lean FRO את Signal Shot, מיזם שמטרתו לאמת ב-Lean את פרוטוקול Signal ואת האפליקציה. מאמר DeepMind מציג את התוצאות כצעד משמעותי לקראת היעד הזה. אהרן קרט (Ehren Kret), מנהל הטכנולוגיה של Signal, תיאר בבלוג של DeepMind את התרגום של קוד חי לטענות Lean תקפות בעזרת סוכני AI כפריצת דרך גדולה, ובאותה הצהרה אמר שעבודות אימות קודמות התמקדו בחלקים קטנים יותר של הקוד.

איך לקרוא את ההישג

נכון ל-15 בנובמבר 2026, כל המספרים והטענות מגיעים מ-Google DeepMind עצמה: מהבלוג, מהמאמר ומאתר הפרויקט. המאמר פורסם באתר של החברה, לא צוין שעבר ביקורת עמיתים, ולא פורסמה בדיקה חיצונית של המפרטים. ההוכחות עצמן ניתנות לבדיקה במחשב בידי כל אחד, כי הן פתוחות לציבור והליבה של Lean בודקת אותן. השאלה הפתוחה היא אחרת: האם המפרטים אומרים בדיוק את מה שאנחנו רוצים לדעת על Signal. החוקרים עצמם כותבים שמפרט של מערכת מורכבת הוא בעצמו תוכנה מורכבת, ושמפרטים כמו שלהם יצטרכו סבבים רבים של ביקורת פתוחה עד שיתייצבו. לכן התוצאה אינה אומרת ש-Signal נקייה מבאגים. היא אומרת שהתכונות שהוגדרו התקיימו, בהנחות שנקבעו, בקוד המכונה של גרסה אחת. חידוש מרכזי אחד הוא המחיר: לפי DeepMind, עבודה שהייתה דורשת שנים נעשתה בשבועות. החוקרים כותבים שהם רוצים להשתמש בשיטה כדי לאמת גרסאות חדשות של libsignal לפני שהן יוצאות, וחוזים מצב שבו כל שינוי בקוד יאומת לפני שהוא נכנס.