NuminaMath-LEANは、NuminaとKimiチームが2025年に共同でリリースした数学の問題データセットです。関連する論文結果は「Kimina-Prover プレビュー: 強化学習を用いた大規模形式推論モデルの構築に向けて」は、自動定理証明モデルのトレーニングと評価のために、手動で注釈が付けられた正式なステートメントと証明を提供することを目的としています。 このデータセットには、国際数学オリンピック（IMO）や米国数学オリンピック（USAMO）といった権威ある大会のものを含む、10万問の数学競技問題が含まれています。データの種類には、問題文、問題種別、解答、出典、正式な証明、注釈情報、強化学習の学習プロセス記録などが含まれます。

引用

@article{kimina_prover_2025, タイトル = {Kimina-Prover プレビュー: 強化学習を用いた大規模形式推論モデルに向けて}, 著者 = {Wang, Haiming および Unsal, Mert および Lin, Xiaohan および Baksys, Mantas および Liu, Junqi および Santos, Marco Dos および Sung, Flood および Vinyes, Marina および Ying, Zhenzhe および Zhu, Zekai および Lu, Jianqiao および Saxcé, Hugues de および Bailey, Bolton および Song, Chendong および Xiao, Chenjun および Zhang, Dehao および Zhang, Ebony および Pu, Frederick および Zhu, Han および Liu, Jiawei および Bayer, Jonas および Michel, Julien および Yu, Longhui および Dreyfus-Schmidt, Léo および Tunstall, Lewis および Pagani, Luigi および Machado, Moreira および Bourigault, Pauline および Wang, Ran および Polu, Stanislas および Barroyer, Thibaut および Li, Wen-Ding および Niu, Yazhe およびフルロー、ヤンと胡、襄陽と余、周良と王、紫漢と楊、志林と劉、正英と李、賈}、 年 = {2025}、 url = {http://arxiv.org/abs/2504.11354}, }