NuminaMath-LEAN 数学問題データセット

NuminaMath-LEANは、NuminaとKimiチームが2025年に共同でリリースした数学の問題データセットです。関連する論文結果は「Kimina-Prover プレビュー: 強化学習を用いた大規模形式推論モデルの構築に向けて」は、自動定理証明モデルのトレーニングと評価のために、手動で注釈が付けられた正式なステートメントと証明を提供することを目的としています。

このデータセットには、国際数学オリンピック（IMO）や米国数学オリンピック（USAMO）といった権威ある大会のものを含む、10万問の数学競技問題が含まれています。データの種類には、問題文、問題種別、解答、出典、正式な証明、注釈情報、強化学習の学習プロセス記録などが含まれます。