An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
share
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.
READ FULL TEXT