GNN, automated reasoning, neural networks

In this contribution, we will demonstrate how Graph Neural Networks (GNNs) can be utilized in the field of automated reasoning, specifically in theorem proving. Proving process can be viewed as a transition from one state to another. Logical formulae are transformed by applying specific and strictly given rules (or applying previously proven propositions). The goal is to find the chain of such formulae in which each formula is logically consequent to the previous one (by those rules). The last formula in that chain is the one to be proved. Such a chain is called a proof. We can see that graph-structure is inherent to the data connected to logical proofs. The whole process of proving may be seen as a walk through the graph whose nodes are particular expressions and edges are possible transitions. The agent performing the proof has to choose the correct sequence of steps. Logical formulae can also be parsed and encoded as a syntactic tree that is also a graph. Graph Neural Network is a strong tool that can be used to process various graph-structured data. For example, it can be used to encode nodes or whole graph by mapping them to real vectors. Those vectors offer other possibilities for processing (we can, for example, measure their similarity). We aim to explain how exactly GNNs can be incorporated in theorem proving, introduce existing frameworks and propose our future research in the area. Of course, the proving process as a whole is very complex and for that reason, it is convenient to find solutions to its sub-problems rather than whole proof. Those sub-problems include tasks like proof validation or premise selection. Our talk will be centered around those sub-problems.