Η Anthropic αναφέρει ότι το Claude απέδειξε την ασφάλεια 123 βιβλιοθηκών

Η Anthropic αναφέρει ότι το μοντέλο της Claude συνέταξε μαθηματικές αποδείξεις, ελεγμένες από μηχανή, που δείχνουν ότι ο μεταγλωττισμένος κώδικας από 123 βιβλιοθήκες ανοιχτού κώδικα δεν μπορεί να καταρρεύσει υπό καθορισμένες συνθήκες. Το μοντέλο εντόπισε επίσης σφάλματα κατά τη διαδικασία, τα οποία είχαν παραμείνει απαρατήρητα για χρόνια παρά τα τρισεκατομμύρια δοκιμών, σύμφωνα με έρευνα που δημοσιεύθηκε στις 22 Οκτωβρίου από την Frontier Red Team της εταιρείας, η οποία εργάστηκε στο έργο με την εταιρεία τυπικών μεθόδων Theorem.anthropic.com

Η εταιρεία το αποκαλεί αυτό που πιστεύει ότι είναι η πρώτη προσπάθεια μεγάλης κλίμακας για τη χρήση τεχνητής νοημοσύνης στην εφαρμογή τυπικής επαλήθευσης σε λογισμικό παραγωγής σε επίπεδο κώδικα assembly. Υποστηρίζει ότι η τεχνητή νοημοσύνη μπορεί πλέον να εντοπίζει και να εκμεταλλεύεται σφάλματα εύκολα, επομένως ο έλεγχος από μόνος του δεν αρκεί πλέον για την προστασία του λογισμικού, έγραψε η Anthropic.anthropic.com

Από τα fuzz tests στις αποδείξεις

Η ομάδα ξεκίνησε με fuzz tests από το πρόγραμμα OSS-Fuzz της Google και μετέτρεψε το καθένα σε μια τυπική προδιαγραφή. Ο κανόνας ήταν ότι το τεστ δεν καταρρέει ποτέ σε καμία είσοδο μικρότερη των 64 MB όταν μεταγλωττίζεται σε κώδικα μηχανής RISC-V. Μέσα σε λίγες εβδομάδες, το Claude το απέδειξε αυτό για 239 σημεία εισόδου σε 123 βιβλιοθήκες. Οι αποδείξεις ανέρχονται σε περίπου 180 εκατομμύρια γραμμές κώδικα στη γλώσσα αποδείξεων Rocq, και μια τυπική απόδειξη φτάνει περίπου τις 600.000 γραμμές, σύμφωνα με την Anthropic. Ο ελεγκτής αποδείξεων Rocq επιβεβαιώνει ότι κάθε απόδειξη ταιριάζει με τις προδιαγραφές της, επομένως οι προγραμματιστές δεν χρειάζεται να ελέγχουν τον παραγόμενο κώδικα γραμμή προς γραμμή, ανέφερε το Interesting Engineering.interestingengineering.com+1

Η Anthropic δήλωσε ότι ένα υποσύνολο των αποδείξεων δημοσιεύεται, μαζί με τη σημασιολογία RISC-V και Linux που τις υποστηρίζει. Η Theorem προσφέρει δωρεάν την εκτέλεση της ίδιας διαδικασίας για επιλέξιμα έργα ανοιχτού κώδικα μέσω του προγράμματος OSS Verify, ανέφερε το Unite.AI. Η Theorem έχει επίσης κυκλοφορήσει μια δεξιότητα Claude για να βοηθήσει τους συντηρητές να εγγραφούν.unite.ai+1

Σφάλματα που διέφυγαν από τους fuzzers

Η συγγραφή των αποδείξεων αποκάλυψε εκατοντάδες σφάλματα, τα οποία το Claude διόρθωσε πριν αποδείξει τον διορθωμένο κώδικα. Σε έναν αποσυμπιεστή, βρήκε μια υπορροή μετρητή που οδηγούσε σε εγγραφή εκτός ορίων, αλλά μόνο σε εισόδους περίπου 20 MB με μια σπάνια διάταξη. Μια άλλη ανάγνωση εκτός ορίων, σε έναν αποκωδικοποιητή εικόνας, χρειαζόταν είσοδο 64 MB και περισσότερα από 2 GB μνήμης. Το Claude ανακάλυψε επίσης εκ νέου μια γνωστή ευπάθεια στη libexpat και βρήκε ένα λογικό σφάλμα όπου μια δυνατότητα που προοριζόταν να περιορίζει ποια αρχεία μπορεί να φορτώσει μια εφαρμογή δεν επιβαλλόταν πάντα, αναφέρει η έρευνα.anthropic.com

Όρια της εγγύησης

Η Anthropic προειδοποίησε ότι οι αποδείξεις δεν σημαίνουν ότι οι βιβλιοθήκες είναι απαλλαγμένες από σφάλματα. Υποθέτουν ένα single-threaded στατικό δυαδικό αρχείο με σταθερό προϋπολογισμό μνήμης που εκτελείται σε CPU RISC-V υπό Linux. Τυχόν εναπομείναντα σφάλματα είναι είτε εκτός του πεδίου εφαρμογής των αποδείξεων είτε βρίσκονται στα έμπιστα στοιχεία, δηλαδή στα μοντέλα υλικού και λειτουργικού συστήματος, στις δηλώσεις θεωρημάτων και στον ίδιο τον ελεγκτή Rocq, έγραψε η εταιρεία. Τα περισσότερα συστήματα που αναπτύσσονται χρησιμοποιούν άλλες αρχιτεκτονικές επεξεργαστών ή διαμορφώσεις, σημείωσε το Interesting Engineering.interestingengineering.com+1

Η Anthropic εξακολουθεί να πιστεύει ότι τα οικονομικά δεδομένα αλλάζουν. Ενθαρρύνουμε όλους τους προγραμματιστές να εξερευνήσουν την τυπική επαλήθευση με LLMs, ειδικά εκείνους που προσπάθησαν στο παρελθόν με λιγότερο ικανά μοντέλα και διαπίστωσαν ότι δεν λειτούργησε, έγραψε η ομάδα.anthropic.com