Το πιο πρόσφατο της DeepMind: Ένα AI για το χειρισμό μαθηματικών αποδείξεων
Ακριβώς όπως το AlphaZero, το AlphaProof στις περισσότερες περιπτώσεις χρησιμοποιούσε δύο κύρια στοιχεία. Το πρώτο ήταν ένα τεράστιο νευρωνικό δίκτυο με μερικά δισεκατομμύρια παραμέτρους που έμαθαν να εργάζονται στο Lean περιβάλλον μέσω δοκιμής και λάθους. Επιβραβεύτηκε για κάθε αποδεδειγμένη ή απορριφθείσα δήλωση και τιμωρήθηκε για κάθε συλλογιστικό βήμα που έκανε, κάτι που ήταν ένας τρόπος να παρακινηθούν σύντομες, κομψές αποδείξεις. Εκπαιδεύτηκε επίσης να χρησιμοποιεί ένα δεύτερο στοιχείο, το οποίο ήταν ένας αλγόριθμος αναζήτησης δέντρου. Αυτό διερεύνησε όλες τις πιθανές ενέργειες που θα μπορούσαν να γίνουν για να προωθηθεί η απόδειξη σε κάθε βήμα. Επειδή ο αριθμός των πιθανών ενεργειών στα μαθηματικά μπορεί να είναι σχεδόν άπειρος, η δουλειά του νευρωνικού δικτύου ήταν να εξετάσει τους διαθέσιμους κλάδους στο δέντρο αναζήτησης και να δεσμεύσει τον υπολογιστικό προϋπολογισμό μόνο στους πιο πολλά υποσχόμενους. Μετά από μερικές εβδομάδες προπόνησης, το σύστημα θα μπορούσε να σκοράρει καλά στα περισσότερα σημεία αναφοράς μαθηματικών αγώνων με βάση προβλήματα που προήλθαν από προηγούμενους διαγωνισμούς γυμνασίου, αλλά και πάλι δυσκολευόταν με τα πιο δύσκολα από αυτά. Για να τα αντιμετωπίσει, η ομάδα πρόσθεσε ένα τρίτο στοιχείο που δεν υπήρχε στο AlphaZero. Ή οπουδήποτε αλλού. Spark of humanity Το τρίτο συστατικό, που ονομάζεται Test-Time Reinforcement Learning (TTRL), μιμείται κατά προσέγγιση τον τρόπο με τον οποίο οι μαθηματικοί προσεγγίζουν τα πιο δύσκολα προβλήματα. Το μαθησιακό μέρος βασίστηκε στον ίδιο συνδυασμό νευρωνικών δικτύων με αλγόριθμους δέντρων αναζήτησης. Η διαφορά προήλθε από αυτό που έμαθε. Αντί να βασίζεται σε μια ευρεία βάση δεδομένων με αυτόματα επισημοποιημένα προβλήματα, το AlphaProof που εργάζεται στη λειτουργία TTRL ξεκίνησε τη δουλειά του δημιουργώντας ένα εντελώς νέο σύνολο δεδομένων εκπαίδευσης με βάση το πρόβλημα που αντιμετώπιζε. Η διαδικασία περιλάμβανε τη δημιουργία αμέτρητων παραλλαγών της αρχικής δήλωσης, μερικές απλοποιημένες λίγο περισσότερο, άλλες πιο γενικές και άλλες μόνο χαλαρά συνδεδεμένες με αυτήν. Στη συνέχεια το σύστημα προσπάθησε να τις αποδείξει ή να τις διαψεύσει. Ήταν περίπου αυτό που κάνουν οι περισσότεροι άνθρωποι όταν αντιμετωπίζουν ένα ιδιαίτερα σκληρό παζλ, το ισοδύναμο της τεχνητής νοημοσύνης του να λένε, «Δεν το καταλαβαίνω, οπότε ας δοκιμάσουμε πρώτα μια πιο εύκολη εκδοχή αυτού για να εξασκηθούμε». Αυτό επέτρεψε στο AlphaProof να μάθει εν κινήσει και λειτούργησε εκπληκτικά καλά.
Δημοσιεύτηκε: 2025-11-19 15:57:00
πηγή: arstechnica.com
