Το PSI αναφέρει απόδειξη της εικασίας Aaronson-Ambainis, ελεγμένη από υπολογιστή

Η Physical Superintelligence ανακοίνωσε στις 6 Νοεμβρίου 2026 ότι ένα εσωτερικό ερευνητικό σύστημα, το οποίο εκτελούσε στιγμιότυπα ενός μη δημόσιου μοντέλου της Anthropic, είχε βρει απόδειξη της εικασίας Aaronson-Ambainis, ενός προβλήματος της κβαντικής υπολογιστικής που παρέμενε άλυτο από το 2008.

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

Τι λέει η εικασία για την επιτάχυνση μέσω κβαντικών υπολογιστών

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

Στο μοντέλο ερωτημάτων, ένας κλασικός αλγόριθμος διαβάζει ένα bit σε κάθε ερώτημα, ενώ ένα κβαντικό ερώτημα μπορεί να κατανέμεται, μέσω υπέρθεσης, σε πολλές θέσεις της εισόδου. Η εξήγηση του PSI συνδέει αυτό το μοντέλο με τα πολυώνυμα: μετά από T κβαντικά ερωτήματα, η πιθανότητα ο αλγόριθμος να απαντήσει «ναι» είναι ένα φραγμένο πολυώνυμο των bit της εισόδου, βαθμού το πολύ 2T. Επομένως, η προσομοίωση του κβαντικού αλγορίθμου ανάγεται στο ερώτημα πώς μπορεί να εκτιμηθεί αυτό το πολυώνυμο χωρίς να διαβαστούν εκθετικά πολλά bit της εισόδου.

Στην αρχική τους εργασία, ο Scott Aaronson και ο Andris Ambainis διατύπωσαν την εικασία ότι κάθε φραγμένο πολυώνυμο χαμηλού βαθμού έχει μια μεταβλητή με μεγάλη επιρροή. Απέδειξαν ότι, αν ισχύει η εικασία, κάθε κβαντικός αλγόριθμος με T ερωτήματα μπορεί να προσομοιωθεί στις περισσότερες εισόδους από έναν κλασικό αλγόριθμο που εκτελεί πολυωνυμικά πολλά ερωτήματα ως προς το T. Αυτό συνεπάγεται πολυωνυμική και όχι εκθετική αύξηση του αριθμού των κλασικών ερωτημάτων, για κάθε σταθερό σφάλμα προσέγγισης και ποσοστό εισόδων που εξαιρούνται· δεν αποκλείει εκθετικά κβαντικά πλεονεκτήματα σε προβλήματα με κατάλληλη δομή.

Τυπικά, το αποθετήριο εξετάζει ένα πραγματικό πολυώνυμο p βαθμού το πολύ d, του οποίου οι τιμές στον διακριτό κύβο κυμαίνονται από 0 έως 1. Αν η διακύμανσή του ως προς μια ομοιόμορφα τυχαία είσοδο είναι τουλάχιστον ε, τότε κάποια συντεταγμένη έχει επιρροή τουλάχιστον (8√15 / (125π⁴)) · ε^(5/2) / d⁶ και, συνεπώς, τουλάχιστον (ε/d)⁷. Επιρροή είναι η αναμενόμενη τετραγωνική μεταβολή του p όταν αντιστρέφεται το bit της συγκεκριμένης συντεταγμένης.

Πώς κατασκευάστηκε και ελέγχθηκε η απόδειξη

Η επιχειρηματολογία ακολουθεί ένα σχέδιο των Shachar Lovett και Jiapeng Zhang, το οποίο βασίζεται σε κλασματικά πιστοποιητικά και σύνολα στάθμης, αλλά αντικαθιστά μια ανισότητα που το σχέδιό τους άφηνε ως εικασία με μια νέα ανισότητα για όλα τα ζεύγη. Μια ορίζουσα δημιουργεί μια αντιστοίχιση ένα προς ένα μεταξύ των ρυθμίσεων εισόδου. Σύμφωνα με το PSI, αυτή η αντιστοίχιση υπερβαίνει την ασθενέστερη αντιστοίχιση του Butterfly Lemma του David Reimer, επειδή περιορίζει επίσης πόσο συχνά οι αντιστοιχισμένες ρυθμίσεις συμφωνούν σε κάθε συντεταγμένη — ένα όριο απαραίτητο για τη νέα ανισότητα.

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

Σύμφωνα με τον καταγεγραμμένο έλεγχο του αποθετηρίου, η τυπική ανάπτυξη δεν περιέχει θέσεις με ελλείπουσες αποδείξεις ούτε πρόσθετα αξιώματα. Οι δηλώσεις της επανελέγχθηκαν μέσω του πυρήνα του Lean και του lean4lean, μιας ανεξάρτητης υλοποίησης του ελεγκτή τύπων του Lean. Σε μια εκτέλεση σε περιβάλλον απομόνωσης, ένα εργαλείο σύγκρισης που χρησιμοποιούσε τους πυρήνες του nanoda και του Lean αποδέχτηκε τα τέσσερα τελικά θεωρήματα· σε δεύτερο μηχάνημα, αποδέχτηκε μία ορθή μικρή λύση και απέρριψε τέσσερις σκόπιμα λανθασμένες.

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

Ανθρώπινοι ρόλοι και αξιολόγηση από ειδικούς

Ο David Turturean, μέλος του τεχνικού προσωπικού του PSI, ανέπτυξε και έθεσε σε λειτουργία το ερευνητικό σύστημα, καθόρισε το εύρος του προβλήματος, έδωσε εντολή στο μοντέλο να ετοιμάσει ένα πρώτο προσχέδιο, το εξέτασε και είναι υπεύθυνος για την ορθότητα της εργασίας. Το αποθετήριο αναφέρει ότι μοντέλα τεχνητής νοημοσύνης παρήγαγαν τις μαθηματικές διατυπώσεις, το πρώτο προσχέδιο και την τυποποίηση στο Lean. Ο Jim Halverson έλεγξε την απόδειξη και η Phiala Shanahan σχολίασε την τυποποίηση.

Η ανακοίνωση ακολουθεί εργασία που υποβλήθηκε στις 19 Αυγούστου 2026 από τους Guy Blanc, Jordan Docter, Carmen Strassle και Li-Yang Tan. Οι συγγραφείς αυτοί είχαν επιλύσει το αντίστοιχο συμπέρασμα για την κλασική προσομοίωση παράλληλων κβαντικών αλγορίθμων, αποδεικνύοντας ότι ένας αλγόριθμος με t ερωτήματα και d γύρους μπορεί να προσομοιωθεί στις περισσότερες εισόδους με t^(O(d²)) κλασικά ερωτήματα. Το PSI αναφέρει ότι και οι τέσσερις διαβάζουν ολόκληρη την απόδειξη, έχουν υποβάλει σχόλια και ετοιμάζουν μια συντομότερη παρουσίαση για ειδικούς.

Στην αξιολόγησή τους, που δημοσιεύτηκε από την PSI, οι ερευνητές έγραψαν: «Πρόκειται για ένα τεράστιο αποτέλεσμα. Επιλύει μια εικασία δεκαετιών, με σημαντικές επιπτώσεις για τη φύση των προβλημάτων που επιδέχονται κβαντική επιτάχυνση. Η απόδειξη αξιοποιεί και επεκτείνει διάφορες ερευνητικές κατευθύνσεις στην ανάλυση συναρτήσεων Boole και στην πιθανοκρατική συνδυαστική. Όλα συνδυάζονται με έναν μάλλον μαγικό τρόπο.»

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