# AlphaProof Code va Signal: tekshirilgan mashina-kod xavfsizlik isbotlari va ishonchli farazlar

Published: 2026-11-11

Google DeepMind kompaniyasi tanlangan xavfsizlik xususiyatlari boʻyicha kompilyatsiya qilingan libsignal buyruq qatori jabdugʻi uchun mashina tomonidan tekshirilgan isbotlarni eʼlon qildi. Lean isbotni tekshiradi, insonlar esa spetsifikatsiya va uning farazlarini tasdiqlaydi. Alohida taqqoslagich teorema va barcha bogʻliq taʼriflarni tasdiqlangan maqsadga qarshi tekshiradi.

Canonical: https://thedailydiff.dev/uz/video/2026-11-10-signal-machine-proof/

## Bu video nimani qamrab oladi

- AI agentlari nomzod isbotlarni ishlab chiqaradi; Lean yadrosi ularning inson tomonidan tasdiqlangan rasmiy daʼvoni tasdiqlaganligini tekshiradi.
- Tasdiqlangan maqsad maʼlum bir kompilyatsiya qilingan libsignal CLI jabdugʻi boʻlib, u ishonchli semantika va kriptografik shartnomalarga ega.
- Kompilyatsiya qilingan ikkilik faylni isbotlash Rust kompilyatorini ushbu ikkilik faylning belgilangan xususiyatlari uchun ishonchli bazadan olib tashlaydi.
- Tadqiqotchilar oʻzlarining ramziy xavfsizlik teoremasini buzadigan, avval tuzatilgan ikki xatoning alohida qayta kiritilishini maʼlum qilishdi.
- Taqqoslagich teorema va har bir bogʻliq taʼrifni himoyalangan tasdiqlangan spetsifikatsiyaga qarshi tekshiradi; tuzatishlar alohida koʻrib chiqish jarayonidan oʻtadi.

## Savollar va javoblar

### AlphaProof Code Signalning implementatsiyasi haqida nimani isbotladi?

Google DeepMind kompaniyasi kompilyatsiya qilingan libsignal buyruq qatori jabdugʻi uchun tanlangan xavfsizlik xususiyatlarining tekshirilgan isbotlarini maʼlum qildi. Texnik maqola xabar maxfiyligi va autentifikatsiyasini, belgilangan modellar boʻyicha oldinga maxfiylik va buzilishdan keyingi xavfsizlikni oʻz ichiga oladi. Natija hujumchi, sessiya va kriptografik farazlar boʻyicha shartlarni saqlab qoladi. Uning doirasi har bir Signal ilovasi yoki oʻrnatilishi uchun umumiy kafolatni istisno qiladi.

### AI tomonidan yaratilgan xavfsizlik isboti nimani tasdiqlashi kerakligini kim hal qiladi?

Inson koʻrib chiquvchilar spetsifikatsiya va uning farazlarini tasdiqlaydi. Google DeepMindning texnik maqolasida agentlar inson rahbarligi bilan spetsifikatsiyalarni tuzishlari va koʻrib chiquvchilar bayonotlar maʼnoli xavfsizlik xususiyatlarini qamrab olganligini sinovdan oʻtkazishlari tasvirlangan. Lean natijada paydo boʻlgan isbotning mantiqini tekshiradi. Insonlar kuchli maqsadni tanlash, farazlarni koʻrib chiqish va tasdiqlangan spetsifikatsiyaga taklif qilingan oʻzgarishlarni hal qilish uchun masʼul boʻlib qoladilar.

### Nima uchun Rust kompilyatoriga ishonish oʻrniga kompilyatsiya qilingan mashina kodini tekshirish kerak?

Kompilyatsiya qilingan ikkilik fayl haqidagi isbot ushbu artefakt uchun belgilangan xususiyatlarni bevosita tasdiqlaydi. Google DeepMindning maqolasida tushuntirilishicha, ushbu xususiyatlardan birini buzadigan kompilyator xatosi teoremani notoʻgʻri qiladi. Shu sababli Rust kompilyatori ushbu daʼvo uchun ishonchli bazadan chiqadi. Isbot hali ham koʻrsatmalar modeliga, Lean yadrosiga va belgilangan kriptografik shartnomalarga ishonadi.

### Taqqoslagich isbot agentining oʻz maqsadini zaiflashtirishini qanday toʻxtatadi?

