AlphaProof kóði og merki: athugaðar öryggisprófanir vélarkóða og traustar forsendur

Það sem þetta myndband fjallar um

• Gervigreindarforrit framleiða sönnunaruppkast; kjarni Lean athugar hvort þau staðfesta formlega kröfu sem maður hefur samþykkt.
• Staðfesta markmiðið er sérstakt þýtt libsignal CLI-tengibúnaður, með traustri merkingarfræði og dulritunarsamningum.
• Með því að sanna þýdda tvíundarskrá er Rust þýðandinn fjarlægður úr traustum grunni fyrir tilgreinda eiginleika þeirrar tvíundarskrár.
• Vísindamennirnir greina frá tveimur einangruðum endurtekningum á áður löguðum villum sem brjóta í bága við táknræna öryggissetningu þeirra.
• Samanburðurinn athugar setninguna og hverja háða skilgreiningu gegn verndaðri samþykktri forskrift; breytingar fara í gegnum sérstakt endurskoðað ferli.

Þýtt afrit

Þýtt úr upprunalegri enskri frásögn. Tiltækt hljóð og textar eru stjórnaðir af YouTube.

Hver athugar öryggissönnun gervigreindar?

0:00 Öryggisúttekt á gervigreind hljómar samt eins og að treysta spjallbotni. Ný niðurstaða Google um Signal kemur með stærðfræðilegum sönnunum sem sérstakur kjarni athugar. Í þessu myndbandi, hvað sannaði Google? Og hvernig koma þeir í veg fyrir að forrit breyti markmiðum? Hér er gagnlegt svarið. Líkön skrifa drög að sönnunum, og Lean athugar sannanirnar gegn mannlega samþykktri kröfu um valinn þýddan kóða. Menn eiga enn kröfuna og forsendurnar.

0:21 Þú getur athugað niðurstöðuna án þess að trúa sigurræðu líkansins. Sérstök athugun kemur í veg fyrir að spurningunni sé breytt í laumi. Við munum fylgja henni niður í skilgreiningarnar. Það er þriðjudagur, tíundi nóvember, og þetta er The Daily Diff. AlphaProof Code er rammi Google til að skrifa hugbúnaðarforskriftir með mannlegri leiðsögn og búa til athugaðar sannanir með gervigreindarforritum. Þessi rannsókn miðar á libsignal, Rust bókasafnið sem innleiðir samskiptareglur Signal, innan sérstaks skipanalínuforrits.

0:45 Google tilkynnti verkið í dag. Í grein þess segir að fimm vísindamenn hafi unnið í fjórar vikur. Forrit skrifuðu sannanirnar, á meðan menn lögðu mestu áhersluna á forskriftirnar. Kröfur hafa fundið leið til að verða enn dýrari fundir. Forskriftin segir hvað forritið verður að gera,

Hvernig verður krafa að sönnunarmarkmiði?

0:59 hvað árásarmaður stjórnar, og hvaða forsendur röksemdin þarf. Endurskoðendur spyrja hvort hún fangi öryggi sem fólki er annt um. Fallegt athugað svar við veikri spurningu lætur þá spurningu ósnerta. Teymið byggir á fyrri rannsóknum á handabandi Signal og skilaboðalykilnum ratchet. Formlegar greiningar höfðu þegar rannsakað þessa hönnun. Krafa Google tengir öryggisrök þeirra við óbreytta framleiðslu þýðingu bókasafnsins, þar sem hönnunin þarf að lifa af snertingu við raunverulegan kóða. Tæknistjóri Signal, Ehren Kret,

1:27 lýsir útvíkkun út fyrir fyrri staðfestingar minni gildissvið. Útfærsluupplýsingar innihalda skilaboð utan röðar og geymdar fundir fyrir seinkað skilaboð. Raunverulegur hugbúnaður heldur kvittunum sem glæsilega skýringarmyndin þín henti burt. Vísindamennirnir þýða óbreytta Rust bókasafnið með staðlaða

Af hverju að sanna þýdda tvíundarskránna?

1:41 þýðandanum í Arm sextíu og fjögurra Linux keyrsluskrá. Setningar þeirra lýsa þeirri tvíundarskrá með formlegu leiðbeiningalíkani, sem nær yfir bilið milli frumkóða og fínstillts vélarkóða. Þýðandavilla sem brýtur tilgreindan eiginleika myndi gera setningu hans ranga. Þýðandinn fer því úr traustum grunni fyrir þessa tvíundarskrá. Þú treystir enn leiðbeiningalíkaninu og Lean athuguninni. Traustamörk færðust, og það hefur heimilisfang. Um sex og hálf milljón línur af athugaðri sönnun hvíla á um tuttugu og sex

2:06 þúsund traustum forskriftar- og leiðbeiningarmerkjalínum. Þetta eru talningar á verkum. Að líta á þær sem greindarvísitölu er eins og að raða þróunaraðilum eftir stærð node_modules möppunnar þeirra.

Hvaða öryggiseiginleikar lifðu af framkvæmdarmuninn?

2:16 Röksemdirnar fjalla um trúnað skilaboða og auðkenningu, með framvirku leyndarmáli og öryggi eftir málamiðlun undir tilgreindum líkönum. Þessi síðustu tvö lýsa takmörkunum á skaða af stolnum lyklum og endurheimt eftir nýjar skipti. Hver ábyrgð hefur skilyrði um árásarmanninn og fundinn. Dulritunarfrumgerðir sitja á bak við trausta samninga. Sönnunin gerir ráð fyrir að þessar venjur hegði sér eins og tilgreint er og byggir á dulritunarfræðilegum öryggisforsemdum. Ein sönnun hugsjónar dulritun; hin rökstyður um árásarárangurslíkur.

2:42 Báðar hafa takmarkanir á þeim aðstæðum sem þær ná yfir. Spurðu hvaða byggingu, hvaða eiginleika og hvaða forsendur. Þessi niðurstaða varðar skipanalínuviðmót rannsakenda. Hópaskilaboð eru framtíðarverk, og tölvufræðilega líkanið útilokar fjöltækjaástand. Að kalla allar Signal uppsetningar villulausar fer út fyrir setninguna. Rannsakendur endurkynntu tvær áður lagaðar Signal villur í

Getur forskriftin hafnað gallaðum kóða?

3:02 einangruðum afritum og þýddu þær. Athugaðar sannanir sýndu að þessar tvíundarskrár brutu gegn táknrænu öryggiskenningunni. Þetta prófaði hvort forskriftin gæti hafnað raunverulegum gölluðum útfærslum. Græni hakarinn þinn þarf rauða prófun. Google birtir forskriftirnar og sannanirnar með athugunarforskriftum. Geymslan segir að hrein bygging taki klukkustundir og umtalsvert minni. Að lesa tilkynninguna er töluvert auðveldara á fartölvunni. Vélbúnaðarlíkanið og traustir samningar þurfa enn endurskoðun.

3:26 Ég hef ekki endurbyggt hinn risastóra grip fyrir þennan þátt. Við erum að segja frá birtri niðurstöðu og mörkum hennar. Utanaðkomandi hafa leið til að skoða það, sem skiptir mig meira máli en annar AI sigurhringur. Nú gildran.

Getur rétt sönnun svarað rangri spurningu?

3:36 Lean getur tekið við réttri sönnun á staðhæfingu sem biður um næstum ekkert. Ómögulegar forsendur geta gert setningu innihaldslausa. Að breyta skilgreiningu sem er grafin undir fyrirsagnarsetningunni getur veikt markmiðið. Greinin hannar athuganir gegn þessu. Hliðvörðurinn heldur samþykktri forskrift sem sönnunarforrit geta ekki skrifað í. Þau geta lagt fram tillögur um leiðréttingar í gegnum sérstakt breytingarferli. Öryggisveikingum er fylgt eftir sem mögulegum villum. Yfirlýsing sönnunarmannsins um árangur hefur enga heimild hér.

4:00 Menn dæma um breytingar á traustum forsendum, beint eða í gegnum stefnu sína, og endurskoða breytingar eftir hverja herferð. Sérfræðidómur er enn á ábyrgð. Forritið getur óskað eftir annarri úthlutun. Það getur ekki gefið sér sjálfu nægjanlega einkunn.

Hvað kemur í veg fyrir breytingar á markmiðinu?

4:13 Hér er lofaða athugunin. Samanburður Lean ber saman setninguna og hverja skilgreiningu sem hún byggir á við þetta verndaða samþykkta afrit. Það athugar einnig leyfileg frumstæðuákvæði og endurspilar sönnunina í nýjum kjarna. Því veldur því að það að veikja í laumi hjálparskilgreiningu breytir því sem er borið saman. Samþykkt sönnun verður að staðfesta samþykkta markmiðið. Það skilur enn menn eftir ábyrga fyrir því að velja sterkt markmið og heiðarlegar forsendur. Fyrir þitt eigið gervigreindarvinnuflæði, hafðu samþykkisskilyrðin utan

4:37 breytingarheimilda starfsmannsins og endurskoðaðu tillögur um breytingar sérstaklega. Niðurstaða Google gerir þann aðskilnað áþreifanlegan. Sönnunarhöfundurinn vinnur verkið; athugunarmörk ráða hvort það teljist. Ef þú vilt frekar lesa þetta en heyra mig segja það, þá lendir diffið í pósthólfinu þínu á hverjum morgni, ókeypis á the daily diff dot dev, hlekkur hér að neðan. Svo dómur dagsins er SHIP IT.

Myndi ég nota þetta sönnunarvinnuflæði?

4:54 Ég myndi SHIP IT þetta athugaða sönnunarferli vegna þess að samþykkt krafa er aðskilin frá forritinu sem framleiðir svarið. Ég myndi halda gildissviði og forsendum tengdum hverri niðurstöðu. Gerast áskrifandi, ýttu á bjölluna, og segðu mér í athugasemdum ef þú hefðir stimplað það öðruvísi. Og það er diffið fyrir í dag. Ég er Niko frá Axrisi. Sameinast á ábyrgan hátt.

Heimildir

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