# Machine Learning Meets The Herbrand Universe

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 26 references that are in the map.
- First posted on arXiv 7 Oct 2022.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [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)
- [Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic](https://mlsanity.com/paper/1910.11797/) (2019)
- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)

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

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Alien Coding](https://mlsanity.com/paper/2301.11479/) (2023)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)

## Abstract (arXiv)

The appearance of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is thus to apply SAT solvers to expressive formalisms such as first-order logic, for which large corpora of general mathematical problems exist today. This is possible due to Herbrand's theorem, which allows reduction of first-order problems to propositional problems by instantiation. The core challenge is choosing the right instances from the typically infinite Herbrand universe. In this work, we develop the first machine learning system targeting this task, addressing its combinatorial and invariance properties. In particular, we develop a GNN2RNN architecture based on an invariant graph neural network (GNN) that learns from problems and their solutions independently of symbol names (addressing the abundance of skolems), combined with a recurrent neural network (RNN) that proposes for each clause its instantiations. The architecture is then trained on a corpus of mathematical problems and their instantiation-based proofs, and its performance is evaluated in several ways. We show that the trained system achieves high accuracy in predicting the right instances, and that it is capable of solving many problems by educated guessing when combined with a ground solver. To our knowledge, this is the first convincing use of machine learning in synthesizing relevant elements from arbitrary Herbrand universes.