Fast and Slow Enigmas and Parental Guidance

TL;DR

This paper enhances the ENIGMA system for guiding clause selection in the E theorem prover by integrating GPU acceleration, intelligent pre-filtering, and parent-based rejection, leading to significant performance improvements on large benchmarks.

Contribution

It introduces GPU-accelerated guidance, trainable fast pre-filters, and parent-based clause rejection, combining fast and slow reasoning for improved theorem proving efficiency.

Findings

Significant speed-up of neural guidance via GPU evaluation.

Improved clause filtering with trainable fast pre-filters.

Enhanced performance on Mizar Mathematical Library benchmarks.

Abstract

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.