# Property Invariant Embedding for Automated Reasoning

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

## Key facts

- Cited by 22 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Nov 2019.

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

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [The Role of Entropy in Guiding a Connection Prover](https://mlsanity.com/paper/2105.14706/) (2021)
- [Fast and Slow Enigmas and Parental Guidance](https://mlsanity.com/paper/2107.06750/) (2021)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [A Study of Continuous Vector Representationsfor Theorem Proving](https://mlsanity.com/paper/2101.09142/) (2021)
- [An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations](https://mlsanity.com/paper/2305.08676/) (2023)
- [Machine Learning Meets The Herbrand Universe](https://mlsanity.com/paper/2210.03590/) (2022)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Improving ENIGMA-Style Clause Selection While Learning From History](https://mlsanity.com/paper/2102.13564/) (2021)
- [Adversarial Learning to Reason in an Arbitrary Logic](https://mlsanity.com/paper/2204.02737/) (2022)
- [Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)](https://mlsanity.com/paper/2206.06986/) (2022)
- [gym-saturation: Gymnasium environments for saturation provers (System description)](https://mlsanity.com/paper/2309.09022/) (2023)
- [Solving Hard Mizar Problems with Instantiation and Strategy Invention](https://mlsanity.com/paper/2406.17762/) (2024)
- [Names Don't Matter: Symbol-Invariant Transformer for Open-Vocabulary Learning](https://mlsanity.com/paper/2601.23169/) (2026)
- [Efficient Neural Clause-Selection Reinforcement](https://mlsanity.com/paper/2503.07792/) (2025)
- [Partial Label Learning for Automated Theorem Proving](https://mlsanity.com/paper/2507.03314/) (2025)
- [Imitation Learning for Connection-Tableau Construction](https://mlsanity.com/paper/2608.26009/) (2026)

## Abstract (arXiv)

Automated reasoning and theorem proving have recently become major challenges for machine learning. In other domains, representations that are able to abstract over unimportant transformations, such as abstraction over translations and rotations in vision, are becoming more common. Standard methods of embedding mathematical formulas for learning theorem proving are however yet unable to handle many important transformations. In particular, embedding previously unseen labels, that often arise in definitional encodings and in Skolemization, has been very weak so far. Similar problems appear when transferring knowledge between known symbols. We propose a novel encoding of formulas that extends existing graph neural network models. This encoding represents symbols only by nodes in the graph, without giving the network any knowledge of the original labels. We provide additional links between such nodes that allow the network to recover the meaning and therefore correctly embed such nodes irrespective of the given labels. We test the proposed encoding in an automated theorem prover based on the tableaux connection calculus, and show that it improves on the best characterizations used so far. The encoding is further evaluated on the premise selection task and a newly introduced symbol guessing task, and shown to correctly predict 65% of the symbol names.