Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers

शीर्षक: फ्लैट और पदानुक्रमित (Hierarchical) एजेंटिक थ्योरम प्रूवर के बीच घातीय नमूना जटिलता पृथक्करण (Exponential Sample Complexity Separation)

लेखक: शो सोनोडा, शुंटा अकीयमा, युया उएज़ातो
संबद्धता: साइबर एजेंट, RIKEN AIP
दिनांक: 7 मई, 2026

1. समस्या विवरण

हाल के एजेंटिक थ्योरम प्रूवर अक्सर अपघटन रणनीतियों (decomposition strategies) का उपयोग करते हैं—जैसे कि मध्यवर्ती लेम्मा (lemmas), प्रूफ स्केच, या सबगोल (subgoal) अपघटन उत्पन्न करना—टैक्टिक-स्तर की खोज में संलग्न होने से पहले। जबकि शास्त्रीय प्रमाण सिद्धांत (classical proof theory) यह सुझाव देता है कि लेम्मा निगमन (derivations) को छोटा कर सकते हैं, इन मध्यवर्ती चरणों को खोजने और सिद्ध करने की सांख्यिकीय शिक्षण लागत (statistical learning cost) एक खुला प्रश्न बना हुआ है। विशेष रूप से, यदि एक लेम्मा को सिद्ध करना स्वयं कठिन है, तो एक सीखा हुआ प्रूवर इसके लिए प्रयास क्यों करे?

यह शोध पत्र इस सांख्यिकीय शिक्षण समस्या को संबोधित करता है कि क्या एक पुन: प्रयोज्य प्रमाण संरचना (पदानुक्रमित) सीखना, पूरी तरह से इनलाइन किए गए प्रमाण ट्रेसेस (flat traces) से सीखने की तुलना में, एक निश्चित खोज बजट के भीतर सत्यापित प्रमाण खोजने की संभावना को बढ़ाता है। लेखक डेटा वितरण का विश्लेषण एक "टीचर" प्रूवर द्वारा प्रेरित होते हैं, जिसमें प्रारंभिक प्रमेय अवस्थाएं और सफल सत्यापित प्रमाण ट्रेसेस शामिल हैं, न कि सभी सूत्रों के लिए वर्स्ट-केस प्रमाण जटिलता (worst-case proof complexity)।

2. कार्यप्रणाली

लेखक थ्योरम प्रुरिंग को एक नियतात्मक परिमित-क्षित क्षितिज मार्कोव निर्णय प्रक्रिया (deterministic finite-horizon MDP) के रूप में मॉडल करते हैं, जहाँ अवस्थाएँ प्रमाण अवस्थाएँ हैं और क्रियाएँ टैक्टिक्स, अनुमान नियम (inference rules), या उच्च-स्तरीय अपघटन चालें हैं। वे सफल टीचर ट्रेसेस से ऑफलाइन इमिटेशन लर्निंग (imitation learning) का विश्लेषण तीन अलग-अलग सेटिंग्स के तहत करते हैं:

• सेटिंग 1 (फ्लैट - Flat): टीचर पूरी तरह से इनलाइन किए गए लो-लेवल प्रमाण ट्रेसेस उत्पन्न करता है। छात्र इन ट्रेसेस का अनुकरण करता है बिना किसी ग्राफ प्रेडिक्शन या मेमोइज़ेशन के। बार-बार आने वाले उप-प्रमाण (subproofs) प्रशिक्षण और परीक्षण डेटा में अलग, कॉपी किए गए उदाहरणों के रूप में दिखाई देते हैं।
• सेटिंग 2 (पदानुक्रमित - Hierarchical): टीचर एक उच्च-स्तरीय प्रमाण निर्देशित अचक्रीय ग्राफ (DAG) बनाता है जहाँ नोड्स पुन: प्रयोज्य प्रमाण ब्लॉकों का प्रतिनिधित्व करते हैं। छात्र एक ग्राफ प्रेडिक्टर और उच्च-स्तरीय ग्राफ क्रियाओं (ब्लॉक चुनना, विस्तार करना, पुनः उपयोग करना) और लो-लेवल स्थानीय समाधान के लिए नीतियां सीखता है। प्रशिक्षण डेटा इनलाइन किए गए ट्रेसेस से बना होता है, जिसके लिए छात्र को गुप्त (latent) प्रमाण DAG संरचना का अनुमान लगाना आवश्यक होता है।
• सेटिंग 3 (तुलना - Comparison): दोनों फ्लैट छात्र और पदानुक्रमित छात्र को एक ही स्रोत डेटा पर प्रशिक्षित किया जाता है जो पदानुक्रमित टीचर द्वारा उत्पन्न (इनलाइन ट्रेसेस) है। फ्लैट छात्र गुप्त ग्राफ संरचना को त्याग देता है, जबकि पदानुक्रमित छात्र इसे अनुमानित करता है। यह सेटिंग प्रतिनिधित्व (representation) के प्रभाव को आइसोलेट करती है।

