Fast and Slow Enigmas and Parental Guidance
This work addresses efficiency and intelligence in automated theorem proving for mathematical reasoning, representing an incremental advancement.
The authors tackled the problem of improving clause selection in automated theorem proving by enhancing the ENIGMA system with GPU acceleration, fast-slow thinking combinations, and parent-based inference rejection, resulting in good improvements over state-of-the-art methods on the Mizar Mathematical Library benchmark.
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.