6.5 מיליון שורות הוכחה ושאלה אחת פתוחה: מה באמת הוכיחה DeepMind על הקוד של Signal

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

את שני הבאגים האלה איתרו במקור החוקרים Cheval, Jacomme ו-Richards, בניתוח אוטומטי של הפרוטוקול. הפעם, השאלה הייתה אם המכונה תמצא אותם בעצמה. היא מצאה: עבור כל אחת משתי הגרסאות הפגומות, המערכת הפיקה הוכחה שנבדקה במחשב, שלפיה הגרסה הזאת מפרה את תכונת האבטחה שהוגדרה לה. לא אזהרה, לא "חשד סביר", אלא הוכחה.

זה הרגע שבו רוב הכותרות של השבוע עצרו: AI הוכיח מתמטית שההצפנה של Signal מאובטחת. הכותרת הזאת נוחה, והיא מפספסת את מה שקרה באמת. מה שהמערכת הוכיחה הוא שקוד מסוים עומד בדרישות מסוימות, תחת הנחות מסוימות. כל אחת משלוש המילים האלה, "מסוים", היא סיפור בפני עצמו. בכתבה הזאת נפרק איך המערכת עובדת, למה הבדיקה מול קוד מכונה היא קפיצה אמיתית, ולמה השאלה המעניינת כבר איננה "האם הוכיחו" אלא "מי ניסח את מה שהוכיחו". בדרך נעבור גם בפרק ישראלי מפתיע בהיסטוריה של התחום.

מה בדיוק נבדק, ולמה דווקא קוד מכונה

נתחיל מהמנגנון עצמו, כי הוא פשוט יותר ממה שנשמע. הפרוטוקול של Signal בנוי משני חלקים עיקריים. הראשון, PQXDH, הוא לחיצת היד: הדרך שבה שני טלפונים שמעולם לא דיברו מסכימים על סוד משותף, גם אם מישהו מקשיב לכל מילה. Signal הוסיפה אותו ב-2023 כדי להתגונן מפני תוקף שמקליט תעבורה היום ומקווה לפענח אותה בעתיד בעזרת מחשב קוונטי. החלק השני, ה-Triple Ratchet, הוא מנגנון שמחליף מפתחות כל הזמן לאורך השיחה. Signal הכריזה עליו באוקטובר 2025, כשהוסיפה לשני ה"מחגרים" הקלאסיים שכבה שלישית עמידה לקוונטים, בשם SPQR.

הקוד שמממש את כל זה נקרא libsignal, והוא כתוב ב-Rust. לפי המאמר, החוקרים לקחו את הגרסה 0.105.4 שלו יחד עם רכיב ה-SPQR, הקיפו אותה בתוכנית מעטפת קטנה שכתבו בעצמם, והידרו הכול לקובץ הרצה אחד למעבדי Arm של 64 ביט. ואז עשו את הדבר החריג: הם לא הוכיחו טענות על קוד ה-Rust, אלא על קוד המכונה שיצא מהמהדר. כלומר, על ההוראות שהמעבד באמת מריץ.

למה זה חשוב? כי בין הקוד שמתכנת כותב לבין מה שהמעבד מבצע יושב מהדר, ומהדרים הם תוכנות ענקיות שיכולות לטעות. הוכחה על קוד המקור מניחה בשקט שהמהדר תרגם נאמנה. הוכחה על קוד המכונה מוציאה את המהדר מרשימת הדברים שצריך לסמוך עליהם. המחיר: צריך לתאר במדויק, בשפה מתמטית, מה כל הוראת מעבד עושה. הצוות כתב תיאור כזה ב-Lean, שמכסה לפי המאמר 467 הוראות ו-31 קריאות מערכת, ובדק אותו מול אמולטורים ומול המודל הרשמי של Arm.

Lean עצמה היא שפת תכנות ומוכיח משפטים, שפותחה במקור על ידי Leonardo de Moura במיקרוסופט. הייחוד שלה הוא "גרעין" קטן מאוד, שתפקידו היחיד הוא לבדוק שכל צעד בהוכחה נובע מקודמיו. לא משנה מי כתב את ההוכחה, אדם או מודל שפה: אם הגרעין מקבל אותה, היא נכונה.

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

