तकनीकी सारांश: एक औपचारिक स्वयंसिद्ध प्रणाली में स्व-पर्यवेक्षित प्रमेय खोज (Self-Supervised Theorem Discovery)

समस्या विवरण

हाल के एआई सिस्टम, विशेष रूप से लार्ज लैंग्वेज मॉडल्स (LLMs), ने गणितीय तर्क में महत्वपूर्ण प्रगति प्रदर्शित की है, लेकिन वे काफी हद तक मानव-प्रदत्त पूर्व-ज्ञान (priors) जैसे कि गणितीय पाठ, कोड और मौजूदा प्रमेय पुस्तकालयों पर निर्भर करते हैं। एक महत्वपूर्ण खुला प्रश्न यह बना हुआ है: क्या एक एजेंट केवल एक औपचारिक स्वयंसिद्ध प्रणाली के मूल नियमों से शुरू होकर, मानव पूर्व-ज्ञान, मौजूदा प्रमेय पुस्तकालयों या प्रशिक्षण समस्या सेटों तक पहुँच के बिना, स्वायत्त रूप से उपयोगी प्रमेयों की खोज कर सकता है?

वर्तमान विधियाँ अक्सर तर्क को बूटस्ट्रैप करने के लिए मानव-निर्मित ज्ञान पर निर्भर करती हैं। स्वयंसिद्ध डोमेन में स्वयं-सुधार करने वाले एजेंट भी अक्सर खोजे गए प्रमेयों की उपयोगिता का मूल्यांकन करने के लिए बाहरी न्यायाधीशों (judges) पर निर्भर करते हैं। यह शोध इस बात की जांच करता है कि क्या एक एजेंट न केवल प्रमेयों की खोज कर सकता है, बल्कि "उपयोगी" प्रमेयों की पहचान और उपयोग भी कर सकता है ताकि अपने स्वयं के प्रमाण खोज (proof search) और बाहरी तर्क प्रणालियों के प्रदर्शन में सुधार किया जा सके, जो पूरी तरह से स्वयंसिद्धों और निष्कर्ष नियमों (inference rules) पर आधारित हो।

कार्यप्रणाली (Methodology)

1. औपचारिक सेटिंग: स्टैक मशीन के रूप में हिल्बर्ट सिस्टम (Hilbert System)

लेखक समस्या को प्रपोजिशनल लॉजिक के लिए एक हिल्बर्ट स्वयंसिद्ध प्रणाली के भीतर स्थापित करते हैं। यह प्रणाली जानबूझकर न्यूनतम रखी गई है, जिसमें शामिल हैं:

• तीन स्वयंसिद्ध (Axioms):
  • $Ax1: A \to (B \to A)$ (वीकनिंग/Weakening)
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (डिस्ट्रीब्यूशन/Distribution)
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ (कॉन्ट्रापोजीशन/Contraposition)
• एक निष्कर्ष नियम (Inference Rule): मोडस पोनेंस (Modus Ponens - MP), जो $X$ और $X \to Y$ से $Y$ को व्युत्पन्न करता है।

सीखने की प्रक्रिया को सुगम बनाने के लिए, लेखक प्रमेय सिद्ध करने को एक नियत (deterministic), लक्ष्य-आधारित स्टैक-मशीन निर्णय प्रक्रिया $(S, A, s_0, P)$ के रूप में तैयार करते हैं:

• अवस्था (State - $S$): सूत्रों (formulas) का एक परिमित स्टैक।
• क्रियाएँ (Actions - $A$): $Ax1, Ax2, Ax3$ के उदाहरणों को स्टैक पर पुश करना, या मोडस पोनेंस (MP) लागू करना।
• तंत्र (Mechanism): MP क्रिया हिंडली-मिलनर यूनिफिकेशन (Hindley–Milner unification) का उपयोग करती है। यदि स्टैक का शीर्ष तत्व $X \to Y$ के साथ यूनिफाई होता है और उसके नीचे वाला तत्व $X$ के साथ यूनिफाई होता है, तो दोनों को पॉप किया जाता है, और $Y$ को पुश किया जाता है।
• सफलता (Success): एक प्रमाण तब सफल होता है जब स्टैक में एक एकल सूत्र होता है जो लक्षित लक्ष्य (target goal) से मेल खाता है।

2. स्व-पर्यवेक्षित प्रमेय खोज एल्गोरिथ्म

मुख्य योगदान एक एल्गोरिथ्म है जो प्रमाण खोज (proof search) और उपयोगी-प्रमेय निष्कर्षण (useful-theorem extraction) के बीच बारी-बारी से कार्य करता है, जिससे प्रमेयों की एक लाइब्रेरी बनाई जाती है जो भविष्य की खोज के लिए लेम्मा (lemmas) के रूप में कार्य करती है।

A. लक्ष्य-आधारित नीति सीखना (Goal-Conditioned Policy Learning)

एजेंट वर्तमान स्टैक $S$ और लक्ष्य $g$ दिए जाने पर अगली क्रिया की भविष्यवाणी करने के लिए एक नीति $\pi_\theta(A|S, g)$ सीखता है।

