AlphaProof Code და Signal: შემოწმებული მანქანური კოდის უსაფრთხოების მტკიცებულებები და სანდო დაშვებები

რას მოიცავს ეს ვიდეო

• AI აგენტები წარმოქმნიან კანდიდატ მტკიცებულებებს; Lean-ის ბირთვი ამოწმებს, ადასტურებენ თუ არა ისინი ადამიანის მიერ დამტკიცებულ ფორმალურ მოთხოვნას.
• დადასტურებული სამიზნე არის კონკრეტული კომპილირებული libsignal CLI აპლიკაცია, სანდო სემანტიკითა და კრიპტოგრაფიული კონტრაქტებით.
• კომპილირებული ბინარულის დამტკიცება აშორებს Rust კომპილატორს სანდო ბაზიდან ამ ბინარულის მითითებული თვისებებისთვის.
• მკვლევარები იუწყებიან ადრე გამოსწორებული შეცდომების ორ იზოლირებულ ხელახალ შემოტანას, რომლებიც არღვევენ მათ სიმბოლურ უსაფრთხოების თეორემას.
• კომპარატორი ამოწმებს თეორემას და ყოველ დამოკიდებულ განმარტებას დაცული დამტკიცებული სპეციფიკაციის მიმართ; ცვლილებები გადის ცალკეულ გადამოწმებულ პროცესში.

ნათარგმნი ტრანსკრიპტი

ნათარგმნია ორიგინალური ინგლისური ნარატივიდან. ხელმისაწვდომი აუდიო და სუბტიტრები კონტროლდება YouTube-ის მიერ.

ვინ ამოწმებს AI უსაფრთხოების მტკიცებულებას?

0:00 AI უსაფრთხოების აუდიტი კვლავ ჩატბოტის ნდობას ჰგავს. Google-ის ახალ Signal-ის შედეგს მოყვება მათემატიკური მტკიცებულებები ცალკეული ბირთვი ამოწმებს. ამ ვიდეოში, რა დაამტკიცა Google-მა? და როგორ აჩერებენ ისინი აგენტს მიზნების გადაადგილებას? აი, სასარგებლო პასუხი. მოდელები წერენ კანდიდატ მტკიცებულებებს, და Lean ამოწმებს მტკიცებულებებს ადამიანის მიერ დამტკიცებულ მოთხოვნასთან შერჩეული კომპილირებული კოდის შესახებ. ადამიანები კვლავ ფლობენ მოთხოვნას და დაშვებებს.

0:21 შეგიძლიათ შეამოწმოთ შედეგი მოდელის გამარჯვების სიტყვის დაჯერების გარეშე. ცალკეული შემოწმება იჭერს კითხვის ჩუმად შეცვლას. ჩავყვებით მას განმარტებებამდე. სამშაბათია, ათი ნოემბერი, და ეს არის The Daily Diff. AlphaProof Code არის Google-ის ჩარჩო პროგრამული უზრუნველყოფის სპეციფიკაციების დასაწერად ადამიანის ხელმძღვანელობით და შემოწმებული მტკიცებულებების გენერირებისთვის AI აგენტებით. ეს კვლევა მიზნად ისახავს libsignal-ს, Rust ბიბლიოთეკას, რომელიც ახორციელებს Signal-ის შეტყობინებების პროტოკოლს, კონკრეტულ ბრძანების ხაზის პროგრამაში.

0:45 Google-მა დღეს გამოაცხადა ნამუშევარი. მის ნაშრომში ნათქვამია, რომ ხუთმა მკვლევარმა იმუშავა ოთხი კვირის განმავლობაში. აგენტებმა დაწერეს მტკიცებულებები, ხოლო ადამიანებმა თავიანთი ძალისხმევის უმეტესი ნაწილი დახარჯეს სპეციფიკაციებზე. მოთხოვნებმა იპოვეს გზა, რომ კიდევ უფრო ძვირიანი შეხვედრები გამხდარიყვნენ. სპეციფიკაცია ამბობს, რა უნდა გააკეთოს პროგრამამ,

როგორ ხდება მოთხოვნა მტკიცებულების სამიზნედ?

0:59 რას აკონტროლებს თავდამსხმელი, და რა დაშვებები სჭირდება არგუმენტს. რეცენზენტები კითხულობენ, ასახავს თუ არა ის უსაფრთხოებას, რაც ხალხს აინტერესებს. სუსტ კითხვაზე ლამაზად შემოწმებული პასუხი ამ კითხვას ხელუხლებლად ტოვებს. გუნდი ეფუძნება Signal-ის ხელჩართულობისა და მისი შეტყობინების გასაღების ჩამკეტის ადრეულ კვლევას. ფორმალურმა ანალიზებმა უკვე შეისწავლეს ეს დიზაინები. Google-ის მოთხოვნა აკავშირებს მათ უსაფრთხოების არგუმენტებს შეუცვლელ წარმოების ბიბლიოთეკის კომპილირებულ იმპლემენტაციასთან, სადაც დიზაინმა უნდა გაუძლოს კონტაქტს რეალურ კოდთან. Signal-ის ტექნოლოგიური დირექტორი, ერენ კრეტი,

1:27 აღწერს გაფართოებას ადრეული ვერიფიკაციის უფრო მცირე ფარგლებს მიღმა. იმპლემენტაციის დეტალები მოიცავს არასწორი თანმიმდევრობით შეტყობინებებს და არქივირებულ სესიებს დაგვიანებული შეტყობინებებისთვის. რეალური პროგრამული უზრუნველყოფა ინახავს ქვითრებს, რომლებიც თქვენმა ელეგანტურმა დიაგრამამ გადააგდო. მკვლევარები კომპილირებენ შეუცვლელ Rust ბიბლიოთეკას სტანდარტული

რატომ უნდა დამტკიცდეს კომპილირებული ბინარული?

1:41 კომპილატორით Arm 64 Linux შესრულებად ფაილად. მათი თეორემები აღწერს ამ ბინარულ ფაილს ფორმალური ინსტრუქციის მოდელის გამოყენებით, წყაროსა და ოპტიმიზებულ მანქანურ კოდს შორის არსებული ხარვეზის გადალახვით. კომპილატორის შეცდომა, რომელიც არღვევს მითითებულ თვისებას, მის თეორემას ცრუს გახდის. ამიტომ, კომპილატორი ტოვებს სანდო ბაზას ამ ბინარული ფაილისთვის. თქვენ მაინც ენდობით ინსტრუქციის მოდელს და Lean-ის შემოწმებას. ნდობის საზღვარი გადაინაცვლა, და მას აქვს მისამართი. დაახლოებით ექვსნახევარი მილიონი ხაზი შემოწმებული მტკიცებულება ეფუძნება დაახლოებით ოცდაექვსი

2:06 ათას სანდო სპეციფიკაციის და ინსტრუქციის სემანტიკის ხაზს. ეს არის არტეფაქტების რაოდენობა. მათი ინტელექტის ქულებად განხილვა ჰგავს დეველოპერების რანჟირებას მათი node modules საქაღალდის ზომის მიხედვით. მათი 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