NuminaMath-LEAN est un ensemble de données de problèmes mathématiques publié conjointement par Numina et Kimi Team en 2025. Les résultats de l'article associé sont «Aperçu de Kimina-Prover : Vers de grands modèles de raisonnement formel avec apprentissage par renforcement", qui vise à fournir des énoncés formels et des preuves annotés manuellement pour la formation et l'évaluation de modèles automatisés de démonstration de théorèmes. Cet ensemble de données contient 100 000 problèmes de compétitions mathématiques, dont ceux issus de compétitions de référence telles que l'Olympiade internationale de mathématiques (IMO) et l'Olympiade américaine de mathématiques (USAMO). Les types de données incluent les énoncés de problèmes, les classifications des types de questions, les réponses, les sources, les preuves formelles, les informations des annotateurs et les enregistrements des processus d'apprentissage par renforcement.

Citation

@article{kimina_prover_2025, titre = {Aperçu de Kimina-Prover : Vers de grands modèles de raisonnement formel avec apprentissage par renforcement}, auteur = {Wang, Haiming et Unsal, Mert et Lin, Xiaohan et Baksys, Mantas et Liu, Junqi et Santos, Marco Dos et Sung, Flood et Vinyes, Marina et Ying, Zhenzhe et Zhu, Zekai et Lu, Jianqiao et Saxcé, Hugues de et Bailey, Bolton et Song, Chendong et Xiao, Chenjun et Zhang, Dehao et Zhang, Ebony et Pu, Frederick et Zhu, Han et Liu, Jiawei et Bayer, Jonas et Michel, Julien et Yu, Longhui et Dreyfus-Schmidt, Léo et Tunstall, Lewis et Pagani, Luigi et Machado, Moreira et Bourigault, Pauline et Wang, Ran et Polu, Stanislas et Barroyer, Thibaut et Li, Wen-Ding et Niu, Yazhe et Fleureau, Yann et Hu, Yangyang et Yu, Zhouliang et Wang, Zihan et Yang, Zhilin et Liu, Zhengying et Li, Jia}, année = {2025}, url = {http://arxiv.org/abs/2504.11354}, }