Νέα

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Νέα Έκθεση Σοφίας

Επιμέλεια: Τμήμα Σύνταξης

[Εισαγωγή στη Νέα Σοφία] Μόλις τώρα, το τελευταίο μαθηματικό μοντέλο της Google DeepMind κέρδισε το ασημένιο μετάλλιο της Μαθηματικής Ολυμπιάδας του ΙΜΟ! Όχι μόνο έλυσε 4 από τις 6 ερωτήσεις με τέλεια βαθμολογία, μόλις 1 βαθμό μακριά από το χρυσό μετάλλιο, αλλά χρειάστηκε μόνο 19 δευτερόλεπτα για να λύσει την 4η ερώτηση Η ποιότητα και η ταχύτητα επίλυσης του προβλήματος κατέπληξε τους κριτές που σημείωσαν .

Το AI κέρδισε το ασημένιο μετάλλιο της Μαθηματικής Ολυμπιάδας του IMO!

Μόλις τώρα, το Google DeepMind ανακοίνωσε ότι οι πραγματικές ερωτήσεις της φετινής Διεθνούς Μαθηματικής Ολυμπιάδας δημιουργήθηκαν από το δικό της σύστημα AI.

Μεταξύ αυτών, η τεχνητή νοημοσύνη όχι μόνο ολοκλήρωσε με επιτυχία 4 από τις 6 ερωτήσεις, αλλά έλαβε επίσης πλήρη βαθμολογία για κάθε ερώτηση, η οποία ισοδυναμεί με την υψηλότερη βαθμολογία ενός ασημένιου μεταλλίου - 28 βαθμούς.

Αυτό το αποτέλεσμα απέχει μόλις 1 βαθμό από το χρυσό μετάλλιο!

Μεταξύ 609 διαγωνιζομένων, μόνο 58 κέρδισαν χρυσά μετάλλια

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

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

Αυτό που συνέβαλε σημαντικά αυτή τη φορά ήταν δύο συστήματα AI - το AlphaProof και το AlphaGeometry 2.

Σημαντικό σημείο: Το 2024 IMO δεν περιλαμβάνεται στα δεδομένα εκπαίδευσης αυτών των δύο AI.

Ο Scott Wu, ένας από τους ιδρυτές πίσω από τον μηχανικό AI Devin (τρεις φορές χρυσός Ολυμπιονίκης του IOI) θρηνούσε: «Όταν ήμουν παιδί, οι Ολυμπιάδες ήταν το μόνο που είχα, ποτέ δεν πίστευα ότι μόλις 10 χρόνια αργότερα θα αντικατασταθούν από την AI λύθηκε».

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

Η μαθηματική συλλογιστική ικανότητα του AI σοκάρει τον καθηγητή

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

Οι δύο παίκτες AI που εμφανίστηκαν μαζί σήμερα έσπασαν αυτόν τον περιορισμό. είναι αντίστοιχα--

- AlphaProof, ένα νέο σύστημα επίσημης μαθηματικής συλλογιστικής που βασίζεται στην ενισχυτική μάθηση

- AlphaGeometry 2, το δεύτερης γενιάς γεωμετρικό σύστημα επίλυσης προβλημάτων

Οι απαντήσεις που δόθηκαν από τα δύο AI βαθμολογήθηκαν σύμφωνα με τους κανόνες από τους διάσημους μαθηματικούς, καθηγητή Timothy Gowers (χρυσό μετάλλιο του IMO και μετάλλιο Fields) και τον Dr. Joseph Myers (δύο φορές Χρυσό Μετάλλιο του IMO και Πρόεδρο της Επιτροπής Επιλογής Ερωτήσεων του IMO 2024). .

Στο τέλος, το AlphaProof έλυσε σωστά δύο αλγεβρικές ερωτήσεις και μια ερώτηση θεωρίας αριθμών.

Υπάρχουν μόνο δύο συνδυαστικά προβλήματα μαθηματικών που δεν έχουν κατακτηθεί.

