Make E Smart Again
This work is incremental, showing that machine learning can compensate for disabled features in automated theorem proving.
The authors tackled the problem of guiding the E theorem prover without standard functionalities like term ordering and literal selection, and demonstrated that the ENIGMA system using XGBoost can achieve performance comparable to evolved strategies.
In this work in progress, we demonstrate a new use-case for the ENIGMA system. The ENIGMA system using the XGBoost implementation of gradient boosted decision trees has demonstrated high capability to learn to guide the E theorem prover's inferences in real-time. Here, we strip E to the bare bones: we replace the KBO term ordering with an identity relation as the minimal possible ordering, disable literal selection, and replace evolved strategies with a simple combination of the clause weight and FIFO (first in first out) clause evaluation functions. We experimentally demonstrate that ENIGMA can learn to guide E as well as the smart, evolved strategies even without these standard automated theorem prover functionalities. To this end, we experiment with XGBoost's meta-parameters over a dozen loops.