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%.

翻译：近期，利用强化学习进行自动定理证明的方法备受关注。现有方法常使用依赖逻辑语句中名称的表示形式，导致模型通常无法跨领域迁移。这些表示的规模以及是否包含完整理论或部分理论，也是影响方法性能及运行时效率的重要决策。本文提出NIAGRA——一种集成式名称不变图表示（Name InvAriant Graph RepresentAtion）。NIAGRA通过以下策略解决上述问题：1）改进图神经网络，针对公式的特性学习名称不变的表示；2）提出高效的集成方法用于自动定理证明。实验评估表明，在来自不同领域的多个数据集上，本方法取得当前最优性能，相比最佳学习方法提升高达10%。此外，迁移学习实验显示，本方法显著优于其他学习方法，性能提升幅度达28%。