Learning Theorem Proving Components

TL;DR

This paper introduces algorithms and experiments with ENIGMA, a graph neural network-enhanced theorem prover that evaluates clauses contextually within the clause graph, improving clause selection in automated theorem proving.

Contribution

It advances the use of graph neural networks for contextual clause evaluation in saturation-style theorem provers, enhancing clause selection strategies.

Findings

ENIGMA improves clause selection accuracy

Graph neural networks effectively model clause relationships

Contextual evaluation outperforms isolated clause heuristics

Abstract

Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selection heuristics in such systems are, however, often evaluating clauses in isolation, ignoring other clauses. This has changed recently by equipping the E/ENIGMA system with a graph neural network (GNN) that chooses the next given clause based on its evaluation in the context of previously selected clauses. In this work, we describe several algorithms and experiments with ENIGMA, advancing the idea of contextual evaluation based on learning important components of the graph of clauses.