तकनीकी सारांश: ForEx – तार्किक दोष पहचान में व्याख्यात्मक तर्क के लिए एक औपचारिक सत्यापन ढांचा (Formal Verification Framework)

1. समस्या विवरण (Problem Statement)

तार्किक दोष (logical fallacy) पहचान पर लार्ज लैंग्वेज मॉडल्स (LLMs) के मूल्यांकन वर्तमान में मुख्य रूप से भविष्यवाणी सटीकता (लेबल की शुद्धता) पर निर्भर करते हैं। हालाँकि, यह दृष्टिकोण इस बात को सत्यापित करने में विफल रहता है कि मॉडल द्वारा प्रदान किया गया तर्क वास्तव में अनुमानित लेबल का समर्थन करता है या नहीं। सही भविष्यवाणियाँ वास्तविक तार्किक व्युत्पत्ती के बजाय सतही सहसंबंधों (superficial correlations) से उत्पन्न हो सकती हैं, जबकि गलत भविष्यवाणियों के साथ ऐसा तर्क भी हो सकता है जो एक विशिष्ट व्याख्या के तहत औपचारिक रूप से सुदृढ़ है लेकिन मानव एनोटेशन से भिन्न है।

इसके अतिरिक्त, मौजूदा प्रतीकात्मक दृष्टिकोण (जैसे NL2FOL) आमतौर पर संतुष्टि (satisfiability) की जाँच करने के लिए इनपुट तर्क को औपचारिक रूप देते हैं, न कि मॉडल द्वारा उत्पन्न तर्क श्रृंखला को। इसके अलावा, मानक एनोटेशन प्रथाएं अक्सर व्याख्यात्मक विविधताओं को एकल "गोल्ड" लेबल में संकुचित कर देती हैं, जिससे तर्क की वैकल्पिक व्याख्याओं को छिपाया जा सकता है। एक ऐसे ढांचे का अभाव है जो अनुमानित लेबल, उत्पन्न स्पष्टीकरण और उन स्पष्टीकरणों की औपचारिक व्युत्पत्ति क्षमता (formal derivability) का संयुक्त रूप से विश्लेषण कर सके।

2. कार्यप्रणाली: ForEx ढांचा (Methodology: The ForEx Framework)

लेखक ForEx (Formal Verification for Explainable Reasoning) प्रस्तावित करते हैं, जो LLM-जनित प्राकृतिक भाषा स्पष्टीकरणों को Lean4 (एक औपचारिक प्रमाण सहायक/formal proof assistant) में अनुवादित करता है ताकि यह सत्यापित किया जा सके कि अनुवादित तर्क एन्कोडेड आधारों (premises) के तहत व्युत्पन्न (derivable) है या नहीं। यह वर्कफ़्लो तीन चरणों में विभाजित है:

A. तर्क उम्मीदवारों का सृजन (Reasoning Candidates Generation)

एक "रीज़नर" (Reasoner) मॉडल एक इनपुट कथन प्राप्त करता है और $k$ उम्मीदवार उत्पन्न करता है। प्रत्येक उम्मीदवार एक टुपल $(f_i, a_i, s_i)$ होता है जिसमें शामिल हैं:

• $f_i$: अनुमानित तार्किक दोष का प्रकार।
• $a_i$: प्राकृतिक भाषा स्पष्टीकरण (तर्क/rationale)।
• $s_i$: स्पष्टीकरण को औपचारिक रूप देने वाला Lean4 संरचना।

एक "मॉडिफायर" (Modifier) $s_i$ को प्रारंभिक Lean4 कोड में परिवर्तित करता है।

B. निष्पादन फीडबैक और Lean4 सत्यापन (Execution Feedback & Lean4 Verification)

यह चरण यह सुनिश्चित करने के लिए एक पुनरावृत्ति सुधार लूप (iterative repair loop) का उपयोग करता है कि उत्पन्न Lean4 कोड संकलित (compile) हो सके:

1. संकलन प्रयास (Compilation Attempt): "एक्सेक्यूटर" (Executor) Lean4 कोड को संकलित करने का प्रयास करता है।
2. फीडबैक लूप: यदि संकलन विफल (state F) होता है, तो एक्सेक्यूटर को कोड को संशोधित करने के लिए त्रुटि संदेश और मूल स्पष्टीकरण $a_i$ प्राप्त होता है।
3. बाधाएं (Constraints): संशोधन को मूल स्पष्टीकरण और प्रारंभिक कोड तक ही सीमित रखा जाता है ताकि अर्थ संबंधी विचलन (semantic drift) को रोका जा सके; एक्सेक्यूटर कोई नया तार्किक विषय (logical content) पेश नहीं कर सकता।
4. समाप्ति (Termination): लूप तब तक जारी रहता है जब तक कि कोड सफलतापूर्वक संकलित (state T) न हो जाए या अधिकतम सुधार पुनरावृत्ति ($iter_{max}$) समाप्त न हो जाए।

