ENIGMA: Efficient Learning-based Inference Guiding Machine
This work addresses efficiency in automated theorem proving, which is incremental as it builds on existing methods with a learning-based enhancement.
The authors tackled the problem of clause selection in saturation-based theorem provers by developing ENIGMA, a learning-based method that trains a classification model on proof search data to rank clauses efficiently. The result was a large increase in the E prover's performance on the CASC 2016 AIM benchmark.
ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many proof searches are classified as positive and negative based on their participation in the proofs. An efficient classification model is trained on this data, using fast feature-based characterization of the clauses . The learned model is then tightly linked with the core prover and used as a basis of a new parameterized evaluation heuristic that provides fast ranking of all generated clauses. The approach is evaluated on the E prover and the CASC 2016 AIM benchmark, showing a large increase of E's performance.