HOList : Un Environnement pour l'Apprentissage Automatique de la Démonstration de Théorèmes d'Ordre Supérieur

Nous présentons un environnement, un benchmark et un démonstrateur de théorèmes automatisé basé sur l'apprentissage profond pour la logique d'ordre supérieur. Les démonstrateurs de théorèmes interactifs d'ordre supérieur permettent la formalisation de théories mathématiques arbitraires, ce qui constitue un défi intéressant et ouvert pour l'apprentissage profond. Nous fournissons un cadre open-source basé sur le démonstrateur de théorèmes HOL Light qui peut être utilisé comme environnement d'apprentissage par renforcement. HOL Light couvre une large gamme de théorèmes mathématiques fondamentaux sur le calcul et la preuve formelle de la conjecture de Kepler, à partir desquels nous avons établi un benchmark exigeant pour le raisonnement automatisé. Nous présentons également DeepHOL, un démonstrateur de théorèmes automatisé piloté par l'apprentissage profond par renforcement, avec des résultats initiaux prometteurs sur ce benchmark.