Sélection de prémisses pour la démonstration de théorèmes par plongement profond de graphes

Nous proposons une approche basée sur l'apprentissage profond pour le problème de sélection des prémisses : choisir les énoncés mathématiques pertinents pour prouver une conjecture donnée. Nous représentons une formule de logique d'ordre supérieur sous forme de graphe, qui est invariante par rapport au renommage des variables mais préserve néanmoins pleinement les informations syntaxiques et sémantiques. Nous plongeons ensuite ce graphe dans un vecteur grâce à une méthode de plongement novatrice qui conserve l'information de l'ordre des arêtes. Notre approche obtient des résultats d'état de l'art sur le jeu de données HolStep, améliorant la précision de classification de 83% à 90,3%.