Το χάσμα μεταξύ φυσικής γλώσσας και τυπικής επαλήθευσης
Η χρήση μοντέλων παραγωγικής τεχνητής νοημοσύνης (Generative AI) για την αυτόματη μετατροπή μαθηματικών αποδείξεων σε τυπικές γλώσσες (formal languages) όπως η Lean, παρουσιάζεται συχνά ως η λύση για την επαλήθευση πολύπλοκων θεωρημάτων. Ωστόσο, η παρούσα μελέτη αποκαλύπτει ότι η διαδικασία αυτή πάσχει από ένα θεμελιώδες πρόβλημα: την αδυναμία διασφάλισης της σημασιολογικής πιστότητας κατά τη μετάφραση.
Η υπολογιστική πολυπλοκότητα της σημασιολογίας
Οι ερευνητές τοποθετούν το πρόβλημα της επίλυσης ασάφειας σε μαθηματικά κείμενα στο ανώτατο επίπεδο της ιεραρχίας Solvability Complexity Index (SCI). Με SCI=∞, η διαδικασία αυτή καθίσταται μη υπολογίσιμη, ξεπερνώντας σε δυσκολία ακόμη και το κλασικό πρόβλημα του τερματισμού (Halting problem). Αυτό σημαίνει ότι κανένα σύστημα AI δεν μπορεί να εγγυηθεί ότι η τυποποιημένη έκδοση μιας απόδειξης διατηρεί το ακριβές νόημα του πρωτοτύπου.
Κίνδυνοι για την επιστημονική εγκυρότητα
Το πιο ανησυχητικό εύρημα αφορά την πρόσφατη απόδειξη της OpenAI για τις εξισώσεις Navier–Stokes. Η ανάλυση δείχνει ότι η τυποποιημένη απόδειξη στη Lean δεν αντιστοιχεί στο αρχικό μαθηματικό επιχείρημα. Αυτό δημιουργεί μια ψευδαίσθηση ασφάλειας, όπου η μηχανική επαλήθευση (mechanical verification) επιβεβαιώνει ένα τυπικό αντικείμενο που δεν ταυτίζεται με το αρχικό πρόβλημα, καθιστώντας την όλη διαδικασία επιστημονικά επισφαλή.