तकनीकी सारांश: Theoria – अनौपचारिक तर्क अवस्थाओं पर रीराइट-स्वीकार्यता सत्यापन

1. समस्या विवरण

यह शोध पत्र AI तर्क में "विश्वास की समस्या" (trust problem) को संबोधित करता है: यह निर्धारित करना कि कब एक AI-जनित उत्तर विश्वसनीय विश्वास उत्पन्न करने के योग्य है, विशेष रूप से सुरक्षा-महत्वपूर्ण क्षेत्रों (विज्ञान, कानून, वित्त, चिकित्सा) में। वर्तमान दृष्टिकोणों के सामने एक द्वंद्व है:

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

मुख्य चुनौती पूर्ण औपचारिकता की आवश्यकता के बिना अनौपचारिक तर्क को सत्यापित करना है, जबकि यह सुनिश्चित करना है कि त्रुटियाँ—विशेष रूप से अनकही धारणाएँ और तार्किक छलांगें—दृश्यमान और ऑडिट करने योग्य हों।

2. कार्यप्रणाली: Theoria आर्किटेक्चर

Theoria एक सत्यापन आर्किटेक्चर पेश करता है जो एक सॉल्वर के प्राकृतिक-भाषा उत्तर को एक प्रूफ विटनेस (proof witness) में रीराइट करता है: जो कि टाइप किए गए स्टेट ट्रांजिशन (state transitions) का एक क्रम है।

2.1 रीराइट फ्रेमिंग (The Rewrite Framing)

एक प्रमाण को गद्य (prose) के एक ब्लॉक के रूप में मानने के बजाय, Theoria इसे अवस्थाओं (states) के एक प्रक्षेपवक्र $(S_0, S_1, \dots, S_n)$ में विघटित करता है।

• अवस्था (State - $S_i$): स्थापित तथ्यों और वर्तमान लक्ष्य का एक क्रमबद्ध स्ट्रिंग लिस्ट।
• ट्रांजिशन (Transition): $S_{i-1}$ से $S_i$ तक का एक चरण एक विशिष्ट जस्टिफिकेशन टाइप (justification type) द्वारा लाइसेंस प्राप्त होता है:
  1. उद्धरण (Citation): एक प्रमेय (theorem), परिभाषा, या अनुमान का नियम।
  2. गणना (Computation): अंकगणितीय या प्रतीकात्मक हेरफेर।
  3. समस्या दी गई (Problem Given): समस्या टेक्स्ट में स्पष्ट रूप से बताए गए तथ्य।
• परिवर्तन की पूर्णता का इनवेरिएंट (The Completeness-of-Change Invariant): $S_{i-1}$ और $S_i$ के बीच प्रत्येक सिमेंटिक अंतर को घोषित जस्टिफिकेशन द्वारा स्पष्ट किया जाना चाहिए। यदि $S_i$ को प्राप्त करने के लिए किसी प्रिसिस (premise) की आवश्यकता है लेकिन वह पिछले स्टेट या जस्टिफिकेशन में मौजूद नहीं है, तो यह एक अनलाइसेंस्ड म्यूटेशन (unlicensed mutation) माना जाता है।

2.2 सत्यापन पाइपलाइन (Verification Pipeline)

सिस्टम एक लूप में कार्य करता है: Solve $\to$ Formalize $\to$ Judge $\to$ Filter $\to$ Repair।

1. सॉल्वर (Solver): एक प्राकृतिक-भाषा समाधान प्रस्तावित करता है (टूल-ऑगमेंटेड, जैसे वेब सर्च)।
2. फॉर्मलाइज़र (Formalizer): समाधान को स्टेट-ट्रांजिशन विटनेस में रीराइट करता है। यह लागू करता है कि उपयोग से पहले प्रिसिस (premises) स्पष्ट होने चाहिए।
3. समानांतर विशेष जजिंग (Parallel Specialized Judging):
   • कंप्यूटेशन जजेस: चरणों को शुरू से ही पुनर्गणना करते हैं।
   • साइटेशन जजेस: विशिष्ट स्टेट डिफ (diff) के विरुद्ध उद्धृत प्रमेयों के अस्तित्व और प्रयोज्यता को सत्यापित करते हैं।
   • प्रॉब्लम-गिवन जजेस: मूल टेक्स्ट के विरुद्ध तथ्यों की जाँच करते हैं।
   • इनिशियल-स्टेट जज: $S_0$ का ऑडिट करता है ताकि यह सुनिश्चित हो सके कि शुरुआत में कोई अनलाइसेंस्ड प्रिसिस न जोड़ा जाए।
   • सभी जजेस को केवल संभाव्यता की पुष्टि करने के बजाय त्रुटियों को खोजने के लिए एडवर्सरियल रूप से प्रॉम्प्ट किया जाता है।