• हिस्टोरिकल लर्निंग (Hindsight Learning): एक खोज एपिसोड के दौरान, कोई भी अवस्था जहाँ स्टैक में एक एकल सूत्र $f_t$ होता है, उसे "पहुंचा गया प्रमेय" (reached theorem) माना जाता है, चाहे वह मूल लक्ष्य ही क्यों न हो।
• प्रशिक्षण संकेत (Training Signal): $f_t$ तक पहुँचने वाला एक्शन प्रीफिक्स (action prefix) $f_t$ के प्रमाण के रूप में माना जाता है। इन प्रीफिक्सों को क्रॉस-एन्ट्रॉपी लॉस के माध्यम से नीति को अपडेट करने के लिए प्रशिक्षण सेट $D_{train}$ में जोड़ा जाता है।
• लक्ष्य बफर ($G$): एक बफर खोजे गए प्रमेयों को बनाए रखता है। एजेंट आगामी खोज एपिसोड के लिए $G$ से लक्ष्यों को समान रूप से नमूना (sample) लेता है, जो प्रभावी रूप से अपने स्वयं के करिकुलम को बूटस्ट्रैप करता है।

B. उपयोगी प्रमेयों का निष्कर्षण

लाइब्रेरी को तुच्छ या रेडंडेंट (redundant) प्रमेयों से भरने से रोकने के लिए, एल्गोरिथ्म दो मानदंडों के आधार पर खोजे गए प्रमेयों को फ़िल्टर करता है:

1. व्यापकता (Generality): प्रमेयों को उन प्रमेयों को हटाने के लिए फ़िल्टर किया जाता है जो अन्य उम्मीदवारों के केवल विशिष्ट रूप (specializations) हैं। सिस्टम केवल "न्यूनतम" तत्वों को रखता है जो फॉर्मूला प्रतिस्थापन द्वारा परिभाषित आंशिक क्रम (partial order) के तहत आते हैं (अर्थात, सबसे सामान्य रूपों को रखना)।
2. पुनः सिद्ध करने की क्षमता (Reprovability): सिस्टम अनुमान लगाता है कि वर्तमान नीति द्वारा किसी प्रमेय को कितनी बार पुनः सिद्ध किया जा सकता है। एक बेयसियन पोस्टीरियर मीन (Beta(1,1) प्रायर) का उपयोग करते हुए, यह उन प्रमेयों को प्राथमिकता देता है जो खोजे तो गए हैं लेकिन जिन्हें विश्वसनीय रूप से पुनः सिद्ध करना कठिन है। ये "कठिन-से-सिद्ध" प्रमेय मूल्यवान हैं क्योंकि उन्हें लेम्मा के रूप में जोड़ने से कठिन प्रमाण पथ संकुचित (compress) हो जाते हैं।

C. बहु-पीढ़ी लाइब्रेरी विस्तार (Multi-Generation Library Expansion)

यह प्रक्रिया पीढ़ियों (generations) में संचालित होती है:

1. नीति सीखना (Policy Learning): वर्तमान एक्शन स्पेस (शुरुआत में केवल स्वयंसिद्ध और MP) पर नीति को प्रशिक्षित करें।
2. निष्कर्षण (Extraction): व्यापकता और पुन: सिद्ध करने की क्षमता के आधार पर उपयोगी प्रमेयों की पहचान करें।
3. एक्शन स्पेस का विस्तार (Action Space Expansion): निकाले गए प्रमेयों को नए लाइब्रेरी एक्शन (जैसे, $Thm_1, Thm_2$) के रूप में जोड़ें। चुने जाने पर, ये क्रियाएं संबंधित प्रमेय को स्टैक पर पुश करती हैं, जो एक पूर्व-सत्यापित लेम्मा के रूप में कार्य करती हैं।
4. पुनरावृत्ति (Iteration): इस प्रक्रिया को दोहराएं, जिससे एजेंट को नए, अधिक जटिल प्रमेय खोजने के लिए पहले से खोजे गए प्रमेयों का उपयोग करने की अनुमति मिलती है।

मुख्य योगदान

1. प्रारूपण (Formulation): प्रपोजिशनल थ्योरम प्रूविंग को सीधे हिल्बर्ट स्वयंसिद्धों और निष्कर्ष नियमों पर आधारित एक स्टैक-मशीन निर्णय प्रक्रिया के रूप में तैयार किया गया है, जो बाहरी प्रमाण कॉर्पोरा पर निर्भरता से बचता है।
2. एल्गोरिथ्म: एक स्व-पर्यवेक्षित प्रमेय-खोज एल्गोरिथ्म प्रस्तावित किया गया है जो केवल मूल नियमों से प्रमेय लाइब्रेरी विकसित करता है। यह निकाले गए प्रमेयों को आगामी प्रमाण खोज के लिए लेम्मा के रूप में पुन: उपयोग करता है।
3. स्वायत्त खोज: एजेंट ने हजारों प्रमेयों की खोज की और मानव-लिखित बेंचमार्क समस्याओं के लिए प्रमाण खोजे, जिसमें प्रशिक्षण के लिए किसी मानव पूर्व-ज्ञान का उपयोग नहीं किया गया।
4. स्थानांतरणीयता (Transferability): निकाले गए प्रमेय प्रभावी बाहरी ज्ञान के रूप में कार्य करते हैं, जो प्रॉम्प्ट लेम्मा के रूप में प्रदान किए जाने पर बाहरी LLMs के प्रमाण प्रदर्शन में काफी सुधार करते हैं।

