Learning to Guide a Saturation-Based Theorem Prover

Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can be integrated into theorem provers to improve their performance automatically. In...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on pattern analysis and machine intelligence 2023-01, Vol.45 (1), p.738-751
Main Authors: Abdelaziz, Ibrahim, Crouse, Maxwell, Makni, Bassem, Austel, Vernon, Cornelio, Cristina, Ikbal, Shajith, Kapanipathi, Pavan, Makondo, Ndivhuwo, Srinivas, Kavitha, Witbrock, Michael, Fokoue, Achille
Format: Article
Language:English
Subjects:
Benchmark testing
Benchmarks
Deep learning
deep reinforcement learning
Feature extraction
first-order logic
Graph neural networks
Graphical representations
Learning systems
Reinforcement learning
Saturation
Saturation-based theorem proving
Search problems
Theorem proving
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can be integrated into theorem provers to improve their performance automatically. In this work, we describe TRAIL (Trial Reasoner for AI that Learns), a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. TRAIL leverages (a) an effective graph neural network for representing logical formulas, (b) a novel neural representation of the state of a saturation-based theorem prover in terms of processed clauses and available actions, and (c) a novel representation of the inference selection process as an attention-based action policy. We show through a systematic analysis that these components allow TRAIL to significantly outperform previous reinforcement learning-based theorem provers on two standard benchmark datasets (up to 36% more theorems proved). In addition, to the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover on a standard theorem proving benchmark (solving up to 17% more theorems).
ISSN:0162-8828
1939-3539
2160-9292
DOI:10.1109/TPAMI.2022.3140382