Η διατύπωση σημαντικών μαθηματικών εικασιών βασιζόταν παραδοσιακά στην ανθρώπινη διαίσθηση των ειδικών, στερούμενη μιας ενοποιημένης μεθόδου για συστηματική παραγωγή. Μια νέα ερευνητική εργασία που δημοσιεύθηκε στο arXiv προτείνει ένα πλαίσιο βασισμένο σε Μεγάλα Γλωσσικά Μοντέλα (LLMs) για την ανακάλυψη προβλημάτων με «υψηλό γούστο» (high problem taste) — εικασίες, δηλαδή, που θα μπορούσαν να αναδιοργανώσουν τη γλώσσα ενός ερευνητικού πεδίου.
Η Μεθοδολογία των Τριών Σταδίων
Οι ερευνητές ανέπτυξαν μια διαδικασία τριών επιπέδων για τη διασφάλιση της ποιότητας και της εγκυρότητας των προτεινόμενων εικασιών:
- Αναζήτηση Περιοχής: Εξαγωγή στοιχείων από τοπικές ενότητες τεκμηρίωσης.
- Αναστοχαστική Επικύρωση: Αξιολόγηση της θεμελιώδους φύσης, της καινοτομίας και της δυνητικής σημασίας της εικασίας.
- Τυπική Επικύρωση: Χρήση της γλώσσας προγραμματισμού Lean 4 και της βιβλιοθήκης Mathlib για τον έλεγχο της ορθότητας της διατύπωσης.
Πειραματικά Αποτελέσματα
Η εφαρμογή του πλαισίου σε είκοσι υποψήφιες εικασίες έδειξε αξιοσημείωτη σταθερότητα στη μετάφραση από τη φυσική γλώσσα σε τυπικούς μαθηματικούς ελέγχους. Και οι 20 υποψήφιες εικασίες πέρασαν επιτυχώς τον έλεγχο σύνταξης και τύπων (type checking) στο Lean 4. Επιπλέον, καμία από αυτές δεν απορροφήθηκε άμεσα από την εντολή exact? ούτε επιλύθηκε αυτόματα από το εργαλείο aesop, επιβεβαιώνοντας ότι οι προτάσεις δεν ήταν τετριμμένες ή ήδη γνωστές στο σύστημα.
Σύμφωνα με την έρευνα, ο στόχος είναι η ανακάλυψη προβλημάτων των οποίων οι αποδείξεις θα μπορούσαν να προσφέρουν διαρκή βοήθεια στην ανθρώπινη μαθηματική έρευνα, αντί για απλή παραγωγή τυχαίων προτάσεων.
