An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations
This work solves the domain transfer and efficiency issues in automated theorem proving for AI researchers, though it is incremental as it builds on existing graph neural network methods.
The paper tackled the problem of automated theorem proving by addressing the lack of transferability and efficiency in current reinforcement learning approaches, resulting in state-of-the-art performance with up to 10% improvement on multiple datasets and up to 28% better transfer learning.
Using reinforcement learning for automated theorem proving has recently received much attention. Current approaches use representations of logical statements that often rely on the names used in these statements and, as a result, the models are generally not transferable from one domain to another. The size of these representations and whether to include the whole theory or part of it are other important decisions that affect the performance of these approaches as well as their runtime efficiency. In this paper, we present NIAGRA; an ensemble Name InvAriant Graph RepresentAtion. NIAGRA addresses this problem by using 1) improved Graph Neural Networks for learning name-invariant formula representations that is tailored for their unique characteristics and 2) an efficient ensemble approach for automated theorem proving. Our experimental evaluation shows state-of-the-art performance on multiple datasets from different domains with improvements up to 10% compared to the best learning-based approaches. Furthermore, transfer learning experiments show that our approach significantly outperforms other learning-based approaches by up to 28%.