Graph Contrastive Pre-training for Effective Theorem Reasoning

2021/08/24 by Li, Zhaoyu, Chen, Binghong, Si, Xujie
#FOS: Computer and information sciences #Machine Learning (cs.LG)

paper · doi:10.48550/arxiv.2108.10821

Abstract

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.

Related

• Learning to Guide a Saturation-Based Theorem Prover
• An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations
• Learning to Prove Theorems via Interacting with Proof Assistants
• Graph2Tac: Online Representation Learning of Formal Math Concepts
• A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving