तकनीकी सारांश: लार्ज लैंग्वेज मॉडल्स के साथ डेडलॉक-मुक्त संचार प्रोटोकॉल शोधन का विनिर्देश-निर्देशित संश्लेषण

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

वितरित सॉफ्टवेयर प्रणालियों (distributed software systems) में व्यवहार संबंधी शुद्धता सुनिश्चित करना एक महत्वपूर्ण चुनौती है, क्योंकि संचार प्रोटोकॉल में सूक्ष्म विसंगतियां अक्सर डेडलॉक (deadlocks) का कारण बनती हैं। जबकि लार्ज लैंग्वेज मॉडल्स (LLMs) ने सिंटैक्टिक रूप से सही कोड और स्थानीय सिमेंटिक गुणों (जैसे टाइप सुरक्षा) को संतुष्ट करने में दक्षता प्रदर्शित की है, उनमें वैश्विक व्यवहारिक शुद्धता (global behavioural correctness) सुनिश्चित करने के लिए तंत्रों का अभाव है, विशेष रूप से जटिल इंटरेक्शन परिदृश्यों में।

इसके विपरीत, मल्टीपार्टी सेशन टाइप्स (MPST) कठोर औपचारिक गारंटी प्रदान करते हैं, जिसमें संचार सुरक्षा और डेडलॉक फ्रीडम शामिल है, जो एसिंक्रोनस मल्टीपार्टी सबटाइपिंग (AMS) के माध्यम से प्राप्त होती है। AMS एक प्रोटोकॉल (सबटाइप) को एक अन्य (सुपरटाइप) को सुरक्षित रूप से बदलने की अनुमति देता है जबकि इन गुणों को बनाए रखता है। हालांकि, ऐसे वैध प्रोटोकॉल शोधन (refinements) का स्वचालित संश्लेषण गैर-तुच्छ है। समस्या इस तथ्य से और जटिल हो जाती है कि AMS आम तौर पर अनडिसाइडेबल (undecidable) है, और मौजूदा टूलचेन वैध प्रोटोकॉल शोधन के निर्माण के लिए सीमित समर्थन प्रदान करते हैं।

मूल शोध प्रश्न जिसका समाधान किया गया है वह है: एसिंक्रोनस मल्टीपार्टी सबटाइपिंग के तहत व्यवहारिक शुद्धता (विशेष रूप से डेडलॉक फ्रीडम) को बनाए रखते हुए प्रोटोकॉल शोधन को व्यवस्थित रूप से कैसे संश्लेषित किया जा सकता है?

2. कार्यप्रणाली: सिंट्रोपी (Syntropy) फ्रेमवर्क

लेखक सिंट्रोपी का प्रस्ताव करते हैं, जो वैध प्रोटोकॉल शोधन को संश्लेषित करने के लिए LLMs और औपचारिक विनिर्देशों (formal specifications) के बीच के अंतर को पाटने वाला एक फ्रेमवर्क है। यह फ्रेमवर्क दो पूरक मॉड्यूल से बना है: सिंट्रोपी-ट्रेन (Syntropy-Train) और सिंट्रोपी-जेन (Syntropy-Gen)।

2.1 सिंट्रोपी-ट्रेन: सबटाइप जनरेशन सीखना

• फाइन-ट्यूनिंग: लेखक LoRA (Low-Rank Adaptation) का उपयोग करके ओपन-सोर्स LLMs (जैसे Qwen2.5-Coder-7B) को फाइन-ट्यून करते हैं।
• डेटा निर्माण: प्रशिक्षण डेटासेट (supertype, subtype) के जोड़ों से बना है जो MPST साहित्य और सिंथेटिक बेंचमार्क से प्राप्त किए गए हैं। सबटाइप्स को एसिंक्रोनस सबटाइपिंग एल्गोरिदम पर आधारित ह्यूरिस्टिक प्रक्रियाओं के माध्यम से उत्पन्न किया जाता है और एक औपचारिक चेकर द्वारा सत्यापित किया जाता है।
• प्रतिनिधित्व (Representation): सेशन टाइप्स को एक मॉडल-फ्रेंडली, BNF-शैली के सिंटैक्स में परिवर्तित किया जाता है (जैसे कि सेंड के लिए स्पष्ट p!m; T, रिसीव के लिए p?m; T, और रिकर्सन के लिए REC_X_OPEN/CLOSE) ताकि अस्पष्टता को कम किया जा सके।
• प्रॉम्प्टिंग: प्रॉम्प्ट्स में रूपांतरण नियमों (Identity, RefA, RefB, RefIn, RefOut, Unfold) का वर्णन करने वाला सैद्धांतिक संदर्भ शामिल है ताकि मॉडल को संरचनात्मक रूप से वैध रूपांतरणों की ओर निर्देशित किया जा सके।
• लॉस फंक्शन: एक वेटेड टोकन-लेवल लॉस का उपयोग किया जाता है, जो सहायक लेबल के बजाय वैध सबटाइप अनुक्रमों को प्राथमिकता देता है।

