Newsletter Subscribe
Enter your email address below and subscribe to our newsletter
[forminator_form id="25163"]

wired.com.wired.com.wired.com.„Google DeepMind“, priklausančios „Alphabet Inc.“ , tyrėjai panaudojo naują dirbtinio intelekto sistemą „AlphaProof Code“, kad matematiškai įrodytų kelias pagrindines „Signal“ protokolo kriptografines garantijas. Kaip lapkričio 10 d. pranešė „WIRED“, per keturias savaites trukusį koncepcijos įrodymo projektą nebuvo rasta jokių naujų pažeidžiamumų nagrinėtose protokolo dalyse.wired.com
Šis rezultatas svarbus ne tik „Signal“ programėlei. Protokolas taip pat apsaugo pranešimus „Google Messages“ ir „WhatsApp“, priklausančiose „Meta Platforms, Inc.“ , todėl ši analizė suteikia dar vieną nepriklausomą patikrinimą šifravimui, kuris apsaugo didelę dalį pasaulio komunikacijos, teigia „WIRED“. Tai taip pat rodo, kad dirbtinio intelekto agentai gali pagreitinti formalųjį patikrinimą – ilgai siektą, bet lėtą būdą naudojant matematiką įrodyti, kad programinė įranga veikia taip, kaip numatyta.wired.com
Tyrėjai išbandė „AlphaProof Code“ su senesnėmis „Signal“ versijomis, kuriose buvo žinomų pažeidžiamumų, seniai ištaisytų. Įrankis teisingai aptiko tuos trūkumus ir parodė, kad tų versijų nebuvo galima formaliai patikrinti, pranešė „WIRED“. „DeepMind“ viešina specifikaciją ir sukurtą įrodymą, kad kitos tikrinimo iniciatyvos galėtų jais pasinaudoti.wired.com
Apimtis buvo ribota. Darbas neapėmė visos „Signal“ mobiliosios programėlės, o tyrėjai tai apibūdino kaip vieną etapą ilgesniame procese. „Esame labai patenkinti šiuo rezultatu, tačiau dar ilgas kelias iki tol, kol galėsime tai pritaikyti visai pasaulio programinei įrangai, ir mes norime tai padaryti“, – „WIRED“ sakė „DeepMind“ mokslininkas Swaratas Chaudhuri.wired.com
Komanda teigė, kad ankstesnis „Signal“ atliktas formalusis patikrinimas suteikė pranašumą. „Nors ankstesnis formalusis patikrinimas buvo sutelktas į mažesnes kodo dalis, „Google DeepMind“ metodas leidžia reikšmingai plėstis“, – pranešime teigė „Signal“ technologijų vadovas Ehrenas Kretas, pridurdamas, kad patikrinimas suteikia įmonei „dar didesnį pasitikėjimą“, augant dirbtinio intelekto keliamoms saugumo grėsmėms.wired.com
„DeepMind“ darbas pasirodė tuo metu, kai kitos grupės siekia panašių tikslų. 2026 m. balandį „Signal“, „Beneficial AI Foundation“ ir „Lean FRO“ pradėjo „Signal Shot“ – viešą iniciatyvą, skirtą patikrinti „Signal“ protokolą ir jo „Rust“ įgyvendinimą naudojant „Lean“ įrodymų asistentą. Pasak fondo, projektas siekia išversti tikrąjį „Signal“ kodą į „Lean“ ir įrodyti, kad jis atitinka patikrintą protokolo modelį. „DeepMind“ rezultatas yra atskiras nuo to projekto, pažymėjo „Startup Fortune“.beneficialaifoundation.org+2
Vis dar neaišku, ar dirbtinio intelekto automatizuotas patikrinimas gali būti pritaikytas už priimtiną kainą. „DeepMind“ atliko „Signal“ analizę nemokamai kaip mokslinį projektą. „Google“ atsisakė atskleisti, kiek tai kainavo ir ar planuoja komercinį tikrinimo produktą, pranešė „WIRED“.wired.com
S. Chaudhuri teigė, kad pagrindinė pažanga buvo procesas, kuriame dirbtinio intelekto agentai prisideda ir patys taiso savo darbą, o žmonės jį peržiūri svarbiais momentais. „Mes nenorime tokio pasaulio, kur dirbtinis intelektas generuoja tikslus, dirbtinis intelektas generuoja įrodymus ir iš esmės laiko testus, kuriuos pats parašė“, – sakė jis. „Yra vidurio kelias.“wired.com