⚡ electrical engineering

Learning Linear Temporal Specifications from Demonstrations with Uncertainty

यह शोध पत्र हैमिंग दूरी (Hamming distance) के माध्यम से ट्रेस अनिश्चितता को मॉडल करके और समस्या को सूडो-बुलियन ऑप्टिमाइज़ेशन (Pseudo-Boolean Optimization) में बदलकर, अनिश्चित प्रदर्शनों (demonstrations) से न्यूनतम लीनियर टेम्पोरल लॉजिक (LTL) विनिर्देशों को सीखने के लिए एक नवीन रूपरेखा प्रस्तुत करता है, जिससे शोर वाली स्थितियों में ग्राउंड-ट्रुथ सूत्रों को पुनः प्राप्त करने में मौजूदा विधियों से बेहतर प्रदर्शन किया जा सके।

मूल लेखक: Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oes

प्रकाशित 2026-07-14

📖 7 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oes

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक रोबोट को एक आदर्श दिन का वीडियो दिखाकर उसे व्यवहार करना सिखाने की कोशिश कर रहे हैं। आप चाहते हैं कि रोबोट यह नियम सीखे: "यदि कमरा गर्म है और उसमें कोई मौजूद है, तो AC चालू कर दें।" लेकिन यहाँ एक पेंच है: आपने जो वीडियो रिकॉर्ड किया है वह ग्लिच वाला (glitchy) है। शायद किसी सेंसर में खराबी आई, कोई फ्रेम खराब हो गया, या कोई माप थोड़ा गलत हो गया। रोबंतु वह संस्करण देख रहा है जो लगभग सही है, लेकिन जिसके कुछ हिस्से धुंधले और अनिश्चित हैं।

मौजूदा अधिकांश तरीके सख्त शिक्षकों की तरह हैं जो यह मान लेते हैं कि वीडियो एकदम सटीक है। यदि वीडियो दिखाता है कि कमरा ठंडा होने पर भी AC चालू हो गया, तो ये तरीके भ्रमित हो सकते हैं या इस गलती को समझाने के लिए अजीब, जटिल नियम बना सकते हैं। वे मान लेते हैं कि यह केवल एक "लेबलिंग" की गड़बड़ी है (जैसे बिल्ली को कुत्ता कहना), लेकिन वे इस बात पर ध्यान नहीं देते कि वीडियो स्वयं धुंधला या अधूरा हो सकता है।

यह शोध पत्र एक नया, अधिक उदार दृष्टिकोण पेश करता है जिसे Robust LTL Learning कहा जाता है। यह न तो यह मांग करता है कि वीडियो एकदम सही हो, बल्कि यह कहता है, "ठीक है, यह वीडियो धुंधला है। आइए इस वीडियो के उन सभी संभावित संस्करणों की कल्पना करें जो इस ग्लिच (glitch) का कारण बन सकते थे।"

"क्या होगा अगर" का बुलबुला (The "What-If" Bubble)

लेखक एक ग्लिच वाले वीडियो के चारों ओर संभावनाओं का एक "बुलबुला" बनाने के लिए हैमिंग डिस्टेंस (Hamming distance) नामक एक गणितीय उपकरण का उपयोग करते हैं। इसे एक सुरक्षा जाल की तरह समझें। यदि आपका रिकॉर्ड किया गया वीडियो स्टेप 3 पर AC चालू होने का दिखाता है, लेकिन आप जानते हैं कि सेंसर एक स्टेप पीछे या आगे हो सकता है, तो यह तरीका केवल स्टेप 3 को नहीं देखता। यह स्टेप 2, स्टेप 3 और स्टेप 4 को देखता है। यह "ट्रेस एस्टिमेट्स" (trace estimates) का एक समूह बनाता है—वे सभी संभावित तरीके जिनसे वह दिन वास्तव में घटित हुआ होगा, उस छोटी त्रुटि सीमा के भीतर।

