AlphaProof Code eta Signal: egiaztatutako makina-kodearen segurtasun-frogak eta fidatutako suposizioak

Bideo honek zer jorratzen duen

• AI agenteek froga hautagaiak sortzen dituzte; Lean-en kernelak egiaztatzen du giza onartutako aldarrikapen formala ezartzen duten.
• Egiaztatutako helburua libsignal CLI arnes konpilatu jakin bat da, semantika eta kontratu kriptografiko fidagarriekin.
• Konpilatutako bitarra frogatzeak Rust konpilatzailea kentzen du oinarri fidagarritik, bitar horren adierazitako propietateetarako.
• Ikertzaileek aurretik konpondutako bi akatsen berri eman dute, modu isolatuan berriro sartu direnak eta haien segurtasun-teorema sinbolikoa urratzen dutenak.
• Konparagailuak teorema eta menpeko definizio bakoitza babestutako zehaztapen onartu baten aurka egiaztatzen du; zuzenketak berrikusitako prozesu bereizi batetik pasatzen dira.

Itzulitako transkripzioa

Jatorrizko ingelesezko narraziotik itzulia. Eskuragarri dauden audioa eta azpitituluak YouTube-k kontrolatzen ditu.

Nork egiaztatzen du AI segurtasun-froga bat?

0:00 AI segurtasun-ikuskaritza batek chatbot batean fidatzea dirudi oraindik. Google-ren Signal-en emaitza berriak froga matematikoak dakartza kernel bereizi batek egiaztatzen ditu. Bideo honetan, zer frogatu zuen Google-k? Eta nola galarazten diote agente bati helburuak aldatzea? Hona hemen erantzun baliagarria. Ereduak froga hautagaiak idazten dituzte, eta Lean-ek frogak egiaztatzen ditu gizakiak onartutako aldarrikapen baten aurka, hautatutako kode konpilatuari buruz. Gizakiek oraindik dute aldarrikapena eta suposizioak.

0:21 Emaitza egiaztatu dezakezu ereduaren garaipen-hitzaldian sinetsi gabe. Egiaztapen bereizi batek galdera isilean aldatzea harrapatzen du. Definizioetaraino jarraituko dugu. Asteartea da, azaroak hamar, eta hau The Daily Diff da. AlphaProof Code Google-ren esparrua da software-zehaztapenak idazteko gizakiaren gidaritzapean eta AI agenteekin egiaztatutako frogak sortzeko. Ikerketa honek libsignal du helburu, Signal-en mezularitza inplementatzen duen Rust liburutegia, komando-lerroko programa jakin baten barruan.

0:45 Google-k lana gaur iragarri du. Bere paperak dio bost ikertzailek lau astez lan egin zutela. Agenteek frogak idatzi zituzten, eta gizakiek, berriz, ahalegin gehiena zehaztapenetan eman zuten. Betebeharrek are bilera garestiagoak bihurtzeko modu bat aurkitu dute. Zehaztapenak esaten du programak zer egin behar duen,

Nola bihurtzen da aldarrikapen bat froga-helburu?

0:59 erasotzaile batek zer kontrolatzen duen, eta argumentuak zer suposizio behar dituen. Berrikusleek galdetzen dute ea segurtasunari buruzko jendeak axola dion hori jasotzen duen. Galdera ahul bati ederki egiaztatutako erantzun batek galdera hori osorik uzten du. Taldeak Signal-en esku-hartze eta mezu-gakoaren aurreko ikerketan oinarritzen da ratchetan. Analisi formalek jadanik aztertu zituzten diseinu horiek. Google-ren aldarrikapenak haien segurtasun-argudioak lotzen ditu produkzio-liburutegi aldatugabe baten inplementazio konpilatuarekin, non diseinuak benetako kodearekin kontaktuan biziraun behar duen. Signal-eko teknologia zuzendari nagusiak, Ehren Kret-ek,

1:27 aurreko egiaztapenaren esparru txikiagoetatik haratagoko hedapen bat deskribatzen du. Inplementazio-xehetasunen artean, ordena desordenatuko mezuak daude eta atzeratutako mezuetarako artxibatutako saioak. Benetako softwareak gordetzen ditu zure diagrama dotoreak baztertu zituen agiriak. Ikertzaileek aldatugabeko Rust liburutegia konpilatzen dute estandarrarekin

Zergatik frogatu konpilatutako bitarra?

1:41 konpilatzailea Arm hirurogeita lau Linux exekutagarri batean. Haien teoremetan bitar hori deskribatzen dute instrukzio-eredu formal bat erabiliz, iturri-kodearen eta makina-kode optimizatuaren arteko hutsunea zeharkatuz. Adierazitako propietate bat hausten duen konpilatzaile-errore batek bere teorema faltsua bihurtuko luke. Konpilatzaileak, beraz, oinarri fidagarria uzten du bitar honetarako. Instrukzio-ereduan eta Lean-en egiaztatzailean fidatzen zara oraindik. Fidagarritasun-muga mugitu egin da, eta helbide bat du. Sei milioi eta erdi inguru froga-lerro egiaztatuk hogeita sei mila inguru

2:06 zehaztapen fidagarri eta instrukzio-semantika-lerroren gainean daude. Hauek artefaktu-kopuruak dira. Horietatik adimen-puntuazioak ateratzea, garatzaileak beraien nodo-modulu-karpeta tamainaren arabera sailkatzea bezalakoa da. Haien nodo-moduluen karpetaren tamainaren arabera.

