Μια αξιοσημείωτη εξέλιξη στον χώρο της τεχνητής νοημοσύνης (ΤΝ) έρχεται από την Κίνα, όπου ένα πλαίσιο τεχνητής νοημοσύνης κατάφερε να λύσει αυτόνομα ένα ανοιχτό μαθηματικό πρόβλημα, το οποίο είχε τεθεί πριν από πάνω από μια δεκαετία από έναν Αμερικανό μαθηματικό. Η ομάδα από το Πανεπιστήμιο του Πεκίνου, που ανέπτυξε το εν λόγω σύστημα, ανακοίνωσε ότι το πλαίσιο επέλυσε επιτυχώς την εικασία του Dan Anderson, πρώην καθηγητή στο Πανεπιστήμιο της Iowa, ο οποίος απεβίωσε το 2022.
Το πρωτοποριακό σύστημα, περιγράφεται σε μια ερευνητική δημοσίευση που αναρτήθηκε στις 4 Απριλίου. Αξιοποιώντας δεκαετίες μαθηματικής βιβλιογραφίας, η ΤΝ της κινεζικής ομάδας γεφύρωσε το χάσμα μεταξύ της συλλογιστικής σε φυσική γλώσσα και της τυπικής επαλήθευσης από μηχανή. Με αυτόν τον τρόπο, όχι μόνο επιλύθηκε το πρόβλημα που είχε θέσει ο Anderson το 2014, αλλά η ΤΝ επαλήθευσε και τα δικά της ευρήματα. «Χρησιμοποιώντας αυτό το πλαίσιο, επιλύσαμε επιτυχώς ένα ανοιχτό πρόβλημα στην αντιμεταθετική άλγεβρα και τυποποιήσαμε αυτόματα την απόδειξη με ελάχιστη ανθρώπινη παρέμβαση», ανέφεραν οι ερευνητές.
Η ικανότητα της ΤΝ να εκτελεί μαθηματικές εργασίες ταχύτερα από τους ανθρώπους είναι εντυπωσιακή, ξεπερνώντας ακόμη και εργασίες που παραδοσιακά απαιτούν συνεργασία ειδικών από διαφορετικά πεδία. Αυτό το επίτευγμα αποτελεί ένα σαφές παράδειγμα του πώς η μαθηματική έρευνα μπορεί να αυτοματοποιηθεί σε μεγάλο βαθμό μέσω της ΤΝ, όπως αναφέρεται στην εργασία που, παρόλο που δεν έχει ακόμη αξιολογηθεί από ομοτίμους, δημοσιεύτηκε στο arXiv.
Η ομάδα, υπό την καθοδήγηση του καθηγητή Dong Bin, περιλάμβανε επιστήμονες από τα πανεπιστήμια Westlake και Tianjin, καθώς και από το IQuest Research. Η χρήση συστημάτων ΤΝ για την επίλυση μαθηματικών προβλημάτων γνωρίζει ραγδαία ανάπτυξη, ιδιαίτερα χάρη στις προόδους στα μεγάλα γλωσσικά μοντέλα (LLMs), τα οποία έχουν επιτρέψει την μετάβαση από απλά προβλήματα σε ερευνητικού επιπέδου.
Παρόλο που LLMs όπως το Gemini Deep Think της Google έχουν σημειώσει εντυπωσιακές επιδόσεις, οι ερευνητές τονίζουν ότι η χρήση agents ΤΝ σε ερευνητικά προβλήματα απαιτεί σημαντική ανθρώπινη επίβλεψη. «Οι μαθηματικές αποδείξεις απαιτούν απόλυτη αυστηρότητα, και ακόμη και οι αποδείξεις που γράφονται από ειδικούς μπορεί να περιέχουν ανεπαίσθητες αδυναμίες. Οι αποδείξεις που παράγονται από LLMs, τα οποία είναι επιρρεπή σε “παραισθήσεις”, είναι πολύ λιγότερο αξιόπιστες», εξηγούν. «Με βάση αυτό, προτείνουμε ένα πλαίσιο για αυτόνομη αντιμετώπιση και επαλήθευση ερευνητικής μαθηματικής, το οποίο ενσωματώνει έναν agent φυσικής γλώσσας με έναν agent τυποποίησης».
Το σύστημα αποτελείται από δύο κύρια στοιχεία: τον agent Rethlas, ο οποίος χρησιμοποιεί τη μηχανή αναζήτησης μαθηματικών θεωρημάτων (Matlas) για να εξερευνήσει στρατηγικές και να κατασκευάσει υποψήφιες αποδείξεις, και τον agent Archon, ο οποίος μετατρέπει αυτές τις άτυπες αποδείξεις σε πλήρως επαληθευμένα έργα Lean 4, χρησιμοποιώντας τη μηχανή αναζήτησης θεωρημάτων LeanSearch. Το Lean 4, ένα διαδραστικό εργαλείο απόδειξης θεωρημάτων και γλώσσα προγραμματισμού, διαθέτει μια τεράστια βιβλιοθήκη, τη Mathlib, με εκατοντάδες χιλιάδες θεωρήματα και ορισμούς.
Η ομάδα εφάρμοσε το πλαίσιο ΤΝ για την επίλυση του ανοιχτού προβλήματος του Anderson σχετικά με τους quasi-complete Noetherian local rings, μια έννοια στην αντιμεταθετική άλγεβρα. Μετά την εύρεση μιας άτυπης απόδειξης για ένα αντίθετο παράδειγμα που απέκλειε την υπόθεση του ανοιχτού ερωτήματος, το σύστημα ολοκλήρωσε την τυποποίηση εντός 80 ωρών. Η μόνη ανθρώπινη παρέμβαση αφορούσε τη λήψη αρχείων που η ΤΝ δεν μπορούσε να ανακτήσει μόνη της, χωρίς να απαιτείται καμία μαθηματική κρίση.
Η ερευνητική ομάδα διαπίστωσε ότι, αν και η ΤΝ μπορούσε να λύσει το πρόβλημα αυτόνομα, ένας μαθηματικός θα μπορούσε να καθοδηγήσει τον Archon, παρόμοια με τον τρόπο που θα εξηγούσε μια απόδειξη σε έναν μεταπτυχιακό φοιτητή, επιταχύνοντας έτσι τη διαδικασία. «Συνολικά, τα αποτελέσματά μας δείχνουν ότι, για ένα πραγματικό ανοιχτό πρόβλημα στα μαθηματικά, οι agents άτυπης συλλογιστικής και οι τυπικοί agents μπορούν να συνεργαστούν αποτελεσματικά», κατέληξαν οι ερευνητές.
«Στον πυρήνα της αποστολής μας βρίσκεται η συμβιωτική σχέση μεταξύ ΤΝ και μαθηματικών», αναφέρεται στον προσωπικό ιστότοπο της ερευνητικής ομάδας. «Ενώ τα μαθηματικά παρέχουν το θεωρητικό θεμέλιο για την ανάπτυξη της ΤΝ, τα εργαλεία ΤΝ μπορούν να επιταχύνουν την ίδια την μαθηματική έρευνα».