Taqqoslagich teorema va u bogʻliq boʻlgan har bir taʼrifni himoyalangan tasdiqlangan spetsifikatsiyaga qarshi tekshiradi. Google DeepMindning maqolasida aytilishicha, isbot agentlari ushbu saqlanib qolgan nusxaga yozishga qodir emas. Tekshiruvchi shuningdek ruxsat etilgan aksiyomalarni tekshiradi va isbotni yangi yadroida qayta ijro etadi. Taklif qilingan spetsifikatsiya tuzatishlari alohida koʻrib chiqish jarayonidan oʻtadi, insonlar esa maqsadning mustahkamligi uchun masʼul boʻlib qoladilar.

### The Daily Diff'ning tekshirilgan isbot ish jarayoni haqidagi hukmi qanday boʻldi?

The Daily Diff'ning hukmi SHIP IT boʻldi. Niko tekshirilgan isbot ish jarayonini SHIP qilar edi, chunki tasdiqlangan daʼvo javobni ishlab chiqaruvchi agentdan alohida qoladi. U har bir natijaga doira va farazlarni biriktirib qolar edi. Epizod Googlening eʼlon qilingan isbot artefaktini mustaqil ravishda qayta qurmasdan xabar beradi va ushbu dalil chegaralari ichidagi ish jarayonini tasdiqlaydi.

## Boblar

- 0:00 AI xavfsizlik isbotini kim tekshiradi?
- 0:57 Daʼvo qanday qilib isbotlash maqsadiga aylanadi?
- 1:39 Nima uchun kompilyatsiya qilingan ikkilik faylni isbotlash kerak?
- 2:16 Qaysi xavfsizlik xususiyatlari implementatsiya boʻshligʻidan omon qoldi?
- 2:59 Spetsifikatsiya buzilgan kodni rad eta oladimi?
- 3:36 Toʻgʻri isbot notoʻgʻri savolga javob bera oladimi?
- 4:13 Harakatlanuvchi maqsadlarni nima ushlab turadi?
- 4:53 Men bu isbot ish jarayonini SHIP qilar edimmi?

## Tarjima qilingan transkript

Asl inglizcha hikoyadan tarjima qilingan. Mavjud audio va subtitrlar YouTube tomonidan boshqariladi.

### AI xavfsizlik isbotini kim tekshiradi?

0:00 AI xavfsizlik auditi hali ham chatbotga ishonish kabi eshitiladi. Googlening yangi Signal natijasi alohida yadro tomonidan tekshiriladigan matematik isbotlar bilan birga keladi. Bu videoda Google nimani isbotladi? Va ular agentning maqsadlarni oʻzgartirishini qanday toʻxtatadilar? Mana foydali javob. Modellar nomzod isbotlarni yozadi va Lean isbotlarni tanlangan kompilyatsiya qilingan kod haqidagi inson tomonidan tasdiqlangan daʼvoga qarshi tekshiradi. Insonlar hali ham daʼvo va farazlarga egalik qiladi. Siz modelning gʻalaba nutqiga ishonmasdan natijani tekshirishingiz mumkin.

0:21 Alohida tekshiruv savolni jim oʻzgartirishni ushlab turadi. Biz buni taʼriflargacha kuzatib boramiz. Bugun seshanba, oʻn noyabr va bu The Daily Diff. AlphaProof Code bu Googlening inson rahbarligi bilan dasturiy taʼminot spetsifikatsiyalarini yozish va AI agentlari bilan tekshirilgan isbotlarni yaratish uchun moʻljallangan tizimidir. Ushbu tadqiqot Signalning xabarlashuv protokolini amalga oshiruvchi Rust kutubxonasi boʻlgan libsignalni maʼlum bir buyruq qatori dasturi ichida maqsad qiladi. Google bugun bu ishni eʼlon qildi. Uning maqolasida besh nafar tadqiqotchi toʻrt hafta davomida ishlaganligi aytiladi. Agentlar isbotlarni yozgan, insonlar esa oʻzlarining koʻp kuchlarini spetsifikatsiyalarga sarflashgan. Talablar yanada qimmatroq uchrashuvlarga aylanish yoʻlini topdi.

0:45 Spetsifikatsiya dastur nima qilishi kerakligini, hujumchi nimani nazorat qilishini va dalilga qaysi farazlar kerakligini aytadi. Koʻrib chiquvchilar bu xavfsizlikni odamlar qiziqtiradigan darajada qamrab olganmi yoki yoʻqmi deb soʻraydilar. Zaif savolga chiroyli tekshirilgan javob oʻsha savolni oʻzgarishsiz qoldiradi. Jamoa Signalning kelishuviga va uning xabar kaliti ratchetiga oid avvalgi tadqiqotlarga asoslanadi. Rasmiy tahlillar allaqachon bu dizaynlarni oʻrganib chiqqan.

### Daʼvo qanday qilib isbotlash maqsadiga aylanadi?

