AlphaProof Code болон Сигнал: шалгагдсан машины кодын аюулгүй байдлын баталгаа, итгэмжлэгдсэн таамаглалууд

Энэ видео юуг хамардаг

• AI агентууд нэр дэвшигч нотолгоог гаргадаг; Lean-ийн цөм нь тэдгээр нь хүний ​​баталсан албан ёсны нэхэмжлэлийг баталж буй эсэхийг шалгадаг.
• Батлагдсан зорилт нь тодорхой хөрвүүлэгдсэн libsignal CLI програм бөгөөд итгэмжлэгдсэн семантик болон криптографын гэрээтэй.
• Хөрвүүлсэн хоёртын файлыг нотлох нь Rust хөрвүүлэгчийг тухайн хоёртын файлын заасан шинж чанаруудын итгэмжлэгдсэн сууриас хасдаг.
• Судлаачид өмнө нь засагдсан, тэдний бэлгэдлийн аюулгүй байдлын теоремыг зөрчсөн хоёр тусгаарлагдсан алдааг дахин оруулсан тухай тайлагнажээ.
• Харьцуулагч нь теорем болон бүх хамааралтай тодорхойлолтыг хамгаалагдсан батлагдсан тодорхойлолтын эсрэг шалгадаг; нэмэлт өөрчлөлтүүд нь тусдаа хянан үзэх үйл явцаар дамждаг.

Орчуулсан бичлэг

Англи хэл дээрх эх хувилбараас орчуулсан. Боломжтой дуу болон хадмал орчуулгыг YouTube хянадаг.

AI аюулгүй байдлын нотолгоог хэн шалгадаг вэ?

0:00 AI аюулгүй байдлын аудит чатботод итгэхтэй адил сонсогдож байна. Google-ийн шинэ Signal-ийн үр дүн нь математик нотолгоо, тусдаа цөмтэй хамт ирдэг. шалгадаг. Энэ видеонд Google юуг баталсан бэ? Тэгээд тэд агентыг зорилгоо өөрчлөхөөс хэрхэн зогсоодог вэ? Энэ бол ашигтай хариулт. Загварууд нэр дэвшигч нотолгоог бичдэг ба Lean нь нотолгоог хүний ​​баталсан, сонгогдсон хөрвүүлсэн кодын талаарх нэхэмжлэлийн эсрэг шалгадаг. Хүмүүс нэхэмжлэл болон таамаглалыг хэвээр эзэмшдэг.

0:21 Та загварын ялалтын үгэнд итгэхгүйгээр үр дүнг шалгаж болно. Тусдаа шалгалт нь асуултыг чимээгүйхэн өөрчлөхийг илрүүлдэг. Бид үүнийг тодорхойлолтууд руу дагана. Өнөөдөр арваннэгдүгээр сарын арван, энэ бол The Daily Diff. AlphaProof Code нь Google-ийн програм хангамжийн тодорхойлолтыг хүний ​​удирдлагатайгаар бичиж, AI агентуудаар шалгагдсан нотолгоог үүсгэх хүрээ юм. Энэхүү судалгаа нь Signal-ийн мессежний протоколыг хэрэгжүүлдэг Rust сан болох libsignal-ийг тодорхой командын мөрийн програм дотор чиглүүлдэг.

0:45 Google өнөөдөр энэхүү ажлыг зарлалаа. Түүний цаасанд таван судлаач дөрвөн долоо хоногийн турш ажилласан гэж бичжээ. Агентууд нотолгоог бичсэн бол хүмүүс ихэнх хүчин чармайлтаа тодорхойлолтуудад зарцуулсан. Шаардлагууд улам үнэтэй уулзалтууд болж хувирсан. Тодорхойлолтод програм юу хийх ёстой,

Нэхэмжлэл хэрхэн нотолгооны зорилт болдог вэ?

0:59 халдлага үйлдэгч юуг хянах, маргаан ямар таамаглал шаарддагийг заасан. Шүүмжлэгчид энэ нь хүмүүсийн анхаардаг аюулгүй байдлыг илэрхийлж байгаа эсэхийг асуудаг. Сул асуултад маш сайн шалгагдсан хариулт нь тэр асуултыг хэвээр үлдээнэ. Баг нь Signal-ийн гар барилцалт болон түүний мессеж-түлхүүрийн рачетын талаарх өмнөх судалгаанууд дээр тулгуурласан. Албан ёсны шинжилгээнүүд эдгээр загваруудыг аль хэдийн судалсан. Google-ийн нэхэмжлэл нь тэдний аюулгүй байдлын аргументуудыг өөрчлөгдөөгүй үйлдвэрлэлийн сангийн хөрвүүлэгдсэн хэрэгжилттэй холбодог бөгөөд загвар нь бодит кодтой харьцахаас давж гарах ёстой. Signal-ийн технологийн ахлах захирал Ehren Kret,