4. पेडेंट्री फ़िल्टर (Pedantry Filter): सारभूत त्रुटियों और अनौपचारिक नोटेशन या संपीड़न के संबंध में अत्यधिक कठोरता के बीच अंतर करता है।
5. कन्वेंशन लिफ्ट (Convention Lift): सिस्टम को एक चरण स्वीकार करने की अनुमति देता है यदि एक मानक, उद्धृत डोमेन कन्वेंशन अस्वीकृति को हल कर देता है, बशर्ते कि धारणा को स्पष्ट रूप से रिकॉर्ड किया गया हो।
6. सर्टिफाई-ऑर-डिक्लाइन (Certify-or-Decline): सिस्टम एक बाइनरी निर्णय आउटपुट करता है। यदि सभी चरण पास हो जाते हैं (या कन्वेंशन लिफ्ट के माध्यम से हल हो जाते हैं), तो उत्तर सर्टिफाइड (Certified) है। यदि कोई भी चरण विफल होता है और सीमाओं के भीतर मरम्मत नहीं किया जा सकता है, तो उत्तर डिक्लाइंड (Declined) है।

3. मुख्य योगदान

शोध पत्र का प्राथमिक योगदान कई मॉडलों का उपयोग या स्टेप-चेकिंग नहीं है, बल्कि विशिष्ट विटनेस फॉर्मेट और इसके सैद्धांतिक गारंटी है:

• एक्सपोज़र गारंटी (प्रपोजिशन 4.4): 'कम्प्लीटनेस-ऑफ-चेंज' इनवेरिएंट छिपे हुए प्रिसिस (hidden premises) (ग्लोबल रीजनिंग गैप्स) को स्थानीय, दृश्यमान अनलाइसेंस्ड म्यूटेशन में बदल देता है। एक छिपे हुए प्रिसिस को या तो स्टेट में एक नए तत्व के रूप में प्रकट होना चाहिए (जो लाइसेंस चेक को ट्रिगर करता है) या इनवेरिएंट का उल्लंघन करना चाहिए। यह त्रुटियों को सतह पर लाता है जहाँ उन्हें स्थानीय जजेस द्वारा पकड़ा जा सके।
• एरर-क्लास प्रेडिक्शन (प्रपोजिशन 4.5): फॉर्मेट भविष्यवाणी करता है कि सत्यापन लाभ निम्नलिखित में केंद्रित होंगे:
  • छिपे हुए प्रिसिस (Hidden Premises): अनलाइसेंस्ड म्यूटेशन के रूप में उजागर होते हैं।
  • मनगढ़ंत उद्धरण (Fabricated Citations): उजागर होते हैं क्योंकि साक्ष्य को स्पष्ट रूप से टाइप किया गया है और डिफ (diff) के विरुद्ध जांचा गया है।
  • कोई लाभ नहीं: अंकगणितीय त्रुटियां और प्रमेय का गलत अनुप्रयोग (जहाँ प्रमेय मौजूद है लेकिन गलत तरीके से लागू किया गया है) संरचनात्मक एक्सपोजर लाभ प्राप्त नहीं करते हैं, क्योंकि त्रुटि सिमेंटिक है न कि स्ट्रक्चरल।
• विफलता का विखंडन (Decomposition of Failure): पेपर एक्सपोज़र फेलियर (फॉर्मेट त्रुटि को छिपा देता है) और जज फेलियर (जज उजागर त्रुटि को मिस कर देता है) के बीच अंतर करता है। Theoria का लक्ष्य पहले को कम करना है, दूसरे को अनुभवजन्य रूप से संबोधित किया जाना है।

4. अनुभवजन्य परिणाम (Empirical Results)

मूल्यांकन HLE-Verified Gold (185 विशेषज्ञ समस्याएँ) और GPQA Diamond (65 स्नातक-स्तरीय विज्ञान समस्याएँ) पर किया गया।

4.1 HLE-Verified Gold पर प्रदर्शन

• सर्टिफाइड प्रिसिजन: 91.4% (105/105 में से 96 सही) 95% विल्सन सीआई [84.5%, 95.4%] के साथ।
• कवरेज: 56.8% (185 में से 105 समस्याएँ सर्टिफाइड)।
• एसिमेट्री (Asymmetry): डिक्लाइंड उत्तर प्रमाणित उत्तरों की तुलना में गलत होने की संभावना ~5.0$\times$ अधिक थी (42.5% बनाम 8.6% त्रुटि दर)।
• सोल्वर-ओनली के साथ तुलना: एक वेब-ऑगमेंटेड सॉल्वर ने 100% कवरेज पर 83.8% सटीकता प्राप्त की। Theoria के पाइपलाइन ने त्रुटियों के एक बड़े हिस्से को फ़िल्टर किया, जिससे सर्टिफाइड बकेट में त्रुटि दर घटकर 8.6% रह गई।
• होलिस्टिक जजेस के साथ तुलना: होलिस्टिक LLM जजेस (एक एकल कॉन्फिडेंस स्कोर असाइन करने वाले) ने मैच किए गए कवरेज पर तुलनीय प्रिसिजन (92.4–93.3%) प्राप्त किया। हालांकि, वे अलग-अलग समस्याओं पर विफल रहे (जैकर्ड इंडेक्स 0.14–0.36), जो पूरक त्रुटि कवरेज का संकेत देते हैं।

