ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
यह शोध पत्र ImProver 2 को प्रस्तुत करता है, जो एक न्यूरोसिम्बोलिक ढांचा है जो डेटा-कुशल विशेषज्ञ पुनरावृत्ति (expert iteration) को एक संरचनात्मक स्कैफोल्डिंग प्रणाली के साथ जोड़ता है ताकि छोटे भाषा मॉडलों को Lean 4 में जटिल औपचारिक प्रमाणों (formal proofs) को प्रभावी ढंग से अनुकूलित करने में सक्षम बनाया जा सके, जो काफी बड़े मॉडलों से बेहतर प्रदर्शन करता है और प्रमाण अनुकूलन को एक स्केलेबल, सीखने योग्य कार्य के रूप में स्थापित करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आपके पास गणितीय प्रमाणों (mathematical proofs) का एक विशाल, बढ़ता हुआ पुस्तकालय है। ये केवल कहानियाँ नहीं हैं; ये कठोर, कंप्यूटर द्वारा जाँचे गए ब्लूप्रिंट हैं जो सिद्ध करते हैं कि चीजें सच हैं। हाल ही में, कंप्यूटरों (विशेष रूप से AI) ने मनुष्यों को प्रमाण लिखने में मदद करना शुरू कर दिया है, जिससे इस पुस्तकालय का आकार तेजी से बढ़ा है।
लेकिन एक समस्या है: पुस्तकालय अव्यवस्थित होता जा रहा है। कुछ प्रमाण सही तो हैं लेकिन लिखने का तरीका भ्रमित करने वाला है, कुछ बहुत लंबे हैं, और कुछ अन्य नियमों की एक विशाल सूची पर निर्भर हैं जो उन्हें बनाए रखना कठिन बना देते हैं। यह एक ऐसे घर की तरह है जहाँ प्लंबिंग तो काम करती है, लेकिन पाइप उलझे हुए हैं, दीवारें अलग-अलग रंगों से टकरा रही हैं, और आपको लाइट जलाने के लिए भी एक बैकपैक में अतिरिक्त औजार लेकर चलने पड़ते हैं।
मिलिए ImProver 2 से।
ImProver 2 को एक अति-व्यवस्थित, स्वयं-सुधार करने वाले लाइब्रेरियन के रूप में सोचें जो केवल किताबें रखने का काम नहीं करता, बल्कि उन्हें बेहतर बनाने के लिए फिर से लिखता है। इसका काम एक सही प्रमाण को लेना और उसे छोटा, साफ या अधिक मॉड्यूलर (modular) बनाने के लिए फिर से लिखना है, बिना गणित को तोड़े।
यह कैसे काम करता है, यहाँ कुछ सरल उपमाओं का उपयोग किया गया है:
1. "अभ्यास ही पूर्णता है" लूप (पुनरावृत्ति स्व-सुधार)
आमतौर पर, कंप्यूटर को कोई कार्य सिखाने के लिए, आप उसे मनुष्यों द्वारा लिखे गए हजारों उदाहरण दिखाते हैं। लेकिन प्रमाण अनुकूलन (proof optimization) के लिए, अच्छे उदाहरण दुर्लभ हैं।
ImProver 2 इसे स्वयं को सिखाकर हल करता है।
- ड्राफ्ट (The Draft): यह एक प्रमाण लेता है और उसे कई अलग-अलग तरीकों से फिर से लिखने की कोशिश करता है (जैसे एक लेखक कहानी के 10 अलग-अलग अंतों के बारे में विचार मंथन करता है)।
- ग्रेडिंग (The Grading): यह जाँचता है कि कौन से पुनर्लेखन अभी भी गणितीय रूप से सही हैं। फिर, यह उन्हें हमारे लक्ष्यों के आधार पर स्कोर देता है: क्या यह छोटा है? क्या यह बाहरी संदर्भों का कम उपयोग करता है? क्या इसे स्पष्ट चरणों में तोड़ा गया है?
- सबक (The Lesson): यह अपने "विजेता" पुनर्लेखनों की तुलना अपने "हारने वाले" पुनर्लेखनों से करता है। यह सीखता है, "ओह, जब मैंने यह किया, तो प्रमाण छोटा हो गया और सही रहा। जब मैंने वह किया, तो यह टूट गया।"
- रीप्ले बफर (The Replay Buffer): AI को जो सीखा है उसे भूलने या बुरे विचारों के लूप में फंसने से बचाने के लिए, यह पुराने अच्छे उदाहरणों को नए उदाहरणों के साथ मिलाकर एक "मेमोरी बैंक" रखता है। यह सुनिश्चित करता है कि यह केवल अपनी गलतियों को दोहराने के बजाय समय के साथ बेहतर होता रहे।
2. "न्यूरोसिम्बोलिक स्कैफोल्ड" (ट्रेनिंग व्हील्स)
कल्पना कीजिए कि आप बिना किसी मैनुअल या आरेख के एक जटिल इंजन को ठीक करने की कोशिश कर रहे हैं। यह कठिन है। अब कल्पना करें कि आपके पास एक आरेख है जो ठीक उसी हिस्से को हाइलाइट करता है जिस पर आप काम कर रहे हैं, समझाता है कि वह हिस्सा क्या करता है, और आपके पास मौजूद आवश्यक औजारों की सूची देता है।
ImProver 2 हर प्रमाण के लिए AI को यह "आरेख" देता है। इसे न्यूरोसिम्बोलिक ऑगमेंटेशन (Neurosymbolic Augmentation) कहा जाता है। यह प्रदान करता है:
- मानचित्र (The Map): यह प्रमाण की वर्तमान स्थिति दिखाता है (अब तक क्या सिद्ध हुआ है, आगे क्या करना बाकी है)।
- संदर्भ (The Context): यह उस विशिष्ट प्रमाण से संबंधित विशिष्ट परिभाषाओं और नियमों को निकालता है, ताकि AI अनुमान लगाने के बजाय सटीक रहे।
- अनुवाद (The Translation): यह एक "साधारण अंग्रेजी" सारांश देता है कि प्रमाण क्या करने की कोशिश कर रहा है, जिससे AI को कोड लिखने से पहले लक्ष्य समझने में मदद मिलती है।
यह "स्कैफोल्ड" छोटे, कम शक्तिशाली कंप्यूटरों को बहुत बड़े, स्मार्ट कंप्यूटरों की तरह प्रदर्शन करने में मदद करता है।
3. तीन लक्ष्य (Metrics)
लाइब्रेरियन केवल यह नहीं चाहता कि प्रमाण "सही" हो। वह विशिष्ट गुणों के लिए अनुकूलन चाहता है, जैसे एक शेफ रेसिपी को व्यवस्थित करता है:
- लंबाई (The "Golf" Metric): गोल्फ की तरह ही, लक्ष्य कम से कम प्रहारों के साथ गेंद को छेद में डालना है। ImProвer 2 अनावश्यक चरणों को हटाकर प्रमाणों को छोटा करने का प्रयास करता है।
- निर्भरता (The "Self-Contained" Metric): कल्पना कीजिए कि एक रेसिपी कहती है "पड़ोसी के घर से गुप्त सॉस डालें।" यह एक निर्भरता है। ImProver 2 प्रमाणों को इस तरह से फिर से लिखने का प्रयास करता है ताकि वे इतने सारे बाहरी "पड़ोसी के सॉस" पर निर्भर न रहें, जिससे उन्हें स्वयं उपयोग करना आसान हो सके।
- मॉड्यूलरिटी (The "Lego" Metric): एक अस्त-व्यस्त प्रमाण मिट्टी के एक बड़े ब्लॉक की तरह है। एक मॉड्यूलर प्रमाण लेगो (Legos) के सेट की तरह है—छोटे, अलग और पुन: प्रयोज्य टुकड़े। ImProver 2 बड़े प्रमाणों को छोटे, स्वतंत्र उप-प्रमाणों (जैसे "h1 प्राप्त करें," "h2 प्राप्त करें") में तोड़ने का प्रयास करता है ताकि तर्क अधिक स्पष्ट हो सके।
परिणाम: छोटा ही शक्तिशाली है
सबसे आश्चर्यजनक खोज यह है कि ImProver 2 ने एक छोटे AI मॉडल (7 बिलियन पैरामीटर्स) को इन कार्यों में एक विशाल AI मॉडल (कुछ सैकड़ों अरबों पैरामीटर्स वाले) से बेहतर होने के लिए प्रशिक्षित किया जो इस विशेष प्रशिक्षण के बिना थे।
यह एक कॉम्पैक्ट, कुशल स्पोर्ट्स कार को उसके इंजन को इतना सटीक रूप से ट्यून करने जैसा है कि वह एक विशिष्ट दौड़ में एक भारी ट्रक को हरा दे, भले ही ट्रक का इंजन बड़ा हो। छोटा मॉडल, जब उसे सही "स्कैफोल्ड" और सही "प्रैक्टिस लूप" दिया जाता है, तो वह दिग्गजों की तुलना में जटिल गणितीय तर्कों को बेहतर ढंग से पुनर्गठित करना सीख जाता है।
संक्षेप में: ImProver 2 एक ऐसा सिस्टम है जो छोटे AI मॉडल को विशेषज्ञ प्रमाण संपादक (proof editor) बनने के लिए सिखाता है। उन्हें समस्या का एक स्पष्ट मानचित्र देकर और उन्हें उनके अपने सर्वोत्तम प्रयासों से सीखने देकर, यह बिखरे हुए गणितीय पुस्तकालयों को साफ कर सकता है, जिससे वे छोटे, साफ और बनाए रखने में आसान बन सकते हैं, और वह भी बिना सबसे महंगे, विशाल सुपरकंप्यूटरों की आवश्यकता के।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।