Formally Verified Code Synthesis for Structured Data Translation in a Medical Internet of Things

तकनीकी सारांश: स्ट्रक्चर्ड डेटा ट्रांसलेशन के लिए औपचारिक रूप से सत्यापित कोड संश्लेषण (Formally Verified Code Synthesis)

समस्या विवरण
मौजूदा मेडिकल इंटरनेट ऑफ थिंग्स (MIoT) नेटवर्क में नए चिकित्सा उपकरणों के एकीकरण के साथ महत्वपूर्ण चुनौतियाँ आती हैं, विशेष रूप से तब जब मानव सॉफ्टवेयर विकास विशेषज्ञता उपलब्ध नहीं होती है। हालांकि लार्ज लैंग्वेज मॉडल्स (LLMs) शक्तिशाली कोड संश्लेषण क्षमताएं प्रदान करते हैं, वे मतिभ्रम (hallucinations) और सूक्ष्म कमजोरियों के प्रति संवेदनशील होते हैं, जिससे वे सुरक्षा-महत्वपूर्ण स्वास्थ्य सेवा डोमेन के लिए अविश्वसनीय हो जाते हैं। मुख्य समस्या जो यहाँ संबोधित की गई है वह है विश्वसनीय, भरोसेमंद ट्रांसलेशन कोड को स्वचालित रूप से उत्पन्न करने की आवश्यकता, जो डिवाइस-विशिष्ट प्रारूपों (जैसे, कस्टम JSON स्कीमा) को मानकीकृत इंटरऑपरेबिलिटी प्रारूपों (जैसे, FHIR) में परिवर्तित कर सके, बिना किसी मैनुअल सत्यापन के, जो बड़े पैमाने पर अक्सर अव्यवहार्य होता है।

कार्यप्रणाली (Methodology)
लेखक एक न्यूरो-सिम्बोलिक आर्किटेक्चर का प्रस्ताव करते हैं जो सही-से-निर्माण (correct-by-construction) कोड को संश्लेषित करने के लिए LLMs को औपचारिक सत्यापन (formal verification) के साथ एकीकृत करता है। यह प्रणाली ShinkaEvolve पर आधारित है, जो एक ओपन-सोर्स इवोल्यूशनरी कोड ऑप्टिमाइज़ेशन फ्रेमवर्क है। पाइपलाइन इस प्रकार कार्य करती है:

1. LLMs के साथ इवोल्यूशनरी सर्च: सिस्टम एक मल्टी-आइलैंड इवोल्यूशनरी एल्गोरिदम का उपयोग करता है जहाँ LLMs ऑपरेटर के रूप में कार्य करते हैं। रैंडम म्यूटेशन के बजाय, LLMs पैरेंट प्रोग्राम, "इंस्पिरेशन" प्रोग्राम और उनके फिटनेस स्कोर वाले प्रॉम्प्ट के आधार पर अर्थपूर्ण प्रोग्राम संपादन, पुनर्लेखन या म्यूटेशन प्रस्तावित करते हैं।
2. फिटनेस फंक्शन के रूप में औपचारिक सत्यापन: विश्वसनीयता सुनिश्चित करने के लिए, सिस्टम एक थ्योरम प्रूवर (theorem prover) के रूप में प्रोटोटाइप वेरिफिकेशन सिस्टम (PVS) का उपयोग करता है। LLM को PVS के डोमेन-विशिष्ट भाषा (DSL) में एक ट्रांसलेशन थ्योरम उत्पन्न करने का कार्य दिया जाता है जो एक इनपुट JSON स्कीमा को आउटपुट JSON स्कीमा से मैप करता है।
   • फिटनेस फंक्शन बाइनरी है: एक कैंडिडेट प्रोग्राम को 1 स्कोर मिलता है यदि PVS थ्योरम प्रूवर यह सत्यापित करता है कि ट्रांसलेशन सही है (अर्थात, सभी वैध इनपुट वैध आउटपुट पर मैप होते हैं जो लक्षित स्कीमा को संतुष्ट करते हैं), और अन्यथा 0 मिलता है।
   • PVS के साथ LLM की सीमित परिचितता को कम करने के लिए, प्रॉम्प्ट में एक लैंग्वेज रेफरेंस और सरल स्कीमा ट्रांसलेशन के इन-कॉन्टेक्स्ट उदाहरण शामिल किए गए हैं।
