Για να επαληθευτεί τυπικά ο μικρός πυρήνας λειτουργικού συστήματος seL4, χρειάστηκαν 20 ανθρωποέτη δουλειάς ειδικών. Το Claude της Anthropic έγραψε σε λίγες εβδομάδες περίπου 180 εκατομμύρια γραμμές κώδικα αποδείξεων για 123 βιβλιοθήκες ανοιχτού κώδικα. Το αναφέρει το The Decoder, με βάση το πείραμα της Frontier Red Team της Anthropic και της εταιρείας Theorem.
Η τυπική επαλήθευση (formal verification) δεν ελέγχει απλώς αν ένα πρόγραμμα περνά κάποια τεστ. Αποδεικνύει μαθηματικά ότι δεν θα αστοχήσει υπό συγκεκριμένες συνθήκες. Επειδή κοστίζει τόσο πολύ, μένει για ακραίες περιπτώσεις, όπως το λογισμικό αεροηλεκτρονικών της Airbus.
Τα τεστ γίνονται θεωρήματα
Το Claude δεν έγραψε νέο κώδικα. Πήρε υπάρχον λογισμικό από προγράμματα δοκιμών του OSS-Fuzz, του έργου ασφαλείας της Google, και μετέτρεψε τις δοκιμές κατάρρευσης σε μαθηματικά προβλήματα. Ανέλυσε τον μεταγλωττισμένο κώδικα μηχανής και έγραψε τις αποδείξεις.
Τις αποδείξεις ελέγχει αυτόματα ένα ανεξάρτητο πρόγραμμα επαλήθευσης, το Rocq. Σύμφωνα με την Anthropic, σχεδόν δεν χρειάζονται άνθρωποι ελεγκτές. Οι ερευνητές μιλούν για «πλήρως αυτόνομη» παραγωγή αποδείξεων, αν και τα εργαλεία και τα τυπικά θεμέλια τα έφτιαξαν άνθρωποι της Theorem.
Σφάλματα που δεν έβγαιναν στα τεστ
Καθώς έγραφε τις αποδείξεις, το Claude έπεφτε πάνω σε σφάλματα, εκατοντάδες συνολικά, και είχε άδεια να τα διορθώνει. Πολλά, λένε οι ερευνητές, θα ξέφευγαν από τα συμβατικά τεστ, επειδή εμφανίζονται μόνο σε ειδικές συνθήκες: ασυνήθιστα μεγάλα αρχεία ή μια συγκεκριμένη σειρά προσβάσεων στη μνήμη.
Σε μια προσπάθεια επαλήθευσης ενός ευρέως χρησιμοποιούμενου προγράμματος ανάγνωσης PDF, η ομάδα βρήκε σε μία εβδομάδα τόσα σφάλματα ασφαλείας όσα αναφέρονται συνήθως για το πρόγραμμα σε ολόκληρο έτος. Σε άλλη εφαρμογή, το Claude εντόπισε λογικό λάθος που έμενε απαρατήρητο πάνω από μια δεκαετία. Ακόμη κι όταν μια απόδειξη τελικά αποτυγχάνει, λέει η Anthropic, η προσπάθεια φέρνει στην επιφάνεια πραγματικά σφάλματα.
Το «επαληθευμένο» δεν σημαίνει «αλάνθαστο»
Η ίδια η εταιρεία παραδέχεται τα όρια. Οι αποδείξεις ισχύουν μόνο για συγκεκριμένη αρχιτεκτονική επεξεργαστή, για προγράμματα με ένα νήμα εκτέλεσης και για δεδομένα εισόδου κάτω από 64 MB. Στην πράξη, οι βιβλιοθήκες τρέχουν σε διαφορετικό υλικό και με άλλες ρυθμίσεις.
Το κόστος σε υπολογιστική ισχύ είναι μεγάλο: μεμονωμένες αποδείξεις καταναλώνουν εκατοντάδες εκατομμύρια tokens, δηλαδή τα τμήματα κειμένου που επεξεργάζεται ένα μοντέλο. Το συνολικό κόστος του έργου δεν δημοσιεύεται. Ένα μικρότερο τεστ έδειξε πάντως ότι οι αποδείξεις μπορούν να ξαναχρησιμοποιηθούν και ότι τα νεότερα μοντέλα γίνονται πιο αποδοτικά: το Opus 5.5 λύνει τις μισές αποδείξεις με περίπου 40% λιγότερα tokens από το Opus 5.
Η Anthropic περιμένει η τυπική επαλήθευση με AI να γίνει σύντομα τόσο πρακτική όσο τα συνηθισμένα τεστ. Ο οδικός χάρτης της Theorem στοχεύει ήδη κρίσιμες υποδομές όπως οι glibc, OpenSSL και cURL.
Πηγή: The Decoder