विश्लेषण तीन प्रमुख मात्राओं पर निर्भर करता है:

1. $L$ (औसत लंबाई): एक सफल प्रमाण में निर्णयों की औसत संख्या।
2. $\eta$ (आंतरिक खोज हानि - Intrinsic Search Loss): वह संभाव्यता द्रव्यमान (probability mass) जो इसलिए खो जाता है क्योंकि टीचर की अगली क्रिया छात्र की शीर्ष-$k$ उम्मीदवार सूची में नहीं होती (स्थानीय पूर्वानुमान क्षमता)।
3. $e$ (अनुकरण त्रुटि - Imitation Error): छात्र की नीति और टीचर की नीति के बीच कुलबैक-लीब्लर (KL) डाइवर्जेंस।

लेखक छात्र की शीर्ष-$k$ सूची में टीचर की क्रियाओं के होने के आधार पर ट्सबाकोव-प्रकार की मार्जिन स्थिति (Tsyakobov-type margin condition) का उपयोग करते हैं और मान लेते हैं कि यदि टीचर की क्रियाएं छात्र की शीर्ष-$k$ सूची में शामिल हैं, तो खोज पूर्णता (search completeness) बनी रहती है।

3. मुख्य योगदान

• औपचारिकीकरण (Formalization): शोध पत्र सत्यापनकर्ता-निर्देशित थ्योरम प्रुरिंग को एक परिमित-क्षित क्षितिज MDP के रूप में औपचारिक रूप देता है और "सांख्यिकीय प्रमाण योग्यता" को प्रारंभिक अवस्थाओं के वितरण पर एक सत्यापित प्रमाण खोजने की औसत संभावना के रूप में परिभाषित करता है।
• सफलता गारंटी (Success Guarantees): लेखक दोनों फ्लैट छात्रों (इनलाइन ट्रेसेस पर प्रशिक्षित) और पदानुक्रमित छात्रों (पुन: प्रयोज्य DAGs की भविष्यवाणी करने के लिए प्रशिक्षित) के लिए परिमित-नमूना सफलता सीमाएं (finite-sample success bounds) प्राप्त करते हैं। ये सीमाएं निर्णयों की संख्या, आंतरिक शीर्ष-$k$ हानि और सीखी गई रैंकिंग त्रुटि को स्पष्ट रूप से अलग करती हैं।
• घातीय पृथक्करण (Exponential Separation): प्राथमिक सैद्धांतिक परिणाम पर्याप्त नमूना जटिलता (sample complexity) में घातीय पृथक्करण है। जब एक पुन: प्रयोज्य प्रमाण DAG को एक ट्री (tree) में सपाट (flatten) किया जाता है, तो समान उप-प्रमाणों को घातीय रूप से डुप्लिकेट किया जाता है। शोध पत्र सिद्ध करता है कि पदानुक्रमित शिक्षार्थी के लिए पर्याप्त-नमूना प्रमाण, फ्लैट शिक्षार्थी की तुलना में घातीय रूप से छोटा हो सकता है, भले ही उन्हें एक ही डेटा स्रोत पर प्रशिक्षित किया गया हो।
• गुप्त ग्राफ लर्निंग (Latent Graph Learning): शोध पत्र एक EM-शैली के पोस्टीरियर-वेटेड दृष्टिकोण का उपयोग करके इनलाइन किए गए ट्रेसेस से गुप्त प्रमाण DAGs को अनुमानित करने वाले पदानुक्रमित छात्र के लिए लर्निंग रेट प्रदान करता है, जिसमें ग्राफ प्रेडिक्शन त्रुटियों और पोस्टीरियर मिसमैच को ध्यान में रखा गया है।

4. परिणाम

मुख्य परिणाम थ्योरम 6 में प्रस्तुत किया गया है, जो लक्ष्य विफलता स्तर $\delta$ प्राप्त करने के लिए प्रमाणित पर्याप्त नमूना गणना ($\bar{N}$) की तुलना करता है:

• फ्लैट बाउंड: $\bar{N}_{flat}(\delta) \propto (L_{flat}/\delta)^{1/(p\gamma)}$
• पदानुक्रमित बाउंड: $\bar{N}_{hier}(\delta) \propto \max(L_{hi}, L_{lo}/\delta)^{1/(p\gamma)}$

