# Graph Contrastive Pre-training for Effective Theorem Reasoning

arXiv: https://arxiv.org/abs/2108.10821 · HTML: https://mlsanity.com/paper/2108.10821/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 22 references that are in the map.
- First posted on arXiv 24 Aug 2021.

## Builds on (most cited first, 14 of 14)

- [A Simple Framework for Contrastive Learning of Visual Representations](https://mlsanity.com/paper/2002.05709/) (2020)
- [Representation Learning with Contrastive Predictive Coding](https://mlsanity.com/paper/1807.03748/) (2018)
- [Momentum Contrast for Unsupervised Visual Representation Learning](https://mlsanity.com/paper/1911.05722/) (2019)
- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Deep Graph Contrastive Representation Learning](https://mlsanity.com/paper/2006.04131/) (2020)
- [GCC: Graph Contrastive Coding for Graph Neural Network Pre-Training](https://mlsanity.com/paper/2006.09963/) (2020)
- [Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networks](https://mlsanity.com/paper/1503.00075/) (2015)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving](https://mlsanity.com/paper/1703.00426/) (2017)

## Built on by (most cited first, 3 of 3)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4](https://mlsanity.com/paper/2410.16429/) (2024)
- [What are the Right Symmetries for Formal Theorem Proving?](https://mlsanity.com/paper/2605.22257/) (2026)

## Abstract (arXiv)

Interactive theorem proving is a challenging and tedious process, which requires non-trivial expertise and detailed low-level instructions (or tactics) from human experts. Tactic prediction is a natural way to automate this process. Existing methods show promising results on tactic prediction by learning a deep neural network (DNN) based model from proofs written by human experts. In this paper, we propose NeuroTactic, a novel extension with a special focus on improving the representation learning for theorem proving. NeuroTactic leverages graph neural networks (GNNs) to represent the theorems and premises, and applies graph contrastive learning for pre-training. We demonstrate that the representation learning of theorems is essential to predict tactics. Compared with other methods, NeuroTactic achieves state-of-the-art performance on the CoqGym dataset.