AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
यह शोध पत्र AoA को प्रस्तुत करता है, जो एक नवीन इंटरैक्टिव थ्योरम प्रूविंग एजेंट है जो सीरियलाइज्ड सोर्स टेक्स्ट के बजाय एक पुनर्गठित भाषा (Minilang) के एब्स्ट्रैक्ट सिंटैक्स ट्री (AST) पर सीधे कार्य करता है, जिससे सत्यापन बेंचमार्क पर समाधान की गति और सफलता दर में सुधार करते हुए API लागत, टोकन उपयोग और टूल कॉल्स को काफी कम किया जाता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक प्रतिभाशाली लेकिन थोड़े अनाड़ी रोबोट को जटिल गणितीय पहेलियाँ हल करना सिखाने की कोशिश कर रहे हैं। यह रोबोट एक "लार्ज लैंग्वेज मॉडल" (LLM) है, जो मानव भाषा को समझने में तो अद्भुत है लेकिन कभी-कभी औपचारिक तर्क के कठोर और सटीक नियमों के साथ संघर्ष करता है। "इंटरएक्टिव थ्योरम प्रूविंग" का क्षेत्र मानव और कंप्यूटर के बीच शतरंज के एक उच्च-दांव वाले खेल की तरह है, जहाँ आपकी हर चाल गणितीय रूप से एकदम सही होनी चाहिए। यदि आप एक छोटी सी भी गलती करते हैं, तो पूरा खेल ढह जाता है। दशकों तक, मनुष्यों को यह काम मैन्युअल रूप से करना पड़ा है, जो धीमा, महंगा और थका देने वाला था। हाल ही में, लोगों ने इन प्रमाणों (proofs) में मदद करने के लिए एआई रोबोटों का उपयोग करना शुरू किया, लेकिन एक समस्या थी: इन रोबोटों को चलाना अविश्वसनीय रूप से महंगा था। वे बार-बार एक ही जानकारी मांगते रहते थे, जैसे कोई छात्र बार-बार शिक्षक से निर्देश दोहराने के लिए कहता रहता है क्योंकि उसने वर्कशीट खो दी है, जिससे हर सवाल के साथ पैसा और समय बर्बाद होता है।
बड़ा सवाल जो शोधकर्ता पूछ रहे हैं वह यह है: क्या हम इन प्रूफ-सॉल्विंग रोबोटों को बिना उन्हें शुरू से फिर से प्रशिक्षित (retrain) किए, अधिक स्मार्ट और सस्ता बना सकते हैं? इसका उत्तर इस बात में छिपा है कि हम उनसे कैसे बात करते हैं। रोबोट को कोड का एक लंबा, अव्यवस्थित पैराग्राफ पढ़ने और गलतियों का अनुमान लगाने के बजाय, एक स्पष्ट, संरचित मानचित्र (map) देने के बजाय, क्या होगा यदि हम उसे तर्क का एक स्पष्ट, संरचित ढांचा दें? यहाँ लेखक "एजेंट ओवर एएसटी" (Agent over AST - AoA) नामक एक नया तरीका पेश करते हैं। टेक्स्ट फ़ाइल को लाइन-दर-लाइन एडिट करने के लिए रोबोट को मजबूर करने के बजाय, वे रोबोट को तर्क के एक "पेड़" (tree) को एडिट करने देते हैं। इसे एक उपन्यास में वाक्य को ठीक करने के प्रयास और एक डिजिटल एडिटर का उपयोग करने के बीच के अंतर के रूप में सोचें, जो आपको कहानी की संरचना को एक वंशावली (family tree) के रूप में दिखाता है। इस पेड़ के साथ, आप देख सकते हैं कि किस शाखा को ठीक करने की आवश्यकता है, और कंप्यूटर आपको तुरंत परिणाम बताता है, बिना आपको यह पूछे कि "रुको, यहाँ संदर्भ (context) क्या है?"
शोधकर्ताओं ने पाया कि टेक्स्ट-आधारित दृष्टिकोण से पेड़-आधारित दृष्टिकोण पर स्विच करके, वे इन प्रूफ एजेंटों को चलाने की लागत में भारी कटौती कर सकते हैं। जब उन्होंने अपने नए सिस्टम, AoA का परीक्षण एक अग्रणी मौजूदा एजेंट (अमेज़न का इसाबेल एजेंट) के विरुद्ध किया, तो परिणाम चौंकाने वाले थे। AoA ने 2.9 से 6.9 गुना कम "टोकन" (डेटा की इकाइयाँ जिन्हें एआई प्रोसेस करता है) का उपयोग किया और 3.9 से 8.9 गुना कम टूल कॉल किए। पैसों के मामले में, इसका मतलब था कि नया एजेंट प्रति समस्या चलाने के लिए 2.3 से 4.7 गुना कम महंगा था। इससे भी अधिक प्रभावशाली बात यह है कि इसने कार्यों को 1.4 से 2.0 गुना तेज़ी से पूरा किया।
इस कार्य का एक बहुत ही चतुर हिस्सा यह है कि यह एक बिल्कुल नई प्रमाण भाषा "मिनिलैंग" (Minilang) को कैसे संभालता है। इस भाषा को विशेष रूप से एआई के समझने के लिए आसान बनाने के उद्देश्य से डिज़ाइन किया गया था, लेकिन क्योंकि यह इतनी नई है, एआई मॉडल्स को इस पर प्रशिक्षित नहीं किया गया था। आमतौर पर, यह एक बड़ी बाधा होती; आप सोचेंगे कि एआई विफल हो जाएगा क्योंकि वह इसके नियमों को नहीं जानता। हालाँकि, लेखकों ने दिखाया कि मिनिलैंग के नियमों को एक संरचित प्रारूप (JSON) में अनुवाद करके, जिसे एआई पहले से ही अच्छी तरह समझता है, वे रोबोट को इस नई भाषा में प्रमाण हल करने में सक्षम बना सकते हैं, बिना इसके कि उसने पहले कभी इसका एक भी उदाहरण देखा हो। उन्होंने सिद्ध किया कि आपको एआई को नया खेल सिखाने के लिए नई किताबों का विशाल पुस्तकालय खिलाने की आवश्यकता नहीं है; आपको बस नियमों को ऐसे समझाना है जिसे वह स्वाभाविक रूप से समझ सके।
अपने प्रयोगों में, AoA ने न केवल पैसे बचाए; बल्कि यह समस्याओं को हल करने में वास्तव में बेहतर भी हुआ। कठिन गणितीय चुनौतियों के एक सेट पर, इसने 99.6% उन्हें हल किया, जो अब तक के सर्वश्रेष्ठ परिणामों के बराबर है। कंप्यूटर-वेरिफिकेशन की पेचीदा समस्याओं के एक सेट पर, इसने 89.2% को हल किया, जो एक नया रिकॉर्ड बनाता है। लेखक सुझाव देते हैं कि यह दृष्टिकोण—अव्यवस्थित टेक्स्ट एडिटिंग से हटकर संरचित, पेड़-आधारित इंटरैक्शन की ओर बढ़ना—एआई प्रूफ असिस्टेंट को वास्तविक दुनिया के उपयोग के लिए व्यावहारिक बनाने का एक शक्तिशाली तरीका है। वे स्वीकार करते हैं कि जबकि यह मिनिलैंग के लिए बहुत अच्छा काम करता है, यह अभी तक हर संभावित भाषा के लिए सिद्ध नहीं हुआ है, लेकिन परिणाम इतने मजबूत हैं कि वे संकेत देते हैं कि यह स्वचालित गणित और सॉफ्टवेयर सत्यापन के भविष्य के लिए एक आशाजनक दिशा है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।