Improving ENIGMA-Style Clause Selection While Learning From History
  We re-examine the topic of machine-learned clause selection guidance in
saturation-based theorem provers. The central idea, recently popularized by the
ENIGMA system, is to learn a classifier for recognizing clauses that appeared
in previously discovered proofs. In subsequent runs, clauses classified
positively are prioritized for selection. We propose several improvements to
this approach and experimentally confirm their viability. For the
demonstration, we use a recursive neural network to classify clauses based on
their derivation history and the presence or absence of automatically supplied
theory axioms therein. The automatic theorem prover Vampire guided by the
network achieves a 41% improvement on a relevant subset of SMT-LIB in a real
time evaluation.
