Код і сігнал AlphaProof: правераныя доказы бяспекі машыннага кода і давераныя здагадкі

Што ахоплівае гэта відэа

• Агенты штучнага інтэлекту ствараюць кандыдаты доказаў; ядро Lean правярае, ці ўстанаўліваюць яны зацверджанае чалавекам фармальнае сцвярджэнне.
• Правераная мэта - гэта канкрэтная скампіляваная абалонка CLI libsignal з даверанай семантыкай і крыптаграфічнымі кантрактамі.
• Даказанне скампіляванага двайковага файла выдаляе кампілятар Rust з даверанай базы для заяўленых уласцівасцей гэтага двайковага файла.
• Даследчыкі паведамляюць пра два ізаляваныя паўторныя ўвядзенні раней выпраўленых памылак, якія парушаюць іх сімвалічную тэарэму бяспекі.
• Кампаратар правярае тэарэму і кожнае залежнае вызначэнне на адпаведнасць абароненай зацверджанай спецыфікацыі; папраўкі праходзяць асобны правераны працэс.

Перакладзеная стэнаграма

Перакладзена з арыгінальнай англійскай агучкі. Даступнае аўдыя і субтытры кантралююцца YouTube.

Хто правярае доказ бяспекі штучнага інтэлекту?

0:00 Аудыт бяспекі штучнага інтэлекту ўсё яшчэ гучыць як давер чат-боту. Новы вынік Google Signal пастаўляецца з матэматычнымі доказамі асобнага ядра правярае. У гэтым відэа, што даказаў Google? І як яны перашкаджаюць агенту мяняць мэты? Вось карысны адказ. Мадэлі пішуць кандыдацкія доказы, і Lean правярае доказы на адпаведнасць зацверджанай чалавекам заяве аб выбраным скампіляваным кодзе. Людзі па-ранейшаму валодаюць заяўкай і здагадкамі.

0:21 Вы можаце праверыць вынік, не верачы пераможнай прамове мадэлі. Асобная праверка выяўляе ціхае змяненне пытання. Мы пойдзем па ім да вызначэнняў. Аўторак, дзесятае лістапада, і гэта The Daily Diff. AlphaProof Code - гэта фрэймворк Google для напісання спецыфікацый праграмнага забеспячэння з кіраўніцтвам чалавека і генерацыі правераных доказаў з дапамогай агентаў штучнага інтэлекту. Гэта даследаванне накіравана на libsignal, бібліятэку Rust, якая рэалізуе пратакол абмену паведамленнямі Signal, у канкрэтнай праграме каманднага радка.

0:45 Google абвясціў аб працы сёння. У яго артыкуле гаворыцца, што пяць даследчыкаў працавалі на працягу чатырох тыдняў. Агенты пісалі доказы, у той час як людзі трацілі большую частку сваіх намаганняў на спецыфікацыі. Патрабаванні знайшлі спосаб стаць яшчэ больш дарагімі сустрэчамі. Спецыфікацыя кажа, што павінна рабіць праграма,

Як сцвярджэнне становіцца мэтай доказу?

0:59 што кантралюе зламыснік і якія здагадкі патрэбны аргументу. Рэцэнзенты пытаюцца, ці адлюстроўвае ён бяспеку, пра якую клапоцяцца людзі. Прыгожа правераны адказ на слабое пытанне пакідае гэтае пытанне некранутым. Каманда абапіраецца на ранейшыя даследаванні рукапаціскання Signal і яго ключа паведамленняў храпавіка. Фармальны аналіз ужо вывучаў гэтыя канструкцыі. Заява Google звязвае іх аргументы бяспекі з нязменнай вытворчай скампіляванай рэалізацыяй бібліятэкі, дзе дызайн павінен вытрымаць кантакт з фактычным кодам. Тэхнічны дырэктар Signal, Эрэн Крэт,

1:27 апісвае пашырэнне за межы меншых абласцей ранняй праверкі. Дэталі рэалізацыі ўключаюць паведамленні не па парадку і архіваваныя сесіі для адкладзеных паведамленняў. Рэальнае праграмнае забеспячэнне захоўвае квітанцыі, якія ваша элегантная дыяграма выкінула. Даследчыкі кампілююць незменную бібліятэку Rust са стандартным

Навошта даказваць скампіляваны двайковы файл?

1:41 кампілятарам у выканальны файл Arm 64 Linux. Іх тэарэмы апісваюць гэты бінарны файл з выкарыстаннем фармальнай інструкцыйнай мадэлі, перакрываючы разрыў паміж зыходным і аптымізаваным машынным кодам. Памылка кампілятара, якая парушае заяўленую ўласцівасць, зрабіла б яе тэарэму ілжывай. Таму кампілятар пакідае давераную базу для гэтага двайковага файла. Вы па-ранейшаму давяраеце інструкцыйнай мадэлі і праверцы Lean. Мяжа даверу змянілася і мае адрас. Прыкладна шэсць з паловай мільёнаў радкоў праверанага доказу абапіраюцца на прыкладна дваццаць шэсць