התו אמין בדיוק כמו התקן שמאחוריו, ולא שורה אחת יותר.

פס הייצור של הסוכנים

איך מגיעים למיליוני שורות הוכחה בארבעה שבועות? התשובה היא חלוקת עבודה שנראית יותר כמו חברת תוכנה קטנה מאשר כמו מודל אחד. לפי המאמר, מתחילים בסוכן שמנסח טיוטת הגדרה בהנחיית אדם. מעבירים את הטיוטה לסוכנים מבקרים, ולפחות אחד מהם בא ממשפחת מודלים אחרת, כדי שלא יחלוק את אותן נקודות עיוורון. רק אחרי סבבים של הערות, אדם מאשר. בשלב ההגדרות השתתפו, לפי המאמר ולפי דיווח ב-The Next Web, המודלים Gemini 4 Carbon של גוגל ו-Claude Opus 5.5 של Anthropic.

משם הסוכנים עובדים לבד. מריצים צוות של 40 עד 80 סוכנים על מחשב אחד, במשך יממה עד שלוש. יש מתזמר שמחלק משימות, ראשי צוותים, "ארכיטקט", "אינטגרטור" ו"מבקר". את ההוכחות עצמן, כך כותבים החוקרים, הפיקו כולן צוותי סוכנים שרצו על Gemini 4 Carbon. משפט אחד במאמר מסכם את חלוקת התפקידים בלי עקיפות: "לא כתבנו הוכחות".

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

כדי לוודא שהתיאור המתמטי של המעבד תואם את המציאות, החוקרים הריצו את הקובץ האמיתי ואת המודל ב-Lean זה לצד זה, על כ-15.6 מיליון הוראות, וקיבלו אותן תוצאות. וכדי לוודא שההוכחות לא ריקות מתוכן, באו שני הבאגים מפתיחת הכתבה: אם הוכחה "עוברת" גם על קוד פגום, משהו בתקן שבור.

התפנית: ההוכחה נעשתה זולה, והשאלה נעשתה יקרה

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

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

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

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

כשהבודק בלתי ניתן לרמייה, הפיתוי עובר אל מי שכותב את השאלה.

מה נשאר מחוץ לתו התקן

כאן כדאי להאט, כי הפרטים האלה נדחקו לשוליים של הכותרות. המאמר עצמו מפרט אותם ביושר, וגם The Next Web ו-XenoSpectrum סיכמו אותם. ההוכחה מכסה שיחות של אחד על אחד בלבד. קבוצות נשארו לעבודה עתידית. יצירת המפתחות לא אומתה. ההוכחה מניחה תשתית מפתחות ציבוריים אמינה ומפתח זהות ידוע מראש, כך שהרגע שבו משתמש סומך על מספר חדש בפעם הראשונה לא נבדק. מתקפות ערוץ צד, כמו מדידת זמני תגובה או צריכת חשמל, מחוץ לתחום. וכל אבני הבניין הקריפטוגרפיות, כמו פונקציות הגיבוב וחתימות, נחשבות מושלמות בגרסה הסימבולית, ועומדות בהנחות קושי מוכרות בגרסה החישובית.

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

ועכשיו לזווית הישראלית, זו שלא שאלו עליה בכלל. רוב הישראלים לא משתמשים ב-Signal אלא ב-WhatsApp, ו-WhatsApp אכן מריצה גרסה של פרוטוקול Signal. קל לקרוא את הכותרת ולהסיק שגם ההודעות בקבוצת ההורים של הגן "הוכחו". הן לא. מה שנבדק הוא קובץ הרצה שהחוקרים בנו בעצמם מהקוד הפתוח של libsignal, בגרסה מסוימת, על מעבד מסוים. היישום של WhatsApp הוא קוד אחר, של חברה אחרת, ואין לנו שום הוכחה עליו. אפילו אפליקציית Signal עצמה, עם הממשק, הגיבויים והסנכרון בין מכשירים, נמצאת מחוץ לתחום. הפרוטוקול זהה ברוחו; הקוד לא.

