AlphaProof Code and Signal: mašinski provereni sigurnosni dokazi koda i pouzdane pretpostavke

Šta ovaj video pokriva

• AI agenti proizvode predložene dokaze; Lean-ovo jezgro proverava da li oni uspostavljaju formalnu tvrdnju koju su odobrili ljudi.
• Verifikovana meta je specifičan kompajlirani libsignal CLI alat, sa pouzdanom semantikom i kriptografskim ugovorima.
• Dokazivanje kompajliranog binarnog fajla uklanja Rust kompajler iz pouzdane osnove za navedena svojstva tog binarnog fajla.
• Istraživači izveštavaju o dva izolovana ponovna uvođenja prethodno ispravljenih grešaka koje narušavaju njihovu simboličku sigurnosnu teoremu.
• Komparator proverava teoremu i svaku zavisnu definiciju u odnosu na zaštićenu odobrenu specifikaciju; izmene prolaze kroz poseban revidirani proces.

Preveden transkript

Prevedeno sa originalne engleske naracije. Dostupan audio i titlovi kontrolisani su od strane YouTube-a.

Ko proverava AI sigurnosni dokaz?

0:00 AI sigurnosna provera i dalje zvuči kao poverenje u četbot. Google-ov novi Signal rezultat dolazi sa matematičkim dokazima koje posebno jezgro proverava. U ovom videu, šta je Google dokazao? I kako sprečavaju agenta da pomera ciljeve? Evo korisnog odgovora. Modeli pišu predložene dokaze, a Lean proverava dokaze u odnosu na tvrdnju koju su odobrili ljudi o odabranom kompajliranom kodu. Ljudi i dalje poseduju tvrdnju i pretpostavke.

0:21 Možete proveriti rezultat bez verovanja u pobednički govor modela. Posebna provera hvata tiho menjanje pitanja. Pratićemo je do definicija. Utorak je, deseti novembar, i ovo je The Daily Diff. AlphaProof Code je Google-ov okvir za pisanje softverskih specifikacija sa ljudskim vođenjem i generisanje proverenih dokaza sa AI agentima. Ova studija cilja libsignal, Rust biblioteku koja implementira Signal-ov protokol za razmenu poruka, unutar određenog programa komandne linije.

0:45 Google je danas najavio rad. Njegov rad kaže da je pet istraživača radilo četiri nedelje. Agenti su pisali dokaze, dok su ljudi većinu svog truda posvetili specifikacijama. Zahtevi su pronašli način da postanu još skuplji sastanci. Specifikacija kaže šta program mora da uradi,

Kako tvrdnja postaje meta dokazivanja?

0:59 šta napadač kontroliše i koje pretpostavke argumentu trebaju. Recenzenti pitaju da li obuhvata sigurnost do koje je ljudima stalo. Prelepo proveren odgovor na slabo pitanje ostavlja to pitanje netaknutim. Tim se nadovezuje na ranija istraživanja Signal-ovog rukovanja i njegovog ključa za poruke ratchet. Formalne analize su već proučavale te dizajne. Google-ova tvrdnja povezuje njihove sigurnosne argumente sa neizmenjenom produkcijskom kompajliranom implementacijom biblioteke, gde dizajn mora preživeti kontakt sa stvarnim kodom. Signal-ov glavni tehnički direktor, Ehren Kret,

1:27 opisuje proširenje izvan manjih opsega ranije verifikacije. Detalji implementacije uključuju poruke koje nisu po redu i arhivirane sesije za odložene poruke. Pravi softver čuva potvrde koje je vaš elegantan dijagram odbacio. Istraživači kompajliraju neizmenjenu Rust biblioteku sa standardnim

Zašto dokazivati kompajlirani binarni fajl?

1:41 kompajlerom u Arm šezdesetčetvorobitni Linux izvršni fajl. Njihove teoreme opisuju taj binarni fajl koristeći formalni model instrukcija, premošćujući jaz između izvornog i optimizovanog mašinskog koda. Greška kompajlera koja narušava navedeno svojstvo učinila bi teoremu lažnom. Kompajler stoga napušta pouzdanu osnovu za ovaj binarni fajl. I dalje verujete modelu instrukcija i Lean-ovom proverivaču. Granica poverenja se pomerila i ima adresu. Oko šest i po miliona linija proverenog dokaza počiva na otprilike dvadeset šest

2:06 hiljada pouzdanih linija specifikacije i semantike instrukcija. Ovo su brojevi artefakata. Tretiranje njih kao skorova inteligencije je kao rangiranje programera po veličini njihovog foldera node modules.

Koja su sigurnosna svojstva preživela jaz u implementaciji?