2:06 тысяч давераных радкоў спецыфікацыі і семантыкі інструкцый. Гэта колькасць артэфактаў. Разглядаць іх як паказчыкі інтэлекту - гэта ўсё роўна, што ранжыраваць распрацоўшчыкаў па памеры іх папкі модуляў node.

Якія ўласцівасці бяспекі вытрымалі разрыў у рэалізацыі?

2:16 Аргументы ахопліваюць канфідэнцыяльнасць і аўтэнтыфікацыю паведамленняў, з прамой сакрэтнасцю і бяспекай пасля кампраметацыі ў рамках заяўленых мадэляў. Апошнія два апісваюць абмежаванні на шкоду ад выкрадзеных ключоў і аднаўленне пасля свежых абменаў. Кожная гарантыя мае ўмовы для зламысніка і сесіі. Крыптаграфічныя прымітывы знаходзяцца за даверанымі кантрактамі. Доказ мяркуе, што гэтыя працэдуры паводзяць сябе так, як паказана, і абапіраецца на крыптаграфічныя здагадкі бяспекі. Адзін доказ ідэалізуе крыптаграфію; іншы разважае пра верагоднасці поспеху зламысніка.

2:42 Абодва маюць абмежаванні на сцэнарыі, якія яны ахопліваюць. Спытайце, якая зборка, якая ўласцівасць і якія здагадкі. Гэты вынік датычыцца каманднага радка даследчыкаў. Групавыя паведамленні - гэта будучая праца, і вылічальная мадэль выключае шматпрыладны стан. Называць кожную ўстаноўку Signal без памылак - гэта выходзіць за межы тэарэмы. Даследчыкі зноў увялі дзве раней выпраўленыя памылкі Signal у

Ці можа спецыфікацыя адхіляць зламаны код?

3:02 ізаляваныя копіі і скампілявалі іх. Правераныя доказы паказалі, што гэтыя двайковыя файлы парушаюць сімвалічную тэарэму бяспекі. Гэта праверыла, ці можа спецыфікацыя адхіляць рэальныя зламаныя рэалізацыі. Ваш зялёны сцяжок патрабуе чырвонага тэсту. Google публікуе спецыфікацыі і доказы з інструкцыямі па праверцы. У рэпазітарыі гаворыцца, што чыстая зборка займае гадзіны і значны аб'ём памяці. Чытанне аб'явы значна прасцей на ноўтбуку. Мадэль абсталявання і давераныя кантракты ўсё яшчэ патрабуюць перагляду.

3:26 Я не перабудоўваў велізарны артэфакт для гэтага эпізоду. Мы паведамляем апублікаваны вынік і яго межы. Аутсайдары маюць шлях да яго праверкі, што для мяне важней, чым чарговае пераможнае кола штучнага інтэлекту. Цяпер пастка.

Ці можа правільны доказ адказаць на няправільнае пытанне?

3:36 Lean можа прыняць правільны доказ сцвярджэння, якое амаль нічога не патрабуе. Немагчымыя здагадкі могуць зрабіць тэарэму пустым. Змена вызначэння, пахаванага пад галоўнай тэарэмай, можа аслабіць мэту. У артыкуле прадугледжаны праверкі на гэта. Вартаўнік захоўвае зацверджаную спецыфікацыю, якую агенты доказу не могуць запісваць. Яны могуць прапаноўваць выпраўленні праз асобны працэс унясення паправак. Аслабленне бяспекі эскалуецца як патэнцыйная памылка. Заява праверніка аб поспеху тут не мае ніякай сілы.

4:00 Людзі разглядаюць змены ў давераных здагадках, непасрэдна або праз сваю палітыку, і пераглядаюць папраўкі пасля кожнай кампаніі. Экспертнае меркаванне застаецца на кручку. Агент можа запытаць іншае прызначэнне. Ён не можа даваць сабе прахадны бал.

Што перашкаджае зменным мэтам?

4:13 Вось абяцаная праверка. Кампаратар Lean параўноўвае тэарэму і кожнае вызначэнне, ад якога яна залежыць, з гэтай абароненай зацверджанай копіяй. Ён таксама правярае дазволеныя аксіёмы і перагульвае доказ у свежым ядры. Ціхае аслабленне дапаможнага вызначэння, такім чынам, змяняе тое, што параўноўваецца. Прыняты доказ павінен усталяваць зацверджаную мэту. Гэта па-ранейшаму пакідае людзей адказнымі за выбар моцнай мэты і сумленных здагадак. Для ўласнага працоўнага працэсу штучнага інтэлекту, захоўвайце крытэрыі прыняцця па-за

4:37 дазволамі на рэдагаванне работніка і асобна пераглядайце прапанаваныя змены. Вынік Google робіць гэтае падзел канкрэтным. Аўтар доказу робіць працу; мяжа праверкі вырашае, ці гэта лічыцца. Калі вы аддаеце перавагу прачытаць гэта, чым пачуць ад мяне, "The Daily Diff" прыходзіць на вашу электронную пошту кожную раніцу, бясплатна на "thedailydiff.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