---
title: "Mathematical Reasoning in Latent Space — Lee 2019"
description: "The paper investigates if neural networks are able to carry out multiple steps of approximate… 7 references, cited by 11 papers here."
authors: ["Dennis Lee", "Christian Szegedy", "Markus N. Rabe", "Sarah M. Loos", "Kshitij Bansal"]
year: 2019
venue: "arXiv:1909.11851"
source: "https://arxiv.org/abs/1909.11851"
doi: "10.48550/arxiv.1909.11851"
arxiv: "1909.11851"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/lee-2019-mathematical-reasoning-latent-space/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/lee-2019-mathematical-reasoning-latent-space/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2019](https://md.research.elamur.ai/free/en/papers/2019/page/7/) / Mathematical Reasoning in Latent Space

# Mathematical Reasoning in Latent Space

**Authors:** [Dennis Lee](https://md.research.elamur.ai/free/en/authors/dennis-lee/), [Christian Szegedy](https://md.research.elamur.ai/free/en/authors/christian-szegedy/), [Markus N. Rabe](https://md.research.elamur.ai/free/en/authors/markus-n-rabe/), [Sarah M. Loos](https://md.research.elamur.ai/free/en/authors/sarah-m-loos/) and [Kshitij Bansal](https://md.research.elamur.ai/free/en/authors/kshitij-bansal/) · **Year:** 2019 · **Venue:** arXiv:1909.11851 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1909.11851) · [PDF](https://arxiv.org/pdf/1909.11851v1) · [DOI 10.48550/arxiv.1909.11851](https://doi.org/10.48550/arxiv.1909.11851) · [arXiv 1909.11851](https://arxiv.org/abs/1909.11851) · [OpenAlex](https://openalex.org/W2995238154)

**Citations:** 22 citations (OpenAlex, 2026-10-14) · [11](https://md.research.elamur.ai/free/en/papers/lee-2019-mathematical-reasoning-latent-space/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper investigates if neural networks are able to carry out multiple steps of approximate mathematical deduction entirely inside a fixed-size vector space, instead of calling symbolic search at each step. Using the HOList benchmark built on the HOL Light proof assistant, the authors study the rewrite tactic. For a goal theorem T and a parameter theorem P, they record whether rewriting succeeds and what formula results. Graph neural networks embed formulas into 1024-dimensional spaces. Model σ predicts rewrite success, ω also predicts the embedding of the rewritten formula, and α aligns the two embedding spaces. The authors then chain predicted embeddings over several rewrites without seeing the intermediate formulas and test how well the resulting vectors still predict rewrite success. After four latent steps, a regime never seen in training, quality drops but stays well above random and usage baselines. Predicted vectors also remain much closer to the true embeddings than random ones do. This points to the feasibility of latent-space reasoning and offers a fast evaluation method for formula representations.

## Key points
- Data: the HOList theorem database (19,591 theorems from HOL Light, covering topology, calculus, analysis, measure theory and more), split into 11,655 training, 3668 validation and 3620 test theorems.
- Training pairs (T, P) are built from training theorems, where P must precede T in the database to avoid circularity. A rewrite counts as successful only if REWRITE_TAC finishes in time and actually changes T.
- Architecture: a two-tower graph neural network (following Paliwal et al., 2019, the DeepHOL design) without weight sharing. The concatenated embeddings feed a three-layer ReLU perceptron and a logistic output.
- Three separate models (σ, ω, α) are used instead of one end-to-end network. This keeps the embedding fixed and makes ablations easier; merging them is left for future work.
- Evaluation over up to 4 multi-step latent rewrites is compared against a random-statement baseline and a parameter-usage baseline, and also measured by l2 distance to the true embeddings. The authors suggest applications to premise selection and to DeepHOL-Zero-style learning.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Google](https://md.research.elamur.ai/free/en/companies/google/) — Company, Mountain View, United States · 533 works · 443,884 citations

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,959 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,789 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos and Kshitij Bansal. 2019. Mathematical Reasoning in Latent Space. arXiv:1909.11851.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{lee2019mathematical,
  title = {{Mathematical Reasoning in Latent Space}},
  author = {Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos and Kshitij Bansal},
  year = {2019},
  doi = {10.48550/arxiv.1909.11851},
  eprint = {1909.11851},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1909.11851}
}
```

- [← previous Handling Syntactic Divergence in Low-resource Machine Translation](https://md.research.elamur.ai/free/en/papers/zhou-2019-handling-syntactic-divergence-low-resource/)
- [next → Neural Arabic Text Diacritization: State of the Art Results and a Novel Approach for Machine Translation](https://md.research.elamur.ai/free/en/papers/fadel-2019-neural-arabic-text-diacritization-state/)
- [↑ back to papers of 2019](https://md.research.elamur.ai/free/en/papers/2019/page/7/)

## References

7 references, 3 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Alemi, A. A., Chollet, F., Irving, G., Eén, N., Szegedy, C., and Urban, J. (2016). [Deepmath-deep sequence models for premise selection](https://md.research.elamur.ai/free/en/papers/alemi-2016-deepmath-deep-sequence-models-premise/). In Advances in Neural Information Processing Systems, pages 2235–2243.
2. Bansal, K., Loos, S. M., Rabe, M. N., and Szegedy, C. (2019a). [Learning to reason in large theories without imitation](https://md.research.elamur.ai/free/en/papers/bansal-2019-learning-reason-large-theories-without/). arXiv preprint arXiv:1905.10501.
3. Bansal, K., Loos, S. M., Rabe, M. N., Szegedy, C., and Wilcox, S. (2019b). [HOList: An environment for machine learning of higher-order theorem proving](https://md.research.elamur.ai/free/en/papers/bansal-2019-holist-environment-machine-learning-higher/). ICML 2019. International Conference on Machine Learning.
4. Brunner, G., Fritsche, M., Richter, O., and Wattenhofer, R. (2018). Using state predictions for value regularization in curiosity driven deep reinforcement learning. In 2018 IEEE 30th International Conference on Tools with Artificial Intelligence (ICTAI), pages 25–29. IEEE. [find](https://scholar.google.com/scholar?q=Brunner%2C+G%2E%2C+Fritsche%2C+M%2E%2C+Richter%2C+O%2E%2C+and+Wattenhofer%2C+R%2E+%282018%29%2E+Using+state+predictions+for+value+regularization+in+curiosity+driven+deep+reinforcement+learning%2E+In+2018+IEEE+30th+International+Co)
5. Chiappa, S., Racanière, S., Wierstra, D., and Mohamed, S. (2017). Recurrent environment simulators. CoRR, abs/1704.02254. — [arXiv:1704.02254](https://arxiv.org/abs/1704.02254) [find](https://scholar.google.com/scholar?q=Chiappa%2C+S%2E%2C+Racanie%CC%80re%2C+S%2E%2C+Wierstra%2C+D%2E%2C+and+Mohamed%2C+S%2E+%282017%29%2E+Recurrent+environment+simulators%2E+CoRR%2C+abs%2F1704%2E02254%2E+%E2%80%94+%5BarXiv%3A1704%2E02254%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1704%2E02254%29)
6. Coq. The Coq Proof Assistant. [http://coq.inria.fr](http://coq.inria.fr). [↗](http://coq.inria.fr)
7. Dosovitskiy, A. and Koltun, V. (2017). Learning to act by predicting the future. ICLR 2017. [find](https://scholar.google.com/scholar?q=Dosovitskiy%2C+A%2E+and+Koltun%2C+V%2E+%282017%29%2E+Learning+to+act+by+predicting+the+future%2E+ICLR+2017%2E)

*Updated 3 November 2026*