Theory-Scale Auto-Formalization of Logics for Computer Science
यह शोध पत्र LCS-Bench प्रस्तुत करता है, जो एक नवीन अर्ध-स्वचालित एजेंटिक पाइपलाइन के माध्यम से 327 पाठ्यपुस्तक मदों से प्राप्त 3,000 से अधिक लीन (Lean) घोषणाओं वाला एक व्यापक सिद्धांत-स्तर का बेंचमार्क है, जो यह प्रकट करता है कि वर्तमान अत्याधुनिक मॉडल सुसंगत, बड़े पैमाने पर ऑटो-फॉर्मलाइजेशन (auto-formalization) में संघर्ष करते हैं, और केवल 20.1% सफलता दर प्राप्त करते हैं।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आपके पास एक जटिल मशीन बनाने के लिए एक विशाल, विस्तृत निर्देश पुस्तिका (instruction manual) है। यह मैनुअल मानवीय भाषा में लिखा गया है, जिसमें चित्र, क्रॉस-रेफरेंस और सूक्ष्म धारणाएं शामिल हैं जिन्हें एक मानव विशेषज्ञ सहजता से समझ लेता है। अब, कल्पना कीजिए कि आप एक रोबोट को उस पूरे मैनुअल को एक सख्त, कंप्यूटर-पठनीय प्रोग्रामिंग भाषा में अनुवाद करने के लिए कहना चाहते हैं, जहाँ मशीन चलाने से पहले हर एक कदम को गणितीय रूप से सिद्ध किया जाना अनिवार्य है।
यह वास्तव में इस शोध पत्र, "Theory-Scale Auto-Formalization of Logics for Computer Science," के बारे में है। शोधकर्ता AI को तर्क (logic) की एक पूरी पाठ्यपुस्तक को Lean नामक एक औपचारिक प्रोग्रामिंग भाषा में अनुवाद करना सिखाने की कोशिश कर रहे हैं, न कि केवल वाक्य-दर-वाक्य, बल्कि एक पूर्ण, परस्पर जुड़े हुए तंत्र के रूप में।
यहाँ उनके कार्य का सरल उपमाओं (analogies) का उपयोग करके विवरण दिया गया है:
1. समस्या: "द्वीप" बनाम "महाद्वीप"
AI को यह कौशल सिखाने के पिछले प्रयास किसी को अलग-थलग द्वीपों का अनुवाद करने के लिए कहने जैसे थे। वे एक गणितीय प्रमेय (theorem) लेते थे, उसका अनुवाद करते थे, और जाँचते थे कि क्या वह काम करता है। लेकिन वास्तविक गणित एक महाद्वीप है। परिभाषाएँ लेम्मा (lemmas) पर निर्भर करती हैं, जो अन्य परिभाषाओं पर निर्भर करते हैं। यदि आप एक छोटा सा हिस्सा भी गलत करते हैं, तो पूरी संरचना ढह जाती है।
लेखकों का तर्क है कि मौजूदा AI बेंचमार्क बहुत छोटे हैं। वे एक पायलट को सिम्युलेटर में केवल एक मोड़ पर मुड़ने का परीक्षण करने के बजाय, उसे न्यूयॉर्क से लंदन तक उड़ान भरने और तूफानों तथा ईंधन की सीमाओं के बीच रास्ता खोजने के लिए कहने जैसा है। यह नया प्रोजेक्ट, LCS-Bench, "न्यूयॉर्क से लंदन की उड़ान" है। यह एक पूरी पाठ्यपुस्तक (Logics for Computer Science) को लेता है और पूरी चीज़ को औपचारिक रूप देने की कोशिश करता है—327 आइटम, 4,000 से अधिक कोड घोषणाएं, और 85,000 पंक्तियों का कोड।
2. समाधान: "वास्तुकार और निर्माता" पाइपलाइन
इस विशाल अनुवाद को बनाने के लिए, टीम ने केवल AI को "इसे करने" के लिए नहीं कहा। उन्होंने एक अर्ध-स्वचालित पाइपलाइन (semi-automated pipeline) बनाई जो एक निर्माण दल की तरह कार्य करती है:
- वास्तुकार (योजना बनाना - The Architect): सबसे पहले, एक AI पाठ्यपुस्तक का विश्लेषण करके एक "अवधारणा मानचित्र" (concept map) बनाता है। यह पता लगाता है कि प्रत्येक विचार अगले विचार से कैसे जुड़ता है (जैसे, "आप 'प्रूफ ट्रीज़' को तब तक नहीं समझ सकते जब तक आप 'फॉर्मुलों' को नहीं समझते")।
- निर्माता (कार्यान्वयन - The Builder): दूसरा AI उस मानचित्र के आधार पर वास्तविक कोड लिखने का प्रयास करता है।
- सुरक्षा निरीक्षक (मानवीय विशेषज्ञ - The Safety Inspector): यह महत्वपूर्ण है। मनुष्य "छिपे हुए जाल" को ठीक करने के लिए हस्तक्षेप करते हैं। उदाहरण के लिए, एक पाठ्यपुस्तक कह सकती है, "मान लें कि X शेष अध्याय के लिए सत्य है," बिना इसे स्पष्ट रूप से लिखे। एक AI इसे मिस कर सकता है और एक अस्थिर नींव बना सकता है। मनुष्य इन लुप्त धारणाओं को पकड़ लेते हैं।
- प्रति-उदाहरण शिकारी (The Counter-Example Hunter): यदि AI फंस जाता है, तो सिस्टम उस चीज़ के विपरीत को सिद्ध करने की कोशिश करता जिसे वह सिद्ध करने का प्रयास कर रहा है। यदि वह सफल होता है, तो उसे पता चल जाता है कि AI की परिभाषा गलत थी (जैसे एक भारी ट्रक चलाकर पुल में दरार ढूंढना)।
3. बेंचमार्क: "बाधा दौड़" (The Obstacle Course)
एक बार जब उन्होंने यह विशाल लाइब्रेरी बना ली, तो उन्होंने इसे अन्य AI के लिए एक परीक्षण (बेंचमार्क) में बदल दिया। उन्होंने पाँच अलग-अलग "ट्रैक" या बाधा दौड़ बनाई:
- आइटम-स्तर (Item-Level): एक विशिष्ट परिभाषा या प्रमेय का अनुवाद करें।
- उप-अनुभाग-स्तर (Subsection-Level): एक बार में पुस्तक के पूरे अनुभाग का अनुवाद करें।
- "डिस्ट्रैक्टर" टेस्ट (The "Distractor" Test): AI को सही उत्तर दें लेकिन उसे अप्रासंगिक, भ्रमित करने वाले कोड के ढेर के भीतर छिपा दें ताकि यह देखा जा सके कि क्या वह शोर में संकेत (signal) को खोज सकता है।
- प्रमेय सिद्ध करना (Theorem Proving): AI को कोड दें लेकिन "प्रूफ" वाले हिस्से को खाली छोड़ दें (जिसे
sorryनामक प्लेसहोल्डर से चिह्नित किया गया है) और देखें कि क्या वह तर्क को भर सकता है।
उत्तरों को ग्रेड करने के लिए, उन्होंने एक DefEq Checker का आविष्कार किया। इसे एक अत्यंत सटीक रूलर (रूलर) के रूप में समझें। यह केवल यह जाँच नहीं करता कि कोड संकलित (compile) होता है या नहीं; यह जाँचता है कि AI का अनुवाद मूल पाठ्यपुस्तक के बिल्कुल समान अर्थ रखता है या नहीं, भले ही AI ने अलग शब्दों या वेरिएबल नामों का उपयोग किया हो।
4. परिणाम: "वास्तविकता की जाँच" (The Reality Check)
उन्होंने उपलब्ध 14 सबसे स्मार्ट AI मॉडलों का परीक्षण इस कोर्स पर किया (OpenAI, Anthropic और अन्य के शीर्ष-स्तरीय मॉडलों सहित)। परिणाम निराशाजनक थे:
- स्कोर: यहाँ तक कि सर्वश्रेष्ठ AI भी केवल 20% आइटम सही कर पाया।
- कठिनाई: मॉडल उन चीजों के साथ सबसे अधिक संघर्ष करते हैं जिनमें गहरे, अमूर्त तर्क (abstract reasoning) या "बाइंडर सब्स्टीट्यूशन" (binder substitution - एक तकनीकी तरीका जिसका अर्थ है: "यह ट्रैक रखना कि कौन सा वेरिएबल किस नियम का हिस्सा है") की आवश्यकता होती है।
- "ओवरथिंकिंग" का जाल: दिलचस्प बात यह है कि जब मॉडल विफल होते थे, तो वे अक्सर सफल होने की तुलना में अधिक समय और कंप्यूटिंग शक्ति खर्च करते थे। वे समाधान खोजने के बजाय, चक्कर काटते हुए "ओवरथिंक" करते थे।
- डिस्ट्रैक्टर प्रभाव: जब AI को अतिरिक्त, अप्रासंगिक जानकारी (distractors) दी गई, तो इसके प्रदर्शन में काफी गिरावट आई। यह दर्शाता है कि वर्तमान AI बड़े संदर्भ (context) में शोर को फ़िल्टर करने में संघर्ष करते हैं, जो थ्योरी-स्केल कार्य के लिए आवश्यक है।
5. निष्कर्ष
शोध पत्र यह निष्कर्ष निकालता है कि हालांकि AI गणित में बेहतर हो रहा है, थ्योरी-स्केल ऑटो-फॉर्मलाइजेशन (संपूर्ण, सुसंगत ज्ञान निकायों का अनुवाद करना) अभी भी एक बड़ी चुनौती है। वर्तमान मॉडल उन छात्रों की तरह हैं जो एक एकल बीजगणित (algebra) की समस्या को हल कर सकते हैं लेकिन जब उन्हें एक पूरा पाठ्यपुस्तक अध्याय लिखने के लिए कहा जाता है जहाँ प्रत्येक वाक्य पिछले वाक्य पर निर्भर करता है, तो वे खो जाते हैं।
लेखकों को उम्मीद है कि यह बेंचमार्क (LCS-Bench) भविष्य के AI मॉडलों को यह सीखने में मदद करने के लिए एक "प्रशिक्षण मैदान" के रूप में कार्य करेगा कि कंप्यूटर विज्ञान तर्क को वास्तव में समझने और औपचारिक रूप देने के लिए आवश्यक जटिलता, निरंतरता और निष्ठा (faithfulness) को कैसे संभाला जाए।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।