Vampire With a Brain Is a Good ITP Hammer
  Vampire has been for a long time the strongest first-order automatic theorem
prover, widely used for hammer-style proof automation in ITPs such as Mizar,
Isabelle, HOL, and Coq. In this work, we considerably improve the performance
of Vampire in hammering over the full Mizar library by enhancing its saturation
procedure with efficient neural guidance. In particular, we employ a recently
proposed recursive neural network classifying the generated clauses based only
on their derivation history. Compared to previous neural methods based on
considering the logical content of the clauses, our architecture makes
evaluating a single clause much less time consuming. The resulting system shows
good learning capability and improves on the state-of-the-art performance on
the Mizar library, while proving many theorems that the related ENIGMA system
could not prove in a similar hammering evaluation.
