Χρήση αρχιτεκτονικής ασύμμετρου Bi-encoder στο πλαίσιο της αυτόματης απόδειξης θεωρημάτων
Asymmetric Bi-encoder architecture in the field of automated theorem proving
View/
Keywords
Θεώρημα ; Μαθηματικά ; Πρόταση ; Απόδειξη ; Lean ; Lean-Dojo ; ReProver ; Retrieval ; Αυτοματοποίηση ; Ασύμμετρος ; Bi-encoder ; Διανυσματική αναπαράσταση ; ΤΝ ; Διαδραστική απόδειξη θεωρημάτων (ITP) ; Αυτοματοποιημένη απόδειξη θεωρημάτων (ATP)Abstract
This undergraduate thesis investigates the problem of premise selection within the context of automated theorem proving and proposes an alternative asymmetric bi-encoder architecture to enhance the retrieval process. Specifically, a dense vector representation framework is implemented in which proof states and candidate premises are encoded using two distinct neural encoders, allowing differentiated modeling of their structural and semantic characteristics. The proposed architecture is evaluated in terms of retrieval accuracy, highlighting the importance of specialized representations in improving the performance of neural-assisted formal reasoning systems.