प्रयोगात्मक परिणाम

1. प्रमेय खोज और कवरेज

• विकास: खोजे गए प्रमेयों की संख्या छह पीढ़ियों में बढ़ती है, जो एजेंट की अपनी ज्ञान आधार को स्वायत्त रूप से विस्तारित करने की क्षमता को प्रदर्शित करती है।
• बेंचमार्क प्रदर्शन: एजेंट मानव-लिखित बेंचमार्क सेट (क्लीन के टेक्स्टबुक से लिया गया) के 30% के लिए हिल्बर्ट-सिस्टम प्रमाण सफलतापूर्वक खोजता है।
• तुलना: जबकि GPT-5-high (सबसे मजबूत बेसलाइन) इन बेंचमार्क पर बिना सहायता के केवल ~23% सटीकता प्राप्त करता है, एजेंट की 30% प्रमाण खोजने की क्षमता यह दर्शाती है कि वह गैर-तुच्छ प्रमाण खोजता है जो मानव गणितीय दृष्टिकोण से सार्थक हैं।

2. LLM तर्क पर प्रभाव

• प्रॉम्प्ट लेम्मा (Prompt Lemmas): जब निकाले गए प्रमेयों को GPT-4o और GPT-5 वेरिएंट्स को प्रॉम्प्ट लेम्मा के रूप में दिया जाता है, तो बेंचमार्क समस्याओं पर उनकी प्रमाण सफलता दर काफी बढ़ जाती है।
• गुणात्मक विश्लेषण:
  • कुछ खोजे गए प्रमेय प्रसिद्ध सिद्धांतों (जैसे, विस्फोट का सिद्धांत, $\neg A \to (A \to B)$) के अनुरूप हैं, जो आसानी से व्याख्या योग्य हैं।
  • अन्य (जैसे, जटिल इम्पलीकेशन लिफ्टिंग) मनुष्यों के लिए तुरंत स्पष्ट नहीं हैं लेकिन LLM प्रमाणों में सहायक ज्ञान के रूप में प्रभावी ढंग से कार्य करते हैं।
  • यह इंगित करता है कि एजेंट ऐसे उपयोगी लेम्मा सामने ला सकता है जिन्हें मनुष्यों ने स्पष्ट रूप से प्रदान नहीं किया था, और ये लेम्मा विभिन्न तर्क संरचनाओं (एजेंट से LLM तक) में स्थानांतरित होने योग्य हैं।

महत्व और दावे

यह शोध इस प्रमाण को प्रदान करने का दावा करता है कि मानव-प्रदत्त प्रमेय पुस्तकालयों पर निर्भर हुए बिना उपयोगी प्रमेय खोज (proof search) से उभर सकते हैं।

• स्व-विकसित AI (Self-Evolving AI): यह कार्य गणित के लिए स्व-विकसित AI सिस्टम की ओर एक मार्ग का सुझाव देता है जो प्रमाण खोज के माध्यम से अपने औपचारिक ज्ञान को स्वायत्त रूप से विस्तारित कर सकते हैं और यह सुनिश्चित कर सकते हैं कि प्रत्येक खोज औपचारिक रूप से सत्यापन योग्य है।
• औपचारिक सत्यापन (Formal Verifiability): LLMs के विपरीत जो गलत लेकिन प्रशंसनीय लगने वाले कथनों की कल्पना (hallucinate) कर सकते हैं, एजेंट की खोजें हिल्बर्ट प्रणाली के स्वयंसिद्धों और निष्कर्ष नियमों पर सख्ती से आधारित हैं।
• विनम्रता (Modesty): लेखक सामान्य तर्क में अत्याधुनिक (state-of-the-art) LLMs को पछाड़ने का दावा नहीं करते हैं। इसके बजाय, वे एक सीमित, औपचारिक सेटिंग में, यह प्रदर्शित करते हैं कि एक एजेंट अपने स्वयं के ज्ञान को खोजने और उपयोग करने के लिए सीख सकता है जो उन्नत LLMs के लिए भी कठिन समस्याओं को हल करने में सक्षम है, और यह स्व-खोजा गया ज्ञान बाहरी प्रणालियों को सशक्त बना सकता है।

यह अध्ययन एक एकल स्वयंसिद्ध प्रणाली (हिल्बर्ट प्रपोजिशनल लॉजिक) तक सीमित है, लेकिन लेखक मानते हैं कि यह ढांचा फर्स्ट-ऑर्डर लॉजिक या सेट थ्योरी जैसे समृद्ध सिस्टम के लिए सामान्यीकरण योग्य है, जो भविष्य के कार्य के लिए एक दिशा बनी हुई है।