Cryptographic certificates of validity for trustworthy AI

प्रदान किए गए पाठ के आधार पर, मर्डोक जे. गैब्बे द्वारा लिखित शोध पत्र "क्रिप्टोग्राफिक सर्टिफिकेट्स ऑफ वैलिडिटी फॉर ट्रस्टवर्दी एआई" (Cryptographic certificates of validity for trustworthy AI) का विस्तृत तकनीकी सारांश यहाँ दिया गया है।

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

जैसे-जैसे एआई (AI) सिस्टम अनुशंसाएँ (recommendations) देने से स्वायत्त क्रियाओं (autonomous actions) को निष्पादित करने की ओर बढ़ रहे हैं (जैसे कि उड़ान बुक करना, इनवॉइस को मंजूरी देना, कोड तैनात करना), पारंपरिक आश्वासन तंत्र अपर्याप्त होते जा रहे हैं। क्रिप्टोग्राफिक हस्ताक्षर किसी संदेश के मूल (origin) को प्रमाणित करते हैं, लेकिन वे यह सिद्ध नहीं कर सकते कि कोई क्रिया किसी विशिष्ट शुद्धता, सुरक्षा या अनुपालन शर्तों को पूर्व में संतुष्ट करती है। इसी प्रकार, पश्चगामी लॉगिंग (retrospective logging) नीति उल्लंघन होने से पहले उन्हें रोक नहीं सकती। यह शोध पत्र एक ऐसे तंत्र की आवश्यकता को संबोधित करता है जो स्वतंत्र रूप से जांचने योग्य साक्ष्य (independently checkable evidence) प्रदान कर सके कि किसी एजेंट की क्रिया एक सहमत औपचारिक नीति (formal policy) को क्रिया स्वीकार करने से पहले संतुष्ट करती है, और इसके लिए सत्यापनकर्ता (verifier) को एजेंट के आंतरिक कार्यान्वयन पर भरोसा करने या उसकी गणना को पुनः निष्पादित करने की आवश्यकता नहीं होनी चाहिए।

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

यह शोध पत्र औपचारिक तर्क (formal logic) और संक्षिप्त क्रिप्टोग्राफिक प्रमाणों (succinct cryptographic proofs) के बीच सेतु बनाकर वैधता के क्रिप्टोग्राफिक प्रमाणपत्रों (cryptographic certificates of validity) को उत्पन्न करने के लिए एक रूपरेखा प्रस्तावित करता है। कार्यप्रणाली एक तीन-चरणीय पाइपलाइन का अनुसरण करती है:

1. औपचारिक विनिर्देश (Formal Specification): प्रासंगिक नीति या शुद्धता की स्थिति को एक विशिष्ट प्रथम-क्रम तर्क (first-order logic) में एक तार्किक प्रेडिकेट (logical predicate) के रूप में व्यक्त किया जाता है।
2. अरिथमैटाइजेशन (Arithmetisation): इस प्रेडिकेट को बहुपद बाधाओं (polynomial constraints) पर एक विटनेस-चेकिंग समस्या में संकलित किया जाता है। मुख्य गणितीय योगदान प्रथम-क्रम तर्क की वैधता को बहुपद बाधाओं पर निर्णयों में अनुवादित करना है जहाँ:
   • सत्यता (validity) को मान 0 द्वारा दर्शाया जाता है।
   • असत्यता (invalidity) को एक सकारात्मक मान द्वारा दर्शाया जाता है।
   • तार्किक संयोजक (logical connectives) बीजगणितीय संचालनों (algebraic operations) से जुड़े हैं:
     • समानता ($t=t'$) को $(t-t')^2$ के रूप में मैप किया जाता है।
     • संयोजन ($\phi \land \psi$) को $[\phi] + [\psi]$ के रूप में मैप किया जाता है।
     • वियोजन ($\phi \lor \psi$) को $[\phi] \times [\psi]$ के रूप में मैप किया जाता है।
     • एक रेंज पर सार्वभौमिक परिमाणीकरण (Universal quantification) को उस रेंज पर योग (summation) के रूप में मैप किया जाता है।
   • पुनरावृत्ति (recursion) और आगमनात्मक परिभाषाओं (जैसे घातांक) को विटनेस डेटा को मैट्रिसेस (matrices) के रूप में संरचित करके एनकोड किया जाता है, जहाँ कॉलम व्युत्पत्ति चरणों (derivation steps) का प्रतिनिधित्व करते हैं, और एक समर्पित पंक्ति में पॉइंटर्स (pointers) यह सुनिश्चित करते हैं कि पुनरावर्ती संरचना सुव्यवस्थित है।
