Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

तकनीकी निष्कर्ष: Lean में संदर्भ-आधारित प्रमाण शिक्षण के साथ LLMs के माध्यम से नए प्रमेयों की खोज

समस्या विवरण
लार्ज लैंग्वेज मॉडल्स (LLMs) ने औपचारिक प्रमेय सिद्ध करने (formal theorem proving) के क्षेत्र में आशाजनक परिणाम प्रदर्शित किए हैं, लेकिन वे महत्वपूर्ण चुनौतियों का सामना करते हैं: वे मतिभ्रम (hallucinations) उत्पन्न कर सकते हैं, और एक गणितीय अनुमान (conjecture) और उसके प्रमाण को एक साथ उत्पन्न करने से अक्सर सरल या तुच्छ प्रमेयों पर अभिसरण (convergence) हो जाता है। मौजूदा दृष्टिकोण आमतौर पर सुपरवाइज्ड फाइन-ट्यूनिंग (SFT) या वेरिफाइड रिवार्ड्स के साथ रीइन्फोर्समेंट लर्निंग (RLVR) पर निर्भर करते हैं, जिनके लिए व्यापक प्रशिक्षण डेटा की आवश्यकता होती है और जिन्हें क्लोज्ड मॉडल्स (closed models) पर लागू करना कठिन होता है। इसके अलावा, वर्तमान विधियाँ "सिद्ध करने में कठिन" प्रमेयों की खोज करने में संघर्ष करती हैं क्योंकि प्रमेय उत्पन्न करने की संभावना इसके प्रमाण की तत्काल सफलता दर द्वारा भारी रूप प्रकार से भारित (weighted) होती है, जिससे खोज सरल, छोटे प्रमाणों में सिमट जाती है।

कार्यप्रणाली: कंजेक्चरिंग-प्रूविंग लूप (CPL)
लेखक एक कंजेचरिंग-प्रूविंग लूप (CPL) का प्रस्ताव करते हैं, जो एक पाइपलाइन है जिसे स्वचालित रूप से नए गणितीय अनुमान उत्पन्न करने और उन्हें Lean 4 में सत्यापित करने के लिए डिज़ाइन किया गया है। यह ढांचा अनुमान (conjecture) के निर्माण को प्रमाण (proof) के निर्माण से अलग करता है और दोनों चरणों के लिए संदर्भ के रूप में पहले से सत्यापित प्रमेयों की एक लाइब्रेरी का उपयोग करता है।

पाइपलाइन चार मुख्य घटकों के माध्यम से कार्य करती है: एक कंजेक्चरर मॉड्यूल (LLM एजेंट), एक प्रवर मॉड्यूल (LLM एजेंट), एक Lean सर्वर, और एक लाइब्रेरी (Lean कोड डेटा)।

1. अनुमान चरण (Conjecture Phase): कंजेक्चरर वर्तमान लाइब्रेरी के आधार पर Lean 4 फॉर्मेट में नए गणितीय कथनों को उत्पन्न करता है। यह सुनिश्चित करने के लिए कि कथन वाक्य रचना की दृष्टि से वैध (syntactically valid) और नवीन (novel) है (यह सुनिश्चित करना कि कथन पहले से मौजूद प्रमेयों या वर्तमान लाइब्रेरी द्वारा सिद्ध नहीं है), यह Lean सर्वर से क्वेरी करता है।
2. प्रमाण चरण (Proof Phase): प्रत्येक वैध अनुमान के लिए, प्रवर एक औपचारिक प्रमाण बनाने का प्रयास करता है। महत्वपूर्ण रूप से, प्रवर को संदर्भ के रूप में लाइब्रेरी (जिसमें पहले से सत्यापित प्रमेय और प्रमाण शामिल हैं) प्रदान की जाती है। यह मॉडल को बिना पुन: प्रशिक्षण के संदर्भ-आधारित शिक्षण (इन-कॉन्टेक्स्ट लर्निंग) के माध्यम से प्रमाण रणनीतियों को सीखने में सक्षम बनाता है। प्रवर अधिकतम प्रयासों की संख्या (प्रयोगों में 16 निर्धारित) तक पुनरावृत्ति करता है, और अपने प्रयासों को परिष्कृत करने के लिए Lean सर्वर के त्रुटि संदेशों का उपयोग करता है।
3. पुनरावृत्ति (Iteration): सत्यापित अनुमानों और प्रमाणों के युग्मों को लाइब्रेरी में जोड़ा जाता है, जो बाद के पुनरावृत्तियों के लिए संदर्भ के रूप में कार्य करती है।

यह पृथक्करण सिस्टम को प्रमाण की कठिनाई के आधार पर खोज संसाधनों को आवंटित करने की अनुमति देता है। एक साधारण लूप (SL) के विपरीत, जहाँ एक कथन और उसका प्रमाण एक साथ उत्पन्न किया जाता है, CPL एक ही कथन के लिए कई प्रमाणों का प्रयास करता है और फिर उसे त्याग देता है। यह खोज को केवल आसानी से सिद्ध होने वाले प्रमेयों के बजाय उन प्रमेयों की ओर स्थानांतरित करता है जो सिद्ध करने योग्य तो हैं लेकिन कठिन हैं।

मुख्य योगदान

