तकनीकी सारांश: सख्त चरण-स्तरीय सत्यापन के माध्यम से अनुसंधान-स्तर के गणितीय प्रमाणों का मूल्यांकन करना

समस्या विवरण

लार्ज लैंग्वेज मॉडल्स (LLMs) और एआई एजेंटों ने गणितीय समस्या-समाधान में महत्वपूर्ण क्षमताएं प्रदर्शित की हैं; हालाँकि, वे जटिल, अनुसंधान-स्तर के प्रमाणों को कठोरता से सत्यापित करने में संघर्ष करते हैं। मानक वैश्विक मूल्यांकन दृष्टिकोण "संदर्भ विषाक्तता" (context poisoning) से ग्रस्त होते हैं, जहाँ सतही तौर पर प्रशंसनीय कथन सूक्ष्म तार्किक दोषों को छिपा देते हैं, जिससे एजेंट या तो वैधता का भ्रम (hallucination) पाल लेते हैं या अत्यधिक संदेह प्रदर्शित करते हैं। जबकि औपचारिक सत्यापन प्रणालियाँ (जैसे, Lean) पूर्ण गारंटी प्रदान करती हैं, उनका अनुप्रयोग मानव-निर्मित बुनियादी ढांचे और मैन्युअल रूप से बनाए रखे गए पुस्तकालयों की आवश्यकता के कारण बाधित होता है, जो नवीन या अग्रिम गणित को सत्यापित करने के लिए उनकी उपयोगिता को सीमित करता है। वर्तमान एजेंट बिना बाहरी औपचारिकता पर निर्भर हुए, अन्वेषण चरणों के दौरान सुदृढ़ तर्क और त्रुटिपूर्ण तर्क के बीच अंतर करने की अंतर्निहित क्षमता नहीं रखते हैं।

कार्यप्रणाली

यह शोध वैश्विक विसंगति का पता लगाने (global anomaly detection) से रचनात्मक विस्तार (constructive elaboration) के माध्यम से सख्त चरण-स्तरीय सत्यापन की ओर एक बदलाव का प्रस्ताव करता है। मुख्य कार्यप्रणाली सत्यापन कार्य को पुनर्गठित करती है: एक अखंड पाठ में दोष खोजने के बजाय, एजेंट को प्रत्येक कटौती चरण (deduction step) को एक सूक्ष्म-स्तरीय व्युत्पत्ति में स्पष्ट रूप से विस्तारित करने का कार्य दिया जाता है।

त्रिपक्षीय स्पष्टीकरण ढांचा (The Tripartite Explanation Framework)

कठोरता लागू करने और मतिभ्रम (hallucination) को रोकने के लिए, यह ढांचा किसी भी कटौती चरण $s_i$ के तार्किक संबंधों को एक त्रिपक्षीय वास्तुकला $(\Gamma_i, \Sigma_i, T_i)$ का उपयोग करके मॉडल करता है:

1. स्थानीय संदर्भ ($\Gamma_i$): प्रमाण पाठ $S$ से सीधे उत्पन्न कथनों (प्रमेय, परिभाषाएँ, परिकल्पनाएँ) का एक परिमित सेट।
2. बाहरी ज्ञान ($\Sigma_i$): बाहरी साहित्य या स्थापित डोमेन सर्वसम्मति से लिए गए गैर-तुच्छ कथन। एजेंट को अस्तित्वहीन प्रमेयों के मतिभ्रम को रोकने के लिए इन्हें स्पष्ट रूप से उद्धृत या सिद्ध करना चाहिए।
3. पृष्ठभूमि सिद्धांत ($T_i$): तुच्छ कथन, मौलिक तार्किक अभिधारणाएँ (जैसे, Modus Ponens), और सिंथेटिक व्युत्पत्ति के लिए आवश्यक रीराइट नियम। यह घटक कठोर बीजगणितीय पदानुक्रमों के बिना सीधे सुदृढ़ कथनों के हेरफेर की अनुमति देता है।

एक चरण तभी वैध माना जाता है यदि ऐसा स्पष्टीकरण मौजूद हो कि $\Gamma_i \cup \Sigma_i \vdash_{T_i} a_i$, जहाँ $a_i$ चरण का अभिकथन है।

अवस्था-संचालित एजेंटिक वर्कफ़्लो (State-Driven Agentic Workflow)

