Graph Contrastive Pre-training for Effective Theorem Reasoning

• URL: http://arxiv.org/abs/2108.10821v1
• Date: Tue, 24 Aug 2021 16:14:54 GMT
• Title: Graph Contrastive Pre-training for Effective Theorem Reasoning
• Authors: Zhaoyu Li, Binghong Chen, Xujie Si
• Abstract summary: Existing methods show promising results on tactic prediction by learning a deep neural network based model from proofs written by human experts. We propose NeuroTactic, a novel extension with a special focus on improving the representation learning for theorem proving.
• Score: 6.721845345130468
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 papers

• Deep Learning Through A Telescoping Lens: A Simple Model Provides Empirical Insights On Grokking, Gradient Boosting & Beyond [61.18736646013446]
  In pursuit of a deeper understanding of its surprising behaviors, we investigate the utility of a simple yet accurate model of a trained neural network. Across three case studies, we illustrate how it can be applied to derive new empirical insights on a diverse range of prominent phenomena.
  arXiv  Detail & Related papers  (2024-10-31T22:54:34Z)
• Concept Prerequisite Relation Prediction by Using Permutation-Equivariant Directed Graph Neural Networks [3.1688996975958306]
  CPRP, concept prerequisite relation prediction, is a fundamental task in using AI for education. We present a permutation-equivariant directed GNN model by introducing the Weisfeiler-Lehman test into directed GNN learning. Our model delivers better prediction performance than the state-of-the-art methods.
  arXiv  Detail & Related papers  (2023-12-15T14:01:56Z)
• Towards Few-shot Inductive Link Prediction on Knowledge Graphs: A Relational Anonymous Walk-guided Neural Process Approach [49.00753238429618]
  Few-shot inductive link prediction on knowledge graphs aims to predict missing links for unseen entities with few-shot links observed. Recent inductive methods utilize the sub-graphs around unseen entities to obtain the semantics and predict links inductively. We propose a novel relational anonymous walk-guided neural process for few-shot inductive link prediction on knowledge graphs, denoted as RawNP.
  arXiv  Detail & Related papers  (2023-06-26T12:02:32Z)
• Adversarial Attacks on the Interpretation of Neuron Activation Maximization [70.5472799454224]
  Activation-maximization approaches are used to interpret and analyze trained deep-learning models. In this work, we consider the concept of an adversary manipulating a model for the purpose of deceiving the interpretation.
  arXiv  Detail & Related papers  (2023-06-12T19:54:33Z)
• What Can the Neural Tangent Kernel Tell Us About Adversarial Robustness? [0.0]
  We study adversarial examples of trained neural networks through analytical tools afforded by recent theory advances connecting neural networks and kernel methods. We show how NTKs allow to generate adversarial examples in a training-free'' fashion, and demonstrate that they transfer to fool their finite-width neural net counterparts in the lazy'' regime.
  arXiv  Detail & Related papers  (2022-10-11T16:11:48Z)
• How does unlabeled data improve generalization in self-training? A one-hidden-layer theoretical analysis [93.37576644429578]
  This work establishes the first theoretical analysis for the known iterative self-training paradigm. We prove the benefits of unlabeled data in both training convergence and generalization ability. Experiments from shallow neural networks to deep neural networks are also provided to justify the correctness of our established theoretical insights on self-training.
  arXiv  Detail & Related papers  (2022-01-21T02:16:52Z)
• How Neural Processes Improve Graph Link Prediction [35.652234989200956]
  We propose a meta-learning approach with graph neural networks for link prediction: Neural Processes for Graph Neural Networks (NPGNN) NPGNN can perform both transductive and inductive learning tasks and adapt to patterns in a large new graph after training with a small subgraph.
  arXiv  Detail & Related papers  (2021-09-30T07:35:13Z)
• Predicting cognitive scores with graph neural networks through sample selection learning [0.0]
  Functional brain connectomes are used to predict cognitive measures such as intelligence quotient (IQ) scores. We design a novel regression GNN model (namely RegGNN) for predicting IQ scores from brain connectivity. We also propose a emphlearning-based sample selection method that learns how to choose the training samples with the highest expected predictive power.
  arXiv  Detail & Related papers  (2021-06-17T11:45:39Z)
• Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
  TRAIL is a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. To the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover.
  arXiv  Detail & Related papers  (2021-06-07T18:35:57Z)
• Training a First-Order Theorem Prover from Synthetic Data [50.23600875138756]
  A major challenge in applying machine learning to automated theorem proving is the scarcity of training data. We propose an approach that relies on training purely with synthetically generated theorems, without any human data aside from axioms. Our neural prover outperforms the state-of-the-art E-prover on this synthetic data in both time and search steps.
  arXiv  Detail & Related papers  (2021-03-05T17:01:34Z)
• How Neural Networks Extrapolate: From Feedforward to Graph Neural Networks [80.55378250013496]
  We study how neural networks trained by gradient descent extrapolate what they learn outside the support of the training distribution. Graph Neural Networks (GNNs) have shown some success in more complex tasks.
  arXiv  Detail & Related papers  (2020-09-24T17:48:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.