1:27 өмнөх баталгаажуулалтын жижиг хүрээгээс хальсан өргөтгөлийг тайлбарлаж байна. Хэрэгжилтийн нарийвчилсан мэдээлэлд дарааллаас гадуурх мессеж болон хойшлогдсон мессежний архивлагдсан сессүүд багтдаг. Бодит програм хангамж таны гоёмсог диаграммд хаясан баримтуудыг хадгалдаг. Судлаачид өөрчлөгдөөгүй Rust санг стандарт

Яагаад хөрвүүлсэн хоёртын файлыг нотлох ёстой вэ?

1:41 хөрвүүлэгчээр Arm 64-битийн Linux гүйцэтгэгч код болгон хөрвүүлдэг. Тэдний теоремууд нь албан ёсны зааврын загварыг ашиглан тэр хоёртын файлыг тайлбарладаг, эх болон оновчтой машины кодын хоорондох зайг нөхдөг. Заасан шинж чанарыг алдагдуулсан хөрвүүлэгчийн алдаа нь түүний теоремыг худал болгоно. Иймд хөрвүүлэгч энэ хоёртын файлын итгэмжлэгдсэн сууриа орхино. Та зааврын загвар болон Lean-ийн шалгагчид хэвээр итгэдэг. Итгэлийн хил хөдөлсөн бөгөөд түүнд хаягтай. Ойролцоогоор зургаан хагас сая мөр шалгагдсан нотолгоо нь хорин зургаан

2:06 мянган итгэмжлэгдсэн тодорхойлолт болон зааврын семантикийн мөрөн дээр тулгуурладаг. Эдгээр нь бүтээгдэхүүний тоо. Тэднийг оюун ухааны оноо гэж үзэх нь хөгжүүлэгчдийг өөрсдийн "node_modules" хавтасны хэмжээгээр нь эрэмбэлэхтэй адил юм.

Хэрэгжилтийн ялгааг даван туулсан аюулгүй байдлын шинж чанарууд юу вэ?

2:16 Аргументууд нь мессежийн нууцлал болон баталгаажуулалтыг хамардаг, тогтоосон загваруудын хүрээнд урагш нууцлал болон эвдэрсний дараах аюулгүй байдалтай. Эдгээр сүүлийн хоёр нь хулгайлагдсан түлхүүрийн хохирол болон шинэ солилцооны дараах сэргээлтийн хязгаарлалтыг тайлбарладаг. Тус бүрийн баталгаа нь халдлага үйлдэгч болон сессийн нөхцөлтэй. Криптографын анхдагч элементүүд итгэмжлэгдсэн гэрээний ард байрладаг. Нотолгоо нь эдгээр рутинууд заасан ёсоор ажиллана гэж таамаглаж, криптографын аюулгүй байдлын таамаглалд тулгуурладаг. Нэг нотолгоо нь криптографийг идеалчилдаг; нөгөө нь халдлага үйлдэгчийн амжилтын магадлалын талаар үндэслэл гаргадаг.

2:42 Хоёулаа хамардаг хувилбаруудад хязгаарлалттай. Аль бүтээц, аль шинж чанар, аль таамаглал болохыг асуу. Энэ үр дүн нь судлаачдын командын мөрийн програмыг хамардаг. Бүлгийн мессеж нь ирээдүйн ажил бөгөөд тооцооллын загвар нь олон төхөөрөмжийн төлөвийг хасдаг. Signal-ийн бүх суулгалтыг алдаагүй гэж нэрлэх нь теоремоос гадуурх асуудал. Судлаачид өмнө нь засагдсан хоёр Signal-ийн алдааг

Тодорхойлолт эвдэрсэн кодыг хүлээж авахаас татгалзаж чадах уу?