सत्यापन प्रक्रिया को एक असतत संज्ञानात्मक अवस्था $c_i \in \{OPEN, VERIFIED, FLAWED\}$ पर संचालित एक स्वायत्त, अवस्था-संचालित एजेंट के रूप में लागू किया जाता है:

• आरंभीकरण (Initialization): सभी चरण $OPEN$ से शुरू होते हैं।
• विस्तार (Elaboration): एजेंट एक $OPEN$चरण को एक विस्तृत व्युत्पत्ति में विस्तारित करने का प्रयास करता है, स्पष्ट रूप से$(\Gamma_i, \Sigma_i, T_i)$ को निकालता है।
• अवस्था संक्रमण (State Transitions):
  • $OPEN \to VERIFIED$: यह तभी होता है जब विस्तार तार्किक रूप से बंद (logically closed) हो और $\Sigma_i$ में सभी बाहरी आइटम प्रत्यक्ष उप-प्रमाणों या सटीक उद्धरणों द्वारा समर्थित हों।
  • $OPEN \to FLAWED$: यह केवल तभी होता है जब एक स्पष्ट "दोष साक्षी" (flaw witness) (जैसे, एक गलत कथन, अमान्य निष्कर्ष, या गलत लागू किया गया प्रमेय) की पहचान की जाती है।
  • दोष पुष्टि (Flaw Confirmation): सनकी अति-अस्वीकृति (pedantic over-rejection) से बचने के लिए, कोई भी प्रारंभिक $FLAWED$ अवस्था एक प्रतिकूल जांच (adversarial investigation) को ट्रिगर करती है। यदि कथित दोष एक एपिस्टेमिक अस्पष्टता (जैसे, एक अनकहा डोमेन कन्वेंशन) है न कि एक तार्किक विफलता, तो चरण वापस $OPEN$ में चला जाता है।
• हल्टिंग मानदंड (Halting Criteria): प्रक्रिया वैश्विक स्वीकृति (सभी $VERIFIED$), निश्चित अस्वीकृति (एक दोष की पुष्टि), या समाप्ति (बिना प्रगति के पांच लगातार पुनरावृत्ति) पर समाप्त होती है।

एजेंट बाहरी दावों की स्थिति को ट्रैक करने के लिए एक थ्योरम लेजर (Theorem Ledger) बनाए रखता है, यह सुनिश्चित करता है कि डाउनस्ट्रीम तर्क अन-सत्यापित धारणाओं के आधार पर मान्य न हो।

प्रमुख योगदान

1. पद्धतिगत प्रतिमान परिवर्तन: यह शोध प्राकृतिक भाषा प्रमाण सत्यापन को ब्लैक-बॉक्स विसंगति का पता लगाने से रचनात्मक विस्तार में बदल देता है। एजेंटों को $(\Gamma_i, \Sigma_i, T_i)$ ढांचे के माध्यम से तार्किक निर्भरताओं को स्पष्ट रूप से ट्रेस करने के लिए मजबूर करके, यह दृष्टिकोण सतही पैटर्न मिलान और संदर्भ विषाक्तता को कम करता है।
2. स्वायत्त सत्यापन वर्कफ़्लो: एक अवस्था-संचालित एजेंटिक ढांचा प्रस्तावित किया गया है जो पूर्णता के बजाय तार्किक सुदृढ़ता को प्राथमिकता देता है। एक निश्चित पुष्टिकरण चरण और मजबूत हल्टिंग मानदंडों से लैस, यह प्रणाली सूक्ष्म त्रुटियों को अलग करने के लिए इन्फरेंस-टाइम कंप्यूट का प्रभावी ढंग से उपयोग करती है।
3. माइक्रो-बेंचमार्किंग के माध्यम से अनुभवजन्य अंतर्दृष्टि: यह अध्ययन 21 अनुसंधान-ग्रेड प्रमाणों (FirstProof चुनौती से लिए गए) का एक क्यूरेटेड डायग्नोस्टिक सूट पेश करता है जिसमें स्पष्ट ग्राउंड ट्रुथ है। मूल्यांकन से पता चलता है कि जबकि मानक बेसलाइन अमान्य प्रमाणों में छिपाये गए दोषों का पता लगाने में विफल रहती है, प्रस्तावित ढांचा शून्य गलत स्वीकार (false acceptances) प्राप्त करता है। इसके विपरीत, वैध प्रमाणों की अस्वीकृति मुख्य रूप से अनकहे डोमेन कन्वेंशनों के संबंध में "सनकी अति-कठोरता" (pedantic hyper-rigor) के कारण होती है, जो बेस मॉडल्स की एक विशिष्ट भेद्यता को उजागर करती है न कि सत्यापन तर्क की विफलता को।

