Learning the intrinsic value of theorems - Estimating usefulness of theorems with neural networks

Abstract

We investigate whether neural networks can learn some notion of usefulness/interestingness of theorems, or as we chose to call it “intrinsic value”. This we define as the ability to take part in the deduction of other (sufficiently “beautiful” ) theorems. To study this we first devise a definition of what constitutes a “beautiful” theorem. We then construct a symbolic system which, starting from a set of axioms, randomly deduces new theorems from existing ones. Using this symbolic system we gather a lot of beautiful theorems, and consequently theorems with intrinsic value. We experiment with different metrics of intrinsic value to find out which works best. We then use this metric together with the collected theorems to train neural networks to classify a theorem as useful or not. We find, using MPNN and DAG-LSTM architectures, that this is possible. We also find that we can optimize the discovery of beautiful theorems with the aid of these trained neural networks.