2.2 सिंट्रोपी-जेन: टू-लेवल मॉनिटरिंग के साथ कन्सट्रेंड जनरेशन

यह सुनिश्चित करने के लिए कि LLM द्वारा निर्माण के माध्यम से गारंटीकृत सीमाओं से परे भी सिमेंटिक शुद्धता बनी रहे, सिंट्रोपी-जेन बीम सर्च जनरेशन प्रक्रिया के दौरान एक टू-लेवल मॉनिटरिंग रणनीति का उपयोग करता है:

• लेवल 1: टोकन-लेवल डेरिवेटिव चेक (प्रिफिक्स फिल्टरिंग):
  • प्रत्येक डिकोडिंग स्टेप पर, वर्तमान प्रिफिक्स को एक आंशिक सेशन ट्री में पार्स किया जाता है।
  • एक लाइटवेट, कोइंडक्टिव डेरिवेटिव चेक यह सत्यापित करता है कि क्या प्रिफिक्स अभी भी सुपरटाइप के वैध सबटाइप के रूप में विस्तारित किया जा सकता है।
  • यदि चेक विफल हो जाता है (अर्थात, कोई वैध पूर्णता मौजूद नहीं है), तो बीम को तुरंत हटा (prune) दिया जाता है। यह एक मोटे ओवर-एप्रोक्सिमेशन के रूप में कार्य करता है ताकि अयोग्य पथों को जल्दी हटाया जा सके।
• लेवल 2: वाइडनिंग-आधारित फिक्स्पॉइंट चेकर (अंतिम सत्यापन):
  • जब एक कैंडिडेट सीक्वेंस एंड-ऑफ-सीक्वेंस (EOS) टोकन तक पहुँचता है, तो इसे एक पूर्ण सेशन ट्री में पार्स किया जाता है।
  • एक पूर्ण सबटाइप चेकर (डेरिवेटिव रीजनिंग और रिकर्सन को संभालने के लिए वाइडनिंग ऑपरेटर्स पर आधारित) यह सत्यापित करता है कि क्या पूर्ण ट्री सुपरटाइप का एक वैध सबटाइप है।
  • यह चरण रूढ़िवादी (conservative) है; यह वैध सबटाइप्स को स्वीकार करता है लेकिन सामान्य समस्या की अनडिसाइडेबिलिटी के कारण कुछ वैध्स को अस्वीकार भी कर सकता है।

यह टू-लेवल डिज़ाइन कम्प्यूटेशनल दक्षता (लेवल 1) को सिमेंटिक कठोरता (लेवल 2) के साथ संतुलित करता है, यह सुनिश्चित करते हुए कि केवल वे ही कैंडिडेट रिटेन किए जाते हैं जो एसिंक्रोनस सबटाइपिंग संबंध को संतुष्ट करते हैं।

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

1. व्यवहारिक गारंटी के साथ LLM जनरेशन: एक नया दृष्टिकोण जो LLM को डेडलॉक फ्रीडम और संचार सुरक्षा की गारंटी के साथ MPST प्रोटोकॉल शोधन को संश्लेषित करने में सक्षम बनाता है।
2. विनिर्देश-निर्देशित प्रोटोकॉल शोधन: MPST विनिर्देशों का एक व्यवस्थित एनकोडिंग जो LLM जनरेशन को निर्देशित और प्रतिबंधित करता है, जिससे स्थानीय सिंटैक्टिक शुद्धता से आगे बढ़कर वैश्विक व्यवहारिक गुणों तक पहुँचा जा सके।
3. कन्सट्रेंट-इंटीग्रेटेड जनरेशन: एक टू-लेवल जनरेशन वर्कफ़्लो जो प्रिफिक्स फिल्टरिंग और उसके बाद के सत्यापन के माध्यम से प्रत्यक्ष रूप से बाधा सत्यापन (constraint validation) को संश्लेषण प्रक्रिया में एकीकृत करता है।
4. सिंट्रोपी फ्रेमवर्क और मूल्यांकन: उच्च वैधता और विविध, गैर-तुच्छ शोधन उत्पन्न करने की क्षमता का प्रदर्शन करने वाला व्यापक मूल्यांकन।

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

