तकनीकी सारांश: LLM-ग्राउंडेड व्याख्याओं के साथ ध्वनिपूर्ण और पूर्ण न्यूरोसिम्बोलिक तर्क (Sound and Complete Neurosymbolic Reasoning)

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

लार्ज लैंग्वेज मॉडल्स (LLMs) के पास विशाल पैरामीट्रिक ज्ञान है लेकिन वे अंतर्निहित विसंगतियों और अपूर्णता से ग्रस्त हैं, जो उन्हें औपचारिक तर्क (formal reasoning) के लिए एक स्टैंडअलोन नॉलेज बेस के रूप में अविश्वसनीय बनाता है। न्यूरोसिम्बोलिक तर्क के पारंपरिक दृष्टिकोण—जैसे कि LLMs को तार्किक तर्क करने के लिए प्रॉम्प्ट करना, उन्हें बाहरी सॉल्वर के लिए सिम्बोलिक इनपुट उत्पन्न करने के लिए उपयोग करना, या उन्हें प्रमाणों (proofs) पर फाइन-ट्यून करना—जब LLM का ज्ञान विरोधाभासी होता है, तो तर्क प्रक्रिया की ध्वनिपूर्णता (soundness) और पूर्णता (completeness) के संबंध में औपचारिक गारंटी प्रदान करने में विफल रहते हैं। इसके अलावा, मानक तथ्यात्मकता मूल्यांकन विधियाँ आमतौर पर एक एकल सत्य मान (truth value) प्रदान करती हैं, जो LLM की एपिस्टेमिक अवस्था (epistemic state) (जैसे कि क्या वह अनिश्चित है या वास्तव में संघर्षित है) को स्पष्ट नहीं करती हैं। मुख्य चुनौती यह है कि कैसे एक LLM के व्यापक-कवरेज ज्ञान को एक औपचारिक तर्क प्रणाली में एकीकृत किया जाए जबकि तर्क के सैद्धांतिक गुणों (soundness और completeness) को सुरक्षित रखा जा सके और उन विसंगतियों को प्रभावी ढंग से प्रबंधित किया जा सके जो LLM उत्पन्न करता है।

कार्यप्रणाली (Methodology)

लेखक एक ऐसा ढांचा प्रस्तावित करते हैं जो एक पैराकंसिस्टेंट लॉजिक (paraconsistent logic), विशेष रूप से एनालिटिक कंटेनमेंट (Analytic Containment - AC), के इंटरप्रिटेशन फंक्शन में सीधे एक LLM को एकीकृत करता है। AC एक द्विपक्षीय तर्क (bilateral logic) है जो तार्किक विस्फोट (logical explosion) के बिना असंगत जानकारी को संभालने में सक्षम है।

1. द्विपक्षीय तथ्यात्मकता मूल्यांकन (Bilateral Factuality Evaluation)

LLM को एक एकल सत्य मान (True/False) असाइन करने के लिए कहने के बजाय, सिस्टम एक द्विपक्षीय मूल्यांकन दृष्टिकोण का उपयोग करता है। एक LLM जज को एक परमाणु सूत्र (atomic formula) $\phi$ के लिए दो स्थितियों का स्वतंत्र रूप से आकलन करने के लिए प्रॉम्प्ट किया जाता है:

• सत्यापन (Verification - $P^+$): क्या LLM $\phi$ को सत्यापित कर सकता है?
• खंडन (Refutation - $P^-$): क्या LLM $\phi$ का खंडन कर सकता है?

आउटपुट को वीक क्लेने (weak Kleene) सत्य मानों ($t$=true, $f$=false, $e$=undefined/unknown) में मैप किया जाता है। इन्हें एक सामान्यीकृत सत्य मान $\langle u, v \rangle \in V_3 \times V_3$ बनाने के लिए जोड़ा जाता है। इसके परिणामस्वरूप चार प्राथमिक अवस्थाएं होती हैं:

• $\langle t, f \rangle$: सत्यापित (True)।
• $\langle f, t \rangle$: खंडित (False)।
• $\langle t, t \rangle$: ग्लट (Glut) (दोनों सत्यापित और खंडित; विसंगति)।
• $\langle f, f \rangle$: गैप (Gap) (न तो सत्यापित और न ही खंडित; अनिश्चितता/अज्ञानता)।

औपचारिक तर्क के लिए आवश्यक स्थिरता सुनिश्चित करने के लिए, एक कैशिंग तंत्र ($\zeta_c$) का उपयोग किया जाता है, जो गणना किए जाने के बाद परमाणु सूत्रों के मूल्यांकन को अपरिवर्तनीय रूप से संग्रहीत करता है।

