An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic

Automated theorem proving in first-order logic is an active research area which is successfully supported by machine learning. While there have been various proposals for encoding logical formulas into numerical vectors -- from simple strings to much more involved graph-based embeddings --, little is known about how these different encodings compare. In this paper, we study and experimentally compare pattern-based embeddings that are applied in current systems with popular graph-based encodings, most of which have not been considered in the theorem proving context before. Our experiments show that some graph-based encodings help finding much shorter proofs and may yield better performance in terms of number of completed proofs. However, as expected, a detailed analysis shows the trade-offs in terms of runtime.