Αυτόματη σύνθεση προγραμμάτων με χρήση τεχνητής νοημοσύνης

Abstract

Η Αυτοματοποιημένη Διαδραστική Σύνθεση Αποδείξεων με Μηχανική Μάθηση έχει δει σημαντική ανάπτυξη τα τελευταία χρόνια. Είναι ένας τομέας που επιχειρεί να υποκαταστήσει την αλληλεπίδραση των χρηστών με βοηθούς απόδειξης με μοντέλα μηχανικής μάθησης τα οποία είναι υπεύθυνα για την παροχή των υποψήφιων τακτικών. Το CoqGym είναι ένα σύνολο δεδομένων και περιβάλλον μάθησης για Διαδραστική Σύνθεση Αποδείξεων που περιέχει 71 χιλιάδες αποδείξεις γραμμένες από ανθρώπους για τον βοηθό αποδείξεων Coq, το οποίο δημιουργήθηκε εξάγοντας αποδείξεις από 123 σύνολα αποδείξεων. Το CoqGym αποτέλεσε τη βάση για τη δημιουργία διάφορων εργαλείων σύνθεσης αποδείξεων με προβλέψεις μηχανικής μάθησης, όπως το ASTactic το TacTok και το Passport. Σε αυτή την εργασία επιχειρούμε να βελτιώσουμε τις αρχιτεκτονικές που προτάθηκαν από τη βιβλιογραφία, αντικαθιστώντας τους παραδοσιακούς αλγόριθμους αναζήτησης που χρησιμοποιούνται για την εξερεύνηση του χώρου ταακτικών ο οποίος παράγεται από τα μοντέλα μηχανικής μάθησης, και να χρησιμοποιήσουμε Αναζήτηση Δέντρου Μόντε Κάρλο (MCTS). Εισάγουμε τρεις πολιτικές ανταμοιβών για την υλοποίηση μας: την πολιτική ανταμοιβής "σε τερματικές καταστάσεις", την πολιτική ανταμοιβής "βάσει του βάθους" και την πολιτική ανταμοιβής "με βαση τη μείωση των στόχων". Δείχνουμε ότι το MCTS με περιορισμένη ρύθμιση των παραμέτρων του είναι ικανό να παράγει αποτελέσματα πολύ κοντά στα κορυφαία αποτελέσματα που παρουσιάζονται στη βιβλιογραφία.