Une avancée majeure dans le raisonnement mathématique utilise des langages formels vérifiables par ordinateur, comme Lean, pour prouver des théorèmes mathématiques, garantissant ainsi précision et cohérence. L’utilisation des modèles de langue étendus (LLM) formés sur des preuves en langage naturel (NL) pour produire des preuves formelles complètes est une méthode prometteuse pour prouver les théorèmes formels.
Néanmoins, l’absence de données alignées NL et FL pose souvent des obstacles à l’efficacité des LLM contemporains. Pour surmonter ces limitations, des chercheurs de l’Université des Sciences et Technologies de Hong Kong et de l’Université de l’Illinois Urbana-Champaign ont introduit TheoremLlama, une structure complète destinée à spécialiser un LLM polyvalent dans la preuve de théorèmes Lean4.
TheoremLlama comporte plusieurs éléments clés:
1. Génération d’un ensemble de données NL-FL aligné: Il utilise des techniques pour créer un ensemble de données aligné NL-FL, appelé Open Bootstrapped Theorems (OBT), en intégrant des preuves NL dans le code Lean4.
2. Formation formelle pour les prouveurs de théorèmes LLM: Le système applique de nouvelles stratégies de formation pour aider les LLM à devenir des prouveurs de théorèmes Lean4 efficaces.
3. Écriture de preuves Lean4 par LLM: Amélioration de la capacité du LLM à écrire des preuves formelles en Lean4 de manière autonome.
Les résultats expérimentaux démontrent l’efficacité de TheoremLlama, surpassant les résultats de base de GPT-4. En conclusion, TheoremLlama est une avancée significative utilisant les capacités linguistiques des LLM pour formaliser la preuve de théorèmes en Lean4.