# ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

## TL;DR

This paper introduces ENIGMA-NG, an advanced clause guidance system for automated theorem provers that leverages gradient boosted trees and neural networks, achieving significant improvements over previous manual methods.

## Contribution

It presents the first practical integration of gradient-boosted and neural clause guidance in saturation-based theorem provers, enhancing efficiency and effectiveness.

## Key findings

- Gradient boosted trees and neural networks outperform manual guidance.
- Deep integration reduces neural evaluation costs.
- Methods achieve competitive real-time theorem proving results.

## Abstract

We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation where fast linear classifier is trained and used together with manually engineered features, we have started to experiment with more sophisticated state-of-the-art machine learning methods such as gradient boosted trees and recursive neural networks. In particular the latter approach poses challenges in terms of efficiency of clause evaluation, however, we show that deep integration of the neural evaluation with the ATP data-structures can largely amortize this cost and lead to competitive real-time results. Both methods are evaluated on a large dataset of theorem proving problems and compared with the previous approaches. 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.