Με λίγα λόγια
- Η Physical Superintelligence (PSI) ανακοίνωσε ότι ερευνητικό σύστημά της, το οποίο χρησιμοποιούσε ένα μη δημοσιευμένο μοντέλο της Anthropic, απέδειξε την εικασία Aaronson–Ambainis.
- Το πρόβλημα παρέμενε ανοιχτό από το 2008 και αφορά τα όρια του πλεονεκτήματος που μπορούν να έχουν οι κβαντικοί υπολογιστές έναντι των συμβατικών.
- Η απόδειξη έχει δημοσιευτεί μαζί με τυπική επαλήθευση μέσω του Lean, αλλά δεν έχει περάσει ακόμη από αξιολόγηση σε επιστημονικό περιοδικό.
Μια σημαντική ανακοίνωση για τη χρήση της τεχνητής νοημοσύνης στην επιστημονική έρευνα έκανε η Physical Superintelligence (PSI). Η εταιρεία υποστηρίζει ότι ένα δικό της ερευνητικό σύστημα, με τη βοήθεια ενός μη δημοσιευμένου μοντέλου της Anthropic, κατάφερε να αποδείξει ένα δύσκολο μαθηματικό πρόβλημα που απασχολεί τους επιστήμονες εδώ και σχεδόν δύο δεκαετίες.
Πρόκειται για την εικασία Aaronson–Ambainis, ένα ανοιχτό ερώτημα στον τομέα της κβαντικής πληροφορικής από το 2008. Σύμφωνα με την PSI, το σύστημα κατέληξε σε πλήρη απόδειξη μέσα σε τρεις ημέρες. Η ανακοίνωση έχει προκαλέσει ενδιαφέρον, καθώς δείχνει πώς τα σύγχρονα AI μοντέλα μπορούν να συμμετέχουν σε ερευνητικές εργασίες που μέχρι πρόσφατα απαιτούσαν μακρόχρονη ανθρώπινη προσπάθεια.
Τι απέδειξε η AI και γιατί έχει σημασία
Η εικασία Aaronson–Ambainis αφορά ένα θεμελιώδες ερώτημα: μπορούν οι κβαντικοί υπολογιστές να είναι εκθετικά ταχύτεροι από τους συμβατικούς όταν επεξεργάζονται τυχαίες εισόδους, δηλαδή δεδομένα που δεν κρύβουν κάποια ιδιαίτερη μαθηματική δομή;
Γνωστοί κβαντικοί αλγόριθμοι, όπως εκείνος του Peter Shor για την παραγοντοποίηση μεγάλων αριθμών, αξιοποιούν συγκεκριμένα μοτίβα στα δεδομένα. Η εικασία εξετάζει αν μπορεί να υπάρξει αντίστοιχο τεράστιο πλεονέκτημα ακόμη και όταν τέτοια μοτίβα απουσιάζουν.
Η απόδειξη που παρουσιάζει η PSI υποστηρίζει ότι, στο μαθηματικό πλαίσιο που εξετάζει η εικασία, οι κβαντικοί υπολογιστές δεν μπορούν να έχουν εκθετικό πλεονέκτημα στις τυχαίες εισόδους χωρίς να υπάρχει κάποια ιδιαίτερη δομή. Αυτό δεν σημαίνει ότι οι κβαντικοί υπολογιστές χάνουν τη χρησιμότητά τους. Μπορούν να προσφέρουν σημαντικά πλεονεκτήματα σε συγκεκριμένα προβλήματα, όπως άλλωστε δείχνουν ήδη γνωστοί αλγόριθμοι.
Ο ρόλος του μοντέλου της Anthropic και η επαλήθευση της απόδειξης
Η PSI αναφέρει ότι χρησιμοποίησε ένα εσωτερικά ανεπτυγμένο ερευνητικό σύστημα, το οποίο έτρεχε σε δική της υποδομή και ενσωμάτωνε ένα μη δημοσιοποιημένο μοντέλο της Anthropic. Δεν έχει αποκαλύψει ποιο ακριβώς μοντέλο ήταν, ενώ η Anthropic δεν είχε σχολιάσει την ανακοίνωση όταν δημοσιεύτηκαν οι σχετικές αναφορές.
Σύμφωνα με την εταιρεία, το σύστημα έφτασε σε πλήρη απόδειξη την τρίτη ημέρα της διαδικασίας. Στη συνέχεια, συνέχισε να εξετάζει σχετικά προβλήματα και βελτίωσε δύο φορές το αποτέλεσμα. Επικεφαλής της εργασίας ήταν ο David Turturean, ο οποίος ανέπτυξε το ερευνητικό σύστημα, καθόρισε το πρόβλημα και έλεγξε το προσχέδιο της επιστημονικής εργασίας. Η PSI αναφέρει επίσης ότι οι σύμβουλοί της Jim Halverson και Phiala Shanahan συμμετείχαν στον έλεγχο της απόδειξης και της τυπικής επαλήθευσής της.
Ένα σημαντικό στοιχείο είναι η χρήση του Lean, ενός εργαλείου που επιτρέπει τη μαθηματική επαλήθευση αποδείξεων. Σε αντίθεση με έναν απλό έλεγχο από άλλο AI μοντέλο, το Lean ελέγχει αν κάθε βήμα μιας απόδειξης ακολουθεί από τους δηλωμένους μαθηματικούς κανόνες και τις παραδοχές.
Η PSI δημοσίευσε τόσο την επιστημονική εργασία όσο και τον κώδικα της τυπικής απόδειξης στο GitHub. Σύμφωνα με το αποθετήριο, τα βασικά θεωρήματα επαληθεύτηκαν χωρίς κενά στην απόδειξη ή πρόσθετα αξιώματα, ενώ οι έλεγχοι επαναλήφθηκαν και με δεύτερη ανεξάρτητη υλοποίηση του Lean kernel.
Υπάρχει, ωστόσο, μια σημαντική διάκριση: το ότι το Lean επαληθεύει μαθηματικά τη διατύπωση που του δίνεται δεν αποδεικνύει από μόνο του ότι αυτή αντιστοιχεί σωστά στην αρχική εικασία. Αυτό χρειάζεται να το εξετάσουν και να το επιβεβαιώσουν οι ειδικοί.
Η εργασία βρίσκεται ακόμη σε στάδιο δημόσιας επιστημονικής εξέτασης και δεν έχει δημοσιευτεί σε επιστημονικό περιοδικό με αξιολόγηση από ανεξάρτητους κριτές. Η PSI αναφέρει ότι ερευνητές του Stanford που είχαν αποδείξει μια ειδική περίπτωση της εικασίας εξετάζουν την πλήρη απόδειξη και έχουν ήδη στείλει σχόλια.
Το αποτέλεσμα είναι αξιοσημείωτο, αλλά χρειάζεται να αξιολογηθεί με προσοχή. Δεν πρόκειται απλώς για ένα chatbot που έδωσε μια σωστή απάντηση σε ένα δύσκολο μαθηματικό ερώτημα. Πρόκειται για ένα ερευνητικό σύστημα που, σύμφωνα με την PSI, συνέβαλε στην παραγωγή μιας εκτενούς μαθηματικής απόδειξης, η οποία μπορεί πλέον να εξεταστεί από την επιστημονική κοινότητα. Αν επιβεβαιωθεί ανεξάρτητα, θα αποτελέσει ένα ακόμη ισχυρό παράδειγμα του τρόπου με τον οποίο η AI μπορεί να αλλάξει την ίδια την ερευνητική διαδικασία.
