Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling

By Maxwell Crouse, Ibrahim Abdelaziz, Cristina Cornelio, Veronika Thost, Lingfei Wu, Kenneth D. Forbus, Achille Fokoue. 2019

40 citations recorded by the source corpus.

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 growing interest in adapting structure-aware neural methods to work with the underlying graph representations of logical expressions. While more effective than character and token-level approaches, graph-based methods have often made representational trade-offs that limited their ability to capture key structural properties of their inputs. In this work we propose a novel approach for embedding logical formulae that is designed to overcome the representational limitations of prior approaches. Our architecture works for logics of different expressivity; e.g., first-order and higher-order logic. We evaluate our approach on two standard datasets and show that the proposed architecture achieves state-of-the-art performance on both premise selection and proof step classification.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition, Graph Learning

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Vision and Pattern Recognition

In Graph Learning

Citations in the corpus

Directed Acyclic Graph Network for Conversational Emotion Recognition (2021, background): “Directed acyclic graph is a special type of graph structure that can be seen in multiple areas, for example, the parsing results of source code (Alla-manis et al., 2018) and logical formulas (Crouse et al., 2019).”
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic (2020, methodology): “Current research therefore focuses on the development of neural approaches [Bansal et al. , 2019; Chvalovsk´y et al. , 2019; Crouse et al. , 2019b], which are independent of the latter; but, next to the hardness of the proof search, the highly structural and semantic nature of logical formulas…”
On the Paradox of Learning to Reason from Data (2022, methodology): “, 2019), learning embeddings for logical formula (Crouse et al., 2019; Abdelaziz et al., 2020)”
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning (2021, background): “Crouse et al. (2019) have shown that pooling mechanisms can have an impact on the performance of GNNs on logical formulas as well.”