Learning to Prove from Synthetic Theorems
  A major challenge in applying machine learning to automated theorem proving
is the scarcity of training data, which is a key ingredient in training
successful deep learning models. To tackle this problem, we propose an approach
that relies on training with synthetic theorems, generated from a set of
axioms. We show that such theorems can be used to train an automated prover and
that the learned prover transfers successfully to human-generated theorems. We
demonstrate that a prover trained exclusively on synthetic theorems can solve a
substantial fraction of problems in TPTP, a benchmark dataset that is used to
compare state-of-the-art heuristic provers. Our approach outperforms a model
trained on human-generated problems in most axiom sets, thereby showing the
promise of using synthetic data for this task.
