Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

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

यह भाषा एक उच्च-दांव वाले पहेली (high-stakes puzzle) की तरह है। यदि आप एक छोटा सा प्रतीक भी चूक जाते हैं या अपनी तर्कशक्ति (logic) में थोड़ी सी भी गलती करते हैं, तो रेसिपी में मशीन काम तो कर सकती है, लेकिन असल जिंदगी में वह क्रैश हो जाएगी। समस्या यह है कि इन रेसिपीज़ को हाथ से लिखना कठिन और धीमा है। इसलिए, शोधकर्ताओं ने पूछा: क्या हम बस एक आधुनिक AI (एक लार्ज लैंग्वेज मॉडल, या LLM) से हमारे लिए ये रेसिपी लिखवा सकते हैं?

यह पेपर इस सवाल पर पहला बड़ा रिपोर्ट कार्ड है। यहाँ उन्होंने जो पाया है, उसे सरल भाषा में समझाया गया है:

1. "व्याकरण बनाम अर्थ" का अंतर (The "Grammar vs. Meaning" Gap)

शोधकर्ताओं ने 30 अलग-अलग AI से साधारण अंग्रेजी विवरणों के आधार पर ये TLA+ रेसिपी लिखने के लिए कहा।

• अच्छी खबर (व्याकरण): लगभग 26% बार AI ने एक ऐसी रेसिपी लिखी जो सतह पर सही दिखती थी। "स्पेल-चेकर" (जिसे SANY कहा जाता है) ने कहा, "ठीक है, शब्द और प्रतीक सही क्रम में हैं।"
• बुरी खबर (अर्थ): हालाँकि, जब उन्होंने वास्तव में यह देखने के लिए रेसिपी को एक "लॉजिक टेस्टर" (जिसे TLC कहा जाता है) के माध्यम से चलाया कि क्या यह वास्तव में काम करती है, तो केवल 8.6% बार ही यह सफल रही।

उपमा (Analogy): कल्पना कीजिए कि आप एक छात्र को कानूनी अनुबंध (legal contract) लिखने के लिए कह रहे हैं। छात्र सही वर्तनी और व्याकरण का उपयोग करता है (26% सफलता), लेकिन उसके द्वारा लिखा गया अनुबंध वास्तव में उसके इरादे के विपरीत कहता है, या इसमें कोई महत्वपूर्ण क्लॉज छोड़ दिया गया है, जिससे वह कानूनी रूप से बेकार हो जाता है (केवल 8.6% सफलता)। AI भाषा के दिखावे की नकल करने में बहुत अच्छा है, लेकिन यह अक्सर इसके पीछे के तर्क (logic) को समझने में विफल रहता है।

2. बड़ा होना हमेशा बेहतर नहीं होता (Bigger Isn't Always Better)

आमतौर पर, हम मानते हैं कि एक बड़ा, अधिक शक्तिशाली AI बेहतर काम करेगा। लेकिन इस अध्ययन में, ऐसा नहीं हुआ।

• आश्चर्य: एक छोटा AI मॉडल (DeepSeek r1:8b) अपने विशाल "बड़े भाई" (DeepSeek r1:70b) की तुलना में बहुत बेहतर काम कर गया।
• क्यों? छोटे मॉडल को विशेष रूप से "चरण-दर-चरण सोचने" (जैसे कि अपना काम दिखाने वाला गणित का छात्र) के लिए प्रशिक्षित किया गया था, जबकि बड़े मॉडल को इतने अधिक सामान्य इंटरनेट डेटा पर प्रशिक्षित किया गया था कि वह TLA+ के सख्त नियमों से भ्रमित हो गया। यह एक विशेषज्ञ शेफ की तरह है जो जानता है कि सूफ़ले (soufflé) कैसे बनाया जाता है, बनाम एक सामान्य व्यक्ति जो सब कुछ बनाना जानता है लेकिन विशिष्ट रेसिपी के लिए बहुत अधिक सोच-विचार करने लगता है।

3. "कोड विशेषज्ञ" विफल रहे ("Code Experts" Failed)

शोधकर्ताओं ने उन AI का परीक्षण किया जो कंप्यूटर कोड (जैसे Python या Java) लिखने के लिए प्रसिद्ध हैं। आश्चर्यजनक रूप से, ये "कोड विशेषज्ञ" सामान्य-उद्देश्य वाले AI की तुलना में खराब प्रदर्शन करते रहे।

• कारण: ये मॉडल सेमीकोलन (;) या कर्ली ब्रेसेस ({}) के साथ कोड लिखने के इतने आदी हैं कि वे गलती से उन्हें TLA+ रेसिपी में डाल देते रहे। चूंकि TLA+ इन प्रतीकों का उपयोग नहीं करता है, इसलिए रेसिपी तुरंत टूट जाती है। यह एक बढ़ई की तरह है जो घड़ी ठीक करने की कोशिश कर रहा है लेकिन गलती से हथौड़ा इस्तेमाल करने लगता है क्योंकि वह हर चीज़ के लिए उसी का उपयोग करता है।

4. "चरण-दर-चरण" का तरीका सबसे अच्छा रहा (The "Step-by-Step" Trick Worked Best)

शोधकर्ताओं ने AI से मदद मांगने के चार अलग-अलग तरीके आजमाए। सबसे सफल तरीका "प्रोग्रेसिव प्रॉम्प्टिंग" (Progressive Prompting) था।

• यह कैसे काम करता था: पूरी रेसिपी एक बार में लिखने के बजाय, उन्होंने AI को इसे टुकड़ों में बनाने के लिए कहा: "पहले, शीर्षक लिखें। अब, वेरिएबल्स लिखें। अब, नियम लिखें।"
• परिणाम: यही एकमात्र तरीका था जिसने कोई भी पूरी तरह से काम करने वाली रेसिपी बनाई (8.6% सफलता दर)। यह घर बनाने जैसा है: यदि आप एक ही बड़ी छलांग में छत, दीवारें और नींव बनाने की कोशिश करते हैं, तो आप विफल होंगे। लेकिन यदि आप एक समय में एक कमरा बनाते हैं, तो आपकी सफलता की संभावना अधिक होती है।

5. AI के "भ्रम" (The AI's "Hallucinations")

पेपर में पाया गया कि AI ने पाँच विशिष्ट तरीकों से एक ही तरह की गलतियाँ कीं, जिन्हें वे "हैलुसिनेशन" (hallucinations) कहते हैं:

1. गलत प्रतीक: फैंसी गणितीय प्रतीकों (जैसे ∧) का उपयोग करना जिनके बजाय TLA+ को साधारण टेक्स्ट प्रतीकों (जैसे /\) की आवश्यकता होती है।
2. भाषा का मिश्रण: अन्य प्रोग्रामिंग भाषाओं से गलती से सेमीकोलन या बैकथिक्स जोड़ना।
3. सोच को बाहर निकालना: AI कभी-कभी अपनी "सोचने की प्रक्रिया" (जैसे ...) को सीधे अंतिम रेसिपी में पेस्ट कर देता था, जिससे वह टूट जाती थी।
4. गलत लंबाई: कभी-कभी AI ने ऐसी रेसिपी लिखी जो 9 गुना अधिक लंबी थी, या कभी-कभी उसने लगभग कुछ भी नहीं लिखा।
5. टूटी हुई संरचना: रेसिपी के "अंत" के मार्करों को छोड़ देना, जिससे दस्तावेज़ अधूरा रह जाता था।

निष्कर्ष (The Bottom Line)

पेपर निष्कर्ष निकालता है कि वर्तमान AI अभी तक अपने आप भरोसेमंद TLA+ स्पेसिफिकेशन नहीं लिख सकता है। हालांकि यह भाषा के रूप को दोहरा सकता है, लेकिन इसमें अभी भी बहुत सारी तार्किक त्रुटियां होती हैं जिन्हें बिना किसी मानव विशेषज्ञ द्वारा हर एक लाइन की जांच किए भरोसा नहीं किया जा सकता।

शोधकर्ता सुझाव देते हैं कि इसे ठीक करने के लिए, हमें निम्नलिखित की आवश्यकता है:

• "चरण-दर-चरण" प्रॉम्प्टिंग विधि का उपयोग करें।
• विशाल सामान्य मॉडलों के बजाय छोटे, तर्क-केंद्रित (reasoning-focused) मॉडलों का उपयोग करें।
• ऐसे उपकरण बनाएं जो AI के काम शुरू करने से पहले ही सामान्य गलतियों (जैसे गलत प्रतीकों को हटाना) को स्वचालित रूप से ठीक कर सकें।

तब तक, इन महत्वपूर्ण सिस्टम रेसिपीज़ को लिखना मानव विशेषज्ञों का काम बना रहेगा, जिसमें AI एक सहायक लेकिन त्रुटिपूर्ण (error-prone) सहायक के रूप में कार्य करेगा।