Αυτόματη απόδειξη μαθηματικών θεωρημάτων στη Lean 4 με χρήση μεγάλων γλωσσικών μοντέλων

Abstract

Η παρούσα διπλωματική εργασία εστιάζει στην ανάπτυξη, υλοποίηση και αξιολόγηση ενός συστήματος αυτόματης απόδειξης μαθηματικών θεωρημάτων στη γλώσσα Lean 4, αξιοποιώντας Μεγάλα Γλωσσικά Μοντέλα (Large Language Models – LLMs) σε συνδυασμό με εξειδικευμένες τεχνικές ανάκτησης (retriever) και ανακατάταξης (reranker) μαθηματικών προτάσεων. Η ερευνητική προσέγγιση που ακολουθήθηκε επιδιώκει να συνδυάσει τη γλωσσική ισχύ των LLMs με την αυστηρότητα και την ακρίβεια των τυπικών αποδεικτικών συστημάτων, ώστε να παραχθεί ένα πλαίσιο ικανό να επιλύει θεωρήματα με υψηλό βαθμό αυτοματοποίησης. Στο θεωρητικό μέρος της εργασίας παρουσιάζεται το επιστημονικό υπόβαθρο της αυτοματοποιημένης απόδειξης θεωρημάτων, αναλύονται οι κύριες κατηγορίες συστημάτων και εξετάζονται οι σύγχρονες ερευνητικές κατευθύνσεις που ενσωματώνουν βαθιά μάθηση στην αποδεικτική διαδικασία. Ιδιαίτερη έμφαση δίνεται στο σύστημα του Lean 4 και της βιβλιοθήκης Mathlib, καθώς και σε εργαλεία όπως το LeanDojo, τα οποία επιτρέπουν την αλληλεπίδραση των LLMs με το περιβάλλον απόδειξης και την επαλήθευση των παραγόμενων βημάτων. Στο πρακτικό μέρος περιγράφεται η κατασκευή ενός εξειδικευμένου corpus θεωρημάτων γραμμικής άλγεβρας, η εκπαίδευση του retriever για την ανάκτηση των πιο συναφών premises και η ανάπτυξη του reranker για την ανακατάταξή τους με βάση τη σημασιολογική ομοιότητα. Στη συνέχεια, ενσωματώνεται το LLM DeepSeek, το οποίο παράγει δυναμικά Lean τακτικές ακολουθώντας προσεκτικά διαμορφωμένα prompts. Η εκτέλεση και επαλήθευση των παραγόμενων τακτικών πραγματοποιείται μέσω του LeanDojo API, διασφαλίζοντας την εγκυρότητα και την αλληλουχία των αποδεικτικών βημάτων. Η αξιολόγηση του συστήματος πραγματοποιήθηκε μετρώντας το ποσοστό επιτυχίας της ολοκλήρωσης των μαθηματικών αποδείξεων και αναλύοντας την ποιότητα και αποτελεσματικότητα των παραγόμενων τακτικών. Τα αποτελέσματα καταδεικνύουν ότι η συνδυαστική προσέγγιση retriever–reranker–LLM βελτιώνει ουσιαστικά την απόδοση σε σχέση με μεθόδους που βασίζονται αποκλειστικά σε εκπαιδευμένα LLMs. Τέλος η εργασία αυτή συμβάλλει στην κατανόηση και στην πρακτική υλοποίηση μεθόδων που συνδυάζουν LLMs και συστήματα τυπικής επαλήθευσης, ανοίγοντας τον δρόμο για την ανάπτυξη πιο αποδοτικών, επεκτάσιμων και πλήρως αυτοματοποιημένων συστημάτων απόδειξης μαθηματικών θεωρημάτων στο μέλλον.