3:02 тусгаарлагдсан хуулбарт дахин оруулж, хөрвүүлсэн. Шалгагдсан нотолгоонууд нь эдгээр хоёртын файлууд бэлгэдлийн аюулгүй байдлын теоремыг зөрчсөнийг харуулсан. Энэ нь тодорхойлолт бодит эвдэрсэн хэрэгжилтүүдийг үгүйсгэж чадах эсэхийг шалгасан. Таны ногоон чек тэмдэг улаан шалгалт хэрэгтэй. Google тодорхойлолт болон нотолгоог шалгах зааврын хамт нийтэлсэн. Хадгалах газар нь цэвэр бүтээц хийхэд хэдэн цаг, их хэмжээний санах ой шаарддаг гэж бичжээ. Зарлалыг унших нь зөөврийн компьютер дээр илүү хялбар. Техник хангамжийн загвар болон итгэмжлэгдсэн гэрээнд хяналт хэрэгтэй хэвээр байна.

3:26 Би энэ ангийн хувьд асар том бүтээгдэхүүнийг дахин бүтээгээгүй. Бид нийтлэгдсэн үр дүн болон түүний хил хязгаарыг тайлагнаж байна. Гадны хүмүүст үүнийг шалгах зам бий, энэ нь надад өөр AI ялалтын тойргоос илүү чухал. Одоо хавх.

Зөв нотолгоо буруу асуултад хариулж чадах уу?

3:36 Lean бараг юу ч шаардахгүй мэдэгдлийн зөв нотолгоог хүлээн зөвшөөрч чадна. Боломжгүй таамаглалууд теоремыг хоосон болгож чадна. Гарчиг теоремийн доор дарагдсан тодорхойлолтыг өөрчлөх нь зорилгыг сулруулж чадна. Энэ цаас нь үүний эсрэг шалгалтуудыг зохион бүтээсэн. Хамгаалагч нь нотолгооны агентууд бичиж чадахгүй батлагдсан тодорхойлолтыг хадгалдаг. Тэд тусдаа нэмэлт өөрчлөлтийн үйл явцаар дамжуулан засварыг санал болгож болно. Аюулгүй байдлын сулрал нь болзошгүй алдаа гэж үнэлэгддэг. Нотлогчийн амжилтын тунхаг энд ямар ч эрх мэдэлгүй.

4:00 Хүмүүс итгэмжлэгдсэн таамаглалын өөрчлөлтүүдийг шууд эсвэл өөрсдийн бодлогоор зохицуулж, кампанит ажлын дараа нэмэлт өөрчлөлтүүдийг хянадаг. Мэргэжилтний шүүлт хэвээр үлддэг. Агент өөр даалгавар хүсэж болно. Энэ нь өөрийгөө тэнцсэн гэж үнэлж чадахгүй.

Хөдөлж буй зорилгыг юу барьдаг вэ?

4:13 Энэ бол амласан шалгалт. Lean-ийн харьцуулагч нь теорем болон түүний хамааралтай бүх тодорхойлолтыг хамгаалагдсан батлагдсан хуулбартай харьцуулдаг. Энэ нь мөн зөвшөөрөгдсөн аксиомуудыг шалгаж, нотолгоог шинэ цөмд дахин тоглуулдаг. Туслах тодорхойлолтыг чимээгүйхэн сулруулах нь харьцуулж буй зүйлийг өөрчилдөг. Хүлээн зөвшөөрөгдсөн нотолгоо нь батлагдсан зорилгыг батлах ёстой. Энэ нь хүмүүсийг хүчтэй зорилго, шударга таамаглал сонгох үүрэгтэй хэвээр үлдээдэг. Өөрийн AI ажлын урсгалын хувьд хүлээн авах шалгуурыг

4:37 ажилчны засварлах зөвшөөрлөөс гадуур байлгаж, санал болгосон өөрчлөлтүүдийг тусад нь хянаарай. Google-ийн үр дүн нь энэхүү ялгааг бодит болгодог. Нотолгоо бичигч ажлыг хийдэг; шалгах хил хязгаар нь үүнийг тооцох эсэхийг шийддэг. Хэрэв та үүнийг сонсохоос илүү уншихыг хүсвэл, diff өглөө бүр таны имэйл хайрцагт үнэгүй, dailydiff.dev хаягаар, холбоос доор байна. Тиймээс өнөөдрийн шийдвэр бол SHIP IT.

Би энэ нотолгооны ажлын урсгалыг ашиглах уу?

4:54 Би энэ шалгагдсан нотолгооны ажлын урсгалыг ашиглана, учир нь батлагдсан нэхэмжлэл нь хариултыг гаргаж буй агентаас тусдаа байдаг. Би хүрээ болон таамаглалыг үр дүн бүрт хавсаргах байсан. Бүртгүүлж, хонхыг дараад, та өөрөөр тамгалсан бол сэтгэгдэл хэсэгт надад хэлээрэй. Өнөөдрийн diff энэ хүрээд. Би 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