C. लेबल निरंतरता मूल्यांकन (Label Consistency Evaluation)

ढांचा लेबल की शुद्धता को औपचारिक सत्यापन स्थिति से अलग करने के लिए LLM तर्क सत्यापन मैट्रिक्स (LLM Argument Verification Matrix) पेश करता है। मैट्रिक्स दो अक्षों के आधार पर आउटपुट को चार चतुर्थांशों में वर्गीकृत करता है:

1. Lean4 सत्यापन: पास (संकलित) बनाम फेल (संकलित नहीं)।
2. लेबल निरंतरता: मैच (भविष्यवाणी मानव एनोटेशन के बराबर है) बनाम मिसमैच (भिन्नता)।

चार परिणामी श्रेणियां हैं:

• Compilable-Correct (CC): पास और मैच।
• Compilable-Alternative (CA): पास और मिसमैच (यह एक औपचारिक रूप से वैध तर्क श्रृंखला को दर्शाता है जो मानव एनोटेशन से भिन्न लेबल का समर्थन करती है)।
• Uncompilable-Correct (UC): फेल और मैच।
• Uncompilable-Incorrect (UI): फेल और मिसमैच।

D. सर्वसम्मति-निर्देशित एनोटेशन पाइपलाइन (Consensus-Guided Annotation Pipeline)

एनोटेशन अस्पष्टता को संबोधित करने के लिए, लेखक एक पाइपलाइन प्रस्तावित करते हैं जो:

1. मॉडल्स और मानव एनोटेशन को दोष श्रेणियों पर मल्टी-हॉट वेक्टर्स के रूप में प्रस्तुत करती है।
2. आउटलेयर मॉडल्स की पहचान करने और उन्हें फ़िल्टर करने के लिए प्रिंसिपल कंपोनेंट एनालिसिस (PCA) और महलानोबिस दूरी (Mahalanobis distance) का उपयोग करती है।
3. "उच्च-सर्वसम्मति" वाले कथनों की पहचान करने के लिए युग्मवार जैकार्ड दूरी (pairwise Jaccard distances) की गणना करती है।
4. उच्च-सर्वसम्मति वाले कथनों के लिए एनोटेशन को बढ़ाता है यदि कम से कम 50% रिटेन किए गए मॉडल्स औपचारिक सत्यापन के तहत एक विशिष्ट लेबल असाइन करते हैं।

3. प्रमुख योगदान (Key Contributions)

1. ForEx ढांचा: एक नवीन प्रणाली जो LLM-जनित स्पष्टीकरणों को Lean4 में अनुवादित करती है, जिससे केवल इनपुट तर्कों के बजाय औपचारिक तर्क श्रृंखलाओं का मशीन-चेकेबल विश्लेषण संभव होता है।
2. LLM तर्क सत्यापन मैट्रिक्स: एक मीट्रिक जो लेबल निरंतरता को औपचारिक सत्यापन स्थिति से अलग करता है, जिससे वे मामले सामने आते हैं जहाँ मॉडल ऐसे तर्क प्रदान करते हैं जो मौजूदा मानव लेबल के विपरीत औपचारिक रूप से व्युत्पन्न योग्य हैं ("Compilable-Alternative" श्रेणी)।
3. सर्वसम्मति-निर्देशित एनोटेशन पाइपलाइन: एक विधि जो मानव मानकों, मल्टी-LLM सहमति और औपचारिक सत्यापन को जोड़कर एनोटेशन विश्लेषण और रूढ़िवादी लेबल संवर्धन (conservative label augmentation) का समर्थन करती है, जो एनोटेशन असहमति को शोर के बजाय व्याख्यात्मक भिन्नता के संकेत के रूप में देखती है।

4. प्रयोगात्मक परिणाम (Experimental Results)

ढांचे का मूल्यांकन LOGIC-Climate डेटासेट (1,074 उदाहरण, 13 दोष श्रेणियां) पर किया गया, जिसमें 10% नमूना उपसमुच्चय और 15 विभिन्न रीज़नर मॉडल्स (सोचने वाले और गैर-सोचने वाले वेरिएंट सहित) का उपयोग किया गया।

• संकलन सफलता (Compilation Success): चार सुधार पुनरावृत्तियों के बाद Lean4 संकलन के लिए औसत पास दर प्रारंभिक 36.70% से बढ़कर 98.65% हो गई। अधिकांश लाभ पहली पुनरावृत्ति के बाद ही प्राप्त हुए।
• सत्यापन बनाम लेबल समझौता (Verification vs. Label Agreement):
  • संयुक्त Compilable-Correct (CC) + Compilable-Alternative (CA) दर लगातार उच्च रही, जो अधिकांश मॉडल्स के लिए 90% से अधिक थी (97.59% तक पहुँची)। यह इंगित करता है कि अधिकांश LLM आउटपुट को औपचारिक तर्क श्रृंखलाओं में अनुवादित किया जा सकता है जो सत्यापन पास करती हैं।
  • हालांकि, CC दर (मानव लेबल के साथ समझौता) काफी कम थी, जो शीर्ष मॉडल्स के बीच लगभग 17% और 23% के बीच रही।
  • CA दर प्रमुख थी, जो सुझाव देती है कि कई औपचारिक रूप से सत्यापित तर्क श्रृंखलाएं मानव एनोटेशन से भिन्न लेबल का समर्थन करती हैं।
