論理式のグラフニューラルネットワーク表現を部分グラフプーリングを用いて改善する

深層学習と自動定理証明の統合に関する最近の進展は、論理式を深層学習システムへの入力として表現することに焦点を当てている。特に、論理式の下位構造をグラフ表現として扱うことに適応可能な構造認識型ニューラル手法への関心が高まっている。従来の文字レベルおよびトークンレベルのアプローチに比べて効果的であるものの、グラフベースの手法はしばしば入力の重要な構造的性質を捉えきれないという表現上の妥協を強いられてきた。本研究では、こうした先行手法の表現上の制約を克服することを目的として、論理式を埋め込むための新しいアプローチを提案する。本手法のアーキテクチャは、一階論理や高階論理など、異なる表現力を持つ論理体系に対応可能である。標準的な2つのデータセットを用いた実験において、提案手法が前提選択および証明ステップ分類の両タスクで、現行の最先端性能を達成することを示した。