बड़ा विचार यह है: हमें यह जानने की आवश्यकता नहीं है कि वीडियो का कौन सा संस्करण वास्तविक सत्य है। हमें बस एक ऐसा नियम खोजने की आवश्यकता है जो उस बुलबुले के भीतर के कम से कम एक संस्करण के लिए काम करता हो।

"समूह" का नियम (The "Group" Rule)

पुराने तरीके में, यदि एक वीडियो को "अच्छा व्यवहार" लेबल किया गया था, तो रोबोट को उस विशिष्ट वीडियो के लिए नियम का पूरी तरह से पालन करना होता था। यदि वीडियो शोरयुक्त (noisy) था, तो रोबोट विफल हो जाता था।

इस नए तरीके में, रोबोट संभावित वीडियोओं के पूरे समूह को देखता है। वह पूछता है, "क्या इस समूह का कोई भी संस्करण है जहाँ नियम लागू होता है?" यदि उत्तर हाँ है, तो रोबोट इसे स्वीकार कर लेता है। यह एक जासूस की तरह है जो जानता है कि एक गवाह समय बताने में थोड़ा भ्रमित हो सकता है। गवाह को बाहर निकालने के बजाय, जासूस कहता है, "जब तक संदिग्ध उस समय अवधि के दौरान इमारत में मौजूद था जिसका उल्लेख गवाह ने किया है, तब तक अलबी (alibi) मान्य है।"

परिणाम: एक करीब से नज़र (The Results: A Closer Look)

लेखकों ने इस विचार का परीक्षण एक हीटिंग, वेंटिलेशन और एयर कंडीशनिंग (HVAC) सिस्टम का उपयोग करके किया। उन्होंने एक वास्तविक नियम निर्धारित किया: "हमेशा, यदि कमरा गर्म है और उसमें कोई मौजूद है, तो अगले स्टेप में AC चालू होना चाहिए।"

फिर उन्होंने वास्तविक नियम को लिया और सेंसर त्रुटियों को सिम्युलेट करने के लिए डेटा को जानबूझकर बिगाड़ दिया, जिससे अनिश्चितता की खिड़कियाँ पैदा हुईं जहाँ वेरिएबल्स को बदल दिया गया। उन्होंने इस नए तरीके की तुलना दो अन्य दृष्टिकोणों से की:

Flie: एक मानक तरीका जो अनिश्चितता को अच्छी तरह से नहीं संभाल पाता।
Modified Flie: एक सुधारा हुआ संस्करण जो कुछ समस्याओं को ठीक करने की कोशिश करता है लेकिन अभी भी यह मानता है कि डेटा काफी हद तक सही है।

क्या हुआ?

Flie अक्सर जटिल समय-आधारित नियमों को पूरी तरह से छोड़ देता था और सरल लेकिन गलत पैटर्न सीख लेता था जैसे "यदि यह गर्म नहीं है, तो यह बाद में गर्म होगा" (जिसका कोई अर्थ नहीं है)।
Modified Flie बेहतर था, कभी-कभी नियम के कुछ हिस्सों को पकड़ लेता था, लेकिन यह अक्सर कारण-और-प्रभाव (cause-and-effect) को उल्टा कर देता था। यह सीख लेता था कि "यदि AC चालू है, तो कमरे में कोई मौजूद है," जो कि सत्य का उल्टा है।
Robust Method (लेखकों का नया दृष्टिकोण) अधिकांश मामलों में सही टेम्पोरल स्ट्रक्चर (समय संबंधी संरचना) को पुनः प्राप्त करने में सफल रहा, लेकिन इसने अक्सर कारण-संबंधी दिशा (causal direction) को उलट दिया। उदाहरण के लिए, जबकि वास्तविक नियम है "उपस्थिति + गर्मी → AC," रोबस्ट विधि अक्सर "AC → उपस्थिति" सीख लेती थी। हालाँकि, इस उलटाव के बावजूद, यह अन्य तरीकों की तुलना में इच्छित सिस्टम व्यवहार के बहुत करीब था क्योंकि इसने महत्वपूर्ण समय संबंधों (जैसे "अगला स्टेप") को सफलतापूर्वक संरक्षित किया जो अन्यों ने मिस कर दिए थे।

