DeepTheorem est un ensemble de données de raisonnement mathématique qui vise à améliorer les capacités de raisonnement mathématique des grands modèles de langage (LLM) grâce à la preuve informelle de théorèmes basée sur le langage naturel.

Cet ensemble de données contient 121 000 théorèmes et preuves informels de niveau IMO, couvrant plusieurs domaines mathématiques. Chaque paire théorème-preuve est rigoureusement annotée, comme suit :

• Preuves o3-mini : Les preuves générées ou vérifiées par le modèle o3-mini garantissent l'exactitude mathématique.
• Valeur de vérité : La valeur de vérité du théorème extraite de la preuve o3-mini, indiquant si le théorème est vrai ou faux.
• Difficulté : Catégorisé par complexité pour s'adapter à diverses capacités LLM.
• Catégories : Couvre l'algèbre, la géométrie, la théorie des nombres, etc.
• Variante : Une variante positive ou négative d'un théorème qui a la même valeur de vérité ou une valeur opposée à celle du théorème d'origine.