NuminaMath-LEAN은 Numina와 Kimi 팀이 2025년에 공동으로 발표한 수학 문제 데이터 세트입니다. 관련 논문 결과는 다음과 같습니다.Kimina-Prover 미리보기: 강화 학습을 통한 대규모 형식 추론 모델 구축"는 자동화된 정리 증명 모델의 훈련과 평가를 위해 수동으로 주석이 달린 공식적인 진술과 증명을 제공하는 것을 목표로 합니다. 이 데이터셋에는 국제수학올림피아드(IMO) 및 미국수학올림피아드(USAMO)와 같은 권위 있는 대회의 문제를 포함하여 10만 개의 수학 경시대회 문제가 포함되어 있습니다. 데이터 유형에는 문제 진술, 문제 유형 분류, 정답, 출처, 정형 증명, 주석자 정보, 강화 학습 학습 과정 기록 등이 포함됩니다.

소환

@article{kimina_prover_2025, 제목 = {Kimina-Prover 미리보기: 강화 학습을 활용한 대규모 형식 추론 모델 개발} 저자 = {Wang, Haiming and Unsal, Mert and Lin, Xiaohan and Baksys, Mantas and Liu, Junqi and Santos, Marco Dos and Sung, Flood and Vinyes, Marina and Ying, Zhenzhe and Zhu, Zekai and Lu, Jianqiao and Saxcé, Hugues de and Bailey, Bolton and Song, Chendong and Xiao, Chenjun and Zhang, Dehao and Zhang, Ebony and Pu, Frederick and Zhu, Han and Liu, Jiawei and Bayer, Jonas and Michel, Julien and Yu, Longhui and Dreyfus-Schmidt, Léo and Tunstall, Lewis and Pagani, Luigi and Machado, Moreira and Bourigault, Pauline and Wang, Ran and Polu, Stanislas and Barroyer, Thibaut and Li, Wen-Ding and Niu, Yazhe and Fleureau, Yann and Hu, Yangyang and Yu, Zhouliang} 및 Wang, Zihan 및 Yang, Zhilin 및 Liu, Zhengying 및 Li, Jia}, 연도 = {2025}, URL = {http://arxiv.org/abs/2504.11354}, }