जहाँ $L_{flat}$ अनफोल्डेड ट्रेस की लंबाई है और $L_{hier} = L_{hi} + L_{lo}$ पदानुक्रमित प्रतिनिधित्व की लंबाई है।

शोध पत्र प्रदर्शित करता है कि आकार/गहराई पैरामीटर $D$ द्वारा अनुक्रमित प्रमेयों के एक परिवार के लिए, यदि फ्लैटिंग प्रक्रिया प्रमाण की लंबाई को घातीय रूप से बढ़ा देती है ($L_{flat}/L_{hier} = \exp(\Omega(D))$), तो आवश्यक नमूनों का अनुपात भी घातीय रूप से बढ़ता है:
$$\bar{N}_{flat}(\delta) / \bar{N}_{hier}(\delta) \geq \exp(\Omega(D))$$

यह पृथक्करण इसलिए उत्पन्न होता है क्योंकि फ्लैट शिक्षार्थी को प्रत्येक उपस्थिति के लिए समान कठिन स्थानीय तर्क को स्वतंत्र रूप से सीखना पड़ता है, जबकि पदानुक्रमित शिक्षार्थी साझा ब्लॉक को एक बार सीखता है और उसका पुनः उपयोग करता है। पेपर कट-एलमिनेशन (cut-elimination) उदाहरण (परिशिष्ट G) का उपयोग यह दर्शाने के लिए करता है कि कैसे मध्यवर्ती लेम्मा को हटाने (फ्लैटिंग) से प्रमाण का आकार घातीय रूप से बढ़ सकता है, जिससे फ्लैट शिक्षार्थियों के लिए नमूना जटिलता बढ़ जाती है।

5. महत्व और दावे

शोध पत्र दावा करता है कि यह एक ठोस सांख्यिकीय तंत्र प्रदान करता है जो बताता है कि पदानुक्रमित प्रमाणिंग क्यों मदद करती है, जो वर्स्ट-केस प्रमाण जटिलता के तर्कों से भिन्न है। इसका महत्व यह पहचानना है कि अपघटन का लाभ केवल तार्किक निगमन को छोटा करने के बारे में नहीं है, बल्कि शिक्षार्थी पर सांख्यिकीय बोझ को कम करने के बारे में है।

• डेटा वितरण जागरूकता: परिणाम रेखांकित करता है कि सीखने की दक्षता डेटा वितरण की संरचना पर निर्भर करती है। यदि सफल प्रमाण मध्यवर्ती तर्कों का पुन: उपयोग करते हैं, तो एक पदानुक्रमित प्रतिनिधित्व इस साझाकरण को कैप्चर करता है, जबकि एक फ्लैट प्रतिनिधित्व इसे नष्ट कर देता है, जिससे रेडंडेंट (redundant) लर्निंग टास्क पैदा होते हैं।
• सीमाएँ: लेखक अपने दावों के प्रति विनम्र हैं। वे कहते हैं कि यह एक वर्स्ट-केस लोअर बाउंड नहीं है और यह उन फ्लैट शिक्षार्थियों को खारिज नहीं करता है जो पूर्ण कैनोनिकलाइजेशन (परफेक्ट रूप से समान उप-समस्याओं को पहचानना) प्राप्त कर सकते हैं। पृथक्करण विशेष रूप से तब लागू होता है जब फ्लैटिंग पुन: प्रयोज्य प्रमाण संरचना को नष्ट कर देती है और डेटा वितरण में ऐसे प्रमाण होते हैं जहाँ यह साझाकरण प्रचलित है।
• व्यावहारिक निहितार्थ: निष्कर्ष बताते हैं कि सत्यापनकर्ता-आधारित थ्योरम प्रुरिंग के लिए, पुन: प्रयोजable प्रमाण संरचनाओं (लेम्मा, सबगोल) की भविष्यवाणी करना सीखने से, एक दिए गए सफलता संभाव्यता को प्राप्त करने के लिए आवश्यक नमूना जटिलता को घातीय रूप से कम किया जा सकता है, बशर्ते कि ग्राफ प्रेडिक्टर उच्च संभाव्यता के साथ टीचर के सर्टिफिकेट को कवर कर सके।

शोध पत्र निष्कर्ष निकालता है कि लेम्मा को सिद्ध करने का "महंगा चक्कर" (expensive detour) सांख्यिकीय रूप से उचित है जब वे लेम्मा पुन: प्रयोज्य होते हैं, क्योंकि उन्हें एक बार सीखने की लागत, फ्लैट फ्रेमवर्क में उन्हें बार-बार पुनः खोजने की लागत से बहुत कम होती है।