Tags:clause selection, ENIGMA, guidance and machine learning
Abstract:
I will decribe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. In addition to the previously employed fast linear classifier, gradient boosted trees and recursive neural networks are newly introduced. The resulting methods improve on the manually designed clause guidance, providing the first practically convincing application of gradient-boosted and neural clause guidance in saturation-style automated theorem provers.