Graph Representations for Higher-Order Logic and Theorem Proving

2019/05/24 by Aditya Paliwal, Paliwal, Aditya, Sarah Loos +7 · 1 voice · 7 citations
Computer Science · Mathematics · #cs.AI #cs.LG #cs.LO #stat.ML

paper · pdf · doi:10.48550/arxiv.1905.10006

arxiv created 2019/09/13 · arxiv updated 2019/09/16

Abstract

This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem provers allow for the formalization of most mathematical theories and have been shown to pose a significant challenge for deep learning. Higher-order logic is highly expressive and, even though it is well-structured with a clearly defined grammar and semantics, there still remains no well-established method to convert formulas into graph-based representations. In this paper, we consider several graphical representations of higher-order logic and evaluate them against the HOList benchmark for higher-order theorem proving.

Cited by

• Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4
• Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective
• Learning Representations Through Contrastive Neural Model Checking
• A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
• Partial Label Learning for Automated Theorem Proving
• Hierarchical Attention Generates Better Proofs
• AI for Mathematics: Progress, Challenges, and Prospects

Discussions

• Graph Representations for Higher-Order Logic and Theorem Proving (2019) [hn, 104 points, 15 comments]

Related

• Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
• The Logic of Graph Neural Networks
• Demystifying Higher-Order Graph Neural Networks
• Holophrasm: a neural Automated Theorem Prover for higher-order logic
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic