ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)

• URL: http://arxiv.org/abs/2002.05406v2
• Date: Tue, 28 Apr 2020 13:59:26 GMT
• Title: ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
• Authors: Jan Jakub\r{u}v, Karel Chvalovsk\'y, Miroslav Ol\v{s}\'ak, Bartosz Piotrowski, Martin Suda, Josef Urban
• Abstract summary: We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers. For the gradient-boosting guidance, we manually create abstracted features by considering arity-based encodings of formulas. For the neural guidance, we use symbol-independent graph neural networks (GNNs) and their embedding of the terms and clauses.
• Score: 0.4893345190925177
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems. For the gradient-boosting guidance, we manually create abstracted features by considering arity-based encodings of formulas. For the neural guidance, we use symbol-independent graph neural networks (GNNs) and their embedding of the terms and clauses. The two methods are efficiently implemented in the E prover and its ENIGMA learning-guided framework. To provide competitive real-time performance of the GNNs, we have developed a new context-based approach to evaluation of generated clauses in E. Clauses are evaluated jointly in larger batches and with respect to a large number of already selected clauses (context) by the GNN that estimates their collectively most useful subset in several rounds of message passing. This means that approximative inference rounds done by the GNN are efficiently interleaved with precise symbolic inference rounds done inside E. The methods are evaluated on the MPTP large-theory benchmark and shown to achieve comparable real-time performance to state-of-the-art symbol-based methods. The methods also show high complementarity, solving a large number of hard Mizar problems.

Related papers

• Leveraging Joint Predictive Embedding and Bayesian Inference in Graph Self Supervised Learning [0.0]
  Graph representation learning has emerged as a cornerstone for tasks like node classification and link prediction. Current self-supervised learning (SSL) methods face challenges such as computational inefficiency, reliance on contrastive objectives, and representation collapse. We propose a novel joint embedding predictive framework for graph SSL that eliminates contrastive objectives and negative sampling while preserving semantic and structural information.
  arXiv  Detail & Related papers  (2025-02-02T07:42:45Z)
• LASE: Learned Adjacency Spectral Embeddings [7.612218105739107]
  We learn nodal Adjacency Spectral Embeddings (ASE) from graph inputs. LASE is interpretable, parameter efficient, robust to inputs with unobserved edges. LASE layers combine Graph Convolutional Network (GCN) and fully-connected Graph Attention Network (GAT) modules.
  arXiv  Detail & Related papers  (2024-12-23T17:35:19Z)
• Efficient Graph Similarity Computation with Alignment Regularization [7.143879014059894]
  Graph similarity computation (GSC) is a learning-based prediction task using Graph Neural Networks (GNNs) We show that high-quality learning can be attained with a simple yet powerful regularization technique, which we call the Alignment Regularization (AReg) In the inference stage, the graph-level representations learned by the GNN encoder are directly used to compute the similarity score without using AReg again to speed up inference.
  arXiv  Detail & Related papers  (2024-06-21T07:37:28Z)
• Ensemble Quadratic Assignment Network for Graph Matching [52.20001802006391]
  Graph matching is a commonly used technique in computer vision and pattern recognition. Recent data-driven approaches have improved the graph matching accuracy remarkably. We propose a graph neural network (GNN) based approach to combine the advantages of data-driven and traditional methods.
  arXiv  Detail & Related papers  (2024-03-11T06:34:05Z)
• Optimal Inference in Contextual Stochastic Block Models [0.0]
  The contextual block model (cSBM) was proposed for unsupervised community detection on attributed graphs. The cSBM has been widely used as a synthetic dataset for evaluating the performance of graph-neural networks (GNNs) for semi-supervised node classification. We show that there can be a considerable gap between the accuracy reached by this algorithm and the performance of the GNN architectures proposed in the literature.
  arXiv  Detail & Related papers  (2023-06-06T10:02:57Z)
• Scalable Learning of Latent Language Structure With Logical Offline Cycle Consistency [71.42261918225773]
  Conceptually, LOCCO can be viewed as a form of self-learning where the semantic being trained is used to generate annotations for unlabeled text. As an added bonus, the annotations produced by LOCCO can be trivially repurposed to train a neural text generation model.
  arXiv  Detail & Related papers  (2023-05-31T16:47:20Z)
• Neural Structured Prediction for Inductive Node Classification [29.908759584092167]
  This paper studies node classification in the inductive setting, aiming to learn a model on labeled training graphs and generalize it to infer node labels on unlabeled test graphs. We present a new approach called the Structured Proxy Network (SPN), which combines the advantages of both worlds.
  arXiv  Detail & Related papers  (2022-04-15T15:50:27Z)
• GNNRank: Learning Global Rankings from Pairwise Comparisons via Directed Graph Neural Networks [68.61934077627085]
  We introduce GNNRank, a modeling framework compatible with any GNN capable of learning digraph embeddings. We show that our methods attain competitive and often superior performance compared with existing approaches.
  arXiv  Detail & Related papers  (2022-02-01T04:19:50Z)
• VQ-GNN: A Universal Framework to Scale up Graph Neural Networks using Vector Quantization [70.8567058758375]
  VQ-GNN is a universal framework to scale up any convolution-based GNNs using Vector Quantization (VQ) without compromising the performance. Our framework avoids the "neighbor explosion" problem of GNNs using quantized representations combined with a low-rank version of the graph convolution matrix.
  arXiv  Detail & Related papers  (2021-10-27T11:48:50Z)
• Distance Encoding: Design Provably More Powerful Neural Networks for Graph Representation Learning [63.97983530843762]
  Graph Neural Networks (GNNs) have achieved great success in graph representation learning. GNNs generate identical representations for graph substructures that may in fact be very different. More powerful GNNs, proposed recently by mimicking higher-order tests, are inefficient as they cannot sparsity of underlying graph structure. We propose Distance Depiction (DE) as a new class of graph representation learning.
  arXiv  Detail & Related papers  (2020-08-31T23:15:40Z)
• Binarized Graph Neural Network [65.20589262811677]
  We develop a binarized graph neural network to learn the binary representations of the nodes with binary network parameters. Our proposed method can be seamlessly integrated into the existing GNN-based embedding approaches. Experiments indicate that the proposed binarized graph neural network, namely BGN, is orders of magnitude more efficient in terms of both time and space.
  arXiv  Detail & Related papers  (2020-04-19T09:43:14Z)

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.