परिणाम

ढांचे का मूल्यांकन 21-प्रमाण सूट पर किया गया जिसमें 11 वैध और 10 अमान्य प्रमाण शामिल थे।

• बेसलाइन प्रदर्शन: मानक वैश्विक मूल्यांकनकर्ता (Global GPT-5.4, Global Codex) और वाक्य-दर-वाक्य एब्लेशन ने गंभीर प्रणालीगत कमजोरियां प्रदर्शित कीं। वे अक्सर अमान्य प्रमाणों को स्वीकार कर लेते थे (False Negatives) क्योंकि वे संरचनात्मक रूप से कठोर लेकिन गणितीय रूप से शून्य पाठ से धोखा खा जाते थे, और वैध प्रमाणों को खारिज कर देते थे (False Positives) क्योंकि वे मानक नोटेशनल कन्वेंशनों में अंतराल की कल्पना (hallucinate) कर लेते थे।
• एजेंट प्रदर्शन: रचनात्मक सत्यापन एजेंट (Constructive Verification Agent) ने 100% अमान्य प्रमाणों में घातक कटौती दोषों को सफलतापूर्वक पहचाना और अलग किया। वैध प्रमाणों पर, इसने 11 में से 8 मामलों को सही ढंग से सत्यापित किया। वैध प्रमाणों के 3 अस्वीकार मामले तार्किक कमियों के कारण नहीं थे, बल्कि एजेंट की उन निहित डोमेन परंपराओं (जैसे, विशिष्ट Lie group संदर्भों में सबग्रुप्स की रैखिकता) को अनुमानित करने में असमर्थता के कारण थे जिन्हें मानव विशेषज्ञ डिफ़ॉल्ट रूप से मान लेते हैं।
• मजबूती (Robustness): बेसलाइन के विपरीत, जो परीक्षणों के बीच भिन्नता दिखाती थी, एजेंट ने मैक्रो-लेवल निरंतरता प्रदर्शित की, जिससे स्वतंत्र रन के माध्यम से समान अंतिम निर्णय प्राप्त हुए।

महत्व और दावे

यह शोध दावा करता है कि एजेंटों को सतर्क, मानव-गणितज्ञ-समान तरीके से सत्यापन नोट्स व्यवस्थित करने के लिए प्रेरित करने से वैध प्रमाणों को त्रुटिपूर्ण प्रमाणों से अलग करने की उनकी क्षमता में काफी सुधार होता है। प्राथमिक महत्व यह प्रदर्शित करने में निहित है कि विस्तृत विस्तार (detailed elaboration) स्वयं एक तंत्र के रूप में कार्य करता है जो उन सूक्ष्म तार्किक त्रुटियों की खोज को बढ़ाता है जिन्हें मानक तर्क अनदेखा कर देता है।

लेखक इस बात पर जोर देते हैं कि यह कार्य औपचारिक प्रमाण सहायकों या 'मैथमेटिकल वर्नाकुलर' (MV) को फिर से बनाने का लक्ष्य नहीं रखता है। इसके बजाय, यह प्राकृतिक भाषा में संचालित होने वाले स्वचालित प्रमाण-समीक्षा प्रणालियों के लिए एक सैद्धांतिक आधार स्थापित करता है। निष्कर्ष बताते हैं कि मॉडल को विवरण लिखने के लिए मजबूर करके, एजेंट प्रभावी रूप से मृत अंत (dead ends) को काट सकते हैं और फ्रंटियर गणितीय अवधारणाओं में मतिभ्रम को कम कर सकते हैं। शोध निष्कर्ष निकालता है कि हालांकि बेस मॉडल अनकहे कन्वेंशनों के प्रति संवेदनशील बने रहते हैं, प्रस्तावित ढांचा भविष्य के प्राकृतिक भाषा गणितीय एजेंटों की आंतरिक तर्क प्रक्रियाओं में कठोर, चरण-स्तरीय सत्यापन को एकीकृत करने के लिए एक सामान्यीकरण योग्य प्रतिमान (generalizable paradigm) प्रदान करता है।