AlphaProof-kode en -sein: nagekontroleerde masjienkode-sekuriteitsbewyse en vertroude aannames

Wat hierdie video dek

• KI-agente produseer kandidaatbewyse; Lean se kern kontroleer of hulle die mens-goedgekeurde formele aanspraak vestig.
• Die geverifieerde teiken is 'n spesifieke saamgestelde libsignal CLI-harnas, met betroubare semantiek en kriptografiese kontrakte.
• Deur die gekompileerde binêre te bewys, word die Rust-samesteller van die betroubare basis vir daardie binêre se vermelde eienskappe verwyder.
• Die navorsers rapporteer twee geïsoleerde herinvoeringe van voorheen reggestelde foute wat hul simboliese sekuriteitsteorema skend.
• Die vergelyker kontroleer die teorema en alle afhanklike definisies teen 'n beskermde goedgekeurde spesifikasie; wysigings gaan deur 'n afsonderlike geresenseerde proses.

Vertaalde transkripsie

Vertaal uit die oorspronklike Engelse vertelling. Beskikbare klank en onderskrifte word deur YouTube beheer.

Wie kontroleer 'n KI-sekuriteitsbewys?

0:00 'n KI-sekuriteitsoudit klink steeds soos om 'n kletsbot te vertrou. Google se nuwe Sein-resultaat kom met wiskundige bewyse 'n aparte kern kontroleer. In hierdie video, wat het Google bewys? En hoe keer hulle 'n agent om die doelpale te skuif? Hier is die nuttige antwoord. Modelle skryf kandidaatbewyse, en Lean kontroleer die bewyse teen 'n mens-goedgekeurde aanspraak oor geselekteerde saamgestelde kode. Mense besit steeds die aanspraak en aannames.

0:21 U kan die resultaat kontroleer sonder om die model se oorwinningsrede te glo. 'n Aparte kontrole vang die stilswyende verandering van die vraag vas. Ons sal dit tot by die definisies volg. Dit is Dinsdag, tien November, en dit is The Daily Diff. AlphaProof Code is Google se raamwerk vir die skryf van sagtewarespesifikasies met menslike leiding en die generering van nagekontroleerde bewyse met KI-agente. Hierdie studie teiken libsignal, die Rust-biblioteek wat Signal se boodskappe implementeer protokol, binne 'n spesifieke opdraglynprogram.

0:45 Google het vandag die werk aangekondig. Die artikel sê vyf navorsers het oor vier weke gewerk. Agente het die bewyse geskryf, terwyl mense die meeste van hul poging aan die spesifikasies bestee het. Vereistes het 'n manier gevind om nog duurder vergaderings. Die spesifikasie sê wat die program moet doen,

Hoe word 'n aanspraak 'n bewysteiken?

0:59 wat 'n aanvaller beheer, en watter aannames die argument benodig. Beoordelaars vra of dit die sekuriteit vasvang waarvoor mense omgee. 'n Pragtig nagekontroleerde antwoord op 'n swak vraag laat daardie vraag ongeskonde. Die span bou voort op vroeëre navorsing oor Signal se handdruk en sy boodskap-sleutel ratchet. Formele analises het daardie ontwerpe reeds bestudeer. Google se aanspraak verbind hul sekuriteitsargumente met 'n ongemodifiseerde produksie biblioteek se saamgestelde implementering, waar die ontwerp kontak met werklike kode moet oorleef. Signal se hoof tegnologiebeampte, Ehren Kret,

1:27 beskryf 'n uitbreiding bo vroeëre verifikasie se kleiner omvang. Implementeringsbesonderhede sluit buite-orde boodskappe en geargiveerde sessies vir vertraagde boodskappe in. Regte sagteware hou die kwitansies wat u elegante diagram weggegooi het. Die navorsers stel die ongemodifiseerde Rust-biblioteek saam met die standaard

Waarom die gekompileerde binêre bewys?

1:41 samesteller in 'n Arm ses-en-sestig Linux-uitvoerbare program. Hul teoremas beskryf daardie binêre met behulp van 'n formele instruksiemodel, wat strek oor die gaping tussen bron en geoptimaliseerde masjienkode. 'n Samestellerfout wat 'n gestelde eienskap breek, sou sy teorema vals maak. Die samesteller verlaat dus die betroubare basis vir hierdie binêre. U vertrou steeds die instruksiemodel en Lean se kontroleerder. Die vertrouensgrens het verskuif, en dit het 'n adres. Ongeveer ses en 'n half miljoen lyne nagekontroleerde bewys rus op ongeveer ses-en-twintig

2:06 duisend vertroude spesifikasie- en instruksiesemantieklyne. Dit is artefak-tellings. Om hulle as intelligensietellings te behandel, is soos om ontwikkelaars te rangskik volgens die grootte van hul nodemodules-lêergids.

