DeepTheorem : Une Révolution dans le Raisonnement Mathématique des LLM grâce au Langage Naturel et au Reinforcement Learning
DeepTheorem marque une avancée majeure dans la démonstration de théorèmes par les modèles de langage (LLM) en combinant un jeu de données en langage naturel à grande échelle et une stratégie innovante de reinforcement learning. Ce cadre complet atteint des performances inégalées dans le domaine des preuves informelles de théorèmes.
La démonstration de théorèmes constitue un banc d'essai crucial pour évaluer les capacités de raisonnement complexe des LLM. Cependant, les approches traditionnelles (ATP) s'appuient sur des systèmes formels peu compatibles avec les forces des LLM, formés principalement sur des connaissances en langage naturel. DeepTheorem propose une solution à ce décalage.
Le système comprend un jeu de données exceptionnel de 121 000 théorèmes et preuves informels de niveau Olympiade Internationale de Mathématiques (IMO), couvrant divers domaines mathématiques. Chaque élément est annoté rigoureusement pour sa justesse, difficulté et catégorie, accompagné de variantes vérifiables systématiquement construites.
La pièce maîtresse de DeepTheorem est RL-Zero, une stratégie de reinforcement learning spécialement conçue pour les preuves informelles. Elle exploite les variantes de théorèmes pour renforcer l'inférence mathématique. Le cadre propose également des métriques d'évaluation complètes examinant tant la correction des preuves que la qualité des étapes de raisonnement.
Les résultats expérimentaux démontrent une amélioration significative des performances par rapport aux méthodes existantes. Le modèle 7B de DeepTheorem surpasse même des géants comme Gemini et Claude 3.5, sans nécessiter d'annotations de preuves - seule la valeur de vérité du théorème suffit.
Cette innovation ouvre de nouvelles perspectives pour l'exploration mathématique automatisée. Comme le souligne l'équipe : "L'apprentissage par exploration booste considérablement l'utilisation des connaissances acquises en pré-entraînement par les LLM". DeepTheorem prouve ainsi qu'une combinaison judicieuse de données qualité et de reinforcement learning peut révéler le plein potentiel des LLM en raisonnement mathématique.
