Ensuring Logic in the Fog: Sound POMDP Synthesis with LTL Objectives

तकनीकी सारांश: कोहरे में तर्क सुनिश्चित करना: LTL उद्देश्यों के साथ सुदृढ़ POMDP संश्लेषण

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

यह शोध पत्र उन स्वायत्त एजेंटों (autonomous agents) के संश्लेषण की चुनौती को संबोधित करता है जो अनिश्चित वातावरण में नेविगेट करने में सक्षम हों और लीनियर टेम्पोरल लॉजिक (LTL) द्वारा निर्दिष्ट जटिल कालिक बाधाओं (temporal constraints) का पालन करते हों। विशेष रूप से, यह पार्शियली ऑब्जर्वेबल मार्कोव डिसाइजन्स प्रोसेस (POMDPs) को लक्षित करता है जहाँ एजेंट को अनंत ट्रेसेस (infinite traces) पर एक LTL उद्देश्य को संतुष्ट करने की संभावना को अधिकतम करना होता है।

मुख्य कठिनाई POMDPs के लिए मात्रात्मक सत्यापन (quantitative verification) की अनिर्णीयता (undecidability) में निहित है। जबकि पूर्ण-क्षितिज (infinite-horizon) POMDPs में सरल पहुँच योग्यता (reachability) कार्यों के लिए भी इष्टतम नीति संश्लेषण अनिर्णय की स्थिति में होता है, व्यावहारिक दृष्टिकोण अक्सर सन्निकटन (approximations) पर निर्भर करते हैं। मौजूदा विधियाँ दो प्राथमिक सीमाओं का सामना करती हैं:

1. सीमित-ट्रेस प्रतिबंध (Finite-Trace Restrictions): कई दृष्टिकोण सीमित-ट्रेस LTL (LTLf) पर ध्यान केंद्रित करते हैं, जो समस्या को वन-शॉट पहुँच योग्यता (one-shot reachability) तक सीमित कर देता है, जो पूर्ण LTL द्वारा आवश्यक पुनरावृत्ति (recurrence) और निरंतरता (persistence) को पकड़ने में विफल रहता है।
2. आशावादी रिवॉर्ड शेपिंग (Optimistic Reward Shaping): जो दृष्टिकोण अवस्था-आधारित एक्सेप्टिंग मैक्सिमल एंड कंपोनेंट्स (AMECs) का उपयोग करके रिवॉर्ड प्राप्त करते हैं, वे आंशिक अवलोकन (partial observability) के तहत अक्सर विफल हो जाते हैं। वे उन विश्वास अवस्थाओं (belief states) को सकारात्मक रिवॉर्ड दे सकते हैं जहाँ कोई एकल विश्वास-आधारित नीति (एक ऐसी नीति जो विश्वास के सपोर्ट द्वारा साझा की जाती है) वास्तव में उद्देश्य को संतुष्ट नहीं कर सकती है। इसे "कॉमन पॉलिसी इश्यू" (common policy issue) कहा जाता है। इसके अलावा, विश्वास संक्रमणों (belief transitions) में संभाव्यता रिसाव (probability leakage) के कारण सटीक LTL संतुष्टि को रिवॉर्ड सिग्नल के रूप में एनकोड करना अनिर्णय योग्य है।

लक्ष्य एक नियतात्मक विश्वास-आधारित नीति $\pi$ को संश्लेषित करना है जो बिना किसी unverifiable आशावादी धारणाओं पर निर्भर हुए $Pr^\pi_M(\phi)$ की संतुष्टि की संभावना को अधिकतम करे।

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

लेखक एक उन्नत पार्शियली ऑब्जर्वेबल मोंटे कार्लो प्लानिंग (POMCP) ढांचे के भीतर एकीकृत एक सुदृढ़ रिवॉर्ड-शेपिंग तंत्र (sound reward-shaping mechanism) प्रस्तावित करते हैं। कार्यप्रणाली तीन चरणों में चलती है:

2.1 विश्वास सपोर्ट (Belief Supports) के माध्यम से सुदृढ़ सन्निकटन

यह पहचानते हुए कि सटीक संतुष्टि संभावना अनिर्णय योग्य है, यह दृष्टिकोण इस तथ्य का लाभ उठाता है कि लगभग-निश्चित संतुष्टि (almost-sure satisfaction) (संभावना 1) एक निर्णय योग्य गुण है। यह गुण केवल विश्वास समर्थन (belief support) (उन अवस्थाओं का सेट जिनका गैर-शून्य संभाव्यता है) पर निर्भर करता है, न कि सटीक संभाव्यता वितरण पर।

