Graph Contrastive Pre-training for Effective Theorem Reasoning
This work addresses the tedious and expertise-intensive process of theorem proving for mathematicians and computer scientists, offering an incremental improvement over existing methods.
The paper tackles the problem of automating interactive theorem proving by improving tactic prediction through better representation learning of theorems and premises, achieving state-of-the-art performance on the CoqGym dataset.
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.