2. LLM-ग्राउंडेड व्याख्याएँ (LLM-Grounded Interpretations)

पेपर एक LLM-ग्राउंडेड इंटरप्रेटेशन ($I$) को परिभाषित करता है जहाँ परमाणु सूत्रों का इंटरप्रेटेशन कैश किए गए द्विपक्षीय मूल्यांकन फंक्शन $\zeta_c$ द्वारा निर्धारित होता है।

• सैद्धांतिक एकीकरण: लेखक सिद्ध करते हैं कि प्रत्येक LLM-ग्राउंडेड इंटरप्रेटेशन के लिए, एक समतुल्य मानक इंटरप्रेटेशन मौजूद है, और इसके विपरीत भी।
• गुणों का संरक्षण: वे प्रदर्शित करते हैं कि AC (विशेष रूप से $AC^{rQ}$) के एनालिटिक टैबलो सिस्टम की ध्वनिपूर्णता (soundness) और पूर्णता (completeness) संरक्षित रहती है, भले ही इंटरप्रेटेशन LLM पर आधारित हो। इसका अर्थ है कि तर्क करने वाला सिस्टम (reasoner) समान गारंटियों के साथ निष्कर्ष निकाल सकता है जैसा कि एक मानक लॉजिक में होता है, बावजूद इसके कि LLM का ज्ञान संभावित रूप से असंगत हो सकता है।

3. कार्यान्वयन: एक बेलनैप कंप्यूटर (Implementation: A Belnap Computer)

लेखकों ने पायथन में एक अवधारणा-प्रूफ बेलनैप कंप्यूटर (एक ऐसा रीज़नर जिसे असंगत जानकारी को संभालने के लिए डिज़ाइन किया गया है) को लागू किया है।

• आर्किटेक्चर: यह फॉरवर्ड-चेनिंग इन्फरेंस (नियमों से नए तथ्यों को निकालना) को टैबलो-आधारित सैटिस्फिएबिलिटी चेकिंग के साथ जोड़ता है।
• LLM मूल्यांकन नियम: टैबलो निर्माण के दौरान, एक llm-eval नियम परमाणु सूत्रों के द्विपक्षीय सत्य मान के लिए LLM जज को क्वेरी करता है।
• ग्लट हैंडलिंग: जब ग्लट का पता चलता है (उदाहरण के लिए, सिस्टम $P(a)$ का अनुमान लगाता है लेकिन LLM इसका खंडन करता है), तो टैबलो बंद (explode) नहीं होता है। इसके बजाय, यह अभिकथन (assertion) और उसके खंडन दोनों को बनाए रखता है, जिससे विरोधाभास स्थानीयकृत (localized) रहता है।

मुख्य योगदान (Key Contributions)

1. द्विपक्षीय तथ्यात्मकता मूल्यांकन: एक नवीन विधि जो LLM की एपिस्टेमिक अवस्था (सुसंगत, असंगत, या अनिश्चित) को उजागर करती है, न कि एक एकल निर्णय थोपती है, जो एकपक्षीय (unilateral) मूल्यांकन की तुलना में अधिक क्रियाशील डायग्नोस्टिक्स प्रदान करती है।
2. LLM-ग्राउंडेड व्याख्याएँ: एक सैद्धांतिक ढांचा जो LLMs को सीधे एक पैराकंसिस्टेंट लॉजिक के औपचारिक अर्थ विज्ञान (formal semantics) में एकीकृत करता है, जिससे अंतर्निहित तर्क प्रणाली की ध्वनिपूर्णता और पूर्णता बनी रहती है।
3. अनुभवजन्य सत्यापन: यह प्रदर्शित करना कि द्विपक्षीय मूल्यांकन तथ्य जांच बेंचमार्क (GPQA और SimpleQA) पर एकपक्षीय बेसलाइन की तुलना में मैक्रो-F1 स्कोर में सुधार (~6 प्रतिशत अंक) करता है, हालांकि अनिश्चित मामलों में परहेज (abstention) के कारण कवरेज कम हो जाता है।
4. व्यावहारिक प्रणाली: एक कार्यशील बेलनैप कंप्यूटर का कार्यान्वयन जो नॉलेज बेस में चिकित्सकीय रूप से महत्वपूर्ण त्रुटियों (ग्लट्स) का सफलतापूर्वक पता लगाता है और समग्र सैटिस्फिएबिलिटी को बनाए रखता है।

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

लेखकों ने विभिन्न LLMs (फ्लैगशिप और डिस्टिल्ड मॉडल्स) के साथ GPQA और SimpleQA बेंचमार्क से प्राप्त डेटासेट का उपयोग करके दृष्टिकोण का मूल्यांकन किया।

