קוד וסיגנל של AlphaProof: הוכחות אבטחה קוד מכונה בדוקות והנחות מהימנות

מה מכסה הסרטון הזה

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

תמליל מתורגם

תורגם מהקריינות המקורית באנגלית. זמינות אודיו וכתוביות נשלטת על ידי YouTube.

מי בודק הוכחת אבטחה של AI?

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

0:21 אתה יכול לבדוק את התוצאה מבלי להאמין בנאום הניצחון של המודל. בדיקה נפרדת תופסת שינוי שקט של השאלה. נרד לפרטים. זה יום שלישי, העשירי בנובמבר, וזה The Daily Diff. AlphaProof Code היא המסגרת של גוגל לכתיבת מפרטי תוכנה עם הדרכה אנושית וייצור הוכחות בדוקות עם סוכני AI. מחקר זה מתמקד ב-libsignal, ספריית Rust המיישמת את פרוטוקול ההודעות של Signal, בתוך תוכנית שורת פקודה מסוימת.

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

כיצד טענה הופכת ליעד הוכחה?

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

1:27 מתאר הרחבה מעבר להיקפים הקטנים יותר של אימות קודם. פרטי יישום כוללים הודעות לא לפי הסדר והפעלות בארכיון עבור הודעות מושהות. תוכנה אמיתית שומרת את הקבלות שהתרשים האלגנטי שלך השליך. החוקרים מהדרים את ספריית Rust הלא מורשית עם המהדר הסטנדרטי

למה להוכיח את הבינארי המהודר?

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

2:06 אלף שורות מפרט וסמנטיקת הוראות מהימנות. אלה ספירות ארטיפקט. התייחסות אליהם כאל ציוני אינטליגנציה היא כמו דירוג מפתחים לפי גודל תיקיית ה-node_modules שלהם. תיקיית ה-node_modules שלהם.

אילו מאפייני אבטחה שרדו את פער היישום?

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

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

האם המפרט יכול לדחות קוד שבור?

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

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

האם הוכחה נכונה יכולה לענות על השאלה הלא נכונה?

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

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

מה תופס את המטרות הנעות?

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

4:37 של העובד ובדוק שינויים מוצעים בנפרד. התוצאה של גוגל הופכת את ההפרדה הזו לקונקרטית. כותב ההוכחות עושה את העבודה; גבול הבדיקה מחליט אם זה נחשב. אם אתה מעדיף לקרוא את זה מאשר לשמוע אותי אומר את זה, ההבדל נוחת בתיבת הדואר הנכנס שלך כל בוקר, בחינם ב-the daily diff dot dev, קישור למטה. אז פסק הדין של היום הוא SHIP IT.

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

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

מקורות

1. AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeepingSwarat Chaudhuri and colleagues / Google DeepMind and Google
2. Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO responsePushmeet Kohli and Swarat Chaudhuri / Google DeepMind
3. Code-verification repository — initial commit, public artifacts and checking instructionsGoogle DeepMind / GitHub
4. The PQXDH Key Agreement Protocol — older official specification and prior-analysis contextEhren Kret and Rolfe Schmidt / Signal
5. The Double Ratchet Algorithm — Triple Ratchet sectionTrevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
6. Google DeepMind leadership — Demis Hassabis's relevant lab identityGoogle DeepMind
7. Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsementChristopher P. Michel / Cmichel67 / Wikimedia Commons
8. Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlikeCreative Commons
9. Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claimImgflip / user-uploaded meme template
10. Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claimBoomerang Official / GIPHY / Tom and Jerry
11. Boomerang GIF source link — uploader-provided provenanceBoomerang
12. AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claimsHacker News
13. Code-verification licence — Apache 2.0 for Google code, third-party licences retainedGoogle / GitHub