Faithful Autoformalization via Roundtrip Verification and Repair

तकनीकी सारांश: राउंडट्रिप सत्यापन और मरम्मत के माध्यम से निष्ठापूर्ण ऑटोफॉर्मलाइजेशन (Faithful Autoformalization)

समस्या विवरण
यह शोध पत्र ऑटोफॉर्मलाइजेशन में एक महत्वपूर्ण अंतराल को संबोधित करता है: यह सत्यापित करने के लिए एक विश्वसनीय विधि का अभाव कि क्या एक लार्ज लैंग्वेज मॉडल (LLM) प्राकृतिक भाषा के कथन को औपचारिक, मशीन-जांच योग्य प्रतिनिधित्व में अनुवादित करते समय उसके अर्थ को निष्ठापूर्वक (faithfully) पकड़ पाया है। मौजूदा मूल्यांकन विधियाँ सिंटैक्टिक वैधता या डाउनस्ट्रीम टास्क की सफलता पर निर्भर करती हैं, जो सीधे तौर पर सिमेंटिक फिडेलिटी (अर्थ संबंधी निष्ठा) का परीक्षण नहीं करती हैं। इसके अलावा, जब त्रुटियां होती हैं, तो वर्तमान मरम्मत रणनीतियां एंड-टू-एंड पुनरुत्पादन (regeneration) तक सीमित हैं, जिनमें अनुवाद पाइपलाइन में अर्थ कहाँ खो गया, इसका निदान करने की क्षमता का अभाव है। यह विशेष रूप से वैधानिक कानून (statutory law) जैसे डोमेन में चुनौतीपूर्ण है, जहाँ ग्राउंड-ट्रुथ फॉर्मलाइजेशन उपलब्ध नहीं होते हैं।

कार्यप्रणाली (Methodology)
लेखक एक राउंडट्रिप सत्यापन और स्कोप्ड रिपेयर फ्रेमवर्क (Roundtrip Verification and Scoped Repair Framework) प्रस्तावित करते हैं जो बिना किसी ग्राउंड-ट्रुथ एनोटेशन के कार्य करता है। मुख्य तंत्र में तीन-चरणीय अनुवाद पाइपलाइन शामिल है:

1. T1 (ऑटोफॉर्मलाइजेशन): प्राकृतिक भाषा इनपुट $x$ को लक्षित फॉर्मलिज्म $\Sigma$ में एक औपचारिक अभिव्यक्ति $y_{orig}$ में अनुवादित करता है।
2. T2 (बैक-ट्रांसलेशन): $y_{orig}$ को वापस प्राकृतिक भाषा $x'$ में अनुवादित करता है।
3. T3 (री-फॉर्मलाइजेशन): $x'$ को वापस एक औपचारिक अभिव्यक्ति $y_{rt}$ में अनुवादित करता है।

सत्यापन (Verification): सिस्टम एक औपचारिक टूल (विशेष रूप से प्रयोगों में एक SMT सॉल्वर) का उपयोग करके प्रारंभिक फॉर्मलाइजेशन ($y_{orig}$) और राउंडट्रिप फॉर्मलाइजेशन ($y_{rt}$) के बीच तार्किक समानता की जांच करता है। यदि $y_{orig} \equiv_\Sigma y_{rt}$ है, तो पाइपलाइन को स्व-सुसंगत (self-consistent) माना जाता है।