1. पाइपलाइन प्रस्ताव: CPL का परिचय, एक ढांचा जो अनुमान निर्माण को प्रमाण निर्माण से अलग करता है, जिससे लंबे और अधिक जटिल प्रमाणों की खोज संभव होती है।
2. क्लोज्ड मॉडल्स के लिए संदर्भ-आधारित शिक्षण: यह प्रदर्शन कि क्लोजed LLMs (विशेष रूप से ChatGPT-o3) अपने स्वयं के पहले से सत्यापित आउटपुट से संदर्भ-आधारित शिक्षण के माध्यम से अपनी प्रमाण क्षमताओं में सुधार कर सकते हैं, जिससे पैरामीटर अपडेट या फाइन-ट्यूनिंग की आवश्यकता समाप्त हो जाती है।
3. सैद्धांतिक और अनुभवजन्य सत्यापन: यह कार्य एक सैद्धांतिक मॉडल प्रदान करता है जो दिखाता है कि CPL, समवर्ती पीढ़ी (simultaneous generation) वाले ढांचों की तुलना में कठिन-से-सिद्ध होने वाले प्रमेयों को उत्पन्न करने की संभावना को बढ़ाता है। प्रयोगात्मक रूप से, यह पुष्टि की गई है कि CPL सफलतापूर्वक एक विशिष्ट शोध-स्तर के प्रमेय को पुनः खोज सका जिसे बेसलाइन फ्रेमवर्क नहीं खोज पाया था।

प्रायोगिक परिणाम
लेखकों ने टोपोलॉजिकल अवधारणाओं (सेमी-ओपन सेट्स, $\alpha$-ओपननेस, और प्री-ओपननेस) का उपयोग करके CPL का मूल्यांकन एक साधारण लूप (SL) वाले बेसलाइन के विरुद्ध किया, जो Mathlib के भीतर परिभाषित हैं लेकिन अभी तक लाइब्रेरी में शामिल नहीं किए गए हैं। लक्ष्य यह प्रमेय था कि दो $\alpha$-ओपन सेट्स का प्रतिच्छेदन (intersection) $\alpha$-ओपन है।

• खोज दर (Discovery Rate): 20 प्रायोगिक रन में, CPL ने लक्षित प्रमेय को 5 बार खोजा। इसके विपरीत, SL फ्रेमवर्क ने (औसतन 328 बनाम 106 प्रमेय उत्पन्न करते हुए) लक्षित प्रमेय को एक बार भी उत्पन्न करने में विफल रहा। एक सटीक फिशर टेस्ट ने पुष्टि की कि यह अंतर सांख्यिकीय रूप से महत्वपूर्ण है ($p = 0.024$)।
• प्रमाण की लंबाई (Proof Length): CPL ने SL की तुलना में काफी लंबी प्रमाण लंबाई (कैरेक्टर काउंट में) वाले प्रमेय उत्पन्न किए, जो इस सैद्धांतिक दावे का समर्थन करता है कि फ्रेमवर्क अधिक कठिन प्रमाणों की ओर ध्यान केंद्रित करता है।
• संदर्भ की प्रभावशीलता (Effectiveness of Context):
  • पुनः सिद्ध करना (Re-proving): उत्पन्न प्रमेयों को पुनः सिद्ध करते समय, लाइब्रेरी को संदर्भ के रूप में प्रदान करने से सफलता दर 91% से बढ़कर 99% हो गई ($p = 4 \times 10^{-35}$)।
  • लक्षित प्रमेय: $\alpha$-ओपन सेट्स के संबंध में लक्षित प्रमेय को सिद्ध करने का प्रयास करते समय, जब उत्पन्न लाइब्रेरी को संदर्भ के रूप में प्रदान किया गया, तो प्रवर 80 प्रयासों में से 7 बार सफल रहा। लाइब्रेरी के बिना, यह 100% बार विफल रहा।
  • प्राकृतिक भाषा में बेसलाइन: जब ChatGPT-4o से प्राकृतिक भाषा में प्रमेय को सिद्ध करने के लिए कहा गया, तो इसने अक्सर प्रमेय को गलत बताया या गलत प्रमाण दिए; ChatGPT-o3 ने लगातार इसे गलत बताया, जो इंगित करता है कि प्रमेय मॉडल्स के प्री-ट्रेंड ज्ञान से बाहर था। Lean 4 में सफलता का श्रेय उत्पन्न लाइब्रेरी से प्रमाण रणनीतियों के संदर्भ-आधारित शिक्षण को दिया गया।

महत्व और दावे
यह कार्य दावा करता है कि CPL स्वयं-जनित, सत्यापित प्रमाणों से संदर्भ-आधारित शिक्षण का लाभ उठाकर गैर-तुच्छ (non-trivial) प्रमेया खोजने में LLMs की सीमा को प्रभावी ढंग से संबोधित करता है। लेखक इस बात पर जोर देते हैं कि यह दृष्टिकोण औपचारिक गणितीय पुस्तकालयों (जैसे Mathlib) के स्वचालित विस्तार को सक्षम बनाता है, उन अवधारणाओं के लिए प्रस्ताव उत्पन्न करके जो शायद LLM को स्पष्ट रूप से ज्ञात न हों। यह कार्य सुझाव देता है कि अनुमान और प्रमाण चरणों को अलग करना, और पुनरावृत्त संदर्भ संवर्धन (iterative context enrichment) के साथ जोड़ना, न्यूरल थ्योरम प्रूविंग के लिए एक व्यवहार्य रणनीति है, विशेष रूप से उन क्लोज्ड मॉडल्स के लिए जहाँ पारंपरिक प्रशिक्षण विधियाँ लागू नहीं होती हैं। लेखक एक विनम्र रुख बनाए रखते हैं, यह नोट करते हुए कि जबकि फ्रेमवर्क ने सफलतापूर्वक एक ज्ञात शोध-स्तर के प्रमेय को पुनः खोज लिया है, गहरे और अधिक महत्वपूर्ण गणितीय कथनों के लिए पीढ़ी प्रक्रिया को परिष्कृत करने हेतु भविष्य के कार्य की आवश्यकता है।