डीपसीक ने रिकर्सिव प्रूफ सर्च और नए ProverBench बेंचमार्क के साथ DeepSeek-Prover-V2 जारी किया

डीपसीक एआई ने DeepSeek-Prover-V2 जारी किया है, जो लीन 4 में औपचारिक प्रमेय सिद्ध करने के लिए एक ओपन-सोर्स बड़ा भाषा मॉडल है। यह DeepSeek-V3 के माध्यम से प्रशिक्षण डेटा उत्पन्न करने के लिए एक रिकर्सिव पाइपलाइन का उपयोग करता है, MiniF2F और PutnamBench पर नवीनतम परिणाम प्राप्त करता है, और 325 समस्याओं वाला एक नया बेंचमार्क ProverBench पेश करता है।

डीपसीक एआई ने डीपसीक-प्रूवर-V2 की घोषणा की, जो लीन 4 में औपचारिक प्रमेय सिद्ध करने के लिए एक ओपन-सोर्स बड़ा भाषा मॉडल है। यह मॉडल एक पुनरावर्ती प्रमेय-सिद्ध करने वाली पाइपलाइन का उपयोग करता है, जो जटिल प्रमेयों को उप-लक्ष्यों में विघटित करके और उन्हें औपचारिक बनाकर उच्च-गुणवत्ता वाला आरंभीकरण डेटा उत्पन्न करने के लिए डीपसीक-V3 का उपयोग करती है। एक 7 बिलियन पैरामीटर वाला मॉडल फिर इन उप-लक्ष्यों को सिद्ध करता है, और पूर्ण प्रमाणों को प्रशिक्षण के लिए डीपसीक-V3 की चेन-ऑफ-थॉट तर्क प्रक्रिया के साथ जोड़ा जाता है। बाइनरी फीडबैक के साथ सुदृढ़ीकरण सीखना मॉडल को और अधिक परिष्कृत करता है। 671 बिलियन पैरामीटर वाला संस्करण MiniF2F-test पर 88.9% स्कोर करता है और 658 PutnamBench समस्याओं में से 49 को हल करता है। डीपसीक ने ProverBench भी पेश किया, जो गणितीय तर्क के मूल्यांकन के लिए AIME प्रतियोगिताओं और पाठ्यपुस्तकों से 325 समस्याओं का एक डेटासेट है। यह मॉडल दो आकारों में उपलब्ध है: 7 बिलियन और 671 बिलियन पैरामीटर।

स्रोत: Synced — मूल