Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling

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 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.

References in corpus (11)

• Adam: A Method for Stochastic Optimization
• Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift
• Neural Message Passing for Quantum Chemistry
• Effective Approaches to Attention-based Neural Machine Translation
• Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
• DeepMath - Deep Sequence Models for Premise Selection
• MizAR 40 for Mizar 40
• GamePad: A Learning Environment for Theorem Proving
• Property Invariant Embedding for Automated Reasoning
• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
• Premise selection with neural networks and distributed representation of features

Cited by in corpus (7)

• Measuring Mathematical Problem Solving With the MATH Dataset
• Directed Acyclic Graph Neural Networks
• Directed Acyclic Graph Network for Conversational Emotion Recognition
• LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
• A Study of Continuous Vector Representationsfor Theorem Proving
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving