NuminaMath-LEAN ist ein mathematischer Problemdatensatz, der 2025 gemeinsam von Numina und dem Kimi-Team veröffentlicht wurde. Die zugehörigen Papierergebnisse sind „Kimina-Prover-Vorschau: Auf dem Weg zu großen formalen Argumentationsmodellen mit bestärkendem Lernen“, dessen Ziel darin besteht, manuell annotierte formale Aussagen und Beweise für das Training und die Evaluierung automatisierter Theorembeweismodelle bereitzustellen. Dieser Datensatz enthält 100.000 Mathematikwettbewerbsaufgaben, darunter auch Aufgaben aus renommierten Wettbewerben wie der Internationalen Mathematik-Olympiade (IMO) und der US-amerikanischen Mathematik-Olympiade (USAMO). Die Datentypen umfassen Problemstellungen, Fragetypklassifizierungen, Antworten, Quellen, formale Beweise, Anmerkungsinformationen und Aufzeichnungen des Trainingsprozesses für bestärkendes Lernen.

Zitat

@article{kimina_prover_2025, Titel = {Kimina-Prover Vorschau: Auf dem Weg zu großen formalen Schlussfolgerungsmodellen mit Reinforcement Learning}, Autor = {Wang, Haiming und Unsal, Mert und Lin, Xiaohan und Baksys, Mantas und Liu, Junqi und Santos, Marco Dos und Sung, Flood und Vinyes, Marina und Ying, Zhenzhe und Zhu, Zekai und Lu, Jianqiao und Saxcé, Hugues de und Bailey, Bolton und Song, Chendong und Xiao, Chenjun und Zhang, Dehao und Zhang, Ebony und Pu, Frederick und Zhu, Han und Liu, Jiawei und Bayer, Jonas und Michel, Julien und Yu, Longhui und Dreyfus-Schmidt, Léo und Tunstall, Lewis und Pagani, Luigi und Machado, Moreira und Bourigault, Pauline und Wang, Ran und Polu, Stanislas und Barroyer, Thibaut und Li, Wen-Ding und Niu, Yazhe und Fleureau, Yann und Hu, Yangyang und Yu, Zhouliang und Wang, Zihan und Yang, Zhilin und Liu, Zhengying und Li, Jia}, Jahr = {2025}, url = {http://arxiv.org/abs/2504.11354}, }