OpenAI: Αμφισβητείται η απόδειξη για τις εξισώσεις Navier-Stokes – Οι αποκλίσεις μεταξύ κώδικα και μαθηματικών

Στο επίκεντρο έντονου επιστημονικού διαλόγου βρίσκεται η πολυσυζητημένη μαθηματική απόδειξη της OpenAI σχετικά με τις εξισώσεις Navier-Stokes. Μια νέα ανεξάρτητη μελέτη από τρεις διακεκριμένους μαθηματικούς φέρνει στο φως σημαντικές αποκλίσεις ανάμεσα στη θεωρητική διατύπωση που παρουσίασε η εταιρεία και στον υπολογιστικό κώδικα που προοριζόταν για την αυτοματοποιημένη επαλήθευσή της, θέτοντας υπό αμφισβήτηση την εγκυρότητα της διαδικασίας.

Το ιστορικό πρόβλημα των ρευστών και ο ισχυρισμός της OpenAI

Η OpenAI είχε ανακοινώσει πως ένα εσωτερικό ερευνητικό της μοντέλο τεχνητής νοημοσύνης παρήγαγε μια απόδειξη για τον σχηματισμό μαθηματικής ανωμαλίας σε πεπερασμένο χρόνο στις εξισώσεις Navier-Stokes. Το ζήτημα αυτό συνιστά ένα από τα μεγαλύτερα άλυτα προβλήματα των σύγχρονων μαθηματικών, καθώς περιγράφει τη θεμελιώδη δυναμική και συμπεριφορά των ρευστών.

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

«Lost in Translation»: Οι κρίσιμες αποκλίσεις στον κώδικα Lean

Παρά τις αρχικές θετικές εντυπώσεις, η έρευνα των μαθηματικών Αλεξάντερ Μπαστούνη, Φάμπιαν Τσιρτσέλι και Άντερς Κ. Χάνσεν, υπό τον τίτλο «Navier-Stokes lost in translation», αποκαλύπτει σοβαρές ανακολουθίες. Οι ερευνητές εντόπισαν σημεία όπου ο κώδικας Lean δεν αποτυπώνει πιστά το κείμενο της αρχικής μαθηματικής απόδειξης.

Χαρακτηριστικό είναι το παράδειγμα όπου η γραπτή απόδειξη αναφέρει ότι για μια συγκεκριμένη εκτίμηση απαιτούνται τέσσερις επιπλέον παράγωγοι μιας συνάρτησης, ενώ στον κώδικα Lean απαιτούνται πέντε. Αυτή η διαφοροποίηση καθιστά την έκδοση που επαληθεύτηκε από το μηχάνημα αισθητά ασθενέστερη από αυτή που διατυπώνεται στο αρχικό κείμενο. Παράλληλα, εντοπίστηκαν αναντιστοιχίες και στην απόδειξη μιας εκτίμησης σχετικά με τη ροή πίεσης, γεγονός που σημαίνει ότι ο υπολογιστής επιβεβαίωσε τελικά ένα διαφορετικό μαθηματικό επιχείρημα.

Τα όρια της τυπικής επαλήθευσης και η ανάγκη για peer review

Οι τρεις ερευνητές τονίζουν ότι τα ευρήματά τους δεν αποδεικνύουν απαραίτητα πως η μαθηματική σύλληψη της OpenAI είναι λανθασμένη. Ωστόσο, καθιστούν σαφές ότι η ψηφιοποιημένη εκδοχή δεν επαρκεί για να τεκμηριώσει την ορθότητά της, καθώς η τυπική επαλήθευση έχει αξία μόνο όταν αντικατοπτρίζει πιστά το αρχικό θεώρημα.

Το περιστατικό αναδεικνύει τις προκλήσεις στη χρήση της τεχνητής νοημοσύνης για την επίλυση σύνθετων επιστημονικών προβλημάτων. Είτε οι αποκλίσεις αυτές οφείλονται σε ανθρώπινη παράβλεψη κατά τη μεταφορά είτε σε περιορισμούς του μοντέλου, γίνεται φανερό ότι η αυτοματοποιημένη επαλήθευση δεν μπορεί να αντικαταστήσει την παραδοσιακή αξιολόγηση από ανεξάρτητους επιστήμονες. Μέχρι να υπάρξει πλήρης μαθηματική επιβεβαίωση χωρίς κενά στη μετάφραση, η λύση του ιστορικού προβλήματος Navier-Stokes παραμένει ανοιχτό ζήτημα.