0:59 Googlening daʼvosi ularning xavfsizlik argumentlarini oʻzgartirilmagan ishlab chiqarish kutubxonasining kompilyatsiya qilingan implementatsiyasi bilan bogʻlaydi, bu yerda dizayn haqiqiy kod bilan aloqani saqlab qolishi kerak. Signalning texnik direktori Ehren Kret avvalgi verifikatsiyaning kichikroq doiralaridan tashqariga kengayishni tasvirlaydi. Implementatsiya tafsilotlari tartibsiz xabarlar va kechiktirilgan xabarlar uchun arxivlangan sessiyalarni oʻz ichiga oladi. Haqiqiy dasturiy taʼminot sizning nafis diagrammangiz tashlab yuborgan kvitansiyalarni saqlaydi. Tadqiqotchilar oʻzgartirilmagan Rust kutubxonasini standart kompilyator bilan Arm oltmish toʻrt Linux ijro etiluvchisiga kompilyatsiya qiladilar. Ularning teoremalari manba va optimallashtirilgan mashina kodi orasidagi boʻshliqni kesib oʻtib, ushbu ikkilik faylni rasmiy koʻrsatmalar modeli yordamida tasvirlaydi. Belgilangan xususiyatni buzadigan kompilyator xatosi uning teoremasini notoʻgʻri qiladi. Shu sababli kompilyator ushbu ikkilik fayl uchun ishonchli bazadan chiqadi.

1:27 Siz hali ham koʻrsatmalar modeliga va Lean tekshiruvchisiga ishonasiz. Ishonch chegarasi oʻzgardi va uning manzili bor. Taxminan olti yarim million qator tekshirilgan isbot yigirma olti mingga yaqin ishonchli spetsifikatsiya va koʻrsatmalar-semantika qatorlariga asoslanadi. Bular artefakt hisoblari. Ularni aql ballari deb hisoblash dasturchilarni ularning node\_modules papkasi hajmi boʻyicha baholashga oʻxshaydi.

### Nima uchun kompilyatsiya qilingan ikkilik faylni isbotlash kerak?

1:41 Dalillar xabar maxfiyligi va autentifikatsiyasini oʻz ichiga oladi, belgilangan modellar boʻyicha oldinga maxfiylik va buzilishdan keyingi xavfsizlik bilan. Oxirgi ikkitasi oʻgʻirlangan kalit zarari va yangi almashinuvlardan keyin tiklanish chegaralarini tasvirlaydi. Har bir kafolat hujumchi va sessiya boʻyicha shartlarga ega. Kriptografik primitivlar ishonchli shartnomalar ortida turadi. Isbot ushbu tartiblar belgilanganidek harakat qilishini faraz qiladi va kriptografik xavfsizlik farazlariga tayanadi. Bir isbot kriptografiyani ideallashtiradi; boshqasi hujumchi muvaffaqiyat ehtimolliklari haqida fikr yuritadi. Ikkalasi ham ular qamrab oladigan stsenariylarga cheklovlarga ega. Qaysi tuzilma, qaysi xususiyat va qaysi farazlar haqida soʻrang.

2:06 Bu natija tadqiqotchilarning buyruq qatori jabdugʻiga tegishli. Guruhli xabarlar kelajakdagi ish hisoblanadi va hisoblash modeli koʻp qurilmali holatni istisno qiladi. Har bir Signal oʻrnatilishini xatosiz deb atash teoremadan tashqariga chiqadi. Tadqiqotchilar avval tuzatilgan ikkita Signal xatosini alohida nusxalarga qayta kiritdilar va ularni kompilyatsiya qildilar.

### Qaysi xavfsizlik xususiyatlari implementatsiya boʻshligʻidan omon qoldi?

2:16 Tekshirilgan isbotlar bu ikkilik fayllar ramziy xavfsizlik teoremasini buzganligini koʻrsatdi. Bu spetsifikatsiya haqiqiy buzilgan implementatsiyalarni rad eta oladimi yoki yoʻqmi sinovdan oʻtkazdi. Sizning yashil belgiz red testga muhtoj. Google spetsifikatsiyalarni va isbotlarni tekshirish koʻrsatmalari bilan eʼlon qiladi. Repozitoriya toza tuzilma soatlar va katta xotira talab qilishini aytadi. Eʼlonni oʻqish noutbukda ancha oson. Uskuna modeli va ishonchli shartnomalar hali ham koʻrib chiqishga muhtoj. Men ushbu epizod uchun ulkan artefaktni qayta qurmadim.

