mlsanityData to 14 Oct 2026

Graph Representations for Higher-Order Logic and Theorem Proving

arXiv 1905.10006 ↗First posted 24 May 2019cs.LG cs.AI cs.LOcited by 55

Not on the map. Why?

Abstract (arXiv)

This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem provers allow for the formalization of most mathematical theories and have been shown to pose a significant challenge for deep learning. Higher-order logic is highly expressive and, even though it is well-structured with a clearly defined grammar and semantics, there still remains no well-established method to convert formulas into graph-based representations. In this paper, we consider several graphical representations of higher-order logic and evaluate them against the HOList benchmark for higher-order theorem proving.

Key facts. Cited by 55 papers in the map (data through 14 Oct 2026). First posted on arXiv 24 May 2019.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 14; 2022: 6; 2023: 9; 2024: 17; 2025: 5; 2026: 4.

55 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  2. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  3. 2021Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoningcited by 383
  4. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  5. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  6. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 58
  7. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  8. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  9. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  10. 2022Towards Data-and Knowledge-Driven Artificial Intelligence: A Survey on Neuro-Symbolic Computingcited by 35
  11. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 27
  12. 2021Neural Circuit Synthesis from Specification Patternscited by 17
38 more
  1. 2021Neural Termination Analysiscited by 16
  2. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  3. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  4. 2023Learning Differentiable Logic Programs for Abstract Visual Reasoningcited by 12
  5. 2021Embedding Symbolic Temporal Knowledge into Deep Sequential Modelscited by 11
  6. 2023Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matricescited by 9
  7. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 9
  8. 2024Can Transformers Do Enumerative Geometry?cited by 8
  9. 2023Multi-Operational Mathematical Derivations in Latent Spacecited by 6
  10. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5
  11. 2021A Study of Continuous Vector Representationsfor Theorem Provingcited by 4
  12. 2021An energy-based model for neuro-symbolic reasoning on knowledge graphscited by 4
  13. 2023An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representationscited by 4
  14. 2021Graph Contrastive Pre-training for Effective Theorem Reasoningcited by 3
  15. 2021Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rulescited by 3
  16. 2022Gym-saturation: an OpenAI Gym environment for saturation proverscited by 3
  17. 2024NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesiscited by 3
  18. 2024Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AIcited by 3
  19. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learningcited by 3
  20. 2025Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphscited by 3
  21. 2022OCTAL: Graph Representation Learning for LTL Model Checkingcited by 2
  22. 2023Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Methodcited by 2
  23. 2024Learning Structure-Aware Representations of Dependent Typescited by 2
  24. 2024Graph Pruning for Enumeration of Minimal Unsatisfiable Subsetscited by 2
  25. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2
  26. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  27. 2022Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)cited by 1
  28. 2022Learning to Prove Trigonometric Identitiescited by 1
  29. 2024Learning Better Representations From Less Data For Propositional Satisfiabilitycited by 1
  30. 2024Guiding Genetic Programming with Graph Neural Networkscited by 1
  31. 2024Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)cited by 1
  32. 2025Hierarchical Attention Generates Better Proofscited by 1
  33. 2025Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspectivecited by 1
  34. 2026What are the Right Symmetries for Formal Theorem Proving?cited by 1
  35. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  36. 2021Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learningcited by 0
  37. 2022Generating Intermediate Steps for NLI with Next-Step Supervisioncited by 0
  38. 2023OCTAL: Graph Representation Learning for LTL Model Checkingcited by 0

50 most cited of 55 All 55 (JSON)