Thor : Utiliser des marteaux pour intégrer des Modèles de Langage et des Démonstrateurs Automatisés de Théorèmes

Dans la preuve de théorèmes, la sélection de prémisses utiles parmi une vaste bibliothèque afin de débloquer la preuve d'une conjecture donnée est une tâche cruciale. Ce défi est particulièrement prononcé pour tous les prouveurs automatiques, notamment ceux fondés sur des modèles linguistiques, en raison de leur capacité limitée à raisonner sur de grandes quantités de prémisses présentées sous forme textuelle. Ce papier présente Thor, un cadre intégrant des modèles linguistiques et des prouveurs automatiques de théorèmes afin de surmonter cette difficulté. Dans Thor, une catégorie de méthodes appelées « hammers », qui exploitent la puissance des prouveurs automatiques, est utilisée pour la sélection de prémisses, tandis que toutes les autres tâches sont attribuées aux modèles linguistiques. Thor améliore le taux de réussite d’un modèle linguistique sur le jeu de données PISA de 39 % à 57 %, tout en résolvant 8,2 % des problèmes que ni les modèles linguistiques ni les prouveurs automatiques ne parviennent à résoudre seuls. De plus, avec un budget computationnel nettement réduit, Thor atteint un taux de réussite sur le jeu de données MiniF2F équivalent à celui des meilleures méthodes existantes. Thor peut être facilement instancié pour la majorité des prouveurs interactifs populaires grâce au protocole simple que nous proposons.