2:42 Biz eʼlon qilingan natija va uning chegaralari haqida xabar beramiz. Tashqaridagilar uni tekshirish uchun yoʻlga ega, bu menga boshqa AI gʻalaba raqsidan koʻproq ahamiyatli. Endi tuzoq. Lean deyarli hech narsa talab qilmaydigan bayonotning toʻgʻri isbotini qabul qilishi mumkin. Imkonsiz farazlar teoremani mazmunsiz qilib qoʻyishi mumkin. Sarlavha teoremasi ostiga koʻmilgan taʼrifni oʻzgartirish maqsadni zaiflashtirishi mumkin. Maqola bunga qarshi tekshiruvlarni yaratadi.

### Spetsifikatsiya buzilgan kodni rad eta oladimi?

3:02 Darvozabon isbot agentlari yozishga qodir boʻlmagan tasdiqlangan spetsifikatsiyani saqlaydi. Ular alohida tuzatish jarayoni orqali tuzatishlar taklif qilishlari mumkin. Xavfsizlikning zaiflashuvi potentsial xato sifatida koʻrib chiqiladi. Isbotlovchining muvaffaqiyat haqidagi eʼlonining bu yerda hech qanday vakolati yoʻq. Insonlar ishonchli farazlarga oʻzgarishlarni bevosita yoki oʻz siyosatlari orqali hal qiladilar va har bir kampaniyadan keyin tuzatishlarni koʻrib chiqadilar. Mutaxassisning hukmi javobgarlikda qoladi. Agent boshqa topshiriqni soʻrashi mumkin. U oʻziga oʻtish bahosini bera olmaydi.

3:26 Mana vaʼda qilingan tekshiruv. Lean taqqoslagichi teorema va u bogʻliq boʻlgan har bir taʼrifni himoyalangan tasdiqlangan nusxa bilan taqqoslaydi. U shuningdek ruxsat etilgan aksiyomalarni tekshiradi va isbotni yangi yadroida qayta ijro etadi. Shu sababli yordamchi taʼrifni jim zaiflashtirish taqqoslanayotgan narsani oʻzgartiradi.

### Toʻgʻri isbot notoʻgʻri savolga javob bera oladimi?

3:36 Qabul qilingan isbot tasdiqlangan maqsadni tasdiqlashi kerak. Bu hali ham kuchli maqsadni tanlash va halol farazlarni tanlash uchun insonlarni masʼul qoldiradi. Oʻzingizning AI ish jarayonlaringiz uchun qabul qilish mezonlarini ishchining tahrir ruxsatlaridan tashqarida saqlang va taklif qilingan oʻzgarishlarni alohida koʻrib chiqing. Googlening natijasi bu ajratishni aniq qiladi. Isbot yozuvchi ishni bajaradi; tekshirish chegarasi u hisobga olinadimi yoki yoʻqmi hal qiladi. Agar buni eshitishdan koʻra oʻqishni afzal koʻrsangiz, diff har kuni ertalab sizning pochta qutingizga keladi, daily diff dot dev manzilida bepul, pastdagi havola. Shunday qilib, bugungi hukm SHIP IT.

4:00 Men bu tekshirilgan isbot ish jarayonini SHIP qilar edim, chunki tasdiqlangan daʼvo javobni ishlab chiqaruvchi agentdan alohida qoladi. Men har bir natijaga doira va farazlarni biriktirib qolar edim. Obuna boʻling, qoʻngʻiroqni bosing va agar siz boshqacha qilib muhrlagan boʻlsangiz, izohlarda menga ayting. Va bugun uchun diff shunday. Men Axrisidan Nikoman.

### Harakatlanuvchi maqsadlarni nima ushlab turadi?

4:13 Masʼuliyat bilan birlashtiring. Assalomu alaykum Hurmatli tomoshabinlar Bugun men siz bilan juda qiziqarli va muhim mavzu haqida gaplashmoqchiman. Bu mavzu

4:37 AlphaProof Code va Signal mashina-kod xavfsizlik isbotlari va ishonchli farazlar haqida. Google DeepMind kompaniyasi tanlangan xavfsizlik xususiyatlari boʻyicha kompilyatsiya qilingan libsignal

### Men bu isbot ish jarayonini SHIP qilar edimmi?

4:54 buyruq qatori jabdugʻi uchun mashina tomonidan tekshirilgan isbotlarni eʼlon qildi. Lean isbotni tekshiradi, insonlar esa spetsifikatsiya va uning farazlarini tasdiqlaydi. Alohida taqqoslagich teorema va barcha bogʻliq taʼriflarni tasdiqlangan maqsadga qarshi tekshiradi. Bu juda katta yutuqdir.

## Manbalar

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [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 endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [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 claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub