Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
यह शोध पत्र एक न्यूरो-सिम्बोलिक ढांचे को प्रस्तुत करता है जो एक GLLM जनरेटर को सेपरेशन लॉजिक (Separation Logic) वेरीफायर के साथ एकीकृत करता है ताकि तार्किक प्रमाण विफलताओं (logical proof failures) को सटीक स्थानिक निर्देशों (spatial directives) में अनुवादित करके पुनरावृत्ति परिशोधन (iterative refinement) के माध्यम से G-कोड के स्व-सुधारात्मक, टकराव-मुक्त उत्पादन को सक्षम बनाया जा सके।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने नहीं लिखा है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक बहुत ही रचनात्मक, कल्पनाशील कलाकार (एक AI) को एक रोबोटिक आर्म का उपयोग करके संगमरमर के ब्लॉक से एक मूर्ति तराशना सिखाने की कोशिश कर रहे हैं। यह कलाकार आपके विवरण ("एक पक्षी बनाओ") को समझने में बहुत अच्छा है और वह रोबोट के लिए निर्देश लिख सकता है। हालाँकि, उसने वास्तव में कार्यशाला (वर्कशॉप) को कभी नहीं देखा है। उसे यह नहीं पता कि संगमरमर को पकड़ने वाले भारी क्लैम्प्स कहाँ हैं, या रोबोट के हाथ का आकार कितना बड़ा है। वह ऐसे निर्देश लिख सकता है जो कागज पर तो एकदम सही दिखते हैं, लेकिन रोबोट को सीधे किसी क्लैम्प से टकराकर मशीन तोड़ देंगे।
यह पेपर इस समस्या का समाधान प्रस्तावित करता है, जो एक रचनात्मक कलाकार को एक सख्त, गणितीय रूप से सटीक सुरक्षा निरीक्षक (सेफ्टी इंस्पेक्टर) के साथ टीम बनाने के माध्यम से काम करता है।
यहाँ उनके इस साझेदारी का विवरण सरल चरणों में दिया गया है:
1. दो साथी
- कलाकार (AI): यह एक लार्ज लैंग्वेज मॉडल है जिसे GLLM कहा जाता है, जिसे पिछले कार्यों से लिया गया है। GLLM आपके प्राकृतिक भाषा के अनुरोध (जैसे "पक्षी तराशें") को रोबोटिक निर्देशों (G-code) की एक सूची में बदलने में माहिर है। यह रिट्रीवल-ऑगमेंटेड जनरेशन (मशीन और कार्य के बारे में संदर्भ प्राप्त करना) को संभालता है और यह जाँचता है कि कोड सिंटैक्टिकली (syntactically) और सिमेंटिकली (semantically) तर्कसंगत है या नहीं। यह क्या नहीं करता है, और इसे कभी डिज़ाइन ही नहीं किया गया था, वह यह है कि रोबोट को भौतिक रूप से टकराने से बचाए—इसमें बिल्ट-इन कोलिजन अवॉयडेंस (टकराव से बचाव) की सुविधा नहीं है।
- निरीक्षक (सेफ्टी प्रोवर): यह एक सेपरेशन लॉजिक प्रोवर (Separation Logic prover) है जिसे लेखकों ने अपने स्वयं के पिछले कार्य से लाया है—विशेष रूप से पेपर Separation Logic for Verifying Physical Collisions of CNC Programs (arXiv:2605.10437), जहाँ स्पेशियल हीप मॉडल (Spatial Heap model) और प्रोवर को पहली बार पेश किया गया था। निरीक्षक का एकमात्र काम भौतिक टकरावों का पता लगाना है—ऐसी स्थितियाँ जहाँ टूल और कोई बाधा एक ही समय में एक ही स्थान घेरने की कोशिश करते हैं। यह कोई सामान्य-उद्देश्य वाला कोड समीक्षक नहीं है; यह यह जाँच नहीं कर रहा है कि कोड "गलत" है या नहीं; यह विशुद्ध रूप से एक क्रैश डिटेक्टर है।
यह पेपर वास्तव में इन दो मौजूदा उपकरणों के बीच के जुड़ाव में योगदान देता है, जो एक न्यूरो-सिम्बोलिक फीडबैक लूप है जिसमें निरीक्षक के टकराव संबंधी निष्कर्षों को कलाकार के लिए संरचित मार्गदर्शन में अनुवादित किया जाता है।
2. "डिजिटल सैंडबॉक्स" (स्पेशियल हीप)
गणित को काम करने के लिए, सिस्टम भौतिक कार्यशाला को छोटे क्यूब्स के एक विशाल 3D ग्रिड में बदल देता है (जैसे कि Minecraft का 3D संस्करण)।
- कुछ क्यूब्स को "मार्बल" (संगमरमर) के रूप में चिह्नित किया गया है (वह सामग्री जिसे काटा जाना है)।
- कुछ क्यूब्स को "क्लैम्प्स" (Clamps) के रूप में चिह्नित किया गया है (बाधाएं)।
- कुछ क्यूब्स को "खाली हवा" (Empty Air) के रूप में चिह्नित किया गया है (सुरक्षित स्थान)।
- रोबोट का टूल भी क्यूब्स का एक विशिष्ट आकार है।
महत्वपूर्ण बात यह है कि निरीक्षक वास्तव में रोबोट को चलते हुए नहीं देखता है और न ही कभी ज्यामितीय सिमुलेशन (geometric simulation) चलाता है। यह सीधे G-code स्क्रिप्ट को पढ़ता है, लाइन दर लाइन, और यह गणना करता है कि प्रत्येक टूल मूव को किन क्यूब्स को घेरना होगा। यह जिस नियम को लागू करता है वह सरल है: टूल द्वारा दावा किए गए क्यूब्स पहले से ही किसी क्लैम्प या अन्य बाधा द्वारा दावा किए गए क्यूब्स के साथ ओवरलैप नहीं होने चाहिए।
3. सुरक्षा बफर (द "फ्लफी कोट")
रोबोट एकदम सटीक नहीं होते। वे थोड़ा डगमगा सकते हैं, या टूल थोड़ा मुड़ सकता है। इसे ध्यान में रखने के लिए, सिस्टम केवल टूल के सटीक आकार की जाँच नहीं करता है। यह टूल को एक "फ्लफी कोट" (एक गणितीय सुरक्षा मार्जिन) प्रदान करता है।
- यदि टूल 5mm चौड़ा है, तो सिस्टम सुरक्षा के लिए इसे 7mm चौड़ा मान लेता है।
- निरीक्षक जाँचता है कि क्या यह "फ्लफी टूल" किसी चीज़ से टकराता है। यदि ऐसा होता है, तो वह मूव वर्जित है।
4. "डेटा रेस" (क्रैश अलार्म)
कंप्यूटर विज्ञान में, "डेटा रेस" तब होता है जब दो प्रोग्राम एक ही समय में एक ही मेमोरी का उपयोग करने की कोशिश करते हैं। लेखक भौतिक क्रैश को "स्पेशियल डेटा रेस" (Spatial Data Race) कहते हैं।
जब कलाकार एक ऐसा मूव लिखता है जिससे क्रैश हो सकता है:
- निरीक्षक 3D ग्रिड को देखता है।
- वह देखता है कि "टूल क्यूब्स" और "क्लैम्प क्यूब्स" ओवरलैप हो रहे हैं।
- गणितीय प्रमाण विफल हो जाता है। निरीक्षक चिल्लाता है, "रुकिए! आप एक ही स्थान घेरने की कोशिश कर रहे हैं!"
5. फीडबैक लूप (द "वहाँ मत जाओ" नोट)
अतीत में, यदि AI कोई गलती करता था, तो आप बस उसे कह सकते थे, "फिर से प्रयास करें," और उम्मीद कर सकते थे कि वह भाग्यशाली होगा। यह अक्षम है।
यह सिस्टम अधिक स्मार्ट है। जब निरीक्षक एक क्रैश पाता है, तो वह केवल "नहीं" नहीं कहता। वह क्रैश के सटीक स्थान की पहचान करता है और उसके चारों ओर एक छोटा, सटीक बॉक्स बनाता है।
- संदेश: "आपने निर्देशांक X, Y, Z पर जाने की कोशिश की। इस विशिष्ट बॉक्स के अंदर एक क्लैम्प है। इस बॉक्स में न जाएँ।"
- सुधार: यह नोट वापस कलाकार को भेजा जाता है। कलाकार नोट को पढ़ता है, अपनी गलती को समझता है, और निर्देशों को उस बॉक्स के चारों ओर से जाने के लिए फिर से लिखता है।
6. परिणाम: "करेक्ट-बाय-कंस्ट्रक्शन" (निर्माण-दर-निर्माण सही)
वे इस लूप को जारी रखते हैं—कलाकार लिखता है, निरीक्षक जाँचता है, निरीक्षक टकराव बताता है, कलाकार सुधार करता है—जब तक कि निरीक्षक गणितीय रूप से यह सिद्ध न कर दे कि टूल के टकराने की अत्यधिक संभावना नहीं है।
चूंकि सिस्टम केवल तभी रुकता है जब यह प्रमाण पूरा हो जाता है, इसलिए निर्देशों का अंतिम सेट उस कार्यक्षेत्र और बाधाओं के वर्णन के लिए "करेक्ट-बाय-कंस्ट्रक्शन" है। गारंटी यह है कि, उस स्थानिक मॉडल (spatial model) के तहत जो निरीक्षक को दिया गया है, टूलपाथ किसी भौतिक टकराव को उत्पन्न नहीं करता है। (कोई भी प्रमाण उन टकरावों को खारिज नहीं कर सकता जो कोड जेनरेट होने के बाद कार्यक्षेत्र में बदलाव के कारण होते हैं—जैसे फिक्स्चर का हिलना, नया स्टॉक, या सेल के अंदर किसी ऑपरेटर का टूल छोड़ देना—इसलिए यह वर्कस्पेस-कंडीशनल गारंटी है, अनकंडीशनल नहीं।)
सारांश
पेपर यह वर्णन करता है कि कैसे एक रचनात्मक AI को एक सख्त गणित-आधारित सुरक्षा जांचकर्ता के साथ जोड़कर रोबोट निर्देशों को सुरक्षित बनाया जा सकता है। चेकर भौतिक दुनिया को एक ग्रिड में बदल देता है, ओवरलैप (क्रैश) की जाँच करता है, और सटीक "वहाँ मत जाओ" चेतावनी वापस AI को भेजता है जब तक कि निर्देश गणितीय रूप से वर्तमान स्थानिक मॉडल के विरुद्ध सत्यापित न हो जाएं।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।