The Role of Entropy in Guiding a Connection Prover

• URL: http://arxiv.org/abs/2105.14706v1
• Date: Mon, 31 May 2021 04:57:44 GMT
• Title: The Role of Entropy in Guiding a Connection Prover
• Authors: Zsolt Zombori, Josef Urban, Miroslav Ol\v{s}\'ak
• Abstract summary: We study how to learn good algorithms for selecting reasoning steps in theorem proving. We start by incorporating a state-of-the-art learning algorithm -- a graph neural network (GNN) -- into the plCoP theorem prover.
• Score: 1.279913017771418
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this work we study how to learn good algorithms for selecting reasoning steps in theorem proving. We explore this in the connection tableau calculus implemented by leanCoP where the partial tableau provides a clean and compact notion of a state to which a limited number of inferences can be applied. We start by incorporating a state-of-the-art learning algorithm -- a graph neural network (GNN) -- into the plCoP theorem prover. Then we use it to observe the system's behaviour in a reinforcement learning setting, i.e., when learning inference guidance from successful Monte-Carlo tree searches on many problems. Despite its better pattern matching capability, the GNN initially performs worse than a simpler previously used learning algorithm. We observe that the simpler algorithm is less confident, i.e., its recommendations have higher entropy. This leads us to explore how the entropy of the inference selection implemented via the neural network influences the proof search. This is related to research in human decision-making under uncertainty, and in particular the probability matching theory. Our main result shows that a proper entropy regularisation, i.e., training the GNN not to be overconfident, greatly improves plCoP's performance on a large mathematical corpus.

Related papers

• SGD method for entropy error function with smoothing l0 regularization for neural networks [3.108634881604788]
  entropy error function has been widely used in neural networks. We propose a novel entropy function with smoothing l0 regularization for feed-forward neural networks. Our work is novel as it enables neural networks to learn effectively, producing more accurate predictions.
  arXiv  Detail & Related papers  (2024-05-28T19:54:26Z)
• How Graph Neural Networks Learn: Lessons from Training Dynamics [80.41778059014393]
  We study the training dynamics in function space of graph neural networks (GNNs) We find that the gradient descent optimization of GNNs implicitly leverages the graph structure to update the learned function. This finding offers new interpretable insights into when and why the learned GNN functions generalize.
  arXiv  Detail & Related papers  (2023-10-08T10:19:56Z)
• The Clock and the Pizza: Two Stories in Mechanistic Explanation of Neural Networks [59.26515696183751]
  We show that algorithm discovery in neural networks is sometimes more complex. We show that even simple learning problems can admit a surprising diversity of solutions.
  arXiv  Detail & Related papers  (2023-06-30T17:59:13Z)
• Neural Algorithmic Reasoning for Combinatorial Optimisation [20.36694807847833]
  We propose leveraging recent advancements in neural reasoning to improve the learning of CO problems. We suggest pre-training our neural model on relevant algorithms before training it on CO instances. Our results demonstrate that by using this learning setup, we achieve superior performance compared to non-algorithmically informed deep learning models.
  arXiv  Detail & Related papers  (2023-05-18T13:59:02Z)
• Neural Algorithmic Reasoning with Causal Regularisation [18.299363749150093]
  We make an important observation: there are many different inputs for which an algorithm will perform certain intermediate computations identically. This insight allows us to develop data augmentation procedures that, given an algorithm's intermediate trajectory, produce inputs for which the target algorithm would have exactly the same next trajectory step. We prove that the resulting method, which we call Hint-ReLIC, improves the OOD generalisation capabilities of the reasoner.
  arXiv  Detail & Related papers  (2023-02-20T19:41:15Z)
• Learning Branching Heuristics from Graph Neural Networks [1.4660170768702356]
  We first propose a new graph neural network (GNN) model designed using a probabilistic method. Our approach introduces a new way of applying GNNs towards enhancing the classical backtracking algorithm used in AI.
  arXiv  Detail & Related papers  (2022-11-26T00:01:01Z)
• Graph Neural Networks are Dynamic Programmers [0.0]
  Graph neural networks (GNNs) are claimed to align with dynamic programming (DP) Here we show, using methods from theory and abstract algebra, that there exists an intricate connection between GNNs and DP.
  arXiv  Detail & Related papers  (2022-03-29T13:27:28Z)
• Robustification of Online Graph Exploration Methods [59.50307752165016]
  We study a learning-augmented variant of the classical, notoriously hard online graph exploration problem. We propose an algorithm that naturally integrates predictions into the well-known Nearest Neighbor (NN) algorithm.
  arXiv  Detail & Related papers  (2021-12-10T10:02:31Z)
• Towards Efficient Graph Convolutional Networks for Point Cloud Handling [181.59146413326056]
  We aim at improving the computational efficiency of graph convolutional networks (GCNs) for learning on point clouds. A series of experiments show that optimized networks have reduced computational complexity, decreased memory consumption, and accelerated inference speed.
  arXiv  Detail & Related papers  (2021-04-12T17:59:16Z)
• Fast Learning of Graph Neural Networks with Guaranteed Generalizability: One-hidden-layer Case [93.37576644429578]
  Graph neural networks (GNNs) have made great progress recently on learning from graph-structured data in practice. We provide a theoretically-grounded generalizability analysis of GNNs with one hidden layer for both regression and binary classification problems.
  arXiv  Detail & Related papers  (2020-06-25T00:45:52Z)
• Optimization and Generalization Analysis of Transduction through Gradient Boosting and Application to Multi-scale Graph Neural Networks [60.22494363676747]
  It is known that the current graph neural networks (GNNs) are difficult to make themselves deep due to the problem known as over-smoothing. Multi-scale GNNs are a promising approach for mitigating the over-smoothing problem. We derive the optimization and generalization guarantees of transductive learning algorithms that include multi-scale GNNs.
  arXiv  Detail & Related papers  (2020-06-15T17:06:17Z)

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.