Graph Representations for Higher-Order Logic and Theorem Proving
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingSimilar Papers 제목 키워드 기반
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
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 i…
Automated Theorem ProvingDeep LearningGraph Neural NetworkSuperposition for Lambda-Free Higher-Order Logic
We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are p…
Extracting Higher-Order Goals from the Mizar Mathematical Library
Certain constructs allowed in Mizar articles cannot be represented in first-order logic but can be represented in higher-order logic. We describe a way to obtain higher-order theorem proving problems from Mizar articles …
ArticlesAutomated Theorem ProvingHolophrasm: a neural Automated Theorem Prover for higher-order logic
I propose a system for Automated Theorem Proving in higher order logic using deep learning and eschewing hand-constructed features. Holophrasm exploits the formalism of the Metamath language and explores partial proof tr…
Automated Theorem ProvingHOList: An Environment for Machine Learning of Higher-Order Theorem Proving
We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and the…
Automated Theorem ProvingBIG-bench Machine LearningDeep LearningDeep Reinforcement Learning+3