| dc.contributor.advisor | Σωτηρόπουλος, Διονύσιος | |
| dc.contributor.author | Λιγάτος, Ηλίας | |
| dc.date.accessioned | 2026-04-02T10:14:40Z | |
| dc.date.available | 2026-04-02T10:14:40Z | |
| dc.date.issued | 2026-02 | |
| dc.identifier.uri | https://dione.lib.unipi.gr/xmlui/handle/unipi/19112 | |
| dc.description.abstract | Η παρούσα πτυχιακή εργασία εξετάζει το πρόβλημα της επιλογής μαθηματικών προτάσεων (premise selection) στο πλαίσιο της αυτοματοποιημένης απόδειξης μαθηματικών θεωρημάτων και προτείνει μια εναλλακτική αρχιτεκτονική ασύμμετρου bi-encoder για τη βελτίωση της διαδικασίας ανάκτησης. Συγκεκριμένα, υλοποιείται ένα σύστημα πυκνής διανυσματικής αναπαράστασης (Dense Retrieval ή Dense Embedding system) στο οποίο οι καταστάσεις απόδειξης (proof states) και οι διαθέσιμες μαθηματικές προτάσεις κωδικοποιούνται μέσω δύο διακριτών νευρωνικών κωδικοποιητών (encoders), επιτρέποντας διαφοροποιημένη μοντελοποίηση των δομικών και σημασιολογικών χαρακτηριστικών κάθε τύπου εισόδου. Η προτεινόμενη αρχιτεκτονική αξιολογείται ως προς την ακρίβεια ανάκτησης, αναδεικνύοντας τον ρόλο της εξειδικευμένης αναπαράστασης στη βελτίωση της απόδοσης συστημάτων αυτοματοποιημένης συλλογιστικής. | el |
| dc.format.extent | 46 | el |
| dc.language.iso | el | el |
| dc.publisher | Πανεπιστήμιο Πειραιώς | el |
| dc.title | Χρήση αρχιτεκτονικής ασύμμετρου Bi-encoder στο πλαίσιο της αυτόματης απόδειξης θεωρημάτων | el |
| dc.title.alternative | Asymmetric Bi-encoder architecture in the field of automated theorem proving | el |
| dc.type | Bachelor Dissertation | el |
| dc.contributor.department | Σχολή Τεχνολογιών Πληροφορικής και Επικοινωνιών. Τμήμα Πληροφορικής | el |
| dc.description.abstractEN | 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. | el |
| dc.subject.keyword | Θεώρημα | el |
| dc.subject.keyword | Μαθηματικά | el |
| dc.subject.keyword | Πρόταση | el |
| dc.subject.keyword | Απόδειξη | el |
| dc.subject.keyword | Lean | el |
| dc.subject.keyword | Lean-Dojo | el |
| dc.subject.keyword | ReProver | el |
| dc.subject.keyword | Retrieval | el |
| dc.subject.keyword | Αυτοματοποίηση | el |
| dc.subject.keyword | Ασύμμετρος | el |
| dc.subject.keyword | Bi-encoder | el |
| dc.subject.keyword | Διανυσματική αναπαράσταση | el |
| dc.subject.keyword | ΤΝ | el |
| dc.subject.keyword | Διαδραστική απόδειξη θεωρημάτων (ITP) | el |
| dc.subject.keyword | Αυτοματοποιημένη απόδειξη θεωρημάτων (ATP) | el |
| dc.date.defense | 2026-02-20 | |
