---
title: "Graph Representations for Higher-Order Logic and Theorem"
description: "Neural guidance of proof search in higher-order logic is difficult, partly because there is no standard… 31 references, cited by 23 papers here."
authors: ["Aditya Paliwal", "Sarah Loos", "Markus Rabe", "Kshitij Bansal", "Christian Szegedy"]
year: 2019
venue: "arXiv:1905.10006"
source: "https://arxiv.org/abs/1905.10006"
doi: "10.48550/arxiv.1905.10006"
arxiv: "1905.10006"
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/paliwal-2019-graph-representations-higher-order-logic/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/paliwal-2019-graph-representations-higher-order-logic/)

[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/) / Graph Representations for Higher-Order Logic and Theorem Proving

# Graph Representations for Higher-Order Logic and Theorem Proving

**Authors:** Aditya Paliwal, [Sarah Loos](https://md.research.elamur.ai/free/en/authors/sarah-m-loos/), [Markus Rabe](https://md.research.elamur.ai/free/en/authors/markus-n-rabe/), [Kshitij Bansal](https://md.research.elamur.ai/free/en/authors/kshitij-bansal/) and [Christian Szegedy](https://md.research.elamur.ai/free/en/authors/christian-szegedy/) · **Year:** 2019 · **Venue:** [arXiv:1905.10006](https://md.research.elamur.ai/free/en/venues/proceedings-of-the-aaai-conference-on-artificial-intelligence/) ([Proceedings of the AAAI Conference on Artificial Intelligence 2019](https://md.research.elamur.ai/free/en/venues/proceedings-of-the-aaai-conference-on-artificial-intelligence/2019/)) · **Publisher:** [Association for the Advancement of Artificial Intelligence](https://md.research.elamur.ai/free/en/publishers/association-for-the-advancement-of-artificial-intelligence/) · **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/1905.10006) · [PDF](https://arxiv.org/pdf/1905.10006v2) · [DOI 10.48550/arxiv.1905.10006](https://doi.org/10.48550/arxiv.1905.10006) · [arXiv 1905.10006](https://arxiv.org/abs/1905.10006) · [OpenAlex](https://openalex.org/W2945173409)

**Citations:** 10 citations (OpenAlex, 2026-10-14) · [23](https://md.research.elamur.ai/free/en/papers/paliwal-2019-graph-representations-higher-order-logic/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Neural guidance of proof search in higher-order logic is difficult, partly because there is no standard way to turn formulas into graphs that a neural network can process. The authors use HOL Light terms from the HOList benchmark, which contains more than twenty thousand theorems with human-written proofs. They treat each S-expression syntax tree as a graph with both child and parent edges, then compare several variants: subexpression sharing, leaf sharing, variable blinding, added random edges, and one-directional (top-down or bottom-up) message flow. A message-passing GNN embeds goals and candidate premises. Trained by imitating human proofs, the model selects a tactic and ranks the theorems passed to it as arguments. Every model is evaluated end to end by counting how many validation theorems the DeepHOL prover closes when guided by it. The best setup, which uses subexpression sharing, proves nearly half of the validation set and clearly surpasses earlier HOList results. The study shows that small representation choices strongly affect performance and that context from parent nodes matters. This supports GNNs over TreeRNNs for encoding logic.

## Key points
- This is presented as the first use of GNNs for higher-order proof search. It is evaluated on HOList / DeepHOL, which is built on HOL Light, and the best model proves close to 50% of validation theorems.
- A simple bag-of-words model already outperforms the original HOList reference models.
- Merging identical subexpressions shrinks the example graph for ∀x : x = x from 27 to 15 nodes. Shared representations clearly outperform plain trees, which contrasts with Wang et al. (2017).
- Passing messages only top-down, which emphasizes context, works better than bottom-up only. Moving from 0 to 12 message-passing hops raises successful tactic applications from 33.8% to 38.6%.
- Training details:
  - batches of 4,096 examples with sampled negative premises;
  - a combined loss of cross-entropy and AUCROC;
  - Adam with a learning rate of 0.0001;
  - eight Tesla V100 GPUs.
- Stated limitation: local assumptions of the goal are ignored.

*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 (3): [🖥️ 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 · [🧮 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: Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal and Christian Szegedy. 2019. Graph Representations for Higher-Order Logic and Theorem Proving. arXiv:1905.10006.

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

```bibtex
@misc{paliwal2019graph,
  title = {{Graph Representations for Higher-Order Logic and Theorem Proving}},
  author = {Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal and Christian Szegedy},
  year = {2019},
  doi = {10.48550/arxiv.1905.10006},
  eprint = {1905.10006},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1905.10006}
}
```

- [← previous Morphologically Annotated Corpora for Seven Arabic Dialects: Taizi, Sanaani, Najdi, Jordanian, Syrian, Iraqi and Moroccan](https://md.research.elamur.ai/free/en/papers/alshargi-2019-morphologically-annotated-corpora-seven-arabic/)
- [next → Handling Syntactic Divergence in Low-resource Machine Translation](https://md.research.elamur.ai/free/en/papers/zhou-2019-handling-syntactic-divergence-low-resource/)
- [↑ back to papers of 2019](https://md.research.elamur.ai/free/en/papers/2019/page/7/)

## References

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

1. Bansal, K.; Loos, S. M.; Rabe, M. N.; Szegedy, C.; and Wilcox, S. 2019. [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.
2. Battaglia, P. W.; Hamrick, J. B.; Bapst, V.; Sanchez-Gonzalez, A.; Zambaldi, V. F.; Malinowski, M.; Tacchetti, A.; Raposo, D.; Santoro, A.; Faulkner, R.; Gülçehre, Ç.; Song, F.; Ballard, A. J.; Gilmer, J.; Dahl, G. E.; Vaswani, A.; Allen, K.; Nash, C.; Langston, V.; Dyer, C.; Heess, N.; Wierstra,… — [Relational inductive biases, deep learning, and graph networks](https://md.research.elamur.ai/free/en/papers/battaglia-2018-relational-inductive-biases-deep-learning/)
3. Bentkamp, A.; Blanchette, J. C.; Cruanes, S.; and Waldmann, U. 2018. Superposition for lambda-free higher-order logic. In Galmiche, D.; Schulz, S.; and Sebastiani, R., eds., Automated Reasoning, 28–46. Cham: Springer International Publishing. [find](https://scholar.google.com/scholar?q=Bentkamp%2C+A%2E%3B+Blanchette%2C+J%2E+C%2E%3B+Cruanes%2C+S%2E%3B+and+Waldmann%2C+U%2E+2018%2E+Superposition+for+lambda%2Dfree+higher%2Dorder+logic%2E+In+Galmiche%2C+D%2E%3B+Schulz%2C+S%2E%3B+and+Sebastiani%2C+R%2E%2C+eds%2E%2C+Automated+Reasoning%2C+28%E2%80%9346)
4. Burges, C.; Shaked, T.; Renshaw, E.; Lazier, A.; Deeds, M.; Hamilton, N.; and Hullender, G. N. 2005. [Learning to rank using gradient descent](https://md.research.elamur.ai/free/en/papers/burges-2005-learning-rank-using-gradient/). In Proceedings of the 22nd International Conference on Machine learning (ICML-05), 89–96.
5. Dong, H.; Mao, J.; Lin, T.; Wang, C.; Li, L.; and Zhou, D. 2019. Neural logic machines. ICLR 2019. International Conference on Learning Representations. [find](https://scholar.google.com/scholar?q=Dong%2C+H%2E%3B+Mao%2C+J%2E%3B+Lin%2C+T%2E%3B+Wang%2C+C%2E%3B+Li%2C+L%2E%3B+and+Zhou%2C+D%2E+2019%2E+Neural+logic+machines%2E+ICLR+2019%2E+International+Conference+on+Learning+Representations%2E)
6. Eban, E. E.; Schain, M.; Mackey, A.; Gordon, A.; Saurous, R. A.; and Elidan, G. 2017. Scalable learning of non-decomposable objectives. Proceedings of the 20th International Conference on Artificial Intelligence and Statistics (AISTATS). [find](https://scholar.google.com/scholar?q=Eban%2C+E%2E+E%2E%3B+Schain%2C+M%2E%3B+Mackey%2C+A%2E%3B+Gordon%2C+A%2E%3B+Saurous%2C+R%2E+A%2E%3B+and+Elidan%2C+G%2E+2017%2E+Scalable+learning+of+non%2Ddecomposable+objectives%2E+Proceedings+of+the+20th+International+Conference+on+Artificial+I)
7. Evans, R.; Saxton, D.; Amos, D.; Kohli, P.; and Grefenstette, E. 2018. [Can neural networks understand logical entailment?](https://md.research.elamur.ai/free/en/papers/evans-2018-can-neural-networks-understand-logical/) ICLR 2018. International Conference on Learning Representations.
8. Gauthier, T.; Kaliszyk, C.; and Urban, J. 2017. Tactictoe: Learning to reason with hol4 tactics. In LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46, 125–143. [find](https://scholar.google.com/scholar?q=Gauthier%2C+T%2E%3B+Kaliszyk%2C+C%2E%3B+and+Urban%2C+J%2E+2017%2E+Tactictoe%3A+Learning+to+reason+with+hol4+tactics%2E+In+LPAR%2D21%2E+21st+International+Conference+on+Logic+for+Programming%2C+Artificial+Intelligence+and+Reasoni)
9. Gilmer, J.; Schoenholz, S. S.; Riley, P. F.; Vinyals, O.; and Dahl, G. E. 2017. [Neural message passing for quantum chemistry](https://md.research.elamur.ai/free/en/papers/gilmer-2017-neural-message-passing-quantum-chemistry/). CoRR abs/1704.01212.
10. Gonthier, G.; Asperti, A.; Avigad, J.; Bertot, Y.; Cohen, C.; Garillot, F.; Roux, S. L.; Mahboubi, A.; O’Connor, R.; Biha, S. O.; Pasca, I.; Rideau, L.; Solovyev, A.; Tassi, E.; and Théry, L. 2013. A machine-checked proof of the Odd Order Theorem. In ITP, 163–179. [find](https://scholar.google.com/scholar?q=Gonthier%2C+G%2E%3B+Asperti%2C+A%2E%3B+Avigad%2C+J%2E%3B+Bertot%2C+Y%2E%3B+Cohen%2C+C%2E%3B+Garillot%2C+F%2E%3B+Roux%2C+S%2E+L%2E%3B+Mahboubi%2C+A%2E%3B+O%E2%80%99Connor%2C+R%2E%3B+Biha%2C+S%2E+O%2E%3B+Pasca%2C+I%2E%3B+Rideau%2C+L%2E%3B+Solovyev%2C+A%2E%3B+Tassi%2C+E%2E%3B+and+The%CC%81ry%2C+L%2E+2013%2E+A)
11. Gonthier, G. 2008. Formal proof–the four-color theorem. Notices of the AMS 55(11):1382–1393. [find](https://scholar.google.com/scholar?q=Gonthier%2C+G%2E+2008%2E+Formal+proof%E2%80%93the+four%2Dcolor+theorem%2E+Notices+of+the+AMS+55%2811%29%3A1382%E2%80%931393%2E)
12. Hales, T.; Adams, M.; Bauer, G.; Dang, T. D.; Harrison, J.; Le Truong, H.; Kaliszyk, C.; Magron, V.; McLaughlin, S.; Nguyen, T. T.; et al. 2017. [A formal proof of the kepler conjecture](https://md.research.elamur.ai/free/en/papers/hales-2015-formal-proof-kepler-conjecture/). In Forum of Mathematics, Pi, volume 5. Cambridge University Press.
13. Harrison, J. 1996. HOL Light: A tutorial introduction. In FMCAD, 265–269. [find](https://scholar.google.com/scholar?q=Harrison%2C+J%2E+1996%2E+HOL+Light%3A+A+tutorial+introduction%2E+In+FMCAD%2C+265%E2%80%93269%2E)
14. Huang, D.; Dhariwal, P.; Song, D.; and Sutskever, I. 2018. [Gamepad: A learning environment for theorem proving](https://md.research.elamur.ai/free/en/papers/huang-2018-gamepad-learning-environment-theorem-proving/). ICLR 2018. International Conference on Learning Representations.
15. Kaliszyk, C., and Urban, J. 2014. [Learning-assisted automated reasoning with flyspeck](https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/). Journal of Automated Reasoning 53(2):173–213.
16. Kingma, D. P., and Ba, J. 2014. [Adam: A method for stochastic optimization](https://md.research.elamur.ai/free/en/papers/kingma-2014-adam-method-stochastic-optimization/). arXiv preprint arXiv:1412.6980.
17. Lederman, G.; Rabe, M. N.; and Seshia, S. A. 2018. [Learning heuristics for automated reasoning through deep reinforcement learning](https://md.research.elamur.ai/free/en/papers/lederman-2018-learning-heuristics-quantified-boolean-formulas/). CoRR abs/1807.08058.
18. Li, Y.; Tarlow, D.; Brockschmidt, M.; and Zemel, R. 2015. Gated graph sequence neural networks. arXiv preprint arXiv:1511.05493. [find](https://scholar.google.com/scholar?q=Li%2C+Y%2E%3B+Tarlow%2C+D%2E%3B+Brockschmidt%2C+M%2E%3B+and+Zemel%2C+R%2E+2015%2E+Gated+graph+sequence+neural+networks%2E+arXiv+preprint+arXiv%3A1511%2E05493%2E)
19. Li, Y.; Yu, R.; Shahabi, C.; and Liu, Y. 2017. Graph convolutional recurrent neural network: Data-driven traffic forecasting. CoRR abs/1707.01926. — [arXiv:1707.01926](https://arxiv.org/abs/1707.01926) [find](https://scholar.google.com/scholar?q=Li%2C+Y%2E%3B+Yu%2C+R%2E%3B+Shahabi%2C+C%2E%3B+and+Liu%2C+Y%2E+2017%2E+Graph+convolutional+recurrent+neural+network%3A+Data%2Ddriven+traffic+forecasting%2E+CoRR+abs%2F1707%2E01926%2E+%E2%80%94+%5BarXiv%3A1707%2E01926%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1707%2E01926)
20. Loos, S.; Irving, G.; Szegedy, C.; and Kaliszyk, C. 2017. [Deep network guided proof search](https://md.research.elamur.ai/free/en/papers/loos-2017-deep-network-guided-proof-search/). LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning.
21. Polyak, B. T., and Juditsky, A. B. 1992. Acceleration of stochastic approximation by averaging. SIAM Journal on Control and Optimization 30(4):838– 855. [find](https://scholar.google.com/scholar?q=Polyak%2C+B%2E+T%2E%2C+and+Juditsky%2C+A%2E+B%2E+1992%2E+Acceleration+of+stochastic+approximation+by+averaging%2E+SIAM+Journal+on+Control+and+Optimization+30%284%29%3A838%E2%80%93+855%2E)
22. Polyak, B. T. 1990. A new method of stochastic approximation type. Avtomatika i telemekhanika 7:98– 107. [find](https://scholar.google.com/scholar?q=Polyak%2C+B%2E+T%2E+1990%2E+A+new+method+of+stochastic+approximation+type%2E+Avtomatika+i+telemekhanika+7%3A98%E2%80%93+107%2E)
23. Raposo, D.; Santoro, A.; Barrett, D. G. T.; Pascanu, R.; Lillicrap, T. P.; and Battaglia, P. W. 2017. Discovering objects and their relations from entangled scene representations. CoRR abs/1702.05068. — [arXiv:1702.05068](https://arxiv.org/abs/1702.05068) [find](https://scholar.google.com/scholar?q=Raposo%2C+D%2E%3B+Santoro%2C+A%2E%3B+Barrett%2C+D%2E+G%2E+T%2E%3B+Pascanu%2C+R%2E%3B+Lillicrap%2C+T%2E+P%2E%3B+and+Battaglia%2C+P%2E+W%2E+2017%2E+Discovering+objects+and+their+relations+from+entangled+scene+representations%2E+CoRR+abs%2F1702%2E05068%2E)
24. Sanchez-Stern, A.; Alhessi, Y.; Saul, L. K.; and Lerner, S. 2019. [Generating correctness proofs with neural networks](https://md.research.elamur.ai/free/en/papers/stern-2019-generating-correctness-proofs-neural-networks/). CoRR abs/1907.07794.
25. Santoro, A.; Raposo, D.; Barrett, D. G. T.; Malinowski, M.; Pascanu, R.; Battaglia, P.; and Lillicrap, T. P. 2017. [A simple neural network module for relational reasoning](https://md.research.elamur.ai/free/en/papers/santoro-2017-simple-neural-network-module-relational/). CoRR abs/1706.01427.
26. Scarselli, F.; Gori, M.; Tsoi, A. C.; Hagenbuchner, M.; and Monfardini, G. 2009. The graph neural network model. IEEE Transactions on Neural Networks 20(1):61–80. [find](https://scholar.google.com/scholar?q=Scarselli%2C+F%2E%3B+Gori%2C+M%2E%3B+Tsoi%2C+A%2E+C%2E%3B+Hagenbuchner%2C+M%2E%3B+and+Monfardini%2C+G%2E+2009%2E+The+graph+neural+network+model%2E+IEEE+Transactions+on+Neural+Networks+20%281%29%3A61%E2%80%9380%2E)
27. Selsam, D., and Bjørner, N. 2019. [Guiding high-performance sat solvers with unsat-core predictions](https://md.research.elamur.ai/free/en/papers/selsam-2019-guiding-high-performance-sat-solvers/). SAT 2019, The 22nd International Conference on Theory and Applications of Satisfiability Testing.
28. Wang, M.; Tang, Y.; Wang, J.; and Deng, J. 2017. [Premise selection for theorem proving by deep graph embedding](https://md.research.elamur.ai/free/en/papers/wang-2017-premise-selection-theorem-proving-deep/). In Advances in Neural Information Processing Systems, 2786–2796.
29. Wu, Z.; Pan, S.; Chen, F.; Long, G.; Zhang, C.; and Yu, P. S. 2019. [A comprehensive survey on graph neural networks](https://md.research.elamur.ai/free/en/papers/wu-2019-comprehensive-survey-graph-neural-networks/). CoRR abs/1901.00596.
30. Xu, K.; Hu, W.; Leskovec, J.; and Jegelka, S. 2019. [How powerful are graph neural networks?](https://md.research.elamur.ai/free/en/papers/xu-2018-powerful-graph-neural-networks/) ICLR 2019. International Conference on Learning Representations.
31. Yang, K., and Deng, J. 2019. [Learning to prove theorems via interacting with proof assistants](https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/). CoRR abs/1905.09381.

*Updated 3 November 2026*