Ο καθηγητής Timothy Gowers σοκαρίστηκε επίσης βαθιά κατά τη διαδικασία βαθμολόγησης——

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

AlphaProof

Το AlphaProof είναι ένα σύστημα ικανό να αποδεικνύει μαθηματικές προτάσεις στην επίσημη γλώσσα Lean.

Συνδυάζει ένα προ-εκπαιδευμένο μοντέλο μεγάλης γλώσσας με τον αλγόριθμο μάθησης ενίσχυσης AlphaZero, ο οποίος έμαθε να κυριαρχεί στο σκάκι, το shogi και το Go.

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

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

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

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

Κάθε απόδειξη που βρίσκεται και επαληθεύεται χρησιμοποιείται για την ενίσχυση του γλωσσικού μοντέλου του AlphaProof ώστε να μπορεί να λύσει πιο δύσκολα προβλήματα στο μέλλον.

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

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

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

ΑλφαΓεωμετρία 2

Το AlphaGeometry 2, η αναβαθμισμένη έκδοση του AlphaGeometry, είναι ένα νευρωνικό-συμβολικό υβριδικό σύστημα που εκπαιδεύεται από την αρχή και βασίζεται στο γλωσσικό μοντέλο του Gemini.

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

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

Πριν από τη συμμετοχή του στον ΙΜΟ φέτος, το AlphaGeometry 2 είχε ήδη σημειώσει μεγάλη επιτυχία: μπορούσε να λύσει το 83% των προβλημάτων γεωμετρίας του ΙΜΟ τα τελευταία 25 χρόνια, ενώ η πρώτη γενιά μπορούσε να λύσει μόνο το 53%.

Σε αυτόν τον IMO, η ταχύτητα του AlphaGeometry 2 σόκαρε τους πάντες - μέσα σε 19 δευτερόλεπτα από τη λήψη της επίσημης ερώτησης, έλυσε την ερώτηση 4!

Η ερώτηση 4 απαιτεί απόδειξη ότι το άθροισμα των ∠KIL και ∠XPY είναι ίσο με 180°. Το AlphaGeometry 2 συνιστά την κατασκευή ενός σημείου Ε στη γραμμή BI έτσι ώστε ∠AEB=90°.Το σημείο Ε βοηθά στον προσδιορισμό του μέσου L του AB, σχηματίζοντας πολλά παρόμοια ζεύγη τριγώνων, όπως ABE ~ YBI και ALE ~ IPC, αποδεικνύοντας έτσι το συμπέρασμα

Διαδικασία επίλυσης προβλημάτων AI

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

Σε γενικές γραμμές, η πρώτη ερώτηση (P1) σε κάθε δοκιμή IMO είναι σχετικά εύκολη.

Οι χρήστες του Διαδικτύου είπαν, "Το P1 απαιτεί μόνο γνώσεις μαθηματικών γυμνασίου και οι άνθρωποι που παίζουν συνήθως το ολοκληρώνουν μέσα σε 60 λεπτά."

Η πρώτη ερώτηση του IMO 2024 εξετάζει κυρίως τις ιδιότητες του πραγματικού αριθμού α και απαιτεί την εύρεση ενός πραγματικού αριθμού α που να ικανοποιεί ορισμένες προϋποθέσεις.

Το AI έδωσε τη σωστή απάντηση - ο α είναι άρτιος ακέραιος. Λοιπόν, πώς ακριβώς απαντάται;

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

Το σύνολο στα αριστερά αντιπροσωπεύει ότι όλοι οι πραγματικοί αριθμοί α που πληρούν τις προϋποθέσεις, για οποιονδήποτε θετικό ακέραιο n, n μπορούν να διαιρέσουν το ⌊i*α⌋ από το 1 στο n το σύνολο στα δεξιά αντιπροσωπεύει ότι υπάρχει ένας ακέραιος k, το k είναι ένας άρτιος αριθμός και ο πραγματικός αριθμός α είναι ίσος με k.

Η παρακάτω απόδειξη χωρίζεται σε δύο κατευθύνσεις.

