La démonstration de théorèmes en mathématiques est de plus en plus complexe, posant des défis croissants. Des systèmes formalisés comme Lean, Isabelle et Coq permettent des preuves vérifiables par ordinateur, mais leur création nécessite un effort humain considérable. Les grands modèles de langage (LLM) montrent des promesses en résolvant des problèmes de mathématiques de niveau secondaire à l’aide d’assistants de preuve, mais leurs performances demeurent insuffisantes en raison de la rareté des données. Contrairement aux langages de programmation traditionnels, les langages de preuve formelle contiennent des informations intermédiaires cachées, rendant les corpus bruts inutilisables pour l’entraînement. Les efforts d’auto-formalisation, bien que bénéfiques, ne peuvent remplacer totalement les données créées par les humains en termes de qualité et de diversité.
Des tentatives modernes utilisent des assistants de preuve comme Coq, Isabelle, et Lean, avec une expansion significative au-delà de la logique de premier ordre, augmentant ainsi l’intérêt pour la démonstration de théorèmes automatisée (ATP). L’intégration récente de modèles de langue a encore fait progresser ce domaine. Par exemple, des systèmes comme GPT-f et PACT entraînent des modèles linguistiques sur des paires d’états de preuve et de tactiques suivantes, utilisant la recherche arborescente pour prouver des théorèmes.
Des chercheurs de l’Université Chinoise de Hong Kong proposent LEAN-GitHub, un vaste ensemble de données Lean complétant le dataset Mathlib largement utilisé. Ce projet innovant fournit des dépôts Lean open-source sur GitHub, élargissant considérablement les données disponibles pour l’entraînement de modèles de preuve de théorèmes. Ils ont développé un pipeline évolutif pour améliorer l’efficacité de l’extraction de données, exploitant des corpus non compilés et non extraits auparavant.
Le processus de construction du dataset LEAN-GitHub comprend plusieurs étapes :
– Sélection de 237 dépôts Lean 4 sur GitHub, aboutissant à environ 48 091 théorèmes, et compilation réussie de 61 dépôts sans modifications.
– Développement de scripts automatiques pour trouver les versions officielles les plus proches pour les projets utilisant des versions non officielles de Lean 4.
– Compilation directe avec le compilateur Lean, contournant les limites de l’outil Lake pour les projets et fichiers isolés non conformes.
– Extraction des données, restructuration pour augmenter le parallélisme et surmonter les goulots d’étranglement liés aux connexions réseau et aux redondances computationnelles.
LEAN-GitHub couvre divers domaines mathématiques, incluant la logique, la théorie des matroïdes, et l’arithmétique. Le modèle InternLM2-StepProver, entraîné sur ce dataset, démontre d’excellentes capacités de raisonnement formel, surpassant les performances de modèles précédents sur divers benchmarks. Cela montre l’efficacité du dataset LEAN-GitHub pour l’amélioration de la démonstration automatisée de théorèmes et des mathématiques formelles.