ההוכחה שייכת לקובץ, לא למותג.

מפנואלי ועד Lean: פרק ישראלי בשאלה מה בכלל מוכיחים

הרעיון שאפשר להוכיח שתוכנה נכונה כמעט ישן כמו המחשב. ב-1969 פרסם Tony Hoare את המאמר שהניח בסיס לוגי לנימוק על תוכניות. אבל מערכות כמו תוכנת צ'אט לא "מסתיימות" עם תשובה; הן רצות בלי סוף, מגיבות לאירועים, ואמורות לשמור על תכונות לאורך זמן. "אף פעם לא יקרה שמפתח ידלוף". "בסופו של דבר ההודעה תגיע". איך כותבים דרישה כזאת בשפה מתמטית?

את התשובה נתן מתמטיקאי ממכון ויצמן. ב-1977 פרסם פרופ' אמיר פנואלי את המאמר "הלוגיקה הזמנית של תוכניות", שהכניס למדעי המחשב שפה לתיאור תכונות לאורך זמן. לפי ACM, ב-1996 הוענק לו פרס טיורינג על הכנסת הלוגיקה הזמנית למדעי המחשב ועל תרומתו לאימות תוכניות ומערכות, ובשנת 2000 קיבל את פרס ישראל. כדאי לשים לב למה בדיוק הוא תרם: לא שיטה להוכיח מהר יותר, אלא שפה לנסח את מה שצריך להוכיח. במובן זה, הלקח של DeepMind מ-2026 הוא חזרה לשאלה של פנואלי מ-1977.

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

ומה בעולם? לצד seL4, שכאמור דרש כעשרים שנות אדם, עומד CompCert, מהדר לשפת C שהוכח נכון, גם הוא אחרי שנים של עבודה. ב-2024 הציגה DeepMind את AlphaProof המקורי, שלמד להוכיח טענות מתמטיות ב-Lean ברמה של תחרויות אולימפיאדה. ובאפריל 2026 הכריזו Signal, קרן Beneficial AI Foundation וארגון Lean FRO על אתגר בשם Signal Shot: לאמת ב-Lean את הפרוטוקול ואת האפליקציה של Signal. העבודה של DeepMind היא צעד גדול בכיוון הזה, לא הסיום שלו.

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

המספרים, ומה הם לא מספרים

ארבעה שבועות וחמישה אנשים: הנתון הזה מופיע במאמר עצמו, ומשוחזר ב-The Next Web וב-Hardware Busters. הבלוג של DeepMind מתאר את המשימה כזו ש"לקחה היסטורית לצוותי מומחים שנים". ההשוואה מרשימה, אבל היא לא ניסוי מבוקר. אין קבוצת ביקורת של מומחים אנושיים שניסו לאמת את אותו קוד, והחוקרים עצמם מציינים שנהנו מעבודות אימות קודמות על הפרוטוקול, ואת המודלים הסימבוליים לקחו מחוקרים שקדמו להם.

כ-6.5 מיליון שורות הוכחה, לפי המאמר. הבלוג של החברה כותב "יותר משישה מיליון", וחלק מכלי התקשורת עיגלו לכאן או לכאן. כדאי לזכור שגם הנתון הזה מטעה מעט: שורות הוכחה שמכונה כותבת הן מילוליות במיוחד, ומספר השורות מודד בעיקר כמה עבודה המכונה עשתה, לא כמה ביטחון קיבלנו. הנתון שחשוב באמת הוא הקטן: כ-26 אלף שורות של בסיס אמון, כ-18 אלף מהן הגדרות וכ-8,000 תיאור המעבד ושמות הסמלים. זה מה שבני אדם צריכים לקרוא.

כאחוז אחד מהקוד סומן לבדיקה אנושית. הנתון הזה מגיע מהבלוג של DeepMind: הסוכנים עצמם ביקרו את העבודה וסימנו אזורים שדורשים עין שנייה. לא ברור מהפרסומים איך נבחר האחוז הזה ומה נבדק בו בפועל.

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

מה אנחנו יודעים, ומה לא

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

