NuminaMath-LEAN هي مجموعة بيانات لمشكلات رياضية تم إصدارها بشكل مشترك من قبل Numina وفريق Kimi في عام 2025. نتائج الورقة ذات الصلة هي "معاينة كيمينا-بروفر: نحو نماذج استدلال شكلية كبيرة مع التعلم التعزيزي"، والذي يهدف إلى توفير عبارات رسمية موضحة يدويًا وإثباتات لتدريب وتقييم نماذج إثبات النظرية الآلية. تحتوي هذه المجموعة من البيانات على 100,000 مسألة رياضية، بما في ذلك مسائل من مسابقات معتمدة مثل أولمبياد الرياضيات الدولي (IMO) وأولمبياد الرياضيات الأمريكي (USAMO). تتضمن أنواع البيانات عبارات المسائل، وتصنيفات أنواع الأسئلة، والإجابات، والمصادر، والبراهين الرسمية، ومعلومات المُعلّق، وسجلات عملية تدريب التعلم المُعزّز.

الاستشهاد

@article{kimina_prover_2025, العنوان = {معاينة Kimina-Prover: نحو نماذج استدلال رسمية كبيرة باستخدام التعلم المعزز}, المؤلف = {وانغ، هايمينغ وأونصال، ميرت ولين، شياوهان وباكسيس، مانتاس وليو، جونكي وسانتوس، ماركو دوس وسونغ، فلود وفينيس، مارينا ويينغ، تشنزه وتشو، زيكاي ولو، جيانكياو وساكسي، هيوز دي وبيلي، بولتون وسونغ، تشيندونغ وشياو، تشنججون وتشانغ، ديهاو وتشانغ، إيبوني وبو، فريدريك وتشو، هان وليو، جياوي وباير، جوناس وميشيل، جوليان ويو، لونغهوي ودريفوس-شميدت، ليو وتونستال، لويس وباغاني، لويجي وماتشادو، موريرا وبوريغولت، بولين ووانغ، ران وبولو، ستانيسلاس وباروييه، تيبو ولي، وين-دينغ ونيو، يازه وفلورو، يان وهو، يانغيانغ ويو، Zhouliang وWang، Zihan وYang، Zhilin وLiu، Zhengying and Li، Jia}، السنة = {2025}، url = {http://arxiv.org/abs/2504.11354}, }