Kimi तकनीकी टीम ने हाल ही में Kimina-Prover के पूर्वावलोकन संस्करण की तकनीकी रिपोर्ट जारी की है, और 1.5B और 7B पैरामीटर वाले मॉडल आसवन संस्करण, डेटा जेनरेशन के लिए Kimina-Autoformalizer-7B मॉडल और संशोधित miniF2F बेंचमार्क डेटासेट को ओपन सोर्स किया है। Kimina-Prover, Numina और Kimi टीम द्वारा संयुक्त रूप से विकसित एक गणितीय प्रमेय प्रमाण मॉडल है, जो औपचारिक प्रमेय प्रमाण के क्षेत्र में एक नए प्रकार के, अनुमान-संचालित अन्वेषण प्रतिमान का उपयोग करता है, और उत्कृष्ट प्रदर्शन दिखाता है।
Kimina-Prover, Qwen2.5-72B मॉडल पर आधारित है, और Kimi k1.5 की बड़े पैमाने पर सुदृढीकरण शिक्षा (RL) प्रक्रिया के साथ प्रशिक्षित किया गया है। आधिकारिक miniF2F औपचारिक गणित बेंचमार्क परीक्षण में, Kimina-Prover पूर्वावलोकन संस्करण ने कम नमूना बजट (pass@8192) के साथ 80.7% की उत्तीर्ण दर हासिल की, जो पिछले सर्वोत्तम परिणामों: BFS Prover के 72.95% (pass@2048×2×600+) और DeepSeek-Prover के 50.0% (pass@65536) से काफी आगे है।
औपचारिक प्रमेय प्रमाण गणित और कंप्यूटर विज्ञान का एक महत्वपूर्ण क्षेत्र है, जो गणितीय प्रमेयों की शुद्धता को सत्यापित करने के लिए सख्त गणितीय तर्क और कंप्यूटर प्रोग्राम का उपयोग करता है। हालाँकि, AI को औपचारिक प्रमाण प्राप्त करना बहुत चुनौतीपूर्ण है, पारंपरिक तरीके अक्सर जटिल, गहन अंतर्दृष्टि और रचनात्मकता की आवश्यकता वाले गणितीय समस्याओं से निपटने में असमर्थ होते हैं। हाल के वर्षों में, बड़े भाषा मॉडल (LLM) के उदय ने इस क्षेत्र में नई उम्मीदें जगाई हैं, लेकिन मौजूदा तरीकों में ज्यादातर सीमाएँ हैं, जैसे बाहरी खोज पर निर्भरता, गहन तर्क को पकड़ने में कठिनाई, और मॉडल पैमाने का प्रभाव की कमी आदि।
इन सीमाओं को दूर करने के लिए, Kimina-Prover ने एक नया तरीका अपनाया है, जो बड़े पैमाने पर सुदृढीकरण शिक्षा (RL) को "औपचारिक तर्क मोड" के साथ गहराई से जोड़ता है, और मॉडल द्वारा पूर्ण प्रमाण उत्पन्न करने की आंतरिक "रणनीति" को सीधे अनुकूलित करता है। यह विधि मॉडल को टोकन उत्पन्न करने की प्रक्रिया में विशाल प्रमाण स्थान का स्पष्ट रूप से पता लगाने, स्वतंत्र रूप से अनुमान पथ को नेविगेट करने, गणना लागत को बहुत कम करने और मॉडल को अधिक लचीला, और मानवीय अंतर्ज्ञान के करीब अन्वेषण तरीका देने में सक्षम बनाती है। इसके अतिरिक्त, Kimina-Prover ने अंतिम परिणामों पर आधारित पुरस्कार संकेतों को भी पेश किया है, सुदृढीकरण शिक्षा की प्रशिक्षण प्रक्रिया लक्ष्य-उन्मुख है, केवल पूरी तरह से सही, संकलित प्रमाण ही सकारात्मक पुरस्कार प्राप्त कर सकते हैं।
Kimina-Prover के प्रारंभिक शोध परिणामों में उल्लेखनीय प्रगति हुई है। miniF2F बेंचमार्क परीक्षण में, Kimina-Prover ने 80.7% की उत्तीर्ण दर हासिल की, जो पिछले सर्वोत्तम परिणामों से काफी आगे है। यह अत्यधिक नमूना दक्षता भी दिखाता है, यहां तक कि बहुत कम नमूना बार में भी प्रतिस्पर्धी परिणाम प्राप्त कर सकता है। इसके अतिरिक्त, Kimina-Prover का प्रदर्शन मॉडल पैरामीटर पैमाने के बढ़ने के साथ लगातार सुधार करता है, यह औपचारिक गणित के क्षेत्र में तंत्रिका प्रमेय प्रमाणक में इस तरह के स्पष्ट पैमाने के प्रभाव का पहला अवलोकन है। शीर्ष-स्तरीय सामान्य अनुमान बड़े मॉडल की तुलना में, Kimina-Prover औपचारिक गणित कार्यों में जबरदस्त लाभ दिखाता है, और लगातार औपचारिक रूप से सही, Lean कंपाइलर द्वारा जांचे जा सकने वाले प्रमाण उत्पन्न कर सकता है।
Kimina-Prover की सोच प्रक्रिया में बहुत अधिक व्याख्यात्मकता है, उपयोगकर्ता देख सकते हैं कि मॉडल कैसे चरण दर चरण प्रमाण प्राप्त करता है, यह मॉडल के व्यवहार को समझने, विफलता के कारणों का निदान करने के लिए सुविधा प्रदान करता है, और इसमें गणित शिक्षा सहायक उपकरण बनने की क्षमता भी है। शोध दल ने कहा कि Kimina-Prover का प्रदर्शन मॉडल पैमाने और संदर्भ लंबाई में वृद्धि के साथ उल्लेखनीय रूप से बढ़ सकता है, जिससे "अनुमान-आधारित तंत्रिका प्रमाणक" की क्षमता का प्रारंभिक सत्यापन होता है। बड़े पैमाने पर सुदृढीकरण शिक्षा और मानव जैसे अनुमान मोड के संयोजन से स्वचालित अनुमान और यहां तक कि सामान्य कृत्रिम बुद्धिमत्ता (AGI) के विकास के लिए नए विचार खुलेंगे।
समुदाय की भागीदारी और अनुसंधान प्रगति को बढ़ावा देने के लिए, Kimi तकनीकी टीम ने Kimina-Prover के 1.5B और 7B पैरामीटर वाले आसवन संस्करण, डेटा जेनरेशन के लिए Kimina-Autoformalizer-7B मॉडल और संशोधित miniF2F बेंचमार्क डेटासेट को ओपन सोर्स किया है।
Arxiv तकनीकी रिपोर्ट:https://arxiv.org/abs/2504.11354
GitHub कोड भंडार:https://github.com/MoonshotAI/Kimina-Prover-Preview
Hugging Face मॉडल डाउनलोड करें:https://huggingface.co/collections/AI-MO/kimina-prover-preview-67fb536b883d60e7ca25d7f9
