Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
यह शोध पत्र Visored को प्रस्तुत करता है, जो एक डिपेंडेंट-टाइप-आधारित प्रूवर है जो प्राकृतिक भाषा जैसे इंटरफ़ेस और नियम-संचालित स्वचालन का उपयोग करके प्रमाणों को जांचे गए लीन (Lean) फाइलों में परिवर्तित करके एलएलएम (LLM)-जनित गणित और औपचारिक सत्यापन के बीच सेतु बनाता है, जो बिना किसी विशेष प्रशिक्षण के miniF2F बेंचमार्क पर प्रभावी प्रदर्शन प्रदर्शित करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक प्रतिभाशाली लेकिन थोड़े भ्रमित (hallucination-prone) होने वाले छात्र (एक AI) को गणित का प्रमाण (math proof) लिखना सिखाने की कोशिश कर रहे हैं। यह छात्र साधारण अंग्रेजी में प्रमाण की "कहानी" लिखने में बहुत अच्छा है, लेकिन वह अक्सर उन छोटे, उबाऊ विवरणों को छोड़ देता है जिन्हें एक सख्त गणित शिक्षक यह विश्वास करने के लिए देखना चाहता है कि वह सच है।
वर्तमान में, यदि आप इस छात्र को एक सख्त, कंप्यूटर-पठनीय भाषा (जैसे Lean) में प्रमाण लिखने के लिए कहते हैं, तो वह अक्सर अटक जाता है। उसे नहीं पता होता कि कौन सा विशिष्ट "लाइब्रेरी नियम" चुनना है, या वह "आप शून्य से विभाजित नहीं कर सकते" जैसे सूक्ष्म विवरणों में गलती कर देता है।
Visored एक नया टूल है जिसे इसे ठीक करने के लिए डिज़ाइन किया गया है। यह छात्र की प्राकृतिक भाषा और सख्त कंप्यूटर भाषा के बीच एक अनुवादक और सुरक्षा जाल (safety net) के रूप में कार्य करता है।
यह कैसे काम करता है, यहाँ कुछ उपमाओं (analogies) का उपयोग करके समझाया गया है:
1. "नियंत्रित प्राकृतिक भाषा" (The Script)
AI को तुरंत Lean जैसी कठोर, कोड जैसी भाषा लिखने के लिए मजबूर करने के बजाय, Visored AI को एक नियंत्रित अंग्रेजी संस्करण में लिखने की अनुमति देता है।
- उपमा: इसे एक "मैड लिब्स" (Mad Libs) शैली के स्क्रिप्ट की तरह समझें। AI को कुछ भी लिखने की अनुमति नहीं है; इसे विशिष्ट वाक्य टेम्पलेट्स का उपयोग करना चाहिए जैसे "मान लीजिए x है...", "मान लें कि...", या "तब..."।
- यह क्यों मदद करता है: यह AI को उसके सहज क्षेत्र (अंग्रेजी लिखने) में रखता है, जबकि यह सुनिश्चित करता है कि इसकी संरचना इतनी कठोर हो कि कंप्यूटर इसे समझ सके। यह एक खाली पन्ने के बजाय छात्र को एक 'फिल-इन-द-ब्लैंक' वर्कशीट देने जैसा है।
2. "मध्यस्थ" (The IR)
Visored केवल यह अनुमान नहीं लगाता कि AI का क्या मतलब था। यह उस अंग्रेजी स्क्रिप्ट को एक मध्यवर्ती-परत प्रतिनिधित्व (जिसे IR कहा जाता है) में बदल देता है।
- उपमा: कल्पना करें कि AI एक कच्चा मसौदा (rough draft) लिखता है। Visored उस मसौदे को लेता है और उसमें वे सभी अदृश्य "फुटनोट्स" भर देता है जिन्हें AI ने छोड़ दिया था। क्या AI ने माना कि धनात्मक है? Visored इसे लिख देता है। क्या AI ने किसी वेरिएबल से भाग दिया? Visored जाँचता है कि क्या वह वेरिएबल शून्य से अलग है।
- जादू: यदि AI कोई गलती करता है, तो Visored केवल "गलत" नहीं कहता। यह ठीक उस वाक्य की ओर इशारा करता है जहाँ तर्क टूट गया, जैसे कोई शिक्षक लाल स्याही से किसी विशिष्ट त्रुटि को घेरता है। यह AI को यह स्पष्ट संकेत देता है कि उसे अपने अगले प्रयास को कैसे ठीक करना है।
3. "नियम-आधारित सॉल्वर" (The Auto-Grader)
एक बार जब Visored के पास अपने मध्य-परत प्रारूप में प्रमाण आ जाता है, तो यह "उबाऊ" चरणों की जाँच करने के लिए एक नियम-आधारित इंजन का उपयोग करता है।
- उपमा: एक गणित की पाठ्यपुस्तक के बारे में सोचें। जब एक पाठ्यपुस्तक कहती है कि "इससे यह निष्कर्ष निकलता है...", तो वह अक्सर स्पष्ट होने के कारण बीजगणित (algebra) को छोड़ देती है। Visored का सॉल्वर उन छोड़े गए चरणों को भरने वाले एक अथक रोबोट की तरह है। यह अंकगणित, बीजगणित और छोटे चरणों के तर्क की स्वचालित रूप से जाँच करता है।
- परिणाम: यदि AI मुख्य विचार प्रदान करता है, तो Visored छोटे चरणों को सिद्ध करने के थकाऊ "कठिन परिश्रम" को संभालता है।
4. "बैक-ट्रांसलेशन" (The Lean Output)
यदि Visored अपने प्रमाण से संतुष्ट है, तो यह अंतिम सत्यापन के लिए इसे वापस Lean कोड (सख्त भाषा) में अनुवादित कर सकता है।
- सावधानी: पेपर स्वीकार करता है कि वर्तमान अनुवाद बहुत "शब्दबहुल" (wordy) है। यह एक 1-पेज के सारांश को 200-पेज के कानूनी अनुबंध में विस्तारित करने जैसा है ताकि यह सुनिश्चित किया जा सके कि हर एक शब्द कानूनी रूप से सटीक है। यह काम करता है, लेकिन यह बहुत विशाल है।
उन्होंने वास्तव में क्या हासिल किया?
शोधकर्ताओं ने परीक्षण के लिए 244 गणितीय समस्याओं (ज्यादातर मिडिल-स्कूल प्रतियोगिताओं से) का एक सेट लिया।
- परिणाम: Visored का उपयोग करने वाला एक AI एजेंट इन समस्याओं में से 91% को सफलतापूर्वक हल कर सका।
- सावधानी: AI ने इन्हें अकेले हल नहीं किया। इसने एक लूप में काम किया: AI ने एक मसौदा लिखा, Visored ने इसकी जाँच की और "त्रुटि यहाँ है" कहा, AI ने इसे ठीक किया, और उन्होंने फिर से प्रयास किया।
- सीमा: यह बहुत कठिन समस्याओं (जैसे इंटरनेशनल मैथ ओलंपियाड के प्रश्न) के साथ संघर्ष करता है क्योंकि Visored के "नियम-पुस्तिका" में अभी तक उन उन्नत गणितीय युक्तियों की कमी थी जिनकी आवश्यकता उन्हें होता है।
मुख्य निष्कर्ष (The Bottom Line)
Visored कोई जादुई छड़ी नहीं है जो कठिन गणित समस्याओं को तुरंत हल कर देती है। इसके बजाय, यह एक सहयोगात्मक कार्यक्षेत्र (collaborative workspace) है। यह AI को उस भाषा में प्रमाण लिखने की अनुमति देता है जिसे वह समझता है (अंग्रेजी), जबकि एक कंप्यूटर सिस्टम सख्त तर्क और त्रुटि-जाँच को संभालता है।
पेपर का दावा है कि इस "मध्यस्थ" दृष्टिकोण का उपयोग करके, हम AI से ऐसे गणितीय प्रमाण प्राप्त कर सकते हैं जो वास्तव में विश्वसनीय हैं, बिना AI को औपचारिक प्रमाण प्रणालियों की कठिन, कठोर कोडिंग भाषा को शुरू से सीखने के लिए मजबूर किए। यह AI के "भ्रमों" (hallucinations) को एक संरचित, जांच योग्य प्रक्रिया में बदल देता है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।