• निरंतर विश्वास स्थान को एक परिमित विश्वास-समर्थन MDP (BSMDP) में विविक्त (discretize) किया जाता है।
• BSMDP में अवस्थाएँ $\Theta \subseteq S^\times$ के विश्वास समर्थनों के अनुरूप होती हैं (जहाँ $S^\times$ उत्पाद POMDP की अवस्था स्थान है जो POMDT और LTL सूत्र के लिमिट-डिटरमिनिस्टिक बुची ऑटोमेटन (LDBA) से निर्मित होता है)।
• जीतने वाले सपोर्ट (Winning Supports) की पहचान की जाती है: अवस्थाओं के ऐसे उपसमुच्चय जिनसे बुची उद्देश्य को संभावना 1 के साथ संतुष्ट करने के लिए एक विश्वास-समर्थन नीति मौजूद है।

2.2 सुदृढ़ रिवॉर्ड शेपिंग

सभी जीतने वाले सपोर्ट खोजने की कम्प्यूटेशनल जटिलता से बचने के लिए, लेखक एक छंटनी रणनीति (pruning strategy) पेश करते हैं:

1. स्टेट AMECs तक प्रतिबंध: खोज को उन विश्वास समर्थनों तक सीमित किया जाता है जो स्टेट-स्पेस AMECs के साथ प्रतिच्छेद (intersect) करते हैं, जिससे एक उप-BSMDP बनता है।
2. BS-AMEC पहचान: एल्गोरिदम विश्वास-समर्थन एक्सेप्टिंग मैक्सिमल एंड कंपोनेंट्स (BS-AMECs) की पहचान करता है। एक BS-MEC केवल तभी 'एक्सेप्टिंग' है यदि एक विश्वास-समर्थन नीति मौजूद है जिसके तहत सभी अंतर्नि층 अवस्थाएँ जीतने वाली होती हैं। इसकी पुष्टि BS-MEC को स्टेट डायनेमिक्स के साथ युग्मित एक सहायक उत्पाद MDP का निर्माण करके की जाती है।
3. रिवॉर्ड असाइनमेंट: एक सुदृढ़ रिवॉर्ड फंक्शन $\hat{R}(b^\times)$ को प्रमाणित जीतने वाले सपोर्ट ($\hat{W}^\times$) के आधार पर परिभाषित किया गया है:
   • यदि विश्वास समर्थन पूरी तरह से एक प्रमाणित जीतने वाले सपोर्ट के भीतर है, तो रिवॉर्ड 1 है।
   • यदि विश्वास समर्थन "आंशिक रूप से जीतने वाला" (एक प्रमाणित जीतने वाले सपोर्ट को समाहित करता है) है, तो रिवॉर्ड उस जीतने वाले सपोर्ट को सौंपा गया विश्वास द्रव्यमान (belief mass) है।
   • अन्यथा, रिवॉर्ड 0 है।
   • यह वास्तविक संतुष्टि संभावना पर एक प्रमाणित निचला स्तर (certified lower bound) प्रदान करता है।

2.3 उन्नत POMCP प्लानिंग

मानक POMCP एल्गोरिदम को इन विश्वास-निर्भर रिवॉर्ड्स को समायोजित करने के लिए संशोधित किया गया है:

• पार्टिकल ट्रैकिंग (Particle Tracking): सर्च ट्री में प्रत्येक पार्टिकल को उसके ग्राउंड-ट्रुथ विश्वास समर्थन के साथ संवर्धित किया जाता है, जिसे इतिहास से पुनः प्राप्त किया जा सकता है, जिससे एल्गोरिदम व्यक्तिगत स्टेट पार्टिकल्स के बजाय सपोर्ट स्ट्रक्चर के आधार पर रिवॉर्ड का मूल्यांकन कर सकता है।
• समाप्ति और अन्वेषण (Termination and Exploration): एल्गोरिदम "प्रमाणित जीतने वाले" विश्वासों (जहाँ एजेंट एक सत्यापित नीति पर स्विच कर सकता है) और "आंशिक रूप से जीतने वाले" विश्वासों के बीच अंतर करता है। बाद वाले के लिए, UCB नियम वर्तमान निचले स्तर के साथ समाप्त होने और जीतने वाले सपोर्ट पर विश्वास द्रव्यमान बढ़ाने की संभावना के लिए आगे अन्वेषण करने के बीच संतुलन बनाता है।
• एनीटाइम प्रॉपर्टी (Anytime Property): प्लानर किसी भी समय समाप्त हो सकता है, जो एक ऐसी नीति लौटाता है जिसकी संतुष्टि की संभावना वर्तमान निचले स्तर के बराबर एक गारंटीकृत मान होती है।

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

