1M AI News के अनुसार, मेन्यू LongCat टीम ने LongCat-Flash-Prover को ओपन सोर्स किया है, जो एक 5600 अरब पैरामीटर का MoE मॉडल है जो फॉर्मल प्रमेय प्रमाण भाषा Lean4 के गणितीय तर्क कार्यों के लिए विशेष रूप से डिज़ाइन किया गया है। मॉडल वेट्स MIT लाइसेंस के तहत जारी किए गए हैं और GitHub, Hugging Face और ModelScope पर उपलब्ध हैं।
मॉडल औपचारिक तर्क को तीन स्वतंत्र क्षमताओं में विभाजित करता है: स्वचालित औपचारिकीकरण (प्राकृतिक भाषा के गणितीय प्रश्नों को Lean4 औपचारिक वाक्यों में बदलना), खाका उत्पादन (लेम्मा-शैली के सबूत के ढांचे का निर्माण) और पूर्ण सबूत उत्पादन। तीनों क्षमताएँ Agent टूल समेकित तर्क (TIR) और Lean4 कंपाइलर के साथ वास्तविक समय में बातचीत के माध्यम से सत्यापित की जाती हैं।
टीम ने शीत प्रारंभिक डेटा उत्पन्न करने के लिए हाइब्रिड-एक्सपर्ट्स इटरेशन फ्रेमवर्क का प्रस्ताव रखा है, और MoE मॉडल की दीर्घकालिक कार्य प्रशिक्षण को स्थिर करने के लिए बल प्रशिक्षण चरण में HisPO एल्गोरिथम शामिल किया है, साथ ही पुरस्कार हैकिंग को रोकने के लिए प्रमेय संगतता और कानूनीता जांच तंत्र जोड़ा गया है।
बेंचमार्क दर्शाते हैं कि LongCat-Flash-Prover ने ओपन-सोर्स वेट मॉडल में स्वचालित फॉर्मलाइजेशन और प्रमेय सिद्धि दोनों में SOTA को अपडेट कर दिया है। MiniF2F-Test पर केवल 72 इन्फरेंस के साथ 97.1% पास रेट प्राप्त किया गया, जबकि ProverBench और PutnamBench पर क्रमशः 70.8% और 41.5% प्राप्त किया गया, जहां प्रति प्रश्न इन्फरेंस की संख्या 220 से अधिक नहीं है।