Fast and Slow Enigmas and Parental Guidance
  We describe several additions to the ENIGMA system that guides clause
selection in the E automated theorem prover. First, we significantly speed up
its neural guidance by adding server-based GPU evaluation. The second addition
is motivated by fast weight-based rejection filters that are currently used in
systems like E and Prover9. Such systems can be made more intelligent by
instead training fast versions of ENIGMA that implement more intelligent
pre-filtering. This results in combinations of trainable fast and slow thinking
that improves over both the fast-only and slow-only methods. The third addition
is based on "judging the children by their parents", i.e., possibly rejecting
an inference before it produces a clause. This is motivated by standard
evolutionary mechanisms, where there is always a cost to producing all possible
offsprings in the current population. This saves time by not evaluating all
clauses by more expensive methods and provides a complementary view of the
generated clauses. The methods are evaluated on a large benchmark coming from
the Mizar Mathematical Library, showing good improvements over the state of the
art.
