Matej Petković: Machine Learning on Agda Graphs

Abstract: Agda is a programming language which is primarily used as a tool for verifying mathematical statements. A typical Agda library contains a formal representation of a body of mathematical knowledge.

In this seminar, we will first refresh our memory on how to convert an Agda library into a graph, where the nodes represent definitions from the library, and directed edges represent references between them. Next, we will show how to build a machine learning model from the graph. Given a pair of propositions $(t, u)$, the model predicts whether we could $u$ in the proof of proposition $t$. We will pay attention to the evaluation process of the algorithm's quality, and finally, we will examine the results for a few selected libraries.