高次論理と定理証明のためのグラフ表現

本論文では、グラフニューラルネットワーク（GNNs）を高階証明探索に初めて適用し、この分野における最先端の結果を改善できることが示されています。インタラクティブな高階定理証明器は、ほとんどの数学理論の形式化を可能とし、深層学習にとって大きな挑戦であることが示されています。高階論理は非常に表現力が高く、明確に定義された文法と意味論を持つにもかかわらず、公式をグラフベースの表現に変換する確立された方法はありません。本論文では、高階論理のいくつかのグラフィカルな表現を検討し、それらを高階定理証明のためのHOListベンチマークに対して評価しています。