Η OpenAI ανακοίνωσε ότι ένα εσωτερικό της μοντέλο παρήγαγε απόδειξη που, αν επιβεβαιωθεί, διαψεύδει την Υπόθεση Εκθετικού Χρόνου (ETH), μια βασική παραδοχή της θεωρητικής πληροφορικής για το πόσο δύσκολα λύνονται προβλήματα όπως το 3-SAT. Η εταιρεία δημοσίευσε την απόδειξη και μια τυπική επαλήθευση στη γλώσσα Lean στο GitHub. Ερευνητές όπως ο Ryan Williams, ο Russell Impagliazzo και ο Ramamohan Paturi οργανώνουν ανεξάρτητο έλεγχο, χωρίς αυτό να σημαίνει ότι την υιοθετούν. Η OpenAI παρουσίασε επίσης αποτελέσματα σε άλλα μαθηματικά προβλήματα και νέο τρόπο συνεργασίας με ακαδημαϊκούς.

Τι σημαίνει: Αν το αποτέλεσμα αντέξει τον έλεγχο, θα είναι από τα σημαντικότερα στη θεωρία πολυπλοκότητας εδώ και χρόνια, και μάλιστα προερχόμενο από σύστημα τεχνητής νοημοσύνης. Μέχρι τότε, η σωστή στάση είναι επιφυλακτική: η επαλήθευση σε Lean ελέγχει ότι τα βήματα είναι λογικά σωστά, αλλά οι ειδικοί πρέπει ακόμη να επιβεβαιώσουν ότι η τυπική διατύπωση αντιστοιχεί πράγματι στην υπόθεση που όλοι εννοούν. Για τις επιχειρήσεις, η άμεση πρακτική σημασία είναι μικρή. Ένας αλγόριθμος υποεκθετικού χρόνου δεν σημαίνει αυτόματα γρήγορα προγράμματα, ούτε απειλεί τη σημερινή κρυπτογραφία, που στηρίζεται σε διαφορετικά προβλήματα. Το πιο ενδιαφέρον μήνυμα είναι αλλού: τα μοντέλα αρχίζουν να παράγουν πρωτότυπη έρευνα που μπορεί να ελεγχθεί μηχανικά. Αυτό αφορά κάθε ομάδα λογισμικού που σκέφτεται να χρησιμοποιήσει AI για βελτιστοποίηση, για παράδειγμα σε προγραμματισμό βαρδιών, δρομολόγηση ή έλεγχο κανόνων, όπου η τυπική επαλήθευση γίνεται ολοένα πιο προσιτή. Για τις ελληνικές εταιρείες τεχνολογίας, αξίζει να παρακολουθούν εργαλεία όπως το Lean και τις μεθόδους τυπικής απόδειξης, γιατί ο συνδυασμός τους με AI μπορεί να μειώσει σημαντικά τα σφάλματα σε κρίσιμο κώδικα, όπως οι πληρωμές και οι φορολογικές διασυνδέσεις.

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

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

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