ΑΙ βρήκε μαθηματικές αποδείξεις — για ποιο πρόβλημα;

Το AlphaProof Nexus, ένα σύστημα τεχνητής νοημοσύνης της Google DeepMind, βρήκε αποδείξεις για μαθηματικά ερωτήματα που έμεναν αναπάντητα. Η μελέτη δημοσιεύτηκε στις 8 Οκτωβρίου στο Science, αφού την αξιολόγησαν άλλοι επιστήμονες (Science). Κάθε απόδειξη έχει ελεγχθεί από υπολογιστή βήμα προς βήμα. Ο υπολογιστής όμως πιστοποιεί μόνο την πρόταση που του δόθηκε, όχι το αρχικό πρόβλημα, και σε ορισμένες περιπτώσεις οι μαθηματικοί χρειάστηκε πρώτα να διορθώσουν την ίδια την ερώτηση.

Το πιο καθαρό παράδειγμα ξεκινά από κάτι οικείο. Το δεκαδικό σύστημα έχει δέκα ψηφία. Αν επιτρέψουμε μόνο το 0 και το 1, μένουν αριθμοί όπως το 10, το 11, το 100 και το 101, που αραιώνουν όσο ανεβαίνουμε. Το πρόβλημα #125 του Ούγγρου μαθηματικού Πάουλ Έρντος κάνει το ίδιο σε δύο άλλα συστήματα αρίθμησης, με βάση το 3 και με βάση το 4. Παίρνει έτσι δύο αραιές ομάδες αριθμών και προσθέτει έναν από κάθε ομάδα.

Το ερώτημα είναι τι μερίδιο όλων των φυσικών αριθμών καλύπτουν αυτά τα αθροίσματα καθώς μετράμε όλο και πιο ψηλά. Η απόδειξη που βρήκε το Nexus δείχνει ότι υπάρχουν ολοένα μεγαλύτερες κλίμακες όπου το μερίδιο γίνεται όσο μικρό θέλουμε. Οι μαθηματικοί το διατυπώνουν λέγοντας ότι η «κάτω πυκνότητα» είναι μηδέν (απόδειξη σε Lean). Αν το ίδιο ισχύει σε κάθε μεγάλη κλίμακα, η λεγόμενη «άνω πυκνότητα», μένει ανοιχτό (κατάλογος Erdős).

Ο ελεγκτής που δεν διαβάζει την παραγγελία

Φανταστείτε έναν αυτόματο επιθεωρητή οικοδομών. Βεβαιώνει ότι το κτίριο ακολουθεί κατά γράμμα το σχέδιο, αλλά δεν ξέρει αν το σχέδιο είναι αυτό που ζήτησε ο πελάτης. Το Lean κάνει την ίδια δουλειά για τα μαθηματικά. Είναι μια γλώσσα όπου πρόταση και απόδειξη γράφονται τόσο αυστηρά ώστε ο υπολογιστής να ελέγχει κάθε βήμα απέναντι στους ορισμούς και τα αξιώματα που χρησιμοποιούνται (τεκμηρίωση Lean). Το τι εννοούσε ο Έρντος δεν το ελέγχει.

Το Nexus ξεκινά από πρόταση ήδη γραμμένη σε Lean, όχι από ερώτηση σε ανθρώπινη γλώσσα. Οι πράκτορές του προτείνουν βήματα, βλέπουν πού σκοντάφτει ο ελεγκτής και διορθώνουν (εργασία). Την επιλογή των προβλημάτων και τον έλεγχο των αποτελεσμάτων τα κάνουν ακόμη άνθρωποι, όπως τονίζει ο συνσυγγραφέας Swarat Chaudhuri (El Mundo). Με αυτόν τον τρόπο η ομάδα βρήκε αποδείξεις για 9 από 353 προβλήματα Έρντος και για 44 από 492 εικασίες της OEIS, μιας διαδικτυακής εγκυκλοπαίδειας αριθμητικών ακολουθιών (arXiv).

Στο #125 φάνηκε γιατί ο επιθεωρητής δεν αρκεί. Οι συγγραφείς άλλαξαν την αρχική ερμηνεία της «πυκνότητας» σε κάτω πυκνότητα και έλυσαν τη διορθωμένη διατύπωση (εργασία). Ο Josep Curto, σε σχόλιό του στο Science Media Centre της Ισπανίας, εντοπίζει ακριβώς αυτό το όριο: το Lean πιστοποιεί την απόδειξη της πρότασης όπως γράφτηκε, όχι το αν η πρόταση αποδίδει πιστά το αρχικό πρόβλημα (Science Media Centre España). Δεν ισχυρίζεται ότι βρήκε λάθος στις τελικές εννέα λύσεις, τις οποίες ειδικοί της ομάδας έλεγξαν απέναντι στα αρχικά ερωτήματα.

Τι πρόσθεσε το Science

Η εργασία πρωτοεμφανίστηκε ως προδημοσίευση στις 21 Μαΐου και αναθεωρήθηκε στις 8 Ιουνίου. Ήδη από τότε περιείχε τους βασικούς αριθμούς και το κόστος ανά λύση (arXiv). Περιείχε και μια σύγκριση που ο Curto θεωρεί κρίσιμη. Ένας απλούστερος πράκτορας, που απλώς εναλλάσσει προτάσεις του Gemini με ελέγχους του Lean, έλυσε κι αυτός τους εννέα στόχους Έρντος (SMC España). Το πλήρες σύστημα κέρδισε σε κόστος μόνο σε ορισμένες δύσκολες περιπτώσεις (εργασία). Η αξιολόγηση από ομοτίμους κρίνει τη μέθοδο και την παρουσίαση. Δεν εκτελεί ξανά τα πειράματα ούτε ελέγχει ξεχωριστά την πρωτοτυπία κάθε λύσης.

Η πρωτοτυπία πάντως διαφέρει από πρόβλημα σε πρόβλημα. Το κοινοτικό μητρώο των προβλημάτων Έρντος καταγράφει πλήρη λύση για το #125, χαρακτηρίζει μερικό αποτέλεσμα το #138 και σημειώνει παρόμοια προγενέστερη εργασία για το #152 (μητρώο). Επιπλέον, οι 353 ήταν τα προβλήματα που η κοινότητα είχε ήδη γράψει σε Lean, άρα δεν πρόκειται για τυχαίο δείγμα. Η ακριβής περιγραφή είναι λοιπόν «53 αποδείξεις σε δύο επιλεγμένες δοκιμές», με επιτυχία περίπου 2,5% και 8,9% αντίστοιχα (εργασία).

Οι υπολογιστές ελέγχουν αποδείξεις από την εποχή του Θεωρήματος των Τεσσάρων Χρωμάτων (St Andrews). Το 2024, τα AlphaProof και AlphaGeometry 2 έφτασαν σε επίπεδο αργυρού μεταλλίου σε μαθηματική ολυμπιάδα, λύνοντας όμως διαγωνιστικές ασκήσεις (Nature). Το Nexus περνά σε ανοιχτά ερευνητικά ερωτήματα. Ακολουθεί επίσης διαφορετική διαδρομή από τον ισχυρισμό της OpenAI για τις εξισώσεις Navier–Stokes, ο οποίος έφτασε στο κοινό ως εταιρική ανακοίνωση πριν τον εξετάσει το Clay (To Brief). Η σύγκριση αφορά τον τρόπο δημοσίευσης και αξιολόγησης, όχι τη μαθηματική αξία.

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