निदान और मरम्मत (Diagnosis and Repair): जब समानता विफल हो जाती है, तो फ्रेमवर्क एक स्टेज-आधारित निदान (stage-based diagnosis) प्रक्रिया का उपयोग करता है। एक LLM जज आर्टिफैक्ट्स ($x, y_{orig}, x', y_{rt}$) का परीक्षण करता है ताकि यह पहचाना जा सके कि सिमेंटिक ड्रिफ्ट (अर्थ संबंधी विचलन) किस चरण (चरण 1, 2, या 3) में हुआ था। महत्वपूर्ण रूप से, निदान "स्कोप्ड" है, जिसका अर्थ है कि स्पष्टीकरण केवल उस विशिष्ट चरण से संबंधित आर्टिफैक्ट्स तक ही सीमित है।

• स्कोप्ड रिपेयर (Scoped Repair): पूरे पाइपलाइन को पुन: उत्पन्न करने के बजाय, एक लक्षित रिपेयर ऑपरेटर ($R_i$) केवल पहचाने गए दोषपूर्ण चरण को ठीक करता है। पाइपलाइन की निरंतरता बनाए रखने के लिए बाद के चरणों को फिर से जनरेट किया जाता है।
• पुनरावृत्ति लूप (Iterative Loop): यह प्रक्रिया एक निश्चित बजट ($K=3$) तक तब तक दोहराई जाती है जब तक कि समानता प्राप्त न हो जाए या बजट समाप्त न हो जाए।

सहायक सिमेंटिक सिग्नल (Auxiliary Semantic Signal): फॉर्मलाइजेशन की सिमेंटिक गुणवत्ता का मरम्मत लूप से स्वतंत्र रूप से मूल्यांकन करने के लिए, लेखक एक द्विदिश नेचुरल लैंग्वेज इन्फेरेंस (NLI) मॉडल का उपयोग करते हैं। यह मूल टेक्स्ट और पुनर्निर्मित टेक्स्ट के बीच "ड्रिफ्ट" (जैसे विरोधाभास या असंबंधितता) को मापने के लिए एक पोस्ट-हॉक डायग्नोस्टिक के रूप में कार्य करता है, जो उन नियमों के बीच अंतर करता है जो औपचारिक रूप से सुसंगत हैं लेकिन सिमेंटिक रूप से विचलित हो गए हैं।

मुख्य योगदान

1. राउंडट्रिप वेरिफिकेशन फ्रेमवर्क: बिना ग्राउंड-ट्रुथ फॉर्मलाइजेशन के ऑटोफॉर्मलाइजेशन की निष्ठा का संकेत देने की एक विधि, जो किसी भी ऐसे फॉर्मलिज्म पर लागू होती है जिसमें इक्विलेंस चेक (जैसे SMT, टाइप चेकर्स) संभव है।
2. डायग्नोसिस-गाइडेड स्कोप्ड रिपेयर: एक प्रक्रिया जो त्रुटियों को विशिष्ट अनुवाद चरणों तक स्थानीयकृत करती है, जिससे पूर्ण-पाइपलाइन पुनरुत्पादन के बजाय लक्षित सुधार संभव होता है।
3. बॉटलनेक का अनुभवजन्य विश्लेषण: दो वैधानिक डोमेन (टेक्सास ट्रांसपोर्टेशन कोड और टेक्सास पार्क्स एंड वाइल्डलाइफ कोड) और दो मॉडल परिवारों (Claude Opus 4.6 और GPT-5.2) में एक अध्ययन, जो यह पहचानता है कि डायग्नोसिस स्टेप स्कोप्ड रिपेयर के लिए प्राथमिक बॉटलनेक है, न कि पाइपलाइन या रिपेयर ऑपरेटर्स स्वयं।

परिणाम
फ्रेमवर्क का मूल्यांकन 150 ट्रैफिक नियमों और 77 वाइल्डलाइफ नियमों पर किया गया।

• मरम्मत की प्रभावशीलता: डायग्नोसिस-गाइडेड स्कोप्ड रिपेयर ने सबसे कम लागत पर उच्चतम वेरिफाइड-इक्विवेलेंस दर हासिल की जब डायग्नोसिस फंक्शन विश्वसनीय था।
• मॉडल निर्भरता: क्लॉड (Claude) द्वारा पाइपलाइन और डायग्नोसिस करने पर, स्कोप्ड रिपेयर ने बेसलाइन्स (कोई मरम्मत नहीं, रैंडम स्टेज सिलेक्शन, फुल रिजनरेशन) को पछाड़ दिया। हालांकि, GPT के साथ, डायग्नोसिस स्टेप अविश्वसनीय था (चरण 1 को दोष देने की ओर भारी झुकाव), जिससे स्कोप्ड रिपेयर का प्रदर्शन गिर गया और यह फुल रिजनरेशन की तुलना में अधिक महंगा हो गया।
• क्रॉस-मॉडल हस्तक्षेप: केवल GPT डायग्नोसिस स्टेप को क्लॉड (Claude) से बदलने पर (पाइपलाइन और रिपेयर के लिए GPT को रखते हुए), स्कोप्ड रिपेयर की दक्षता और प्रभावशीलता बहाल हो गई, जो यह सिद्ध करता है कि डायग्नोसिस फंक्शन ही महत्वपूर्ण चर (variable) है।
• फेथफुलनेस प्रेडिक्शन: औपचारिक समानता (Formal equivalence) सिमेंटिक निष्ठा का एक मजबूत भविष्यवक्ता है। वे नियम जिन्होंने इक्विलेंस चेक पास किया (UNSAT), उनमें उन नियमों की तुलना में 1.4× से 2.5× कम NLI ड्रिफ्ट देखा गया जो विफल रहे (SAT)। हालांकि, औपचारिक समानता आवश्यक है लेकिन पर्याप्त नहीं है; लगभग 16% औपचारिक रूप से समान नियम अभी भी सिमेंटिक ड्रिफ्ट प्रदर्शित कर रहे थे।

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

यह कार्य अपने दायरे में विनम्र है, यह नोट करते हुए कि फ्रेमवर्क एक ह्यूरिस्टिक (heuristic) है और यह मूल प्राकृतिक भाषा के इरादे के विरुद्ध शुद्धता की गारंटी नहीं देता है (क्योंकि पाइपलाइन एक सिमेंटिक रूप से भिन्न स्थिर बिंदु पर स्थिर हो सकती है)। लेखक स्पष्ट रूप से कहते हैं कि यह प्रणाली स्वतंत्र विशेषज्ञ समीक्षा के बिना सुरक्षा-महत्वपूर्ण अनुप्रयोगों के लिए उपयुक्त नहीं है और वर्तमान मूल्यांकन अंग्रेजी वैधानिक पाठ तक सीमित है, जिसके लिए कोड या वैज्ञानिक टेक्स्ट जैसे अन्य शैलियों के लिए आगे के अध्ययन की आवश्यकता है।