• त्रुटि विश्लेषण (Error Analysis):
  • Uncompilable-Correct (UC) दरें बहुत कम (<2%) थीं, जो दर्शाती हैं कि इस सेटिंग में सही लेबल बिना सत्यापन योग्य तर्क श्रृंखला के शायद ही कभी आते हैं।
  • Uncompilable-Incorrect (UI) विफलताएं अक्सर "No Fallacy" (कोई दोष नहीं) भविष्यवाणियों के कारण हुईं, जो संभवतः अलग-थलग एकल-वाक्य इनपुट में संदर्भ की कमी के कारण हो सकती हैं।
• एनोटेशन संवर्धन (Annotation Augmentation): सर्वसम्मति-निर्देशित पाइपलाइन ने उच्च-सर्वसम्मति वाले कथनों के उपसमुच्चय की पहचान की। संवर्धित एनोटेशन ने मूल मानव एनोटेशन के विरुद्ध 0.77 रिकॉल प्राप्त किया, जिससे अधिकांश मूल लेबल सुरक्षित रहे और औपचारिक रूप से समर्थित वैकल्पिक लेबल भी जोड़े गए।

5. महत्व और दावे (Significance and Claims)

यह पेपर दावा करता है कि ForEx LLM मूल्यांकन को सरल लेबल शुद्धता से आगे ले जाकर औपचारिक तर्क श्रृंखलाओं के मशीन-चेकेबल विश्लेषण की ओर ले जाता है।

• व्यवस्थित अंतराल (Systematic Gap): परिणाम औपचारिक व्युत्पत्ति और लेबल समझौते के बीच एक व्यवस्थित अंतर को उजागर करते हैं। "Compilable-Alternative" आउटपुट की उच्च व्यापकता यह बताती है कि मौजूदा मानव एनोटेशन शायद इनपुट तर्कों की प्रशंसनीय व्याख्याओं को पूरी तरह से कैप्चर नहीं करते हैं, या मॉडल्स अलग मान्यताओं के तहत सही तर्क दे रहे हैं।
• भविष्यवाणी से परे (Beyond Prediction): ढांचा यह प्रदर्शित करता है कि एक मॉडल एक ऐसी तर्क श्रृंखला प्रदान कर सकता है जो औपचारिक रूप से वैध (एन्कोडेड आधारों के तहत व्युत्पन्न) है, भले ही वह "गोल्ड" लेबल से असहमत हो। यह अंतर मानक भविष्यवाणी-आधारित मेट्रिक्स में अदृश्य रहता है।
• एनोटेशन उपयोगिता (Annotation Utility): ForEx को न केवल एक सत्यापन उपकरण के रूप में बल्कि डाउनस्ट्रीम एनोटेशन विश्लेषण के लिए एक तंत्र के रूप में प्रस्तुत किया गया है। यह उन मामलों की पहचान कर सकता है जहाँ गोल्ड लेबल अपर्याप्त हो सकते हैं या जहाँ कई वैध व्याख्याएँ मौजूद हो सकती हैं, जो सर्वसम्मति-आधारित वैकल्पिक लेबल के साथ एनोटेशन के संवर्धन का समर्थन करता है।

लेखक अपने निष्कर्षों के प्रति विनम्र हैं, यह नोट करते हुए कि Lean4 में औपचारिक सत्यापन एन्कोडेड आधारों के तहत व्युत्पत्ति को प्रमाणित करता है लेकिन मूल प्राकृतिक भाषा कथन के साथ अर्थ संबंधी संरेखण (semantic alignment) की गारंटी नहीं देता है। वे स्वीकार करते हैं कि प्राकृतिक भाषा में पूर्णतः निर्दिष्ट अर्थ संबंधी आधार का अभाव है, और इस प्रकार, औपचारिक परिणाम मॉडल की क्षमता को बढ़ा-चढ़ाकर दिखा सकते हैं यदि औपचारिकीकरण (formalization) स्वयं त्रुटिपूर्ण हो। भविष्य के कार्यों में समृद्ध तर्क संरचनाओं और प्रासंगिक जानकारी को शामिल करके सत्यापन परिणामों और अर्थ संबंधी शुद्धता के बीच संरेखण में सुधार करने का प्रस्ताव दिया गया है।