Deep Learning for Theorem Generation and Premise Selection

I laboured to improve upon Isabelle’s already existing methods of premise selection by using two deep learning techniques.

The first one of these involved modifying WaveNet, a generative model for raw audio, to generate example theorems of our multi-type display calculus. These theorems form a labelled dataset for our classification problem.

The second one was to use the aforementioned generated dataset to train some simple baselane neural network models for premise selection for our calculus.