AlphaProof Code-მ Signal-ის კრიპტოგრაფიული ბირთვი ოთხ კვირაში გადაამოწმა

Google DeepMind-მა წარმოადგინა AlphaProof Code, AI სისტემა, რომელიც მათემატიკურად ამტკიცებს, რომ პროგრამული უზრუნველყოფა უშეცდომოდ აკმაყოფილებს უსაფრთხოების სპეციფიკაციებს. მკვლევარებმა ის Signal-ის დაშიფვრის პროტოკოლზე გამოსცადეს და ოთხ კვირაში დაასრულეს სამუშაო, რომელსაც ჩვეულებრივ წლები სჭირდება. სისტემამ გადაამოწმა მომხმარებლების მოწყობილობებზე მოქმედი კრიპტოგრაფიული ბირთვის რეალური კოდი და არა მხოლოდ თეორიული დიზაინი.

როგორ წარიმართა გადამოწმება

მას შემდეგ, რაც ექსპერტებმა უსაფრთხოების ფორმალური მოთხოვნები განსაზღვრეს, Gemini Carbon-ზე დაფუძნებულმა AI აგენტებმა Lean-ის დამტკიცების ენაზე ექვს მილიონზე მეტი სტრიქონი დაწერეს. მათ კოდბაზის დაახლოებით 1% ხელით გადასამოწმებლად მონიშნეს. ტესტირებისთვის განზრახ ჩასმული ორი ხარვეზი მაშინვე გამოვლინდა. AlphaProof Code-ში AI აგენტები ასევე ეხმარებიან სპეციფიკაციების შექმნაში და შემდეგ დამოუკიდებლად ამტკიცებენ, რომ პროგრამის კოდი მათ აკმაყოფილებს.

უფრო ფართო შედეგები

DeepMind-ის მკვლევრების Pushmeet Kohli-სა და Swarat Chaudhuri-ს ბლოგპოსტის მიხედვით, ადრინდელი გადამოწმების მცდელობები თეორიული დიზაინის ეტაპზე ჩერდებოდა. Signal-ის CTO Ehren Kret-მა თქვა, რომ ეს მიდგომა აძლიერებს ნდობას მონაცემთა კონფიდენციალურობის მიმართ, რადგან AI საფრთხეები იზრდება. DeepMind გეგმავს მეთოდის გავრცელებას ელექტროქსელებსა და სამედიცინო მოწყობილობებზე CodeMender-ის მსგავსი სისტემების მეშვეობით.

წყაროები: The Decoder