# A Study of Continuous Vector Representationsfor Theorem Proving

arXiv: https://arxiv.org/abs/2101.09142 · HTML: https://mlsanity.com/paper/2101.09142/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 63 references that are in the map.
- First posted on arXiv 22 Jan 2021.

## Builds on (most cited first, 23 of 23)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Distributed Representations of Words and Phrases and their Compositionality](https://mlsanity.com/paper/1310.4546/) (2013)
- [WaveNet: A Generative Model for Raw Audio](https://mlsanity.com/paper/1609.03499/) (2016)
- [Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networks](https://mlsanity.com/paper/1503.00075/) (2015)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Learning Continuous Semantic Representations of Symbolic Expressions](https://mlsanity.com/paper/1611.01423/) (2016)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling](https://mlsanity.com/paper/1911.06904/) (2019)
- [Learning Relational Representations with Auto-encoding Logic Programs](https://mlsanity.com/paper/1903.12577/) (2019)
- [Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic](https://mlsanity.com/paper/1910.11797/) (2019)
- [LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL](https://mlsanity.com/paper/1906.08084/) (2019)

## Built on by (most cited first, 4 of 4)

- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Project proposal: A modular reinforcement learning based automated theorem prover](https://mlsanity.com/paper/2209.02562/) (2022)
- [gym-saturation: Gymnasium environments for saturation provers (System description)](https://mlsanity.com/paper/2309.09022/) (2023)

## Abstract (arXiv)

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.