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

要約

自動定理証明に強化学習を使用することは、最近大きな注目を集めています。
現在のアプローチでは、論理ステートメントの表現が使用されており、多くの場合、これらのステートメントで使用されている名前に依存しているため、モデルをあるドメインから別のドメインに転送することはできません。
これらの表現のサイズと、理論全体を含めるか、その一部を含めるかは、これらのアプローチのパフォーマンスと実行時の効率に影響を与える重要な決定です。
この論文では、NIAGRA について紹介します。
InvAriant Graph RepresentAtion というアンサンブル名。
NIAGRA は、1) 固有の特性に合わせて調整された名前不変式表現を学習するための改良されたグラフ ニューラル ネットワーク、2) 自動化された定理証明のための効率的なアンサンブル アプローチを使用することで、この問題に対処します。
私たちの実験的評価では、さまざまなドメインの複数のデータセットで最先端のパフォーマンスが得られ、最良の学習ベースのアプローチと比較して最大 10% の改善が見られました。
さらに、転移学習の実験では、私たちのアプローチが他の学習ベースのアプローチを最大 28% 大幅に上回ることが示されています。

要約(オリジナル)

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

arxiv情報

提供元, 利用サービス

arxiv.jp, Google