Πρώτα να αποδείξετε ότι το σύνολο στα δεξιά είναι ένα υποσύνολο (απλή κατεύθυνση) του συνόλου στα αριστερά.

Στη συνέχεια, αποδείξτε ότι το σύνολο στα αριστερά είναι υποσύνολο του συνόλου στα δεξιά (δύσκολη κατεύθυνση).

Μέχρι το τέλος του κώδικα, η τεχνητή νοημοσύνη κατέληξε σε μια βασική εξίσωση ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋), χρησιμοποιώντας την εξίσωση για να αποδείξει ότι το α πρέπει να είναι Ζυγός αριθμός.

Τέλος, η DeepMind συνόψισε τα τρία αξιώματα στα οποία βασίζεται η τεχνητή νοημοσύνη στη διαδικασία επίλυσης προβλημάτων: propext, Classical.choice και Quot.sound.

Ακολουθεί η πλήρης διαδικασία επίλυσης προβλημάτων του P1: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

P2

Η δεύτερη ερώτηση εξετάζει τη σχέση μεταξύ του ζεύγους των θετικών ακεραίων (a, b), που περιλαμβάνει την ιδιότητα του μεγαλύτερου κοινού διαιρέτη.

Η απάντηση που λύθηκε από το AI είναι:

Το θεώρημα είναι ότι για ένα ζεύγος θετικών ακεραίων (a, b) που ικανοποιεί ορισμένες προϋποθέσεις, το σύνολο του μπορεί να περιέχει μόνο (1,1).

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

Να αποδείξετε ότι η (1,1) είναι η τελική λύση, χρησιμοποιώντας g=2, N=3.

Δείξτε ότι αν το (a,b) είναι η λύση, τότε το ab+1 πρέπει να διαιρέσει το g.

Σε αυτή τη διαδικασία, η τεχνητή νοημοσύνη χρησιμοποίησε το θεώρημα του Euler και τις ιδιότητες των αρθρωτών πράξεων για συλλογισμό.

Τέλος, να αποδείξετε ότι η a=b=1 είναι η μόνη δυνατή λύση.

Ακολουθεί η πλήρης διαδικασία επίλυσης προβλημάτων του P2: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

P4

Το P4 είναι μια ερώτηση γεωμετρικής απόδειξης που απαιτεί την απόδειξη μιας συγκεκριμένης σχέσης γεωμετρικής γωνίας.

Όπως προαναφέρθηκε, αυτό ολοκληρώθηκε από το AlphaGeometry 2 σε 19 δευτερόλεπτα, σημειώνοντας νέο ρεκόρ.

Ανάλογα με τη λύση που δίνεται, όπως και με το AlphaGeometry πρώτης γενιάς, τα βοηθητικά σημεία σε όλες τις λύσεις δημιουργούνται αυτόματα από το γλωσσικό μοντέλο.

Στην απόδειξη, όλες οι γωνίες παρακολούθησης χρησιμοποιούν Gaussian elimination, και d(AB)−d(CD) είναι ίσο με τη γωνία κατεύθυνσης από AB σε CD (modulo π).

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

Στη συνέχεια, ακολουθούν τα βήματα για την επίλυση του προβλήματος της ΑλφαΓεωμετρίας, το οποίο ολοκληρώνεται με τη χρήση της «μέθοδος αντιπαράθεσης».

Χρησιμοποιήστε πρώτα το Lean για να επισημοποιήσετε τις προτάσεις που πρέπει να αποδειχθούν και να οπτικοποιήσετε τη γεωμετρική κατασκευή.

Τα βασικά βήματα στην απόδειξη είναι τα εξής.

Δείτε την παρακάτω εικόνα για την πλήρη διαδικασία επίλυσης προβλημάτων: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

P6

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

Το AI λύνει, c=2.

Ας δούμε πρώτα τη δήλωση του θεωρήματος, η οποία ορίζει τις ιδιότητες της «Υδατοσουλιανής συνάρτησης» και δηλώνει ότι για όλες αυτές τις συναρτήσεις, το σύνολο τιμών f(r)+f(-r) έχει το πολύ 2 στοιχεία.

