An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations

التفاصيل البيبلوغرافية
العنوان: An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations
المؤلفون: Fokoue, Achille, Abdelaziz, Ibrahim, Crouse, Maxwell, Ikbal, Shajith, Kishimoto, Akihiro, Lima, Guilherme, Makondo, Ndivhuwo, Marinescu, Radu
سنة النشر: 2023
المجموعة: Computer Science
مصطلحات موضوعية: Computer Science - Artificial Intelligence, Computer Science - Logic in Computer Science
الوصف: 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%.
Comment: Accepted to IJCAI 2023
نوع الوثيقة: Working Paper
URL الوصول: http://arxiv.org/abs/2305.08676
رقم الأكسشن: edsarx.2305.08676
قاعدة البيانات: arXiv