3. क्रिप्टोग्राफिक प्रमाणन (Cryptographic Certification): एजेंट (या एक संबद्ध प्रूवर) एक संक्षिप्त क्रिप्टोग्राफिक प्रमाण (संभावित रूप से ज़ीरो-नॉलेज) उत्पन्न करता है जो यह प्रदर्शित करता है कि नीति से प्राप्त बहुपद बाधाएं विशिष्ट क्रिया डेटा द्वारा संतुष्ट की गई हैं।

सत्यापन प्रक्रिया में सत्यापनकर्ता द्वारा सार्वजनिक कुंजी (public key) और मापदंडों के विरुद्ध प्रमाण की जाँच करना शामिल है। यदि प्रमाण सत्यापित होता है, तो सिस्टम यह स्वीकार करता है कि क्रिया औपचारिक प्रेडिकेट को संतुष्ट करती है, बिना एजेंट के निजी विटनेस डेटा का निरीक्षण किए या उसकी गणना को पुनः चलाए।

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

• गणितीय अनुवाद (Mathematical Translation): शोध पत्र प्रथम-क्रम तर्क की वैधता को बहुपद बाधाओं में एक संक्षिप्त, अनुप्रयोग-अज्ञेय (application-agnostic) अरिथमैटाइजेशन प्रदान करता है (परिभाषा 2.3–2.7, प्रमेय 2.9)। यह दर्शाता है कि कैसे जटिल तार्किक संरचनाओं, जिसमें पुनरावृत्ति और आगमनात्मक व्युत्पत्ति शामिल हैं, को क्रिप्टोग्राफिक बैकएंड के अनुकूल बीजगणितीय संबंधों में एनकोड किया जा सकता है।
• प्रूफ-कैरिंग एजेंट एक्शन्स (Proof-Carrying Agent Actions): यह एजेंट की क्रियाओं को एक विशिष्ट क्रिप्टोग्राफिक अर्थ में "प्रूफ-कैरिंग" के रूप में अवधारणा देता है। प्रूफ-कैरिंग कोड (PCC) के विपरीत, जिसमें अक्सर सोर्स कोड के निरीक्षण की आवश्यकता होती है, यह दृष्टिकोण अनट्रस्टेड (untrusted), संभावित रूप से ब्लैक-बॉक्स एजेंटों को अनुपालन का संक्षिप्त साक्ष्य प्रदान करने की अनुमति देता है।
• मौजूदा तकनीक के साथ एकीकरण (Integration with Existing Tech): यह रूपरेखा मौजूदा संक्षिप्त तर्क प्रणालियों (जैसे SNARC, zkVM जैसे Cairo या RISC0) और बहुपद प्रतिबद्धता योजनाओं (जैसे Halo2, Zinc) के साथ इंटरफेस करने के लिए डिज़ाइन की गई है। यह प्रस्तावित तर्क को एक उच्च-स्तरीय विनिर्देश परत के रूप में स्थापित करता है जो इन क्रिप्टोग्राफिक प्रिमिटिव्स तक संकलित होता है।
• रनटाइम वेरिफिकेशन से अंतर (Distinction from Runtime Verification): यह दृष्टिकोण रनटाइम वेरिफिकेशन से भिन्न है क्योंकि यह एक पश्चगामी ट्रेस के बजाय एक पूर्व-खाली (pre-emptive), संक्षिप्त प्रमाण प्रदान करता है, और मानक PCC से भिन्न है क्योंकि इसके लिए एजेंट के आंतरिक डिज़ाइन को खुला या विश्वसनीय बनाने की आवश्यकता नहीं है, केवल प्रमाण उत्पन्न करने में सक्षम होना चाहिए।

परिणाम और उदाहरण (Results and Examples)

शोध पत्र अनुभवजन्य बेंचमार्क के बजाय सैद्धांतिक उदाहरणों के माध्यम से दृष्टिकोण को मान्य करता है:

