Elamur Research⌕
☰
home / papers / 2019 / Mathematical Reasoning in Latent Space

Mathematical Reasoning in Latent Space

Paper · 2019 · Dennis Lee, Christian Szegedy, Markus N. Rabe et al.

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

🏢GoogleMountain View · United States533 works · 443,885 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.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. DOI 10.48550/arxiv.1909.11851 · arXiv 1909.11851

@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}
}

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. 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. 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. 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
  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
  6. Coq. The Coq Proof Assistant. http://coq.inria.fr. ↗
  7. Dosovitskiy, A. and Koltun, V. (2017). Learning to act by predicting the future. ICLR 2017. find

Updated

This page in Markdown → https://md.research.elamur.ai/free/en/papers/lee-2019-mathematical-reasoning-latent-space/