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

Sammanfattning

We investigate whether neural networks can learn some notion of usefulness/interestingnessof theorems, or as we chose to call it “intrinsic value”. This we define as the abilityto take part in the deduction of other (sufficiently “beautiful” ) theorems. To studythis we first devise a definition of what constitutes a “beautiful” theorem. We thenconstruct a symbolic system which, starting from a set of axioms, randomly deducesnew theorems from existing ones. Using this symbolic system we gather a lot ofbeautiful theorems, and consequently theorems with intrinsic value. We experimentwith different metrics of intrinsic value to find out which works best. We then usethis metric together with the collected theorems to train neural networks to classifya 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 beautifultheorems with the aid of these trained neural networks.