Représentations graphiques pour la logique d'ordre supérieur et la démonstration de théorèmes

Ce document présente l'utilisation initiale des réseaux neuronaux de graphe (GNNs) pour la recherche de preuves d'ordre supérieur et démontre que les GNNs peuvent améliorer les résultats les plus avancés dans ce domaine. Les démonstrateurs interactifs de théorèmes d'ordre supérieur permettent la formalisation de la plupart des théories mathématiques et ont été montrés comme posant un défi considérable pour l'apprentissage profond. La logique d'ordre supérieur est très expressive et, bien qu'elle soit bien structurée avec une grammaire et une sémantique clairement définies, il n'existe toujours aucune méthode établie pour convertir les formules en représentations basées sur des graphes. Dans cet article, nous examinons plusieurs représentations graphiques de la logique d'ordre supérieur et les évaluons à l'aide du banc d'essai HOList pour la démonstration de théorèmes d'ordre supérieur.