Τα μεγάλα γλωσσικά μοντέλα εκπαιδεύτηκαν να γράφουν κείμενο, όχι να αποδεικνύουν θεωρήματα. Κι όμως, το 2026 παράγουν αποτελέσματα που ελέγχουν κορυφαίοι μαθηματικοί. Για να καταλάβουμε πώς γίνεται αυτό, πρέπει να κοιτάξουμε τους μηχανισμούς ελέγχου που χτίστηκαν γύρω από τα μοντέλα, και αρκετοί από αυτούς είναι, στην ουσία τους, μηχανισμοί μετάφρασης ανάμεσα σε γλώσσες.
Στις 26 Οκτωβρίου η OpenAI και, λίγες ώρες αργότερα, η Anthropic δημοσίευσαν αποδείξεις ότι η Υπόθεση του Εκθετικού Χρόνου (ETH), μια εικασία της θεωρητικής πληροφορικής του 1999, είναι λανθασμένη. Τα αποτελέσματα ελέγχονται ακόμη από ομάδα με επικεφαλής δύο από τους επιστήμονες που διατύπωσαν την εικασία (Scientific American). Το ερώτημα που μας απασχολεί εδώ είναι πιο βασικό: πώς φτάνει ένα σύστημα που προβλέπει λέξεις σε μια μαθηματική απόδειξη;
Ένα μοντέλο που προβλέπει κείμενο
Ένα μεγάλο γλωσσικό μοντέλο δεν υπολογίζει όπως ένα σύστημα συμβολικής άλγεβρας. Παράγει κείμενο λέξη προς λέξη, με βάση πιθανότητες που έμαθε από τεράστιο όγκο γραπτών, ανάμεσά τους και μαθηματικών. Η αντίθεση με τον άνθρωπο είναι ενδιαφέρουσα. Στον ανθρώπινο εγκέφαλο το γλωσσικό δίκτυο μένει σχεδόν ανενεργό όταν λύνουμε μαθηματικά προβλήματα (Fedorenko, Piantadosi & Gibson, Nature 2024). Το γλωσσικό μοντέλο ακολουθεί τον αντίστροφο δρόμο, αφού φτάνει στη μαθηματική σκέψη μόνο μέσα από τη γλώσσα.
Η πρώτη ουσιαστική βελτίωση ήρθε το 2022, όταν φάνηκε ότι αν το μοντέλο γράψει τα ενδιάμεσα βήματα πριν απαντήσει, τη λεγόμενη «αλυσίδα σκέψης», λύνει σωστά πολυβηματικά προβλήματα πολύ συχνότερα (Wei κ.ά., 2022). Χρειάζεται, λοιπόν, κι αυτό ένα πρόχειρο.
Ανταμοιβή μόνο για τη σωστή απάντηση
Το επόμενο βήμα ήταν η ενισχυτική μάθηση. Το μοντέλο λύνει χιλιάδες προβλήματα με ελέγξιμη απάντηση και ανταμείβεται μόνο όταν το αποτέλεσμα είναι σωστό, χωρίς να του δείχνει κανείς πώς να σκεφτεί. Στο DeepSeek-R1, που δημοσιεύτηκε στο Nature και διατίθεται με ανοιχτά βάρη, συμπεριφορές όπως ο αυτοέλεγχος και η επιστροφή σε προηγούμενο βήμα εμφανίστηκαν χωρίς ανθρώπινα παραδείγματα συλλογισμού. Η OpenAI είχε ήδη δείξει ότι η επίδοση ανεβαίνει τόσο με περισσότερη τέτοια εκπαίδευση όσο και με περισσότερο χρόνο «σκέψης» τη στιγμή της απάντησης (OpenAI, 2024). Με παρόμοιες τεχνικές και παράλληλη εξερεύνηση πολλών λύσεων, το Gemini Deep Think έφτασε το 2025 σε επίπεδο χρυσού μεταλλίου στη Διεθνή Μαθηματική Ολυμπιάδα, γράφοντας αποδείξεις σε φυσική γλώσσα μέσα στο χρονικό όριο του διαγωνισμού (Google DeepMind).
Όταν το μοντέλο γράφει πρόγραμμα αντί για απάντηση
Σε προβλήματα κατασκευής, όπου ζητείται ένα σύνολο ή μια διάταξη με συγκεκριμένη ιδιότητα, η στρατηγική αλλάζει. Το μοντέλο γράφει μικρά προγράμματα που παράγουν υποψήφιες λύσεις, ένας αυτόματος αξιολογητής τα βαθμολογεί και τα καλύτερα επιστρέφουν στο μοντέλο για βελτίωση. Έτσι η μέθοδος FunSearch έδωσε νέες κατασκευές σε ένα κλασικό πρόβλημα συνδυαστικής. Η εξέλιξή της, το AlphaEvolve, δοκιμάστηκε από ομάδα με συμμετοχή του Terence Tao σε 67 προβλήματα (Georgiev κ.ά., 2025). Στα περισσότερα ξαναβρήκε τις γνωστές καλύτερες λύσεις και σε ορισμένα τις βελτίωσε, αν και οι συγγραφείς καταγράφουν και περιπτώσεις όπου το σύστημα εκμεταλλεύτηκε αδυναμίες του αξιολογητή.
Η τυπική γλώσσα ως αυστηρός διορθωτής
Η πιο αξιόπιστη προσέγγιση είναι η τυπική επαλήθευση. Η απόδειξη γράφεται στη γλώσσα Lean, όπου κάθε λογικό βήμα ελέγχεται μηχανικά. Για όσους δουλεύουμε με γλωσσικές τεχνολογίες, εδώ βρίσκεται ίσως το πιο ενδιαφέρον σημείο, γιατί το κρίσιμο βήμα είναι μια μετάφραση. Στο AlphaProof της Google DeepMind ένα δίκτυο μετέφρασε περίπου ένα εκατομμύριο προβλήματα γραμμένα σε φυσική γλώσσα σε δεκάδες εκατομμύρια διατυπώσεις Lean, πάνω στις οποίες εκπαιδεύτηκε το σύστημα. Μαζί με ένα σύστημα γεωμετρίας, έφτασε σε επίπεδο αργυρού μεταλλίου στην Ολυμπιάδα του 2024 (Hubert κ.ά., Nature 2025).
Η μετάφραση αυτή, η «αυτόματη τυποποίηση», είναι όμως και το πιο εύθραυστο σημείο. Η μετατροπή ερευνητικών αποδείξεων από φυσική σε τυπική γλώσσα παραμένει εξαιρετικά δύσκολη (Ma κ.ά., ICLR 2026). Επιπλέον, ο ελεγκτής πιστοποιεί τη διατύπωση που του δόθηκε, όχι το αν αυτή αποδίδει πιστά το αρχικό πρόβλημα. Γι’ αυτό και αποτελέσματα ήδη επαληθευμένα σε Lean, όπως η ανατροπή της ETH, περνούν από ανθρώπινο έλεγχο.
Σε όλες αυτές τις περιπτώσεις διακρίνεται το ίδιο σχήμα. Το μοντέλο προτείνει, κάτι εξωτερικό ελέγχει αντικειμενικά, και ο κύκλος επαναλαμβάνεται χιλιάδες φορές. Με αυτόν τον τρόπο ένα μοντέλο γενικής χρήσης της OpenAI ανέτρεψε τον Μάιο του 2026 την εικασία του Erdős για τις μοναδιαίες αποστάσεις, με την απόδειξη να ελέγχεται από εξωτερικούς μαθηματικούς (OpenAI).
Πού σκοντάφτουν
Όπου λείπει αξιόπιστος ελεγκτής, τα λάθη περνούν απαρατήρητα. Όταν ειδικοί βαθμολόγησαν αποδείξεις μοντέλων για την Ολυμπιάδα των ΗΠΑ του 2025, τα περισσότερα έμειναν κάτω από 5%, ενώ οι αυτόματοι βαθμολογητές υπερεκτιμούσαν σταθερά τις λύσεις (Petrov κ.ά., 2025). Στο πρόγραμμα First Proof, όπου μαθηματικοί έθεσαν αδημοσίευτα ερευνητικά προβλήματα, το καλύτερο σύστημα έλυσε 6 στα 10 στη δεύτερη σειρά δοκιμών. Κατά το Epoch AI, εξάλλου, ακόμη και οι πιο εντυπωσιακές συμβολές της ΤΝ ως τώρα εφάρμοζαν γνωστές τεχνικές, και η ανάπτυξη νέας θεωρίας θα ήταν ποιοτικό άλμα που δεν έχει ακόμη συμβεί.
Γιατί η ανοιχτότητα μετράει εδώ
Αν η παραγωγή υποψήφιων λύσεων γίνεται φθηνή, η κρίσιμη δεξιότητα μετατοπίζεται στον έλεγχο, στην εξήγηση και στη διατύπωση του σωστού ερωτήματος. Και ο έλεγχος προϋποθέτει πρόσβαση. Το Lean και η βιβλιοθήκη mathlib είναι ελεύθερο λογισμικό, το DeepSeek-R1 διατίθεται με ανοιχτά βάρη και ο κώδικας του FunSearch είναι δημόσιος. Ο Tao, άλλωστε, προτείνει ανοιχτού κώδικα μοντέλα ειδικά για τα μαθηματικά, καθώς και εκπαιδευτικό υλικό που θα ενσωματώνει τα νέα αποτελέσματα (Tao, «Math 2.0»). Για μια κοινότητα που χτίζει ανοιχτά γλωσσικά δεδομένα και εργαλεία για τα ελληνικά, το συμπέρασμα έχει πρακτικό περιεχόμενο: χωρίς ανοιχτές υποδομές, ο έλεγχος των αποτελεσμάτων μένει στα χέρια λίγων.
Πηγή άρθρου: glossapi.gr