אנחנו לא יודעים אם ההגדרות תופסות את כל מה שחשוב. זו השאלה שאף בודק מכני לא יענה עליה, ו-XenoSpectrum ציינה זאת במפורש: אם איום מסוים חסר בהגדרה, ההוכחה לא תתריע עליו. אנחנו לא יודעים כמה מהגדרות שנוסחו בעזרת מודלים ונבדקו על ידי מודלים אחרים היו נשארות כפי שהן אחרי ביקורת של צוות חיצוני ועצמאי. ולא שמענו עדיין מומחה חיצוני שבחן את ההגדרות לעומק; הכתבות שקראנו לא ציטטו אף מבקר בלתי תלוי. ה"ראשונה" שבכותרות, כלומר הטענה שאף מימוש של פרוטוקול נפוץ כזה לא אומת קודם בשום שיטה, היא טענה של DeepMind, ולא מצאנו מי שאישר אותה באופן עצמאי.

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

איך לקרוא את הכותרת הבאה על "AI הוכיח שזה מאובטח"

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

1. מה בדיוק הוכח, ועל איזה קוד. שם הגרסה, הפלטפורמה, והאם מדובר בקוד המקור או בקוד המכונה. "Signal" הוא מותג; libsignal 0.105.4 על Arm הוא טענה.
2. מה נמצא בבסיס האמון. כמה שורות צריך לקבל בלי הוכחה, ומי קרא אותן. ככל שהבסיס קטן יותר, כך קל יותר לבקר אותו.
3. מה מחוץ למודל התוקף. ערוצי צד, קבוצות, סנכרון בין מכשירים, יצירת מפתחות. מה שלא הוגדר, לא הוכח.
4. מי ניסח ומי ביקר את ההגדרות. מודל שבודק מודל ממשפחה אחרת עדיף על כלום, אבל הוא לא תחליף לעין אנושית עצמאית שלא הייתה שותפה לעבודה.
5. האם ההוכחה הראתה שהיא תופסת באגים ידועים. מבחן ההחזרה של באגים ישנים הוא הסימן הטוב ביותר שההגדרות לא ריקות.
6. האם אפשר לשחזר. קוד פתוח וגרעין בדיקה ציבורי הופכים טענה להוכחה שכל אחד יכול להריץ. מודל סגור שכתב אותה לא פוגע בכך, אבל מקשה על השחזור של התהליך כולו.

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

תו התקן והוועדה

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

אבל אם היו חסרים לנו מומחים שיודעים לכתוב הוכחות, עכשיו יחסרו לנו מומחים שיודעים לכתוב שאלות. החוקר Swarat Chaudhuri מ-DeepMind אמר ל-WIRED שיש עוד "דרך ארוכה" עד שאפשר יהיה להרחיב את השיטה לכל התוכנה שבעולם. סביר שהפער הזה ייסגר מהר יותר בצד ההוכחות מאשר בצד ההגדרות, כי הוכחה אפשר לבדוק במכונה, ושאלה טובה אפשר לבדוק רק בוויכוח.

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

שאלות נפוצות

מה זה AlphaProof Code?

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

האם זה אומר שההודעות שלי ב-WhatsApp מוכחות כמאובטחות?

לא. WhatsApp מריצה גרסה של פרוטוקול Signal, אבל ההוכחה נעשתה על קובץ הרצה שהחוקרים בנו מהקוד הפתוח של libsignal, בגרסה מסוימת. היישום של WhatsApp הוא קוד אחר שלא נבדק. גם אפליקציית Signal המלאה, קבוצות ויצירת מפתחות נשארו מחוץ להוכחה.

אם Lean בודקת כל הוכחה, איפה בכלל יכולה להיות טעות?

בהגדרות ובהנחות. Lean מוודאת שההוכחה נכונה ביחס לשאלה שנוסחה, אבל לא שהשאלה עצמה שלמה. לכן החוקרים מגדירים כ-26 אלף שורות של בסיס אמון, ובהן ההגדרות ותיאור המעבד, שבני אדם צריכים לקרוא ולאשר. איום שלא נכלל בהגדרה לא יתגלה.

האם המערכת מצאה פרצות חדשות ב-Signal?

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