  Deep learning techniques lie at the heart of several significant AI advances
in recent years including object recognition and detection, image captioning,
machine translation, speech recognition and synthesis, and playing the game of
Go. Automated first-order theorem provers can aid in the formalization and
verification of mathematical theorems and play a crucial role in program
analysis, theory reasoning, security, interpolation, and system verification.
Here we suggest deep learning based guidance in the proof search of the theorem
prover E. We train and compare several deep neural network models on the traces
of existing ATP proofs of Mizar statements and use them to select processed
clauses during proof search. We give experimental evidence that with a hybrid,
two-phase approach, deep learning based guidance can significantly reduce the
average number of proof search steps while increasing the number of theorems
proved. Using a few proof guidance strategies that leverage deep neural
networks, we have found first-order proofs of 7.36% of the first-order logic
translations of the Mizar Mathematical Library theorems that did not previously
have ATP generated proofs. This increases the ratio of statements in the corpus
with ATP generated proofs from 56% to 59%.
