Recherche de preuve HyperTree pour la démonstration de théorèmes neuronale

Nous proposons une procédure d'apprentissage en ligne pour un prouveur automatique de théorèmes basé sur les transformateurs. Notre approche exploite un nouvel algorithme de recherche, appelé HyperTree Proof Search (HTPS), inspiré du succès récent d'AlphaZero. Notre modèle apprend à partir de recherches de preuves antérieures grâce à un apprentissage en ligne, ce qui lui permet de généraliser à des domaines éloignés de la distribution d'apprentissage. Nous présentons des ablations détaillées des composants principaux de notre chaîne de traitement, en évaluant les performances sur trois environnements de complexité croissante. En particulier, nous montrons qu’avec HTPS seul, un modèle entraîné sur des preuves annotées parvient à prouver 65,4 % d’un ensemble de théorèmes Metamath non vu, ce qui représente une amélioration significative par rapport à l’état de l’art précédent de 56,5 % atteint par GPT-f. L’apprentissage en ligne sur ces théorèmes non prouvés permet d’atteindre une précision de 82,6 %. Avec un budget computationnel similaire, nous améliorons l’état de l’art sur le jeu de données miniF2F basé sur Lean, passant de 31 % à 42 % de taux de preuve réussie.