DeepTheorem : Faire progresser le raisonnement des LLM pour la démonstration de théorèmes grâce au traitement du langage naturel et à l'apprentissage par renforcement

DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning

May 29, 2025

Auteurs: Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhengwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, Dong Yu

cs.AI

Résumé

La démonstration de théorèmes constitue un banc d'essai majeur pour évaluer les capacités de raisonnement complexe des grands modèles de langage (LLM). Cependant, les approches traditionnelles de démonstration automatique de théorèmes (ATP) reposent fortement sur des systèmes de preuve formels qui s'alignent mal avec la force des LLM, issue des connaissances informelles en langage naturel acquises lors du pré-entraînement. Dans ce travail, nous proposons DeepTheorem, un cadre complet de démonstration informelle de théorèmes exploitant le langage naturel pour améliorer le raisonnement mathématique des LLM. DeepTheorem inclut un jeu de données de référence à grande échelle composé de 121 000 théorèmes et preuves informels de niveau Olympiade Internationale de Mathématiques (IMO), couvrant divers domaines mathématiques, rigoureusement annotés pour leur exactitude, leur difficulté et leurs catégories thématiques, accompagnés de variantes de théorèmes systématiquement construites et vérifiables. Nous concevons une nouvelle stratégie d'apprentissage par renforcement (RL-Zero) explicitement adaptée à la démonstration informelle de théorèmes, exploitant les variantes vérifiées pour inciter une inférence mathématique robuste. De plus, nous proposons des métriques d'évaluation complètes des résultats et du processus, examinant l'exactitude des preuves et la qualité des étapes de raisonnement. Des analyses expérimentales approfondies démontrent que DeepTheorem améliore significativement les performances des LLM en démonstration de théorèmes par rapport aux jeux de données existants et aux protocoles de fine-tuning supervisé, atteignant une précision et une qualité de raisonnement de pointe. Nos résultats mettent en lumière le potentiel de DeepTheorem à faire progresser fondamentalement la démonstration automatique informelle de théorèmes et l'exploration mathématique.

English

Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems that poorly align with LLMs' strength derived from informal, natural language knowledge acquired during pre-training. In this work, we propose DeepTheorem, a comprehensive informal theorem-proving framework exploiting natural language to enhance LLM mathematical reasoning. DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs spanning diverse mathematical domains, rigorously annotated for correctness, difficulty, and topic categories, accompanied by systematically constructed verifiable theorem variants. We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference. Additionally, we propose comprehensive outcome and process evaluation metrics examining proof correctness and the quality of reasoning steps. Extensive experimental analyses demonstrate DeepTheorem significantly improves LLM theorem-proving performance compared to existing datasets and supervised fine-tuning protocols, achieving state-of-the-art accuracy and reasoning quality. Our findings highlight DeepTheorem's potential to fundamentally advance automated informal theorem proving and mathematical exploration.