Zein segurtasun-propietatek iraun zuten inplementazio-hutsunean?

2:16 Argudioek mezuen konfidentzialtasuna eta autentifikazioa hartzen dituzte, aurrerako sekretuarekin eta konpromisoaren osteko segurtasunarekin adierazitako ereduetan. Azken biek lapurtutako gakoen kaltearen mugak eta truke berrien ondoren berreskurapena deskribatzen dituzte. Berme bakoitzak erasotzaileari eta saioari buruzko baldintzak ditu. Primitive kriptografikoak kontratu fidagarrien atzean daude. Frogak suposatzen du errutina horiek zehaztutako moduan jokatzen dutela eta segurtasun kriptografikoaren suposizioetan oinarritzen da. Froga batek kriptografia idealizatzen du; besteak, berriz, erasotzailearen arrakasta-probabilitateei buruz arrazoitzen du.

2:42 Biek mugak dituzte estaltzen dituzten eszenatokietan. Galdetu zein eraikuntza, zein propietate eta zein suposizio. Emaitza hau ikertzaileen komando-lerroko arnesari dagokio. Talde-mezularitza etorkizuneko lana da, eta konputazio-ereduak baztertzen du gailu anitzeko egoera. Signal instalazio bakoitza akatsik gabea dela esateak teorema gainditzen du. Ikertzaileek aurretik konpondutako bi Signal akats berriro sartu zituzten

Zehaztapenak kode hautsi bat baztertu al dezake?

3:02 kopia isolatuetan eta konpilatu egin zituzten. Egiaztatutako frogek frogatu zuten bitar horiek segurtasun-teorema sinbolikoa urratzen zutela. Horrek probatu zuen ea zehaztapenak inplementazio akatsdun errealak baztertu zitzakeen. Zure marka berdeak proba gorri bat behar du. Google-k zehaztapenak eta frogak argitaratzen ditu egiaztapen-argibideekin batera. Biltegiak dio eraikuntza garbi batek orduak eta memoria handia behar dituela. Iragarkia irakurtzea askoz errazagoa da ordenagailu eramangarrian. Hardware-ereduak eta kontratu fidagarriek oraindik berrikuspena behar dute.

3:26 Ez dut artefaktu izugarria berreraiki atal honetarako. Argitaratutako emaitza eta haren mugak jakinarazten ari gara. Kanpotarrek ikuskatzeko bidea dute, eta hori niretzat beste AI garaipen bat baino garrantzitsuagoa da. Orain tranpa.

Froga zuzen batek erantzun okerra eman al dezake?

3:36 Lean-ek ia ezer eskatzen ez duen adierazpen baten froga zuzena onar dezake. Ezinezko suposizioek teorema hutsal bihur dezakete. Titulu nagusiaren azpian ezkutatutako definizio bat aldatzeak helburua ahuldu dezake. Paperrak horren aurkako kontrolak diseinatzen ditu. Atezainak gordeta dauka froga-agenteek idatzi ezin duten zehaztapen onartu bat. Zuzenketak proposa ditzakete zuzenketa-prozesu bereizi baten bidez. Segurtasun-ahultze bat akats potentzial gisa eskalatzen da. Probailearen arrakasta-adierazpenak ez du aginpiderik hemen.

4:00 Gizakiek fidatutako suposizioen aldaketak epaitzen dituzte, zuzenean edo haien politikaren bidez, eta zuzenketak berrikusten dituzte kanpaina bakoitzaren ondoren. Adituaren iritzia da arduraduna. Agenteak beste zeregin bat eskatu dezake. Ezin dio bere buruari gainditu kalifikazioa eman.

Zerk harrapatzen ditu mugitzen diren helburuak?

4:13 Hona hemen agindutako egiaztapena. Lean-en konparagailuak teorema eta horrek menpeko definizio guztiak konparatzen ditu babestutako kopia onartu horrekin. Onartutako axiomaak ere egiaztatzen ditu eta froga kernel berri batean errepikatzen du. Horrela, laguntzaile-definizio bat isilean ahultzeak alderatzen ari den gauza aldatzen du. Onartutako froga batek onartutako helburua ezarri behar du. Horrek gizakien ardura uzten du oraindik helburu sendo bat eta suposizio zintzoak aukeratzearen ardura. Zure AI lan-fluxurako, mantendu onarpen-irizpideak langilearen edizio-baimenetatik kanpo

4:37 eta berrikusi proposatutako aldaketak bereizita. Google-ren emaitzak banaketa hori zehatz bihurtzen du. Froga idazleak egiten du lana; egiaztapen-mugak erabakitzen du balio duen ala ez. Niri esaten entzun beharrean hau irakurtzea nahiago baduzu, diff-a zure sarrera-ontzira iristen da goizero, doan daily diff dot dev-en, beheko estekan. Beraz, gaurko epaia SHIP IT da.

Lan-fluxu hau bidaliko nuke?

4:54 Egiaztatutako froga-lan-fluxu hau bidaliko nuke, onartutako aldarrikapena agenteak ematen duen erantzunetik bereizita mantentzen delako. Emaitza bakoitzari esparrua eta suposizioak erantsita mantenduko nituzke. Harpidetu, sakatu kanpaia, eta esan iruzkinetan ezberdin zigilatuko bazenu. Eta hori da gaurko diff-a. Niko naiz Axrisi-tik. Batu arduraz.

Iturriak

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