mlsanityData to 13 Oct 2026

A Study of Continuous Vector Representationsfor Theorem Proving

arXiv 2101.09142 ↗First posted 22 Jan 2021cs.LGcited by 4

Not on the map. Why?

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.

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

Builds on

23 of 63 references.

References · 23

  1. 2017Attention Is All You Needcited by 60,106
  2. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,304
  3. 2014Adam: A Method for Stochastic Optimizationcited by 37,093
  4. 2017Inductive Representation Learning on Large Graphscited by 6,303
  5. 2013Distributed Representations of Words and Phrases and their Compositionalitycited by 3,467
  6. 2016WaveNet: A Generative Model for Raw Audiocited by 1,717
  7. 2015Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networkscited by 305
  8. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 81
  9. 2018Reinforcement Learning of Theorem Provingcited by 69
  10. 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
  11. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  12. 2017Deep Network Guided Proof Searchcited by 47
11 more
  1. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  2. 2015A formal proof of the Kepler conjecturecited by 42
  3. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  4. 2016Learning Continuous Semantic Representations of Symbolic Expressionscited by 25
  5. 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
  6. 2013MizAR 40 for Mizar 40cited by 23
  7. 2019Property Invariant Embedding for Automated Reasoningcited by 22
  8. 2019Improving Graph Neural Network Representations of Logical Formulae with Subgraph Poolingcited by 20
  9. 2019Learning Relational Representations with Auto-encoding Logic Programscited by 13
  10. 2019Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logiccited by 8
  11. 2019LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOLcited by 3

Built on by

Cited by year

Citing papers per year: 2022: 1; 2023: 1; 2024: 2.

4 papers.

  1. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  2. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  3. 2022Project proposal: A modular reinforcement learning based automated theorem provercited by 1
  4. 2023gym-saturation: Gymnasium environments for saturation provers (System description)cited by 1