हालाँकि, यहाँ एक ट्रेड-ऑफ (समझौता) है। लेख में उल्लेख है कि इस नए तरीके को गणना करने में अधिक समय लगता है। HVAC परीक्षणों में, जबकि अन्य तरीकों ने लगभग 0.8 से 4.4 सेकंड का समय लिया, रोबस्ट तरीके ने जटिलता के आधार पर 6.5 से 73.1 सेकंड तक का समय लिया। यह ऐसा है जैसे रोबोट केवल अनुमान लगाने के बजाय, यह सुनिश्चित करने के लिए कि वह सही हो, एक गहरी सांस ले रहा है और अधिक गहराई से सोच रहा है।

इसका क्या अर्थ है (और क्या नहीं है)

यह शोध पत्र स्पष्ट रूप से इस विचार को खारिज करता है कि हम शोर (noise) को अनदेखा कर सकते हैं या मान सकते हैं कि डेटा एकदम सही है। यह तर्क देता है कि पिछले तरीके विफल होते हैं क्योंकि वे अनिश्चित डेटा को एक साधारण लेबलिंग त्रुटि के रूप में देखते हैं, न कि एक भ्रष्ट सिग्नल के रूप में।

लेखक सुझाव देते हैं कि उनका तरीका वास्तविक दुनिया के अनुप्रयोगों के लिए अधिक आशाजनक दिशा है जहाँ सेंसर विफल होते हैं। वे सिमुलेशन (सिंथेटिक डेटा और HVAC उदाहरण का उपयोग करके) के माध्यम से दिखाते हैं कि उनका तरीका ऐसे फॉर्मूले प्राप्त करता है जो वर्तमान अत्याधुनिक तरीकों की तुलना में "सत्य के अधिक निकट" हैं, भले ही तर्क हमेशा पूर्ण न हो।

वे यह दावा नहीं करते कि उन्होंने समस्या को पूरी तरह से हल कर दिया है। वास्तव में, वे स्वीकार करते हैं कि उनके परिणाम "प्रारंभिक" हैं। उन्होंने यह साबित नहीं किया है कि यह हर संभव रोबोट या वास्तविक दुनिया की आपदा परिदृश्य में काम करेगा। उन्होंने केवल यह दिखाया है कि इन विशिष्ट परीक्षणों में, संभावनाओं के "बुलबुले" को देखना अकेले धुंधले वीडियो को देखने की तुलना में रोबोट को बेहतर नियम सीखने में मदद करता है।

इसलिए, यदि आप एक जिज्ञासु किशोर हैं जो एक ऐसा रोबोट बना रहे हैं जिसे ग्लिच वाले सेंसरों के साथ काम करना है, तो यह शोध पत्र सुझाव देता है: केवल वीडियो पर भरोसा न करें। उन सभी तरीकों की कल्पना करें जिनसे यह अलग हो सकता था, एक ऐसा नियम खोजें जो उन संभावनाओं में से कम से कम एक में फिट बैठता हो, और आपका रोबोट एक खराब पिक्सेल के कारण दीवार से टकराने से बचेगा।

तकनीकी सारांश: अनिश्चितता के साथ प्रदर्शनों से लीनियर टेम्पोरल स्पेसिफिकेशन सीखना

समस्या विवरण