Watter sekuriteitseienskappe het die implementasiegaping oorleef?

2:16 Die argumente dek boodskapvertroulikheid en -verifikasie, met vorentoe-geheimhouding en na-kompromie-sekuriteit onder gestelde modelle. Daardie laaste twee beskryf perke op gesteelde-sleutel-skade en herstel na vars uitruilings. Elke waarborg het voorwaardes op die aanvaller en sessie. Kriptografiese primitiewe sit agter vertroude kontrakte. Die bewys aanvaar dat daardie roetines optree soos gespesifiseer en vertrou op kriptografiese sekuriteitsaannames. Een bewys idealiseer kriptografie; die ander redeneer oor aanvaller sukseswaarskynlikhede.

2:42 Beide het beperkings op die scenario's wat hulle dek. Vra watter bou, watter eienskap, en watter aannames. Hierdie resultaat het betrekking op die navorsers se opdragreël-harnas. Groepboodskappe is toekomstige werk, en die rekenkundige model sluit uit multi-toesteltoestand. Om elke Signal-installasie foutvry te noem, dwaal buite die teorema. Die navorsers het twee voorheen reggestelde Signal-foute weer ingevoer in

Kan die spesifikasie gebroke kode verwerp?

3:02 geïsoleerde kopieë en saamgestel. Gekontroleerde bewyse het getoon dat daardie binêre die simboliese sekuriteitsteorema oortree het. Dit het getoets of die spesifikasie werklike gebroke implementasies kon verwerp. Jou groen regmerkie benodig 'n rooi toets. Google publiseer die spesifikasies en bewyse met kontrole-instruksies. Die bewaarplek sê 'n skoon bou neem ure en aansienlike geheue. Om die aankondiging te lees is aansienlik makliker op die skootrekenaar. Die hardewaremodel en vertroude kontrakte benodig steeds hersiening.

3:26 Ek het nie die enorme artefak vir hierdie episode herbou nie. Ons rapporteer die gepubliseerde resultaat en sy grense. Buite-staanders het 'n pad om dit te inspekteer, wat vir my meer saak maak as nog 'n KI oorwinningsronde. Nou die strik.

Kan 'n korrekte bewys die verkeerde vraag beantwoord?

3:36 Lean kan 'n korrekte bewys van 'n stelling aanvaar wat vir amper niks vra nie. Onmoontlike aannames kan 'n teorema ydel maak. Die verandering van 'n definisie begrawe onder die hoofteorema kan die doel verswak. Die referaat ontwerp kontroles hierteen. Die poortwagter hou 'n goedgekeurde spesifikasie wat bewysagente nie kan skryf nie. Hulle kan korreksies voorstel deur 'n aparte wysigingsproses. Sekuriteitsverswakking word as 'n potensiële fout geëskaleer. Die bewyser se verklaring van sukses het geen gesag hier nie.

4:00 Mense beoordeel veranderinge aan vertroude aannames, direk of deur hul beleid, en hersien wysigings na elke veldtog. Kundige oordeel bly op die haak. Die agent kan 'n ander opdrag aanvra. Dit kan homself nie 'n slaagsyfer gee nie.

Wat vang die bewegende teikens?

4:13 Hier is die beloofde kontrole. Lean se vergelyker vergelyk die teorema en elke definisie waarvan dit afhang met daardie beskermde goedgekeurde kopie. Dit kontroleer ook toegelate aksiomas en speel die bewys in 'n vars kern af. Stilswyende verswakking van 'n hulpdefinisie verander dus die ding wat vergelyk word. 'n Aanvaarde bewys moet die goedgekeurde teiken vestig. Dit laat mense steeds verantwoordelik vir die keuse van 'n sterk teiken en eerlike aannames. Vir u eie KI-werkvloei, hou die aanvaardingskriteria buite die

4:37 werker se redigeerregte en hersien voorgestelde veranderinge afsonderlik. Google se resultaat maak daardie skeiding konkreet. Die bewysskrywer doen die werk; die kontrolegrens besluit of dit tel. As jy dit liewer wil lees as om my dit te hoor sê, land die verskil in jou inkassie gratis by the daily diff dot dev, skakel hieronder. Dus vandag se uitspraak is SHIP IT.

Sou ek hierdie bewyswerkvloei verskeep?

4:54 Ek sou hierdie nagekontroleerde-bewys-werkvloei verskeep, want die goedgekeurde aanspraak bly apart van die agent wat die antwoord produseer. Ek sou die omvang en aannames aan elke resultaat gekoppel hou. Teken in, druk die klokkie, en vertel my in die kommentaar of u dit anders sou gestempel het. En dit is die verskil vir vandag. Ek is Niko van Axrisi. Voeg verantwoordelik saam.

Bronne

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