In this work we develop a recommender system that supports formalisation of mathematics with the proof assistant Agda. We use machine learning to build the recommender system; we train the model on datasets mined from three Agda libraries for formalisation of mathematics. Each dataset consists of two parts: a set of abstract synatx trees for each library entry, and a graph of references between entries. The final recommender system combines a method for embedding abstract syntax trees of Agda entries into a real vector space, a graph neural network for vertex embeddings in the references graph, and an ansamble of decision trees for predicting references between entries. We compare our model to previous work and argue, that although it fails to surpass the best model so far it offers more practical use.
|