फ्रेमवर्क का मूल्यांकन कई LLMs (7B से 32B पैरामीटर्स) का उपयोग करके दो डेटासेट्स (साहित्य-व्युत्पन्न और सिंथेटिक) पर किया गया।

• वैधता (Validity): टू-लेवल मॉनिटरिंग का उपयोग करने पर सिंट्रोपी सभी मॉडलों में 95.6%–99.5% सिमेंटिक वैधता प्राप्त करती है, जबकि मॉनिटरिंग के बिना डायरेक्ट जनरेशन के लिए यह दर काफी कम (जैसे 60.4%) है। सिंटैक्टिक वैधता 95.4%–98.1% के बीच उच्च रहती है।
• विविधता (Diversity): फ्रेमवर्क संरचनात्मक रूप से भिन्न शोधन (reordering (RefA, RefB) और variance (RefIn, RefOut) रूपांतरण सहित) उत्पन्न करता है, न कि केवल तुच्छ बदलाव।
• डेटा स्केल: प्रदर्शन लगभग 9,500 ट्रेनिंग पेयर्स के आसपास संतृप्त (saturate) हो जाता है; इससे अधिक डेटा बढ़ाने से मामूली लाभ होता है।
• एब्लेशन स्टडीज (Ablation Studies):
  • टू-लेवल मॉनिटरिंग को हटाने से सिमेंटिक वैधता में भारी गिरावट (लगभग 60% तक) आती है, जो इसकी आवश्यकता की पुष्टि करती है।
  • प्रॉम्प्टिंग को हटाने से संरचनात्मक विविधता कम हो जाती है और सिमेंटिक वैधता भी थोड़ी कम हो जाती है, जो रूपांतरण कवरेज को निर्देशित करने में इसकी भूमिका को दर्शाती है।
• फ्रंटियर मॉडल्स के साथ तुलना: जबकि फ्रंटियर मॉडल्स (जैसे GPT-5.5, DeepSeek-V4-Pro) उन कुछ मामलों में उच्च वैधता के साथ वैध सबटाइप्स उत्पन्न कर सकते हैं जिन्हें वे कवर करते हैं, उनकी कवरेज अत्यंत सीमित (4%–18%) है। इसके विपरीत, सिंट्रोपी बेंचमार्क सूट में पूर्ण कवरेज प्रदान करती है।

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

पेपर का दावा है कि सिंट्रोपी LLMs की जेनेरेटिव क्षमताओं और वितरित सिस्टम की शुद्धता की कठोर आवश्यकताओं के बीच के अंतर को सफलतापूर्वक संबोधित करती है। औपचारिक विनिर्देशों (MPST) को सीधे जनरेशन लूप में एकीकृत करके, फ्रेमवर्क यह सुनिश्चित करता है कि संश्लेषित प्रोटोकॉल शोधन डेडलॉक-मुक्त और व्यवहारिक रूप से संगत हैं।

लेखक इस बात पर जोर देते हैं कि हालांकि फ्रंटियर LLMs आशाजनक हैं, लेकिन वर्तमान में उनमें व्यापक प्रोटोकॉल शोधन के लिए आवश्यक व्यवस्थित कवरेज की कमी है। सिंट्रोपी यह प्रदर्शित करती है कि फाइन-ट्यून किए गए मॉडल्स, जब औपचारिक सत्यापन बाधाओं के साथ जुड़े होते हैं, तो वे विविध और सही प्रोटोकॉल वेरिएंट को विश्वसनीय रूप से उत्पन्न कर सकते हैं जिन्हें मैन्युअल रूप से बनाना कठिन होता है। यह कार्य उन सुरक्षा-महत्वपूर्ण सॉफ्टवेयर इंजीनियरिंग कार्यों में LLMs को लागू करने की दिशा में एक कदम है जहाँ व्यवहारिक गारंटी अनिवार्य है।

स्वीकृत सीमाएँ:

• सिमेंटिक वैधता मेट्रिक एक ऐसे चेकर पर निर्भर है जो साउंड (sound) है लेकिन इनकम्प्लीट (incomplete) है (AMS की अनडिसाइडेबिलिटी के कारण); अतः, अस्वीकृत कैंडिडेट को निश्चित रूप से गलत सिद्ध नहीं किया जा सकता है।
• वर्तमान मूल्यांकन MPST के भीतर सबटाइप जनरेशन पर केंद्रित है, और अन्य औपचारिकताओं या जनरेशन कार्यों में सामान्यीकरण भविष्य का कार्य है।