4.2 एडवर्सरियल रोबस्टनेस (Adversarial Robustness)

95 पॉइज़न्ड प्रूफ (विशिष्ट त्रुटि प्रकारों को इंजेक्ट करना) के बेंचमार्क पर:

• कुल डिटेक्शन: Theoria ने 94.7% (95/95 में से 90) पकड़ा, जबकि होलिस्टिक जजिंग ने 83.2% (95/95 में से 79) पकड़ा ($p = 0.0017$)।
• एरर क्लास स्पेसिफिक्स:
  • छिपे हुए प्रिसिस (Hidden Premises): Theoria 90.6% बनाम होलिस्टिक 62.5% (28 pp गैप)।
  • मनगढ़ंत उद्धरण (Fabricated Citations): Theoria 100% बनाम होलिस्टिक 90%।
  • अंकगणित/गलत लागू प्रमेय (Arithmetic/Misapplied Theorems): प्रदर्शन समान था (~95% और ~93% क्रमशः), जो इस सैद्धांतिक भविष्यवाणी की पुष्टि करता है कि फॉर्मेट इन त्रुटि प्रकारों के लिए कोई स्ट्रक्चरल लाभ नहीं देता है।

4.3 आउट-ऑफ-डिस्ट्रीब्यूशन (GPQA Diamond)

• सर्टिफाइड प्रिसिजन: 97.1% (34/34 में से 33)।
• कवरेज: 52.3%।
• एक अलग बेंचमार्क पर उच्च प्रिसिजन यह सुझाव देता है कि "सर्टिफाई-ऑर-डिक्लाइन" सीमा तर्क की फॉर्मलाइजेबिलिटी से प्रेरित है, न कि बेंचमार्क-विशिष्ट कैलिब्रेशन से।

4.4 एन्सेम्बल क्षमता (Ensemble Potential)

चूंकि Theoria और होलिस्टिक जज अलग-अलग सेट की समस्याओं पर विफल होते हैं, इसलिए एन्सेम्बल रणनीतियाँ (जैसे, बहुमत वोट) 58.9% कवरेज पर 93.6% प्रिसिजन प्राप्त करती हैं, जो किसी भी एकल विधि से बेहतर है।

5. महत्व और दावे

पेपर का दावा है कि Theoria एक स्केलेबल ओवरसाइट (scalable oversight) तंत्र प्रदान करता है जो कच्चे LLM आउटपुट और औपचारिक सत्यापन के बीच के अंतर को पाटता है।

• ऑडिटेबिलिटी (Auditability): स्केलर स्कोर के विपरीत, Theoria एक मानव-पठनीय प्रूफ ट्रेस बनाता है जहाँ प्रत्येक चरण को स्वतंत्र रूप से चुनौती दी जा सकती है।
• स्ट्रक्चरल एडवांटेज (Structural Advantage): Theoria केवल जज द्वारा गद्य से प्रमाण को पुनर्गठित करने पर निर्भर नहीं है। इसके बजाय, यह सत्यापन कार्य को एक स्थानीय प्रश्न में बदल देता है: "क्या यह जस्टिफिकेशन इस विशिष्ट स्टेट चेंज को लाइसेंस देता है?"
• पूरकता (Complementarity): पेपर तर्क देता है कि Theoria होलिस्टिक जजेस का विकल्प नहीं है, बल्कि एक पूरक दृष्टिकोण है। त्रुटियों पर कम जैकार्ड ओवरलैप यह सुझाव देता है कि संरचनात्मक रूप से भिन्न सत्यापन आर्किटेक्चर को संयोजित करने से उच्च विश्वसनीयता प्राप्त होती है।
• सीमाएँ (Limitations): लेखक स्वीकार करते हैं कि Theoria उन त्रुटियों का पता नहीं लगा सकता है जो कोई दृश्यमान स्टेट म्यूटेशन उत्पन्न नहीं करती हैं (जैसे, $S_0$ में समस्या विवरण की सूक्ष्म गलत व्याख्याएं) और यह वर्तमान में LLM जजेस पर निर्भर करता है न कि औपचारिक बैकएंड (जैसे Lean या SMT सॉल्वर) पर, हालांकि इसे उनके साथ संगत होने के लिए डिज़ाइन किया गया है।

संक्षेप में, Theoria यह प्रदर्शित करता है कि अनौपचारिक तर्क पर कम्प्लीटनेस-ऑफ-चेंज इनवेरिएंट को लागू करके, यह संभव है कि छिपे हुए धारणाओं और मनगढ़ंत साक्ष्यों को सतह पर लाया जा सके जिन्हें मानक होलिस्टिक मूल्यांकन मिस कर देता है, जिससे AI-जनित तर्क में विश्वास के लिए एक कठोर, ऑडिट करने योग्य सीमा प्रदान की जा सके।