Η Anthropic και η Theorem χρησιμοποίησαν το Claude για να παραγάγουν τυπικές αποδείξεις στο σύστημα Rocq για 239 σημεία εισόδου 123 βιβλιοθηκών ανοιχτού κώδικα από το πρόγραμμα OSS-Fuzz. Οι αποδείξεις δείχνουν ότι τα συγκεκριμένα σημεία δεν καταρρέουν για εισόδους έως 64 MB, υπό συγκεκριμένες παραδοχές, όπως εκτέλεση σε ένα νήμα και στατικά συνδεδεμένα προγράμματα RISC-V σε Linux. Συνολικά ελέγχθηκαν περίπου 180 εκατομμύρια γραμμές αποδείξεων και δημοσιεύτηκαν 60 από αυτές για 25 βιβλιοθήκες. Οι ερευνητές τονίζουν ότι αυτό δεν σημαίνει πως οι βιβλιοθήκες είναι γενικά χωρίς σφάλματα.

Τι σημαίνει: Η τυπική επαλήθευση, δηλαδή η μαθηματική απόδειξη ότι ένα πρόγραμμα συμπεριφέρεται σωστά, ήταν μέχρι σήμερα τόσο ακριβή που χρησιμοποιούνταν σχεδόν μόνο σε αεροπορία, κρυπτογραφία και κρίσιμες υποδομές. Αν τα γλωσσικά μοντέλα μειώνουν δραστικά τον χρόνο που απαιτείται, ανοίγει ο δρόμος για ισχυρότερες εγγυήσεις και σε κοινό λογισμικό, όπως βιβλιοθήκες συμπίεσης ή ανάλυσης αρχείων που τρέχουν σε κάθε server. Για τις ελληνικές ομάδες ανάπτυξης, το άμεσο όφελος είναι έμμεσο: οι βιβλιοθήκες που χρησιμοποιούν θα γίνουν πιο ασφαλείς καθώς τέτοιες μέθοδοι διαδίδονται. Χρειάζεται όμως προσοχή στην ερμηνεία. Οι αποδείξεις ισχύουν μόνο για τα συγκεκριμένα σημεία εισόδου και παραδοχές, όχι για πολυνηματική χρήση ή άλλες αρχιτεκτονικές, και δεν καλύπτουν λάθη στη λογική της εφαρμογής που καλεί τη βιβλιοθήκη. Σε μικρότερη κλίμακα, οι ομάδες μπορούν ήδη να ζητούν από εργαλεία AI να γράφουν προδιαγραφές, ελέγχους ιδιοτήτων και fuzzing tests για τα πιο κρίσιμα κομμάτια του κώδικά τους, όπως υπολογισμούς τιμολογίων ή φόρων. Για εταιρείες που φτιάχνουν λογισμικό για ταμειακά συστήματα ή πληρωμές, η τάση αυτή θα μπορούσε μελλοντικά να γίνει και επιχείρημα πιστοποίησης, αφού οι ελεγκτές και οι πελάτες θα ζητούν όλο και συχνότερα αποδείξεις ποιότητας, όχι μόνο δοκιμές.

Διαβάστε το πρωτότυπο στο Anthropic

Σχετική υπηρεσία: Ανάπτυξη λογισμικού

Σχετικές ειδήσεις