• सटीकता बनाम कवरेज (Accuracy vs. Coverage): द्विपक्षीय मूल्यांकन ने एकपक्षीय बेसलाइन (0.633) की तुलना में उच्च मैक्रो-F1 स्कोर (फ्लैगशिप मॉडल्स के लिए GPQA पर लगभग 0.699) प्राप्त किया, लेकिन कम कवरेज (0.589 बनाम 1.000) के साथ। सिस्टम अनिश्चित ($\langle t, t \rangle$) या अज्ञानी ($\langle f, f \rangle$) मामलों पर परहेज करता है, जिससे उन मामलों पर उच्च विश्वसनीयता मिलती है जहाँ यह उत्तर प्रदान करता है।
• एपिस्टेमिक अवस्थाएँ: प्रयोगों से पता चला कि LLMs अक्सर गैप के बजाय ग्लट्स (विसंगतियाँ) उत्पन्न करते हैं। उदाहरण के लिए, SimpleQA डेटासेट पर, GPT मॉडल्स ने विरोधाभास (ग्लट दर ~59%) की ओर उच्च प्रवृत्ति दिखाई, जबकि Claude मॉडल्स अधिक सतर्क थे (उच्च गैप दर)।
• मेडिकेशन सेफ्टी यूज़ केस: सिस्टम का उपयोग दवा सुरक्षा के संबंध में 228 घोषित और 712 अनुमानित कथनों के नॉलेज बेस पर किया गया।
  • इसने चिकित्सकीय रूप से महत्वपूर्ण त्रुटियों (ग्लट्स) के 92 मामलों का पता लगाया (जैसे, यह अनुमान लगाना कि ओपिओइड्स गैर-नशीले हैं या बीटा-ब्लॉकर्स अस्थमा रोगियों के लिए सुरक्षित हैं)।
  • इन 92 विरोधाभासों के बावजूद, सिस्टम सैटिस्फिएबल (satisfiable) रहा, जिसने तार्किक विस्फोट के बिना त्रुटियों को सफलतापूर्वक स्थानीयकृत किया।
  • कम्प्यूटेशनल विश्लेषण से पता चला कि LLM लेटेंसी (latency) प्रमुख बाधा है, लेकिन समानांतरकरण (parallelization) और कैशिंग जैसे मानक अनुकूलन के साथ यह प्रणाली मध्यम आकार के नॉलेज बेस (100k+ कथनों) के लिए स्केलेबल है।

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

पेपर का दावा है कि यह न्यूरोसिंबोलिक तर्क के लिए एक सैद्धांतिक ढांचे के साथ एक व्यावहारिक कार्यान्वयन प्रदान करता है जो LLM के ज्ञान का लाभ उठाता है और अंतर्निहित तर्क की ध्वनिपूर्णता और पूर्णता को सुरक्षित रखता है।

• पैराडाइम शिफ्ट: पिछले कार्यों के विपरीत जो LLMs को तर्क करने के लिए लॉजिक का उपयोग करने का प्रयास करते हैं, यह दृष्टिकोण लॉजिक को LLM का उपयोग करके तर्क करने के लिए बनाता है।
• मजबूती (Robustness): सिस्टम को उन वास्तविक दुनिया के परिदृश्यों के लिए डिज़ाइन किया गया है जहाँ ज्ञान के स्रोत स्वाभाविक रूप से असंगत होते हैं। यह विरोधाधानों को मरम्मत की आवश्यकता वाली घातक त्रुटियों के रूप में नहीं, बल्कि स्थानीयकृत एपिस्टेमिक अवस्थाओं (ग्लट्स) के रूप में मानता है जिन्हें पहचाना और प्रबंधित किया जा सकता है।
• क्रियाशील डायग्नोस्टिक्स: "संघर्षित" (ग्लट) और "अज्ञानी" (गैप) अवस्थाओं के बीच अंतर करके, सिस्टम डाउनस्ट्रीम अनुप्रयोगों को विशिष्ट जानकारी प्रदान करता है कि निष्कर्ष क्यों अनिश्चित है, जिससे अधिक रूढ़िवादी और सुरक्षित निर्णय लेने (जैसे चिकित्सा संदर्भों में) में सक्षम बनाया जा सके।
• स्केलेबिलिटी: लेखक तर्क देते हैं कि हालांकि LLM API लेटेंसी वर्तमान में प्राथमिक लागत है, लॉजिकल ओवरहेड न्यूनतम है, और यह डेस्क्रिप्शन लॉजिक रीज़नर्स के मौजूदा अनुकूलन तकनीकों का उपयोग करके उत्पादन-स्तर के नॉलेज बेस के लिए व्यवहार्य है।