A Study of Continuous Vector Representationsfor Theorem Proving

• URL: http://arxiv.org/abs/2101.09142v1
• Date: Fri, 22 Jan 2021 15:04:54 GMT
• Title: A Study of Continuous Vector Representationsfor Theorem Proving
• Authors: Stanis{\l}aw Purga{\l}, Julian Parsert, Cezary Kaliszyk
• Abstract summary: We develop an encoding that allows for logical properties to be preserved and is additionally reversible. This means that the tree shape of a formula including all symbols can be reconstructed from the dense vector representation. We propose datasets that can be used to train these syntactic and semantic properties.
• Score: 2.0518509649405106
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Applying machine learning to mathematical terms and formulas requires a suitable representation of formulas that is adequate for AI methods. In this paper, we develop an encoding that allows for logical properties to be preserved and is additionally reversible. This means that the tree shape of a formula including all symbols can be reconstructed from the dense vector representation. We do that by training two decoders: one that extracts the top symbol of the tree and one that extracts embedding vectors of subtrees. The syntactic and semantic logical properties that we aim to reserve include both structural formula properties, applicability of natural deduction steps, and even more complex operations like unifiability. We propose datasets that can be used to train these syntactic and semantic properties. We evaluate the viability of the developed encoding across the proposed datasets as well as for the practical theorem proving problem of premise selection in the Mizar corpus.

Related papers

• stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic [0.5956301166481089]
  We propose a semantically grounded vector representation (feature embedding) of logic formulae. We compute continuous embeddings of formulae with several desirable properties. We demonstrate the efficacy of the approach in two tasks: learning model checking and neurosymbolic framework.
  arXiv  Detail & Related papers  (2024-05-23T10:04:56Z)
• A Recursive Bateson-Inspired Model for the Generation of Semantic Formal Concepts from Spatial Sensory Data [77.34726150561087]
  This paper presents a new symbolic-only method for the generation of hierarchical concept structures from complex sensory data. The approach is based on Bateson's notion of difference as the key to the genesis of an idea or a concept. The model is able to produce fairly rich yet human-readable conceptual representations without training.
  arXiv  Detail & Related papers  (2023-07-16T15:59:13Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  We propose a structure-modeled textual encoding framework for inductive logical reasoning over KGs. It encodes linearized query structures and entities using pre-trained language models to find answers. We conduct experiments on two inductive logical reasoning datasets and three transductive datasets.
  arXiv  Detail & Related papers  (2023-05-23T01:25:29Z)
• Data-driven abstractions via adaptive refinements and a Kantorovich metric [extended version] [56.94699829208978]
  We introduce an adaptive refinement procedure for smart, and scalable abstraction of dynamical systems. In order to learn the optimal structure, we define a Kantorovich-inspired metric between Markov chains. We show that our method yields a much better computational complexity than using classical linear programming techniques.
  arXiv  Detail & Related papers  (2023-03-30T11:26:40Z)
• The Many-Worlds Calculus [0.0]
  We propose a colored PROP to model computation in this framework. The model can support regular tests, probabilistic and non-deterministic branching, as well as quantum branching. We prove the language to be universal, and the equational theory to be complete with respect to this semantics.
  arXiv  Detail & Related papers  (2022-06-21T10:10:26Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  This thesis serves as a means of transforming the semantics of a modal and/or constructive logic into an 'economical' proof system. The refinement method connects two proof-theoretic paradigms: labelled and nested sequent calculi. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics.
  arXiv  Detail & Related papers  (2021-07-30T08:27:15Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jl is an extendable symbolic system which uses dynamic multiple dispatch to change behavior depending on the domain needs. We show that by formalizing a generic API on actions independent of implementation, we can retroactively add optimized data structures to our system. We demonstrate the ability to swap between classical term-rewriting simplifiers and e-graph-based term-rewriting simplifiers.
  arXiv  Detail & Related papers  (2021-05-09T14:22:43Z)
• Abelian Neural Networks [48.52497085313911]
  We first construct a neural network architecture for Abelian group operations and derive a universal approximation property. We extend it to Abelian semigroup operations using the characterization of associative symmetrics. We train our models over fixed word embeddings and demonstrate improved performance over the original word2vec.
  arXiv  Detail & Related papers  (2021-02-24T11:52:21Z)
• Building powerful and equivariant graph neural networks with structural message-passing [74.93169425144755]
  We propose a powerful and equivariant message-passing framework based on two ideas. First, we propagate a one-hot encoding of the nodes, in addition to the features, in order to learn a local context matrix around each node. Second, we propose methods for the parametrization of the message and update functions that ensure permutation equivariance.
  arXiv  Detail & Related papers  (2020-06-26T17:15:16Z)
• Lattice Representation Learning [6.427169570069738]
  We introduce theory and algorithms for learning discrete representations that take on a lattice that is embedded in an Euclidean space. Lattice representations possess an interesting combination of properties: a) they can be computed explicitly using lattice quantization, yet they can be learned efficiently using the ideas we introduce. This article will focus on laying the groundwork for exploring and exploiting the first two properties, including a new mathematical result linking expressions used during training and inference time and experimental validation on two popular datasets.
  arXiv  Detail & Related papers  (2020-06-24T16:05:11Z)

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.