Χρήση αρχιτεκτονικής ασύμμετρου Bi-encoder στο πλαίσιο της αυτόματης απόδειξης θεωρημάτων
Asymmetric Bi-encoder architecture in the field of automated theorem proving
Προβολή/
Λέξεις κλειδιά
Θεώρημα ; Μαθηματικά ; Πρόταση ; Απόδειξη ; Lean ; Lean-Dojo ; ReProver ; Retrieval ; Αυτοματοποίηση ; Ασύμμετρος ; Bi-encoder ; Διανυσματική αναπαράσταση ; ΤΝ ; Διαδραστική απόδειξη θεωρημάτων (ITP) ; Αυτοματοποιημένη απόδειξη θεωρημάτων (ATP)Περίληψη
Η παρούσα πτυχιακή εργασία εξετάζει το πρόβλημα της επιλογής μαθηματικών προτάσεων (premise selection) στο πλαίσιο της αυτοματοποιημένης απόδειξης μαθηματικών θεωρημάτων και προτείνει μια εναλλακτική αρχιτεκτονική ασύμμετρου bi-encoder για τη βελτίωση της διαδικασίας ανάκτησης. Συγκεκριμένα, υλοποιείται ένα σύστημα πυκνής διανυσματικής αναπαράστασης (Dense Retrieval ή Dense Embedding system) στο οποίο οι καταστάσεις απόδειξης (proof states) και οι διαθέσιμες μαθηματικές προτάσεις κωδικοποιούνται μέσω δύο διακριτών νευρωνικών κωδικοποιητών (encoders), επιτρέποντας διαφοροποιημένη μοντελοποίηση των δομικών και σημασιολογικών χαρακτηριστικών κάθε τύπου εισόδου. Η προτεινόμενη αρχιτεκτονική αξιολογείται ως προς την ακρίβεια ανάκτησης, αναδεικνύοντας τον ρόλο της εξειδικευμένης αναπαράστασης στη βελτίωση της απόδοσης συστημάτων αυτοματοποιημένης συλλογιστικής.