Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling

Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling Maxwell Crouse * §, Ibrahim Abdelaziz †, Cristina Cornelio †, V eronika Thost ‡, Lingfei Wu †, Kenneth Forbus §, Achille Fokoue † § Northwestern University, † IBM Research, ‡ MIT -IBM Watson AI Lab Abstract --Recent advances in the integration of deep learning with automated theorem proving have centered around the representation of logical formulae as inputs to deep learning systems. In particular, there has been a shift from character and token-level representations to graph-structured representations, in large part driven by the rapidly emerging body of research on geometric deep learning. Typically, structure-aware neural methods for embedding logical formulae have been variants of either Tree LSTMs or GNNs. While more effective than character and token-level approaches, such methods have often made representational tradeoffs that limited their ability to effectively represent the global structure of their inputs. In this work, we introduce a novel approach for embedding logical formulae using DAG LSTMs that is designed to overcome the limitations of both Tree LSTMs and GNNs. The effectiveness of the proposed framework is demonstrated on the tasks of premise selection and proof step classification where it achieves the state-of-the-art performance on two standard datasets. I NTRODUCTION While state-of-the-art classical theorem provers excel at finding complex proofs in restricted domains (e.g. TPTP [1]), they have historically had difficulty when reasoning in broad contexts [2], [3]. With the generation of large logical theories (collections of axioms) for reasoning [4]-[6], there has been interest in extending traditional theorem provers to handle the computational challenges inherent to reasoning at scale.