A Study of Continuous Vector Representationsfor Theorem Proving
arXiv:2101.09142 · doi:10.1093/logcom/exab006
Abstract
Applying machine learning to mathematical terms and formulas requires a suitable representation of formulas that is adequate for AI methods. In this paper, we develop an encoding that allows for logical properties to be preserved and is additionally reversible. This means that the tree shape of a formula including all symbols can be reconstructed from the dense vector representation. We do that by training two decoders: one that extracts the top symbol of the tree and one that extracts embedding vectors of subtrees. The syntactic and semantic logical properties that we aim to reserve include both structural formula properties, applicability of natural deduction steps, and even more complex operations like unifiability. We propose datasets that can be used to train these syntactic and semantic properties. We evaluate the viability of the developed encoding across the proposed datasets as well as for the practical theorem proving problem of premise selection in the Mizar corpus.
References in corpus (12)
- Adam: A Method for Stochastic Optimization
- Distributed Representations of Words and Phrases and their Compositionality
- WaveNet: A Generative Model for Raw Audio
- A formal proof of the four color theorem
- DeepMath - Deep Sequence Models for Premise Selection
- MizAR 40 for Mizar 40
- Machine Learning in Proof General: Interfacing Interfaces
- Premise Selection for Theorem Proving by Deep Graph Embedding
- Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
- Property Invariant Embedding for Automated Reasoning
- Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
- LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL