Google DeepMind: Η τεχνητή νοημοσύνη απέδειξε μαθηματικά την ασφάλεια του πρωτοκόλλου Signal

Η Google DeepMind δημιούργησε πράκτορα τεχνητής νοημοσύνης για να αποδείξει μαθηματικά τις εγγυήσεις ασφαλείας του πρωτοκόλλου Signal.

Η μαθηματική προσέγγιση χρησιμοποιήθηκε από τους ερευνητές της Google DeepMind προκειμένου να εφαρμοστεί στα κρυπτογραφικά μοντέλα της εταιρείας μια τυπική επαλήθευση (formal verification), σύμφωνα με σχετικό άρθρο στο Wired.

Η διπλή σημασία της διαδικασίας

Η τυπική αυτή επαλήθευση στηρίχθηκε στη λογική ενός proof-of-concept, δηλαδή ενός δοκιμαστικού έργου μικρής κλίμακας μέσα από το οποίο αποδεικνύεται αν ένα προϊόν ή μια υπηρεσία μπορεί πράγματι να δουλέψει.

Βέβαια η Google DeepMind δεν εφάρμοσε τη συγκεκριμένη διαδικασία για ολόκληρη την εφαρμογή του Signal, αλλά μόνο για τις κρυπτογραφικές εγγυήσεις του πρωτοκόλλου της.

Η επαλήθευση διήρκησε τέσσερις εβδομάδες, έχοντας διττή σημασία, αφού, αφενός επιβεβαιώνει ανεξάρτητα για ακόμη μία φορά την κρυπτογραφία που προστατεύει τεράστιο όγκο επικοινωνιών παγκοσμίως και, αφετέρου, αναδεικνύει τις δυνατότητες της Google DeepMind στην τυπική επαλήθευση με ένα νέο πλαίσιο τεχνητής νοημοσύνης, το AlphaProof Code.

Ποιο πλεονέκτημα προσφέρει η χρήση της τεχνητής νοημοσύνης

Οι υποστηρικτές της τυπικής επαλήθευσης την χαρακτηρίζουν ως ένα είδος «ιερού δισκοπότηρου», παρόλο που ακόμα δεν έχει γίνει σαφές το πόσο πρακτική θα είναι για ευρεία χρήση και πόσο αποτελεσματικά μπορεί να ασφαλίσει μεγάλους όγκους κώδικα.

Μέχρι πρότινος, για την διεκπεραίωση της διαδικασίας απαιτούνταν ιδιαίτερα πολύς χρόνος, αφού οι άνθρωποι έπρεπε να περιγράψουν τα χαρακτηριστικά του λογισμικού που ήθελαν να αποδείξουν, να μετατρέψουν αυτές τις περιγραφές σε μαθηματικούς τύπους και στη συνέχεια να αναπτύξουν την απόδειξη.

Με τη βοήθεια της τεχνητής νοημοσύνης, η περιγραφή των χαρακτηριστικών αποτελεί παρελθόν και πλέον οι ερευνητές εξοικονομούν πολύ περισσότερο χρόνο.

Όπως αναφέρθηκε παραπάνω, στο επίκεντρο βρέθηκε μόνο ένα μέρος της εφαρμογής του Signal. Oι ερευνητές της DeepMind τονίζουν ότι τα ευρήματά τους στη παρούσα ανάλυση είναι απλώς ένα ορόσημο σε μια μεγαλύτερη διαδρομή, ενώ συμπεριέλαβαν στο έργο τους και σε προηγούμενες εργασίες τυπικής επαλήθευσης που είχε πραγματοποιήσει το Signal Foundation.

«Είμαστε πολύ ενθουσιασμένοι με αυτό το αποτέλεσμα, αλλά έχουμε πολύ δρόμο μπροστά μας μέχρι να μπορέσουμε να το εφαρμόσουμε σε όλο το λογισμικό του κόσμου, και θέλουμε να το κάνουμε», δηλώνει στο WIRED ο Swarat Chaudhuri, ερευνητής στη DeepMind.

«Ενώ οι προηγούμενες τυπικές επαληθεύσεις επικεντρώνονταν σε μικρότερα τμήματα του κώδικα, η προσέγγιση της Google DeepMind επιτρέπει σημαντική διεύρυνση», αναφέρει σε δήλωσή του ο Ehren Kret, επικεφαλής τεχνολογίας του Signal. «Καθώς αυξάνονται οι απειλές ασφαλείας που βασίζονται στην τεχνητή νοημοσύνη, η αυστηρή επαλήθευση της υλοποίησης του πρωτοκόλλου Signal μάς δίνει ακόμη μεγαλύτερη εμπιστοσύνη στις εγγυήσεις ιδιωτικότητας του κώδικά μας».

«Διαδικασία συνεργασίας ανθρώπου και τεχνητής νοημοσύνης»

Σύμφωνα με τους ερευνητές, μία από τις βασικές καινοτομίες του έργου είναι αυτό που ο Chaudhuri ονομάζει «διαδικασία συνεργασίας ανθρώπου και τεχνητής νοημοσύνης».

Οι πράκτορες AI συμμετέχουν σχεδόν σε κάθε στάδιο και διορθώνουν οι ίδιοι τα λάθη τους. Στα κρίσιμα σημεία όμως ζητούν από ανθρώπους να ελέγξουν και να εγκρίνουν τη δουλειά.

Ο Chaudhuri απορρίπτει ένα μοντέλο όπου η τεχνητή νοημοσύνη ορίζει μόνη της τους στόχους, παράγει μόνη της τις αποδείξεις και ουσιαστικά διορθώνει τα δικά της διαγωνίσματα. Όπως λέει, η λύση βρίσκεται κάπου στη μέση.

Το μεγάλο ερώτημα για τον κλάδο της τεχνολογίας είναι αν η τυπική επαλήθευση με τη βοήθεια της τεχνητής νοημοσύνης μπορεί να εφαρμοστεί ευρέως και με κόστος που αντέχει η αγορά.