Η στρατηγική απόδειξης είναι να αποδείξουμε πρώτα ότι για οποιαδήποτε Aquaesulian συνάρτηση, το σύνολο τιμών f(r)+f(-r) έχει το πολύ 2 στοιχεία. Στη συνέχεια κατασκευάστε μια συγκεκριμένη Aquaesulian συνάρτηση έτσι ώστε η f(r)+f(-r) να έχει ακριβώς 2 διαφορετικές τιμές.

Να αποδείξετε ότι όταν f(0)=0, η f(x)+f(-x) παίρνει το πολύ δύο διαφορετικές τιμές, και να αποδείξετε ότι δεν υπάρχει υδατοειδιακή συνάρτηση f(0)≠0.

Να κατασκευάσετε τη συνάρτηση f(x)=-x+2⌈x⌉ και να αποδείξετε ότι είναι υδατοϊσουλιακή συνάρτηση.

Τέλος, να αποδείξετε ότι για αυτή τη συνάρτηση, η f(-1)+f(1) =0 και η f(1/2)+f(-1/2)=2 είναι δύο διαφορετικές τιμές.

Ακολουθεί η πλήρης διαδικασία επίλυσης προβλημάτων: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Μπορείτε να κάνετε ερωτήσεις μαθηματικών της Ολυμπιάδας, αλλά μπορείτε να πείτε ποια είναι μεγαλύτερη, 9,11 ή 9,9;

Ο Andrew Gao, ερευνητής στο Πανεπιστήμιο του Στάνφορντ και στη Sequoia, επιβεβαίωσε τη σημασία αυτής της ανακάλυψης της τεχνητής νοημοσύνης——

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

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

Ο Jim Fan, ανώτερος επιστήμονας της Nvidia, δημοσίευσε ένα μεγάλο άρθρο λέγοντας ότι τα μεγάλα μοντέλα είναι μυστηριώδεις υπάρξεις——

Μπορούν να κερδίσουν ασημένια μετάλλια σε Ολυμπιάδες μαθηματικών και συχνά κάνουν λάθη σε ερωτήσεις όπως "Ποιος αριθμός είναι μεγαλύτερος, 9,11 ή 9,9;"

Όχι μόνο οι Δίδυμοι, αλλά και οι GPT-4o, Claude-3.5 και Llama-3 δεν μπορούν να απαντήσουν 100% σωστά.

Εκπαιδεύοντας μοντέλα AI, εξερευνούμε τεράστιες περιοχές πέρα ​​από τη δική μας νοημοσύνη.Στην πορεία, ανακαλύψαμε μια πολύ περίεργη περιοχή - έναν εξωπλανήτη που μοιάζει με τη Γη αλλά είναι γεμάτος παράξενες κοιλάδες

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

Το AlphaProof και το AlphaGeometry 2 εκπαιδεύονται σε επίσημες αποδείξεις και συμβολικές μηχανές για συγκεκριμένο τομέα. Σε κάποιο βαθμό, είναι καλύτεροι στην επίλυση εξειδικευμένων προβλημάτων Ολυμπιάδας, παρόλο που είναι χτισμένα σε ένα LLM γενικής χρήσης. Το σετ εκπαίδευσης του GPT-4o αναμιγνύεται με μεγάλη ποσότητα δεδομένων κώδικα GitHub, τα οποία μπορεί να υπερβαίνουν κατά πολύ τα μαθηματικά δεδομένα. Μεταξύ των εκδόσεων λογισμικού, το "v9.11 > v9.9" ενδέχεται να παραμορφώσει σοβαρά τη διανομή δεδομένων. Επομένως, αυτό το σφάλμα είναι κατανοητό σε κάποιο βαθμό.

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

Άλλοι χρήστες του Διαδικτύου είπαν ότι υπήρχαν πάρα πολλές πληροφορίες αυτή την εβδομάδα.

Βιβλιογραφικές αναφορές:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://x.com/DrJimFan/status/1816521330298356181