3. कोड जनरेशन: एक बार जब एक थ्योरम को औपचारिक रूप से सत्यापित कर लिया जाता है, तो सिस्टम अतिरिक्त टूलिंग का उपयोग करके सत्यापित PVS थ्योरम को निर्धारित रूप से निष्पादन योग्य C कोड में बदल देता है, जो संसाधन-सीमित MIoT वातावरण में तैनाती के लिए उपयुक्त है।

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

• न्यूरो-सिम्बोलिक पाइपलाइन: सख्त संरचनात्मक आवश्यकताओं को पूरा करने के लिए LLM-संचालित इवोल्यूशनरी सर्च को एक औपचारिक थ्योरम प्रूवर (PVS) के साथ एकीकृत करना।
• MIOT केस स्टडी: एक वाहन-आधारित MIoT नेटवर्क में पल्स ऑक्सीमीटर को एकीकृत करने का एक व्यावहारिक प्रदर्शन। सिस्टम सफलतापूर्वक डिवाइस के कस्टम JSON स्कीमा को मानक FHIR ऑब्जर्वेशन रिसोर्स फॉर्मेट में अनुवादित करता है।
• कम लागत वाली विश्वसनीयता: यह प्रदर्शन कि औपचारिक रूप से सत्यापित कोड को कम कम्प्यूटेशनल और वित्तीय ओवरहेड के साथ लगातार उत्पन्न किया जा सकता है।

प्रायोगिक परिणाम
लेखकों ने पल्स ऑक्सीमीटर के एकीकरण का विश्लेषण करने के लिए 10 स्वतंत्र प्रायोगिक रन आयोजित किए, जिनमें से प्रत्येक में दो इवोल्यूशनरी आइलैंड्स में 20 जनरेशन शामिल थे।

• सफलता दर: सिस्टम ने 37.4% ± 22.4% की सफलता दर प्राप्त की (सत्यापन पास करने वाले LLM-जनरेटेड प्रोग्राम का अंश)।
• दक्षता: सबसे प्रारंभिक सफल थ्योरम औसतन जेनरेशन 5.0 पर पाया गया। पहले सफल प्रोग्राम को खोजने में औसत समय 10.4 मिनट था, और प्रति प्रयोग कुल वॉल-क्लॉक समय 42.7 मिनट था।
• लागत: प्रति प्रयोग औसत कुल API लागत $0.87** थी। महत्वपूर्ण रूप से, पहले सफल प्रूफ को खोजने से पहले हुई लागत केवल **$0.18 (कुल बजट का लगभग 20%) थी।
• मॉडल प्रदर्शन: थॉम्पसन सैंपलिंग के माध्यम से डायनेमिक वेटिंग के साथ मॉडल्स के एक एन्सेम्बल (GPT-5, GPT-5-mini, o4-mini, GPT-5-nano) का उपयोग किया गया। GPT-5 ने 33.7% चयन का प्रतिनिधित्व किया लेकिन 53.5% सफल प्रोग्राम उत्पन्न किए, जो दर्शाता है कि बड़े मॉडल्स सही PVS थ्योरम उत्पन्न करने में अधिक प्रभावी थे।
• अभिसरण (Convergence): अलग-अलग LLM चयन पथों और मध्यवर्ती विफलताओं के बावजूद, सभी 10 प्रयोग अर्थपूर्ण रूप से समान समाधानों पर अभिसरित हुए, जो सुझाव देता है कि FHIR स्कीमा के औपचारिक प्रतिबंध अत्यधिक निर्देशात्मक हैं।

महत्व और दावे
यह शोध पत्र मौजूदा स्वास्थ्य सेवा बुनियादी ढांचे में नए उपकरणों के भरोसेमंद स्वचालित एकीकरण की दिशा में एक "पहला कदम" के रूप में खुद को स्थापित करता है। लेखक दावा करते हैं कि उनका सिस्टम कम लागत पर औपचारिक रूप से सत्यापित ट्रांसलेशन कोड उत्पन्न करने की व्यवहार्यता को प्रदर्शित करता है, यह सुनिश्चित करते हुए कि जनरेट किए गए कोड द्वारा ट्रांसलेट किया गया स्ट्रक्चर्ड डेटा हमेशा लक्षित आउटपुट स्कीमा के अनुरूप होगा।

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