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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
MethodsENIGMA