यह शोध पत्र प्रदर्शनों (demonstrations) से लीनियर टेम्पोरल लॉजिक (LTL) स्पेसिफिकेशन को अनुमानित करने की चुनौती को संबोधित करता है, जो सुरक्षा-महत्वपूर्ण डोमेन (जैसे कि रोबोटिक्स, स्वायत्त वाहन) में महत्वपूर्ण है। जबकि मौजूदा दृष्टिकोण, जो सकारात्मक और नकारात्मक ट्रेसेस (traces) से LTL सीखने के लिए उपयोग किए जाते हैं, इस धारणा पर आधारित हैं कि ट्रेसेस स्वयं सही ढंग से कैप्चर किए गए हैं और वे केवल लेबल मिसक्लासिफिकेशन त्रुटियों को ध्यान में रखते हैं, वास्तविक दुनिया का डेटा अक्सर ट्रेस अनिश्चितता (trace uncertainty) से ग्रस्त होता है। यह अनिश्चितता सेंसर दोषों, माप त्रुटियों, डेटा हानि, या संचार विलंब से उत्पन्न होती है, जिसके परिणामस्वरूप दूषित, अपूर्ण, या असंगत ट्रेसेस प्राप्त होते हैं।

वर्तमान विधियाँ, जो देखे गए ट्रेसेस को 'ग्राउंड ट्रुथ' मानती हैं, उन मामलों में सटीक स्पेसिफिकेशन प्राप्त करने में विफल रहती हैं जहाँ ट्रेस की सामग्री स्वयं अनिश्चित होती है। लेखक रोबस्ट LTL लर्निंग प्रॉब्लम को परिभाषित करते हैं: एक न्यूनतम LTL फॉर्मूला खोजना जो देखे गए ट्रेसेस में पूर्ण सटीकता मानने के बजाय, देखे गए ट्रेसेस में सीमित अनिश्चितता के बावजूद सिस्टम व्यवहार की व्याख्या कर सके।

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

प्रस्तावित ढांचा ट्रेस अनिश्चितता को मॉडल करता है और इसे एक स्यूडो-बुलियन ऑप्टिमाइज़ेशन (Pseudo-Boolean Optimization) समस्या में एकीकृत करता है। कार्यप्रणाली निम्नलिखित चरणों के माध्यम से आगे बढ़ती है:

1. ट्रेस अनिश्चितता का मॉडलिंग

लेखक एक देखे गए ट्रेस और संभावित "सही" ट्रेसेस के बीच हैमिंग डिस्टेंस (Hamming distance) का उपयोग करके अनिश्चितता को मापते हैं।

ट्रेस एस्टीमेट ग्रुप ( $C^k_{tr}$ ): एक देखे गए ट्रेस $tr $और अनिश्चितता सीमा$ k $को देखते हुए, ट्रेस एस्टीमेट का सेट उन सभी ट्रेसेस को शामिल करता है जो$ tr $से$ k$ हैमिंग डिस्टेंस के भीतर हैं।
धारणा: यह माना गया है कि वास्तविक सिस्टम व्यवहार इस अनिश्चितता समूह के भीतर के ट्रेसेस में से एक है, न कि अनिवार्य रूप से देखा गया ट्रेस स्वयं।

2. रोबस्ट लर्निंग फॉर्मूलेशन

लर्निंग समस्या को व्यक्तिगत ट्रेसेस के बजाय इन समूहों को संभालने के लिए पुनर्गठित किया गया है:

ग्रुप मिसक्लासिफिकेशन: इस ढांचे में प्रत्येक देखे गए ट्रेस द्वारा फॉर्मूला को संतुष्ट करने की आवश्यकता के बजाय, यह आवश्यक है कि प्रत्येक अनिश्चितता समूह से कम से कम एक ट्रेस (सकारात्मक ट्रेसेस के लिए) फॉर्मूला को संतुष्ट करे, और प्रत्येक नकारात्मक अनिश्चितता समूह से कम से कम एक ट्रेस फॉर्मूला को संतुष्ट न करे।
लॉस फंक्शन: एक ग्रुप मिसक्लासिफिकेशन लॉस फंक्शन, $\ell_g$ , परिभाषित किया गया है। यह उन मामलों को दंडित करता है जहाँ अनिश्चितता समूह में कोई भी ट्रेस सीखे गए फॉर्मूला के अनुरूप नहीं होता है।

