An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
This work addresses the problem of selecting effective formula encodings for researchers in automated theorem proving, providing empirical guidance for neural-guided approaches.
The paper compared pattern-based and graph-based embeddings for encoding logical formulas in automated theorem proving, finding that graph-based embeddings lead to more efficient search strategies and simpler proofs despite higher runtime costs.
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 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 the advantages of simpler encoding schemes in terms of runtime are outdone by more complex graph-based embeddings, which yield more efficient search strategies and simpler proofs. To support this, we present a detailed analysis across several dimensions of theorem prover performance beyond just proof completion rate, thus providing empirical evidence to help guide future research on neural-guided theorem proving towards the most promising directions.