SubgoalXL : Apprentissage d'experts basé sur des sous-objectifs pour la démonstration de théorèmes

La démonstration formelle de théorèmes, un domaine à l'intersection des mathématiques et de l'informatique, a connu un regain d'intérêt grâce aux progrès réalisés dans les grands modèles linguistiques (LLMs). Cet article présente SubgoalXL, une nouvelle approche qui combine les preuves basées sur des sous-objectifs avec l'apprentissage par des experts pour améliorer les capacités des LLMs en démonstration formelle de théorèmes dans l'environnement Isabelle. SubgoalXL aborde deux défis cruciaux : la rareté de données spécialisées en mathématiques et en démonstration de théorèmes, et le besoin d'améliorer les capacités de raisonnement en plusieurs étapes des LLMs. En optimisant l'efficacité des données et en utilisant une supervision au niveau des sous-objectifs, SubgoalXL extrait des informations plus riches à partir de preuves générées par des humains limitées. Le cadre intègre des stratégies de preuve orientées vers les sous-objectifs avec un système d'apprentissage par des experts, affinant itérativement les générateurs de déclarations formelles, de preuves et de sous-objectifs. En tirant parti des avantages de l'environnement Isabelle pour les preuves basées sur des sous-objectifs, SubgoalXL atteint une nouvelle performance record de 56,1 % sur le jeu de données standard miniF2F dans Isabelle, marquant une amélioration absolue de 4,9 %. Notamment, SubgoalXL résout avec succès 41 problèmes AMC12, 9 problèmes AIME et 3 problèmes IMO du jeu de données miniF2F. Ces résultats soulignent l'efficacité maximale de l'utilisation de données limitées et l'emploi d'une guidance ciblée pour le raisonnement complexe en démonstration formelle, contribuant ainsi à l'avancement continu des capacités de raisonnement artificiel. L'implémentation est disponible à l'adresse \url{https://github.com/zhaoxlpku/SubgoalXL}.