1. सुदृढ़ रिवॉर्ड शेपिंग: यह शोध पत्र एक नवीन तंत्र पेश करता है जो प्रमाणित LTL संतुष्टि पर आधारित विश्वास-निर्भर रिवॉर्ड उत्पन्न करता है। अपने विश्वास समर्थन संरचनाओं का उपयोग करके, यह वास्तविक संतुष्टि संभावना का एक प्रमाणित निचला स्तर प्रदान करता है, जो स्टेट-आधारित आशावादी शेपिंग में निहित "कॉमन पॉलिसी इश्यू" से बचता है।
2. सुदृढ़ एनीटाइम सिंथेसिस: लेखक इन रिवॉर्ड नियमों को एक उन्नत POMCP एल्गोरिदम में एकीकृत करते हैं। दावा किया गया है कि यह POMDPs में पूर्ण LTL के लिए पहला सुदृढ़ और व्यावहारिक एनीटाइम सिंथेसिस एल्गोरिदम है, जो वास्तविक समय में विश्वसनीय विश्वास-आधारित नीतियां उत्पन्न करने में सक्षम है।
3. अनुभवजन्य सत्यापन (Empirical Validation): विधि का सत्यापन विविध LTL कार्यों (पहुँच योग्यता, निरंतरता और पुनरावृत्ति) के साथ मानक POMDP बेंचमार्क (Hallway, Rock Sample, Grid World) पर किया गया है। यह उन परिदृश्यों में प्रभावशीलता प्रदर्शित करता है जहाँ मौजूदा सॉल्वर (आशावादी शेपिंग या परिमित-अवस्था नियंत्रकों का उपयोग करने वाले) वैध नीतियां संश्लेषित करने या गलत संतुष्टि संभावना प्रदान करने में विफल रहते हैं।

4. परिणाम

विभिन्न मॉडल आकार और LTL उद्देश्यों (पहुँच योग्यता, निरंतरता और पुनरावृत्ति) वाले तीन डोमेन में प्रयोग किए गए:

• स्केलेबिलिटी (Scalability): दृष्टिकोण ने 40,000 से अधिक अवस्थाओं वाले उत्पाद मॉडलों के लिए नीतियां सफलतापूर्वक संश्लेषित कीं। सबसे बड़े उदाहरणों के लिए सुदृढ़ रिवॉर्ड निर्माण और प्लानिंग दोनों एक सिंगल CPU थ्रेड पर 190 सेकंड से कम में पूरे हुए।
• प्रदर्शन: विधि ने उन कार्यों में गैर-शून्य संतुष्टि संभावना प्राप्त की जहाँ आशावादी रिवॉर्ड शेपिंग विफल रही (जैसे कि प्रेरित खिलौना उदाहरण जहाँ आशावादी शेपिंग शून्य संतुष्टि की ओर ले गई)।
• दक्षता: पूर्ण LTL की जटिलता के बावजूद, सुदृढ़ रिवॉर्ड निर्माण कुशल रहा (उदाहरण के लिए, कई कार्यों के लिए < 1 सेकंड) क्योंकि प्रासंगिक जीतने वाले क्षेत्र (BS-AMECs) स्टेट स्पेस के छोटे उपसमुच्चयों तक ही सीमित थे।
• तुलना: "Rock Sample" डोमेन में, विधि ने उन कार्यों को प्रभावी ढंग से संभाला जिनमें अनंत-क्षितिज पुनरावृत्ति ($\phi_4, \phi_7$) की आवश्यकता थी, जबकि परिमित-मेमोरी दृष्टिकोण (FSCs) अक्सर इष्टतम मेमोरी आकार चुनने की अनिर्णयता के कारण नाजुक होते हैं।

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

शोध पत्र यह दावा करता है कि यह मात्रात्मक POMDT-LTL संश्लेषण की सैद्धांतिक अनिर्णयता और विश्वसनीय स्वायत्त एजेंटों की व्यावहारिक आवश्यकता के बीच के अंतर को पाटता है।

• सैद्धांतिक योगदान: यह स्थापित करता है कि जबकि सटीक संतुष्टि अनिर्णय योग्य है, एक सुदृढ़ निचला स्तर (sound lower bound) विश्वास-समर्थन संरचनाओं का उपयोग करके संगणना और अनुकूलित किया जा सकता है।
• व्यावहारिक प्रभाव: यह ऐसी नीतियां संश्लेषित करने के लिए एक ढांचा प्रदान करता है जो उनकी सफलता की संभावना में सत्यापन योग्य (verifiable) हैं, न कि उन ह्यूरिस्टिक्स पर निर्भर हैं जो अत्यधिक आशावादी हो सकते हैं।
• विनम्रता: लेखक स्वीकार करते हैं कि यह दृष्टिकोण एक निचला स्तर प्रदान करता है; इस निचले स्तर और वास्तविक संतुष्टि संभावना के बीच का "गैप" विश्वास संक्रमणों में निहित अनिर्णय योग्य रिसाव को दर्शाता है। पद्धति को एक "सुदृढ़ और व्यावहारिक" समाधान के रूप में प्रस्तुत किया गया है, न कि सामान्य समस्या की अनिर्णयता के पूर्ण समाधान के रूप में।
• भावी कार्य: लेखक सुरक्षित सुदृढ़ शिक्षण (safe reinforcement learning) के लिए मॉडल-फ्री सेटिंग्स में इस सुदृढ़ रिवॉर्ड तंत्र को विस्तारित करने की योजना बना रहे हैं, लेकिन उन्होंने अभी तक इसका दावा नहीं किया है।