DeepMind: οι εννέα αποδείξεις περνούν έλεγχο πρωτοτυπίας

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

Ένας κριτής που δεν εντυπωσιάζεται από το ύφος

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

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

Η ομάδα περιγράφει τον αλγόριθμο ως σύστημα που αναζητά αποδείξεις γραμμένες στο Lean. Οι ερευνητές τού έδωσαν επίσης πρόσβαση στο AlphaProof, ένα παλαιότερο σύστημα της DeepMind, σχεδιασμένο ειδικά για αποδείξεις. Στις δοκιμές της ομάδας, όμως, η απλούστερη εκδοχή έφερε τα ίδια αποτελέσματα: ένα γλωσσικό μοντέλο σε συνδυασμό με το Lean, χωρίς το AlphaProof, έλυσε και τα εννέα προβλήματα του Έρντος (The Decoder). Για αυτά τα προβλήματα, το εξειδικευμένο σύστημα αποδείχθηκε περιττό.

Η μελέτη παρουσιάζει αποδείξεις που πέρασαν τον έλεγχο για τα εννέα προβλήματα του Έρντος και για 44 εικασίες — ισχυρισμούς που θεωρούνται αληθείς, αλλά δεν έχουν αποδειχθεί — από το Online Encyclopedia of Integer Sequences, ένα εκτενές αρχείο αριθμητικών μοτίβων (Science). Ανάμεσα στα αποτελέσματα για τον Έρντος είναι η απάντηση σε ένα ερώτημα δύο σκελών για τους ακέραιους αριθμούς, το οποίο είχε θέσει μαζί με τον Άντρας Σάρκοζι το 1970. Το ερώτημα παρέμενε ανοιχτό για περισσότερο από μισό αιώνα (ABC).

Τι δεν μπορεί να κρίνει ο ελεγκτής

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

Το πρόβλημα του 1970 δείχνει γιατί έχουν σημασία τα δύο τελευταία ερωτήματα. Το δεύτερο σκέλος του συνεπάγεται το πρώτο, επομένως μία απόδειξη αρκεί για να λυθούν και τα δύο. Όταν κυκλοφόρησαν οι αποδείξεις του συστήματος, διαπιστώθηκε ότι μια μικρή τροποποίηση σε κατασκευή του αρχικού άρθρου του 1970 αρκεί επίσης για να απαντηθούν και τα δύο σκέλη (arXiv). Οι αποδείξεις του συστήματος ήταν σωστές· απλώς το πρόβλημα βρισκόταν πιο κοντά στη λύση απ’ όσο άφηνε να εννοηθεί ο χαρακτηρισμός του ως «ανοιχτού».

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

Αυτός ο καταμερισμός εργασίας διαφοροποιεί τη μελέτη από ένα ορόσημο του προηγούμενου μήνα. Τότε, το Claude της Anthropic μετέτρεψε στο Lean την ήδη γνωστή απόδειξη του Τελευταίου Θεωρήματος του Φερμά (To Brief). Η μεταφορά μιας διάσημης απόδειξης σε άλλη γλώσσα δεν γεννά αμφιβολίες για την πρωτοτυπία της. Η αναζήτηση ανάμεσα σε προβλήματα που θεωρούνται ακόμη ανοιχτά τις γεννά, και γι’ αυτό ο έλεγχος της πρωτοτυπίας γίνεται κεντρικός.

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