2:16 Argumenti pokrivaju poverljivost i autentičnost poruka, sa prosleđenom tajnošću i sigurnošću posle kompromisa pod navedenim modelima. Ova poslednja dva opisuju ograničenja štete od ukradenog ključa i oporavak nakon svežih razmena. Svaka garancija ima uslove za napadača i sesiju. Kriptografske primitive stoje iza pouzdanih ugovora. Dokaz pretpostavlja da te rutine funkcionišu kako je navedeno i oslanja se na kriptografske sigurnosne pretpostavke. Jedan dokaz idealizuje kriptografiju; drugi rezonuje o verovatnoćama uspeha napadača.

2:42 Obe imaju ograničenja na scenarije koje pokrivaju. Pitajte koji build, koje svojstvo i koje pretpostavke. Ovaj rezultat se odnosi na komandno-linijski alat istraživača. Grupno slanje poruka je budući rad, a računarski model isključuje stanje više uređaja. Zvanje svake Signal instalacije bez grešaka izlazi izvan teoreme. Istraživači su ponovo uveli dve prethodno ispravljene Signal greške u

Može li specifikacija odbiti pokvaren kod?

3:02 izolovane kopije i kompajlirali ih. Provereni dokazi su pokazali da ti binarni fajlovi narušavaju simboličku sigurnosnu teoremu. To je testiralo da li specifikacija može odbiti stvarne pokvarene implementacije. Vaš zeleni znak za potvrdu treba crveni test. Google objavljuje specifikacije i dokaze sa uputstvima za proveru. Repozitorijum kaže da čista izgradnja traje satima i zahteva značajnu memoriju. Čitanje objave je znatno lakše na laptopu. Model hardvera i pouzdani ugovori i dalje zahtevaju reviziju.

3:26 Nisam ponovo izgradio ogroman artefakt za ovu epizodu. Izveštavamo o objavljenom rezultatu i njegovim granicama. Spoljni ljudi imaju put da ga pregledaju, što mi je važnije od još jednog AI kruga pobede. Sada zamka.

Može li tačan dokaz odgovoriti na pogrešno pitanje?

3:36 Lean može prihvatiti ispravan dokaz izjave koja traži gotovo ništa. Nemoguće pretpostavke mogu učiniti teoremu bezvrednom. Promena definicije zakopane ispod naslovne teoreme može oslabiti cilj. Rad dizajnira provere protiv toga. Čuvar čuva odobrenu specifikaciju kojoj agenti za dokazivanje ne mogu pisati. Mogu predložiti ispravke kroz poseban proces amandmana. Sigurnosno slabljenje se eskalira kao potencijalna greška. Izjava dokazivača o uspehu ovde nema autoritet.

4:00 Ljudi donose odluke o promenama pouzdanih pretpostavki, direktno ili kroz svoju politiku, i pregledaju amandmane nakon svake kampanje. Stručno mišljenje ostaje odgovorno. Agent može zatražiti drugačiji zadatak. Ne može sebi dati prolaznu ocenu.

Šta hvata pokretne ciljeve?

4:13 Evo obećane provere. Lean-ov komparator upoređuje teoremu i svaku definiciju od koje zavisi sa tom zaštićenom odobrenom kopijom. Takođe proverava dozvoljene aksiome i ponovo izvršava dokaz u novom jezgru. Tiho slabljenje pomoćne definicije stoga menja stvar koja se upoređuje. Prihvaćen dokaz mora uspostaviti odobrenu metu. To i dalje ostavlja ljude odgovornim za odabir jake mete i iskrenih pretpostavki. Za vaš sopstveni AI tok posla, držite kriterijume prihvatanja izvan

4:37 dozvola za uređivanje radnika i pregledajte predložene promene zasebno. Google-ov rezultat konkretizuje tu separaciju. Pisac dokaza radi posao; granica provere odlučuje da li se to računa. Ako biste radije ovo pročitali nego čuli od mene, diff stiže u vaše sanduče svakog jutra, besplatno na the daily diff dot dev, link ispod. Tako da je današnja presuda SHIP IT.

Da li bih ja koristio ovaj tok posla dokazivanja?

4:54 Poslao bih ovaj tok posla sa proverenim dokazom jer odobrena tvrdnja ostaje odvojena od agenta koji proizvodi odgovor. Držao bih opseg i pretpostavke vezane za svaki rezultat. Pretplatite se, pritisnite zvonce i recite mi u komentarima da li biste ga vi drugačije odobrili. I to je diff za danas. Ja sam Niko iz Axrisi. Spajajte odgovorno.

Izvori

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