# ENIGMA: Efficient Learning-based Inference Guiding Machine

## TL;DR

ENIGMA introduces a learning-based clause selection method for saturation-based theorem provers, significantly improving their performance by training a fast classification model to guide proof search effectively.

## Contribution

It presents a novel, efficient classification approach that integrates with theorem provers to enhance clause selection and proof search efficiency.

## Key findings

- Large performance increase on E prover and CASC 2016 AIM benchmark
- Effective fast feature-based clause classification model
- Improved proof search guidance and efficiency

## Abstract

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.