• मूल तर्क (Basic Logic): यह प्रदर्शित करता है कि कैसे सत्य मान, समानता, संयोजन, वियोजन और रेंज चेक को उन बहुपदों के रूप में एनकोड किया जाता है जो केवल तभी शून्य (zero) होते हैं जब शर्त पूरी होती है।
• पुनरावर्ती गणना (Recursive Computation): एक विस्तृत उदाहरण घातांक ($a^b$) की आगमनात्मक परिभाषा को एनकोड करता है। शोध पत्र दिखाता है कि कैसे विटनेस डेटा का एक मैट्रिक्स एक व्युत्पत्ति वृक्ष (derivation tree) को एनकोड कर सकता है, जहाँ पंक्तियाँ 1-3 इनपुट/आउटपुट नमूनों को संग्रहीत करती हैं और पंक्ति 4 पिछले चरणों के पॉइंटर्स को संग्रहीत करती है। वैधता प्रेडिकेट यह सुनिश्चित करता है कि ये पॉइंटर्स एक सुव्यवस्थित पुनरावर्ती संरचना बनाते हैं।
• मजबूती (Robustness): शोध पत्र नोट करता है कि एक मैट्रिक्स में सही इनपुट-आउटपुट मान हो सकते हैं लेकिन यदि "प्रूफ-कैरिंग" संरचना (पॉइंटर्स) गायब या त्रुटिपूर्ण है, तो वह वैधता प्रेडिकेट में विफल हो जाएगा, जो यह दर्शाता है कि प्रमाणत (certificate) परिणाम के बजाय परिणाम की व्युत्पत्ति (derivation) को मान्य करता है।

महत्व और दायरा (Significance and Scope)

शोध पत्र इस कार्य को सोर्स कोड के औपचारिक सत्यापन और क्रिप्टोग्राफिक प्रमाणीकरण के बीच एक "मध्य मार्ग" के रूप में प्रस्तुत करता है। इसका प्राथमिक महत्व एजेंटिक एआई सिस्टम के लिए "प्रूफ-कैरिंग कोड का क्रिप्टोग्राफिक एनालॉग" प्रदान करने में निहित है।

लेखक इस प्रस्ताव की सीमाओं और दायरे को स्पष्ट रूप से नोट करते हैं:

• दायरा (Scope): इसकी गणितीय वास्तुकला सामान्य है और किसी भी ऐसे डोमेन के लिए लागू है जहाँ अनट्रस्टेड पक्षों को शुद्धता के जांचने योग्य साक्ष्य प्रदान करने की आवश्यकता होती है। एआई एजेंटों के लिए इसका विशिष्ट अनुप्रयोग इसलिए चुना गया है क्योंकि स्वायत्त क्रियाएं एक तत्काल आश्वासन की आवश्यकता पैदा करती हैं।
• सीमाएं (Limitations): एक वैधता प्रमाण यह सिद्ध करता है कि एक औपचारिक विनिर्देश (formal specification) को संतुष्ट किया गया है। यह यह सिद्ध नहीं करता कि औपचारिक विनिर्देश स्वयं "सही" है (अर्थात, क्या वह सुरक्षा, कानूनी या नैतिक आवश्यकताओं को सही ढंग से पकड़ता है)। शोध पत्र इस बात पर जोर देता है कि औपचारिक प्रेडिकेट और वास्तविक दुनिया की सुरक्षा के बीच के अंतर को पाटने के लिए शासन (governance), ऑडिटिंग और जोखिम प्रबंधन प्रक्रियाओं की आवश्यकता होती है (NIST फ्रेमवर्क का संदर्भ देते हुए), जिसे केवल गणित या क्रिप्टोग्राफी द्वारा हल नहीं किया जा सकता है।
• भावी कार्य (Future Work): शोध पत्र व्यावहारिक कार्यान्वयन विवरणों की आवश्यकता की पहचान करता है, जिसमें कंपाइलर डिज़ाइन, प्रमाण लागत (proving costs) का बेंचमार्किंग, और नीति लेखन एवं ऑडिटिंग के लिए शासन स्थापित करना शामिल है।

संक्षेप में, शोध पत्र एजेंटिक एआई क्रियाओं के साथ नीति अनुपालन के संक्षिप्त, क्रिप्टोग्राफिक रूप से सत्यापन योग्य प्रमाण संलग्न करने के लिए एक सैद्धांतिक और गणितीय आधार प्रस्तावित करता है, जो विश्वास के मॉडल को "मूल (origin) पर विश्वास करें" से बदलकर "साक्ष्य पर विश्वास करें" में स्थानांतरित करता है।