Το Astra δείχνει ότι τα προηγμένα μοντέλα μπορούν πλέον να παράγουν νέα επιστημονική γνώση
Η συζήτηση γύρω από την τεχνητή νοημοσύνη αλλάζει επίπεδο. Για χρόνια, η πρόοδος των μεγάλων μοντέλων μετριόταν κυρίως με benchmarks, εξετάσεις, προβλήματα προγραμματισμού και δοκιμασίες μαθηματικού συλλογισμού των οποίων οι απαντήσεις ήταν ήδη γνωστές. Το κρίσιμο ερώτημα, όμως, ήταν διαφορετικό: μπορεί ένα μοντέλο AI να παράγει πραγματικά νέα γνώση, να επιλύσει ένα πρόβλημα για το οποίο η επιστημονική κοινότητα δεν γνωρίζει ήδη την απάντηση;
Τα αποτελέσματα που παρουσιάστηκαν με το Astra, ένα μη δημοσιευμένο ακόμη μοντέλο επόμενης γενιάς της OpenAI, αποτελούν μία από τις ισχυρότερες ενδείξεις ότι η απάντηση αρχίζει να γίνεται θετική.
Το σύστημα παρήγαγε δέκα αποτελέσματα σε μαθηματικά και θεωρητική επιστήμη υπολογιστών, τα οποία είτε επιλύουν είτε προωθούν ουσιαστικά μακροχρόνια ανοιχτά προβλήματα. Τα θέματα εκτείνονται από τη γεωμετρία υψηλών διαστάσεων και τη θεωρία ομάδων μέχρι την κβαντική πολυπλοκότητα, την κρυπτογραφία πλεγμάτων και τη θεωρία Ramsey.
Το σημαντικότερο στοιχείο δεν είναι απλώς ότι ένα AI έδωσε εντυπωσιακές απαντήσεις. Τα επιχειρήματα μετατράπηκαν σε τυπικές αποδείξεις στο Lean, επιτρέποντας σε λογισμικό επαλήθευσης να ελέγξει μηχανικά τη μαθηματική τους ορθότητα.
Από την επίλυση γνωστών ασκήσεων στην ανακάλυψη νέων αποτελεσμάτων
Μέχρι πρόσφατα, ακόμη και τα πιο εντυπωσιακά μαθηματικά benchmarks είχαν έναν βασικό περιορισμό. Το μοντέλο καλούνταν να ανακαλύψει μια λύση που κάποιος άνθρωπος είχε ήδη βρει.
Μια εξαιρετική επίδοση σε μαθηματική ολυμπιάδα αποδεικνύει υψηλή ικανότητα συλλογισμού, αλλά δεν αποτελεί από μόνη της επιστημονική ανακάλυψη. Η σωστή απάντηση υπάρχει ήδη και μπορεί να χρησιμοποιηθεί για την αξιολόγηση του μοντέλου.
Στα ανοιχτά ερευνητικά προβλήματα δεν υπάρχει answer key.
Το σύστημα πρέπει να εξερευνήσει πιθανές κατευθύνσεις, να συνδυάσει προηγούμενα αποτελέσματα, να απορρίψει αποτυχημένες προσεγγίσεις και τελικά να καταλήξει σε ένα επιχείρημα που δεν ήταν προηγουμένως διαθέσιμο στη μαθηματική βιβλιογραφία με αυτή τη μορφή.
Ακριβώς αυτή η μετάβαση κάνει το Astra σημαντικό. Δεν πρόκειται απλώς για ακόμη μία βελτίωση στην ακρίβεια ενός benchmark. Πρόκειται για απόπειρα χρήσης ενός γενικού μοντέλου ως πραγματικού ερευνητικού συστήματος.
Τα δέκα προβλήματα που αντιμετώπισε το Astra
Ένα από τα αποτελέσματα αφορά το sphere packing σε υψηλές διαστάσεις, δηλαδή το πρόβλημα του πόσο πυκνά μπορούν να τοποθετηθούν σφαίρες μέσα σε έναν χώρο πολλών διαστάσεων. Το Astra παρήγαγε νέα ασυμπτωτικά άνω όρια, φτάνοντας στο όριο της μεθόδου Cohn–Elkies.
Η σημασία του προβλήματος ξεπερνά την καθαρή γεωμετρία. Παρόμοιες μαθηματικές δομές συνδέονται με κώδικες διόρθωσης σφαλμάτων, μετάδοση δεδομένων και άλλους τομείς της θεωρίας πληροφορίας.
Ένα δεύτερο αποτέλεσμα αφορά binary και spherical codes, όπου προέκυψαν ισχυρότερα άνω όρια για το μέγιστο μέγεθος κωδίκων με συγκεκριμένη ελάχιστη απόσταση.
Ιδιαίτερη προσοχή προκάλεσε η κατασκευή μιας non-sofic group. Το ερώτημα αν υπάρχουν μη sofic ομάδες αποτελούσε για δεκαετίες σημαντικό ανοιχτό πρόβλημα στη θεωρία ομάδων. Το νέο επιχείρημα κατασκευάζει ρητά ένα τέτοιο αντικείμενο.
Άλλα αποτελέσματα περιλαμβάνουν αντιπαράδειγμα στην conjecture ακαμψίας του Connes, νέα κάτω όρια στην πολυπλοκότητα αριθμητικών κυκλωμάτων για τον permanent, θεώρημα exponential parallel repetition για κβαντικά παιχνίδια δύο παικτών και νέα αποτελέσματα για το Closest Vector Problem, ένα θεμελιώδες πρόβλημα που σχετίζεται και με lattice-based κρυπτογραφία.
Το σύνολο συμπληρώνεται με αποτέλεσμα για την conjecture όγκου του Ehrhart, νέο υπερεκθετικό κάτω όριο για multicolor Ramsey numbers και αποτελέσματα που καταρρίπτουν δύο conjectures στην extremal graph theory.
Η έκταση έχει ιδιαίτερη σημασία. Το Astra δεν φαίνεται να λειτουργεί σαν ένα εξαιρετικά εξειδικευμένο εργαλείο σχεδιασμένο για ένα συγκεκριμένο θεώρημα. Το ίδιο γενικό σύστημα χρησιμοποιήθηκε σε πολύ διαφορετικούς μαθηματικούς κλάδους.
Γιατί το Lean αλλάζει την αξιολόγηση των αποτελεσμάτων
Τα μεγάλα γλωσσικά μοντέλα έχουν ένα γνωστό πρόβλημα όταν χρησιμοποιούνται στα μαθηματικά: μπορούν να παράγουν επιχειρήματα που φαίνονται πειστικά, αλλά περιέχουν ένα μικρό λογικό λάθος που καταστρέφει ολόκληρη την απόδειξη.
Αυτό κάνει δύσκολη την αξιολόγηση εξαιρετικά μεγάλων AI-generated proofs μόνο μέσω ανθρώπινης ανάγνωσης.
Η χρήση του Lean αλλάζει τη διαδικασία. Το Lean είναι proof assistant, ένα σύστημα στο οποίο τα μαθηματικά επιχειρήματα εκφράζονται σε αυστηρή τυπική μορφή. Ο πυρήνας του λογισμικού ελέγχει κάθε λογικό βήμα και δεν αποδέχεται την απόδειξη αν δεν προκύπτει από τους δηλωμένους ορισμούς, αξιώματα και προηγούμενα θεωρήματα.
Για κάθε ένα από τα δέκα αποτελέσματα δημοσιεύτηκε αντίστοιχο Lean certificate, ενώ τα αρχεία μπορούν να ανακατασκευαστούν και να ελεγχθούν ανεξάρτητα.
Αυτό δεν σημαίνει ότι το Lean λύνει κάθε ζήτημα επιστημονικής αξιολόγησης. Ένα proof assistant μπορεί να ελέγξει ότι μια τυποποιημένη πρόταση προκύπτει λογικά από συγκεκριμένες προϋποθέσεις. Δεν αποφασίζει αν το θεώρημα είναι σημαντικό, αν η αρχική φυσική διατύπωση μεταφέρθηκε σωστά στο formal statement ή πόσο πρωτότυπη είναι η κεντρική μαθηματική ιδέα.
Παρόλα αυτά, αφαιρεί ένα από τα σημαντικότερα προβλήματα της generative AI, την πιθανότητα ένα περίπλοκο αλλά λανθασμένο επιχείρημα να περάσει ως σωστό επειδή ακούγεται πειστικό.
Τα περίπου 2.000 δολάρια χρειάζονται προσεκτική ερμηνεία
Ένα ακόμη στοιχείο που προκάλεσε ενδιαφέρον είναι το κόστος. Ο αριθμός των tokens που χρειάστηκαν για την εύρεση των δέκα επιτυχημένων αποτελεσμάτων αντιστοιχεί περίπου σε 2.000 δολάρια με τιμές API του Sol.
Ο αριθμός είναι εντυπωσιακά μικρός σε σχέση με την επιστημονική αξία που θα μπορούσε να έχει ακόμη και μία σημαντική μαθηματική ανακάλυψη.
Δεν πρέπει, όμως, να ερμηνευτεί ως πλήρες κόστος παραγωγής της έρευνας. Δεν περιλαμβάνει κατ’ ανάγκη το συνολικό κόστος ανάπτυξης και εκπαίδευσης του μοντέλου, την υποδομή, την επιλογή των προβλημάτων, τις ανεπιτυχείς απόπειρες σε άλλα προβλήματα, την ανθρώπινη εργασία ή ολόκληρη τη διαδικασία αξιολόγησης.
Το ενδιαφέρον βρίσκεται αλλού. Από τη στιγμή που υπάρχει ήδη ένα frontier model, το οριακό υπολογιστικό κόστος για την εξερεύνηση ενός δύσκολου ερευνητικού προβλήματος μπορεί να αρχίσει να γίνεται αρκετά χαμηλό ώστε να επιτρέπει χιλιάδες παράλληλα πειράματα.
Αυτό μπορεί να αλλάξει δραστικά την οικονομία της επιστημονικής έρευνας.
Το Astra δεν δημιούργησε τα μαθηματικά από το μηδέν
Ο όρος «πρωτότυπη έρευνα» χρειάζεται επίσης προσοχή. Κανένας ερευνητής, ανθρώπινος ή τεχνητός, δεν εργάζεται σε κενό. Τα νέα αποτελέσματα βασίζονται σε δεκαετίες προηγούμενης μαθηματικής γνώσης.
Αυτό έγινε ιδιαίτερα εμφανές στην περίπτωση των non-sofic groups. Η τελική κατασκευή αξιοποιεί σημαντικό προηγούμενο έργο πάνω στο οποίο μπόρεσε να χτιστεί το νέο επιχείρημα. Η αρχική παρουσίαση των αποτελεσμάτων τροποποιήθηκε ώστε να αποδίδει με μεγαλύτερη ακρίβεια τον ρόλο αυτής της προγενέστερης έρευνας.
Η διάκριση είναι σημαντική. Το ενδιαφέρον δεν βρίσκεται στο αν ένα AI «σκέφτηκε μόνο του» χωρίς ανθρώπινη γνώση. Αυτό δεν αποτελεί ρεαλιστικό κριτήριο ούτε για την ανθρώπινη επιστήμη.
Το πραγματικό ερώτημα είναι αν ένα σύστημα μπορεί να πάρει την υπάρχουσα βιβλιογραφία, να συνδυάσει ιδέες με νέο τρόπο και να φτάσει σε ένα αποτέλεσμα που προηγουμένως δεν ήταν γνωστό. Τα πρόσφατα παραδείγματα δείχνουν ότι αυτό αρχίζει να συμβαίνει.
Το προηγούμενο των 80 ετών
Η πορεία προς αυτό το σημείο είχε ήδη γίνει ορατή λίγους μήνες νωρίτερα. Ένα εσωτερικό γενικού σκοπού μοντέλο κατάφερε να ανατρέψει μια conjecture γύρω από το planar unit distance problem, ένα πρόβλημα που είχε τις ρίζες του σε εργασία του Paul Erdős από το 1946.
Το AI ανακάλυψε μια νέα οικογένεια κατασκευών που έδινε καλύτερο αποτέλεσμα από αυτό που θεωρούνταν για δεκαετίες πιθανό.
Εκείνο το αποτέλεσμα ήταν ιδιαίτερα σημαντικό επειδή δεν αφορούσε ένα τεχνητό benchmark σχεδιασμένο για την αξιολόγηση AI. Ήταν πραγματικό ερευνητικό πρόβλημα, με πραγματική ιστορία και πραγματική μαθηματική κοινότητα γύρω του.
Τα δέκα αποτελέσματα του Astra επεκτείνουν τώρα αυτή την εικόνα από ένα μεμονωμένο breakthrough σε ένα ευρύτερο μοτίβο.
Η επόμενη μεγάλη αλλαγή μπορεί να αφορά ολόκληρη την επιστήμη
Τα μαθηματικά βρίσκονται σε ιδιαίτερα ευνοϊκή θέση για την είσοδο της AI στην πρωτότυπη έρευνα, επειδή πολλές απαντήσεις μπορούν να ελεγχθούν με μεγάλη ακρίβεια. Ένα formal proof μπορεί να δοθεί σε έναν theorem prover και να γίνει machine verification.
Στη φυσική, τη βιολογία, τη χημεία ή την ιατρική το πρόβλημα είναι δυσκολότερο. Μια νέα υπόθεση μπορεί να απαιτεί εργαστηριακό πείραμα, κλινικά δεδομένα ή πραγματικές μετρήσεις πριν θεωρηθεί επιβεβαιωμένη.
Αν όμως τα μοντέλα αποκτούν την ικανότητα να διερευνούν προβλήματα για ώρες ή ημέρες, να αναζητούν βιβλιογραφία, να χρησιμοποιούν εργαλεία, να δημιουργούν υποθέσεις και να ελέγχουν τις δικές τους προτάσεις, η ίδια αρχιτεκτονική μπορεί να μεταφερθεί σταδιακά και σε άλλες επιστήμες.
Το σημαντικότερο νέο χαρακτηριστικό των frontier models ίσως επομένως να μην είναι ότι γράφουν καλύτερα, προγραμματίζουν καλύτερα ή απαντούν σε περισσότερες ερωτήσεις.
Είναι ότι αρχίζουν να μπορούν να εξερευνούν το άγνωστο.
Η πραγματική αλλαγή θα έρθει όταν η αξιολόγηση ενός προηγμένου μοντέλου δεν θα βασίζεται κυρίως στο πόσες γνωστές απαντήσεις μπορεί να αναπαράγει, αλλά στο πόσες νέες, επαληθεύσιμες και επιστημονικά χρήσιμες απαντήσεις μπορεί να δημιουργήσει.
Το Astra αποτελεί μία από τις πρώτες σοβαρές ενδείξεις ότι αυτή η εποχή έχει ήδη αρχίσει.
