Inter-GPS : Résolution Interprétable de Problèmes Géométriques avec un Langage Formel et une Raisonnement Symbolique

La résolution de problèmes géométriques a récemment attiré beaucoup d'attention dans la communauté de traitement automatique du langage naturel (TALN). Cette tâche est particulièrement complexe car elle nécessite une compréhension abstraite des problèmes et un raisonnement symbolique basé sur des connaissances axiomatiques. Cependant, les jeux de données actuels sont soit de petite taille, soit non disponibles publiquement. Ainsi, nous avons construit un nouveau benchmark à grande échelle, Geometry3K, composé de 3 002 problèmes géométriques avec une annotation dense en langage formel. Nous proposons également une nouvelle approche de résolution de problèmes géométriques utilisant le langage formel et le raisonnement symbolique, appelée Interpretable Geometry Problem Solver (Inter-GPS). Inter-GPS analyse d'abord le texte du problème et le diagramme en langage formel automatiquement, par le biais d'un analyseur textuel basé sur des règles et d'une détection d'objets neuronale, respectivement. Contrairement à l'apprentissage implicite des méthodes existantes, Inter-GPS intègre les connaissances théoriques sous forme de règles conditionnelles et effectue un raisonnement symbolique étape par étape. De plus, un prédicteur de théorème est conçu pour inférer la séquence d'application des théorèmes fournie au solveur symbolique, afin d'optimiser et rationaliser la recherche. Des expériences étendues sur les jeux de données Geometry3K et GEOS montrent que Inter-GPS réalise des améliorations significatives par rapport aux méthodes existantes. Le projet, incluant le code et les données, est disponible à l'adresse https://lupantech.github.io/inter-gps.