LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
यह शोध पत्र LEAP को प्रस्तुत करता है, जो एक एजेंटिक फ्रेमवर्क है जो अनौपचारिक तर्क (informal reasoning) को लीन (Lean) कंपाइलर फीडबैक के साथ जोड़कर सामान्य-उद्देश्य वाले लार्ज लैंग्वेज मॉडल्स को औपचारिक प्रमेय सिद्ध करने (formal theorem proving) में अत्याधुनिक प्रदर्शन प्राप्त करने के लिए सशक्त बनाता है, जिसने 2025 की पुटनाम प्रतियोगिता (Putnam Competition) की सभी 12 समस्याओं को सफलतापूर्वक हल किया और नए प्रस्तावित लीन-आईएमओ-बेंच (Lean-IMO-Bench) पर विशिष्ट प्रणालियों की तुलना में काफी बेहतर प्रदर्शन किया।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आपके पास एक अत्यंत प्रतिभाशाली, विश्व स्तरीय गणितज्ञ है जो जटिल विचारों को सरल अंग्रेजी में समझा सकता है, एक बेहतरीन कहानी सुना सकता है, और कठिन पहेलियों को सुलझा सकता है। हालाँकि, यह गणितज्ञ कोड लिखने में बहुत खराब है। यदि आप उनसे कोई गणितीय समस्या हल करने के लिए प्रोग्राम लिखने को कहते हैं, तो वे कुछ ऐसा लिख सकते हैं जो सुनने में तो सही लगता है, लेकिन जैसे ही आप इसे चलाने की कोशिश करते हैं, यह तुरंत क्रैश हो जाता है।
गणित में लार्ज लैंग्वेज मॉडल्स (LLMs) की वर्तमान स्थिति यही है। वे "अनौपचारिक" गणित (इसके बारे में बात करना) में अद्भुत हैं, लेकिन "औपचारिक" गणित (एक सख्त, कंप्यूटर द्वारा जांचने योग्य भाषा जैसे कि Lean, जहाँ एक भी टाइपो पूरे प्रमाण को विफल कर सकता है) लिखने में संघर्ष करते हैं।
यह शोध पत्र LEAP (LLM-in-Lean Environment Agentic Prover) पेश करता है, जो एक सुपर-ऑर्गनाइज्ड प्रोजेक्ट मैनेजर की तरह कार्य करता है ताकि इस प्रतिभाशाली गणितज्ञ को अंततः सटीक कोड लिखने में मदद मिल सके।
LEAP कैसे काम करता है, यहाँ सरल उपमाओं का उपयोग किया गया है:
1. समस्या: "वन-शॉट" का जाल
पहले, यदि आप किसी AI को कोई प्रमेय (theorem) सिद्ध करने के लिए कहते थे, तो वह एक ही बार में पूरा समाधान लिखने की कोशिश करता था, जैसे कोई छात्र एक ही सांस में 50 पन्नों का शोध प्रबंध (thesis) लिखने की कोशिश कर रहा हो। यदि उन्होंने तीसरे पन्ने पर कोई गलती की, तो पूरी चीज़ विफल हो जाती थी। शोध पत्र इसे "वन-शॉट फॉर्मलाइजेशन" कहता है, और यह कठिन समस्याओं के लिए शायद ही कभी काम करता है।
2. समाधान: "ब्लूप्रिंट" दृष्टिकोण
LEAP इस प्रक्रिया को बदलकर खेल बदल देता है, ठीक वैसे ही जैसे एक गगनचुंबी इमारत का निर्माण किया जाता है:
- चरण 1: आर्किटेक्ट का स्केच (ब्लूप्रिंट): एक ही बार में पूरी इमारत बनाने की कोशिश करने के बजाय, LEAP पहले AI से एक "ब्लूप्रिंट" बनाने के लिए कहता है। यह एक उच्च-स्तरीय योजना है जो सरल अंग्रेजी में लिखी गई है। यह कहता है, "इसे हल करने के लिए, हमें पहले लेम्मा (Lemma) A को सिद्ध करने की आवश्यकता है, फिर लेम्मा B को, और अंत में उन्हें मिलाना होगा।"
- चरण 2: निर्माण दल (औपचारिक प्रमाण): एक बार ब्लूप्रिंट स्वीकृत हो जाने के बाद, AI योजना के केवल एक छोटे से हिस्से के लिए वास्तविक लीन (Lean) कोड लिखने की कोशिश करता है।
- चरण 3: निरीक्षक (कंपाइलर): लीन कंपाइलर एक सख्त बिल्डिंग इंस्पेक्टर की तरह कार्य करता है। यह कोड की जाँच करता है। यदि यह उत्तम है, तो बहुत अच्छा! यदि कोई त्रुटि है, तो यह एक विशिष्ट संदेश वापस भेजता है: "यहाँ नींव में दरार है।"
- चरण 4: सुधारक (स्व-परिष्करण): AI निरीक्षक के नोट को पढ़ता है, विशिष्ट त्रुटि को ठीक करता है, और फिर से प्रयास करता है। यह दोबारा शुरू नहीं करता; यह केवल उस छेद को भरता (patch) है।
3. गुप्त मंत्र: "मेमोरी मैप" (DAG)
LEA का सबसे चतुर हिस्सा यह है कि यह याद रखता है कि इसने क्या किया है। कल्पना कीजिए कि आप एक विशाल भूलभुलैया (maze) को हल कर रहे हैं।
- पुराना तरीका: यदि आप किसी बंद रास्ते (dead end) पर पहुँच जाते हैं, तो आप भूल सकते हैं कि आप कहाँ से आए थे और चक्कर काटते हुए समय बर्बाद कर सकते हैं।
- LEAP का तरीका: LEAP पूरी भूलभुलैया का एक मानचित्र (जिसे डायरेक्टेड एसाइक्लिक ग्राफ या DAG कहा जाता है) बनाता है।
- यदि यह एक शाखा में एक छोटा सा पहेली (लेम्मा) हल करता है, तो यह उसे मानचित्र पर लिख देता है।
- यदि इसे बाद में किसी अन्य शाखा में वही पहेली मिलती है, तो यह उसे फिर से हल नहीं करता। यह बस मानचित्र को देखता है, देखता है कि समाधान पहले से ही वहाँ है, और उसका उपयोग करता है।
- यह AI को पहिये का पुन: आविष्कार करने में ऊर्जा बर्बाद करने से रोकता है और इसे उन विशाल, जटिल समस्याओं को हल करने की अनुमति देता है जिन्हें हल करने में अन्यथा बहुत समय लगता।
4. परिणाम: शून्य से नायक तक
शोध पत्र ने इस प्रणाली का परीक्षण दुनिया की कुछ सबसे कठिन गणितीय समस्याओं पर किया:
- पुटन प्रतियोगिता (Putnam Competition): यह उत्तरी अमेरिका के विश्वविद्यालय छात्रों के लिए एक कठिन गणित प्रतियोगिता है। 2025 में, औसत छात्र ने 120 में से केवल 2 अंक प्राप्त किए। LEAP ने 100% समस्याओं को हल किया (सभी 12)।
- IMO-Bench: लेखकों ने अंतर्राष्ट्रीय गणितीय ओलंपियाड (IMO) पर आधारित एक नया परीक्षण बनाया है। पिछले विशेष रूप से प्रशिक्षित AI सिस्टमों ने लगभग 48% इन समस्याओं को हल किया। LEAP ने, जो एक सामान्य-उद्देश्य वाला AI है, 70% को हल किया।
5. मुख्य निष्कर्ष
शोध पत्र का तर्क है कि हमें गणित के लिए केवल छोटे, विशिष्ट रोबोट बनाने की आवश्यकता नहीं है। इसके बजाय, हम एक सामान्य-उद्देश्य वाले AI (जो सब कुछ थोड़ा-थोड़ा जानता है) को ले सकते हैं और उसे एक अच्छा वर्कफ़्लो (ब्लूप्रिंट, निरीक्षक और मेमोरी मैप) दे सकते हैं।
इसे इस तरह सोचें: आपको एक आदर्श केक बनाने के लिए केवल बेकिंग में कुशल रोबोट की आवश्यकता नहीं है। आपको बस एक सामान्य-उद्देश्य वाले शेफ की आवश्यकता है जिसे एक अच्छी रेसिपी, एक सख्त स्वाद-परीक्षक (taste-tester) और एक नोटबुक दी जाए कि क्या काम आया। LEAP वह रेसिपी, स्वाद-परीक्षक और नोटबुक प्रदान करता है, जिससे एक "अच्छी बात करने वाला" एक "परफेक्ट प्रूवर" बन जाता है।
संक्षेप में: LEAP AI को अधिक स्मार्ट नहीं बनाता है; यह बस AI को अपने विचारों को व्यवस्थित करने, अपने काम की जाँच करने और अपनी सफलताओं को याद रखने का एक बेहतर तरीका देता है, जिससे यह उन गणितीय समस्याओं को हल करने में सक्षम होता है जो पहले सामान्य AI के लिए असंभव थीं।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।