An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
By Ibrahim Abdelaziz, Veronika Thost, Maxwell Crouse, Achille Fokoue. 2020
6 citations recorded by the source corpus.
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.
Subfields: Artificial Intelligence, Information Systems, Representation & Self-Supervised Learning, Knowledge Graphs & Representation, Automated Theorem Proving & Formal Methods
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Swarnadeep Saha
- Mohit Bansal
- Shashank Srivastava
- Sayan Ghosh
- Caiming Xiong
- Jianfeng Gao
- Hannaneh Hajishirzi
- Luke S. Zettlemoyer
In Information Systems
In Representation & Self-Supervised Learning
- Mohit Bansal
- Shashank Srivastava
- Swarnadeep Saha
- John Wieting
- Zhe Gan
- Kevin Gimpel
- Jianfeng Gao
- Jaemin Cho
In Knowledge Graphs & Representation
Citations in the corpus
- PRover: Proof Generation for Interpretable Reasoning over Rules (2020, methodology): “, 2019), formula embedding (Abdelaziz et al., 2020), approximate (DNF) model counting (Abboud et al.”
- On the Paradox of Learning to Reason from Data (2022, unknown): “…maxSAT (Wang et al., 2019), temporal logical problems (Hahn et al., 2021), DNF counting (Crouse et al., 2019), logical reasoning by learning the embedding of logical formula (Crouse et al., 2019; Abdelaziz et al., 2020) and mathematical problems (Saxton et al., 2019; Lample and Charton, 2020).”