LEGO-Prover : Preuve de théorèmes neuronale avec des bibliothèques évolutives

Malgré les succès des grands modèles linguistiques (LLM), la preuve de théorèmes demeure l’une des tâches de raisonnement les plus difficiles, loin d’être entièrement résolue. Les méthodes antérieures basées sur les modèles linguistiques ont montré des résultats prometteurs, mais elles peinent encore à démontrer des théorèmes de niveau collège. Une limitation courante de ces approches réside dans l’hypothèse d’une bibliothèque de théorèmes fixe tout au long du processus de preuve. Or, comme nous le savons, la création de nouveaux théorèmes utiles, voire de nouvelles théories, n’est pas seulement bénéfique, mais essentielle et nécessaire pour faire progresser les mathématiques et prouver des résultats plus complexes et profonds. Dans ce travail, nous proposons LEGO-Prover, un système qui exploite une bibliothèque de compétences évolutives contenant des lemmes vérifiés, afin d’améliorer les capacités des LLM dans la preuve de théorèmes. En construisant les preuves de manière modulaire, LEGO-Prover permet aux LLM d’utiliser des compétences existantes extraites de la bibliothèque, tout en permettant la création de nouvelles compétences pendant le processus de preuve. Ces compétences sont ensuite enrichies par une phase d’évolution (via une nouvelle stimulation d’un LLM), ce qui permet d’enrichir la bibliothèque à une échelle plus large. Des compétences modulaires et réutilisables sont continuellement ajoutées à la bibliothèque, permettant ainsi de relever des problèmes mathématiques de plus en plus complexes. De plus, la bibliothèque apprise réduit efficacement l’écart entre les preuves humaines et les preuves formelles, en facilitant l’identification des étapes manquantes. LEGO-Prover améliore l’état de l’art en matière de taux de réussite sur miniF2F-valid (passant de 48,0 % à 57,0 %) et miniF2F-test (passant de 45,5 % à 47,1 %). Pendant le processus de preuve, LEGO-Prover parvient à générer plus de 20 000 compétences (théorèmes/lemmes) et à les intégrer à la bibliothèque en croissance. Une étude d’ablation montre que ces compétences nouvellement ajoutées sont effectivement utiles pour prouver des théorèmes, entraînant une amélioration du taux de réussite de 47,1 % à 50,4 %. Nous mettons également à disposition notre code source ainsi que l’ensemble des compétences générées.