mlsanityData to 7 Oct 2026

Graph2Tac: Online Representation Learning of Formal Math Concepts

arXiv 2401.02949 ↗First posted 5 Jan 2024cs.LG cs.AIcited by 15

Not on the map. Why?

Abstract (arXiv)

In proof assistants, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance. Furthermore, lemmas with close proximity regularly exhibit similar proof structures. We show that this locality property can be exploited through online learning techniques to obtain solving agents that far surpass offline learners when asked to prove theorems in an unseen mathematical setting. We extensively benchmark two such online solvers implemented in the Tactician platform for the Coq proof assistant: First, Tactician's online k-nearest neighbor solver, which can learn from recent proofs, shows a 1.72× improvement in theorems proved over an offline equivalent. Second, we introduce a graph neural network, Graph2Tac, with a novel approach to build hierarchical representations for new definitions. Graph2Tac's online definition task realizes a 1.5× improvement in theorems solved over an offline baseline. The k-NN and Graph2Tac solvers rely on orthogonal online data, making them highly complementary. Their combination improves 1.27× over their individual performances. Both solvers outperform all other general-purpose provers for Coq, including CoqHammer, Proverbot9001, and a transformer baseline by at least 1.48× and are available for practical use by end-users.

Key facts. Cited by 15 papers in the map (data through 7 Oct 2026). Builds on 24 of its 46 references that are in the map. First posted on arXiv 5 Jan 2024.

Builds on

24 of 46 references.

References · 24

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  2. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  3. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  4. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  5. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  6. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  7. 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
  8. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  9. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  10. 2019Generating Correctness Proofs with Neural Networkscited by 36
  11. 2017ENIGMA: Efficient Learning-based Inference Guiding Machinecited by 26
  12. 2020ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)cited by 26
12 more
  1. 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
  2. 2013MizAR 40 for Mizar 40cited by 23
  3. 2020The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coqcited by 23
  4. 2022TF-GNN: Graph Neural Networks in TensorFlowcited by 21
  5. 2022Passport: Improving Automated Formal Verification Using Identifierscited by 19
  6. 2018Learning to Reason with HOL4 tacticscited by 14
  7. 2023Machine-Learned Premise Selection for Leancited by 10
  8. 2020Tactic Learning and Proving for the Coq Proof Assistantcited by 8
  9. 2022The Isabelle ENIGMAcited by 8
  10. 2021Online Machine Learning Techniques for Coq: A Comparisoncited by 7
  11. 2015SEPIA: Search for Proofs Using Inferred Automatacited by 4
  12. 2014Machine Learning of Coq Proof Guidance: First Experimentscited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 7; 2025: 5; 2026: 3.

15 papers.

Sort:

By area:

  1. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  2. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  3. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  4. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  5. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  6. 2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
  7. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 8
  8. 2025Premise Selection for a Lean Hammercited by 6
  9. 2024Learning Structure-Aware Representations of Dependent Typescited by 2
  10. 2025Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Provingcited by 2
  11. 2025Neuro-Symbolic AI for Cybersecurity: State of the Art, Challenges, and Opportunitiescited by 2
  12. 2025ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Provingcited by 1
3 more
  1. 2026Harnessing Code Agents for Automatic Software Verificationcited by 1
  2. 2026What are the Right Symmetries for Formal Theorem Proving?cited by 0
  3. 2026PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMscited by 0