एथेरियम के सह-संस्थापक विटालिक ब्यूटेरिन ने एक नई प्रोग्रामिंग भाषा का प्रस्ताव रखा। यह सीधे Lean या HOL में संकलित होगी, जो एक और औपचारिक प्रमाण सहायक है।
यह विचार इस बात पर केंद्रित है कि लोग AI आउटपुट को कैसे पढ़ते हैं। कृत्रिम बुद्धिमत्ता तेजी से बड़े ब्लॉकों में स्वचालित प्रमाण उत्पन्न करती है, अक्सर किसी भी मानव टीम द्वारा हाथ से लिखे जाने की तुलना में तेजी से। कुछ पाठक जल्दी से यह पुष्टि कर सकते हैं कि वे प्रमाण वास्तव में क्या स्थापित करते हैं।
AI प्रमाण पाठकों के लिए केवल एक भाषा
Lean एक प्रमाण सहायक है, एक सॉफ़्टवेयर जिसका उपयोग गणितज्ञ और इंजीनियर प्रमाण लिखने के लिए करते हैं जिसे एक कंप्यूटर पंक्ति दर पंक्ति जांच सकता है। एथेरियम के शोधकर्ता पहले से ही इसका उपयोग क्रिप्टोग्राफ़िक कोड और सहमति लॉजिक को सत्यापित करने के लिए करते हैं। प्रमाण सहायक लगभग 60 वर्षों से मौजूद हैं, फिर भी यह क्षेत्र एक विशेष रुचि का बना हुआ है।
अपने पोस्ट में, ब्यूटेरिन ने तर्क किया कि एक प्रमाण के आंतरिक चरणों में केवल एक आवश्यकता होती है। वह आवश्यकता गणितीय सटीकता है, और कुछ नहीं। पाठक कभी भी उस मशीनरी का सीधे निरीक्षण नहीं करते। परिभाषाएँ और प्रमेय अलग तरीके से काम करते हैं, क्योंकि मनुष्य उन भागों को पढ़ते हैं ताकि यह जान सकें कि एक सॉफ़्टवेयर वास्तव में क्या गारंटी देता है।
ब्यूटेरिन ने मई के ब्लॉग पोस्ट में एक संबंधित विभाजन का अन्वेषण किया। वहाँ, एक गणितीय प्रमाण दिखाता है कि कुशल निम्न-स्तरीय कोड एक अलग, पठनीय विशिष्टता से मेल खाता है, इसलिए एकल ऑडिट दोनों संस्करणों को एक साथ कवर करता है।
उनका समय भी एथेरियम के अपने पुनर्निर्माण प्रयास के साथ मेल खाता है, जिसे एक अलग उपनाम, लीन एथेरियम रोडमैप कहा जाता है। इस बीच, शोधकर्ता एक औपचारिक रूप से सत्यापित ZK-EVM, एथेरियम की वर्चुअल मशीन (EVM) का एक शून्य-ज्ञान-सिद्ध संस्करण, तुलनीय तरीकों का उपयोग करके बना रहे हैं।
AI प्रमाण लिखता है, मानव दावे जांचते हैं
बड़े भाषा मॉडल पहले से ही उपयोगी लीन प्रमाण लिख सकते हैं। बुटेरिन ने क्लॉड और डीपसीक 4 प्रो को सक्षम उपकरणों के रूप में नामित किया है, साथ ही लीनस्ट्राल, एक छोटा मॉडल जो विशेष रूप से लीन के लिए ट्यून किया गया है। एक उदाहरण परियोजना evm-asm है, जो एक EVM कार्यान्वयन है जिसे एक पठनीय संदर्भ के खिलाफ सत्यापित किया गया है। यह क्षमता हाल ही में बुटेरिन AI चुनौती में डेवलपर्स द्वारा प्रदर्शित तर्क कौशल की गूंज है। परीक्षकों ने उस चुनौती को कुछ घंटों के भीतर हल कर दिया।
हालांकि, दांव केवल सुविधा से परे हैं। सुरक्षा शोधकर्ताओं ने इस वर्ष AI-सहायता प्राप्त शोषण प्रयासों में एक कूद का पता लगाया है। औपचारिक रूप से सत्यापित कोड उस प्रवृत्ति के खिलाफ एक रक्षा प्रदान करता है। एक अधिक मित्रवत विनिर्देशन भाषा डेवलपर्स को दावों का ऑडिट करने की अनुमति देगी बिना चारों ओर के प्रमाण के माध्यम से जाने के।
एथेरियम के शोध सर्कल से परे
बुटेरिन इन विचारों का सार्वजनिक रूप से परीक्षण करते रहते हैं, जैसे कि उन्होंने हाल ही में एक गुमनाम बिलबोर्ड का प्रदर्शन किया जो शून्य-ज्ञान प्रमाणों के साथ बनाया गया था। डेमो ने दिखाया कि कैसे सत्यापित दावे शोध भंडार से कार्यशील उत्पादों में स्थानांतरित हो सकते हैं। शोधकर्ताओं ने बग को जल्दी पकड़ने के लिए लीन में सहमति क्लाइंट को औपचारिक रूप से सत्यापित करना भी शुरू कर दिया है।
फिर भी, दिशा एक परिचित पैटर्न को प्रतिध्वनित करती है: तेज़ कोड को पठनीय दावों से अलग करें, फिर साबित करें कि दोनों मेल खाते हैं।
नई भाषा का कोई प्रोटोटाइप अभी तक मौजूद नहीं है, और बुटेरिन ने सटीक सिंटैक्स को खुला छोड़ दिया है। डेवलपर्स एक साझा मानक पर एकत्र हो सकते हैं, या इसके बजाय कई असंगत बोलियों के लिए समझौता कर सकते हैं। यह विकल्प यह निर्धारित कर सकता है कि AI-प्रमाणित कोड उत्पादन प्रणालियों तक कितनी जल्दी पहुंचता है।
स्रोत: BeInCrypto