3. एल्गोरिद्मिक कार्यान्वयन (Pseudo-Boolean Optimization)

समस्या को एक प्रपोजिशनल फॉर्मूला $\Phi$ में एनकोड किया जाता है और Max-SMT (विशेष रूप से स्यूडो-बुलियन ऑप्टिमाइज़ेशन) का उपयोग करके हल किया जाता है। यह फॉर्मूला चार बाधा श्रेणियों (constraint categories) से बना है:

सिंटैक्स कंस्ट्रेंट्स ( $\Phi_{syn}$ ): यह सुनिश्चित करता है कि सीखा गया फॉर्मूला वैध LTL व्याकरण (सिंटैक्स ट्री के रूप में प्रतिनिधित्व) का पालन करता है।
सिमेंटिक कंस्ट्रेंट्स ( $\Phi_{sem}$ ): ट्रेसेस और LTL फॉर्मूला के बीच संतुष्टि संबंध (satisfaction relation) को एनकोड करता है।
सिलेक्शन कंस्ट्रेंट्स ( $\Phi_{sel}$ ): अनिश्चितता समूह से किसी विशिष्ट ट्रेस एस्टीमेट को चुनने के लिए बाइनरी वेरिएबल्स $z_{tr}$ पेश करता है। यदि एक ट्रेस चुना जाता है ( $z_{tr}=1$ ), तो उसे फॉर्मूला को संतुष्ट करना होगा (या संतुष्ट नहीं करना होगा)।
ग्रुप कंस्ट्रेंट्स ( $\Phi_{grp}$ ): एक सॉफ्ट कंस्ट्रेंट जो यह लागू करता है कि प्रत्येक देखे गए ट्रेस के लिए, उसके अनिश्चितता समूह से कम से कम एक ट्रेस एस्टीमेट चुना जाना चाहिए ( $z_{tr'}=1$ )।

उद्देश्य ग्रुप मिसक्लासिफिकेशन लॉस को कम करना (ट्रेसेस की संख्या के आधार पर भारित) है जबकि सभी हार्ड कंस्ट्रेंट्स को पूरा करना है। इसे एक स्यूडो-बुलियन ऑब्जेक्टिव फंक्शन को कम करके हल किया जाता है।

मुख्य योगदान

नया समस्या प्रारूप (Novel Problem Formulation): यह पेपर "रोबस्ट LTL लर्निंग प्रॉब्लम" पेश करता है, जो स्पष्ट रूप से लेबल शोर के बजाय ट्रेस सामग्री (क्षरण/अपूर्णता) में अनिश्चितता को संबोधित करता है।
अनिश्चितता मॉडलिंग: हैमिंग डिस्टेंस का उपयोग करके ट्रेस एस्टीमेट समूहों को परिभाषित करना सिस्टम को किसी भी अवलोकन के लिए संभावित "वास्तविक" व्यवहारों की एक श्रृंखला पर विचार करने की अनुमति देता है।
ग्रुप-आधारित बाधाएं: ढांचा यह सुनिश्चित करता है कि प्रत्येक अनिश्चितता समूह से कम से कम एक ट्रेस सीखा गया फॉर्मूला के अनुरूप होना चाहिए, जिससे लर्निंग एल्गोरिदम को दूषित डेटा पॉइंट्स द्वारा गुमराह होने से रोका जा सके।
ऑप्टिमाइज़ेशन दृष्टिकोण: रोबस्ट लर्निंग समस्या को एक समकक्ष स्यूडो-बुलियन ऑप्टिमाइज़ेशन समस्या में बदलना, जिसे SMT सॉल्वर (जैसे Z3) के माध्यम से हल किया जा सकता है।

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

लेखकों ने अपने मेथड का मूल्यांकन दो बेंचमार्क का उपयोग करके स्टेट-ऑफ-द-आर्ट SAT-आधारित लर्निंग दृष्टिकोणों (विशेष रूप से "Flie" एल्गोरिदम और एक "Modified Flie" वेरिएंट जो यूजर कंस्ट्रेंट्स को शामिल करता है) के विरुद्ध किया:

HVAC कंट्रोल सिस्टम: तापमान, अधिभोग (occupancy), और AC स्थिति के लिए एटॉमिक प्रपोजिशन के साथ एक वास्तविक दुनिया का परिदृश्य।
सिंथेटिक LTLf पैटर्न: विभिन्न ग्राउंड-ट्रुथ LTL फॉर्मूलों के साथ अनिश्चितता इंजेक्ट करने वाले प्रयोग।

निष्कर्ष:

सटीकता (Accuracy): प्रस्तावित रोबस्ट लर्निंग विधि ने ऐसे स्पेसिफिकेशन्स रिकवर किए जो मौजूदा विधियों की तुलना में ग्राउंड-ट्रुथ फॉर्मूलों के अधिक निकट थे।
टेम्पोरल संबंध (Temporal Relationships): जबकि मानक विधियाँ (Flie) अक्सर टेम्पोरल डिपेंडेंसी को कैप्चर करने में विफल रहीं या अनिश्चितता के तहत स्प्यूरियस (spurious) संबंध सीख लिया, और मॉडिफाइड फ्लिए (Modified Flie) ने आंशिक रूप से संबंधों को रिकवर किया लेकिन अक्सर कारण दिशाओं (causal directions) को उलट दिया, रोबस्ट विधि ने महत्वपूर्ण टेम्पोरल संरचनाओं (जैसे ग्लोबल कंडीशंस और इमीडिएट डिपेंडेंसीज) को लगातार सुरक्षित रखा।
कंप्यूटेशनल लागत: रोबस्ट विधि को बेसलाइन्स की तुलना में अधिक कंप्यूटेशन समय की आवश्यकता हुई। लेखक इसका श्रेय स्टैंडर्ड Max-SAT की तुलना में स्यूडो-बुलियन ऑप्टिमाइज़ेशन की बढ़ी हुई जटिलता को देते हैं।

महत्व और दावे

यह पेपर दावा करता है कि इसका ढांचा सैद्धांतिक LTL लर्निंग और व्यावहारिक परिदृश्यों के बीच के अंतर को पाटता है जहाँ डेटा अपूर्ण होता है। इनपुट ट्रेसेस शोरपूर्ण या अधूरे होने के बावजूद, अनिश्चितता को प्रभावी ढंग से कैप्चर करके, यह विधि न्यूनतम, व्याख्या योग्य LTL फॉर्मूलों को इन्फर करने में सक्षम बनाती है जो वास्तविक सिस्टम व्यवहार को दर्शाते हैं।

लेखक इस कार्य को सुरक्षा-महत्वपूर्ण प्रणालियों में अधिक मजबूत औपचारिक सत्यापन (formal verification) और कंट्रोलर सिंथेसिस की दिशा में एक कदम के रूप में देखते हैं। वे विनम्रतापूर्वक नोट करते हैं कि हालांकि परिणाम प्रारंभिक हैं, फिर भी यह दृष्टिकोण वर्तमान स्टेट-ऑफ-द-आर्ट विधियों की तुलना में एक "अधिक सिद्धांतवादी और आशाजनक दिशा" प्रदान करता है जो ट्रेस अखंडता (trace integrity) को मानती हैं। भविष्य के कार्य के रूप में सीखे गए स्पेसिफिकेशन्स की ग्राउंड ट्रुथ के विरुद्ध मात्रात्मक तुलना करने के लिए औपचारिक दूरी मेट्रिक्स (formal distance metrics) का विकास पहचाना गया है।