← नवीनतम पेपर
🤖 AI

Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

यह शोध पत्र तर्क देता है कि सफल ऑटोफॉर्मलाइजेशन का मूल्यांकन केवल अपुष्ट अंतराल ("sorries") की अनुपस्थिति के बजाय परिभाषा की गुणवत्ता और API डिज़ाइन की विशेषज्ञ समीक्षा द्वारा किया जाना चाहिए, जो ग्रोटेंडिएक के वेनिशिंग थ्योरम (vanishing theorem) के एक केस स्टडी के माध्यम से यह प्रदर्शित करता है कि जबकि AI एजेंट स्थानीय यांत्रिक सुधारों को प्रभावी ढंग से लागू कर सकते हैं, वे उच्च-स्तरीय वैचारिक डिज़ाइन में संघर्ष करते हैं।

मूल लेखक: Vasily Ilin, Brian Nugent

प्रकाशित 2026-06-15
📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें
CC BY 4.0

मूल लेखक: Vasily Ilin, Brian Nugent

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक बहुत ही तेज़, बहुत उत्साही प्रशिक्षु (apprentice) को आपके लिए एक घर बनाने के लिए काम पर रख रहे हैं। आप उन्हें ब्लूप्रिंट (एक गणितीय प्रमेय/theorem) और एक पाठ्यपुस्तक का अध्याय देते हैं जो इसे बनाने का तरीका समझाता है।

वह प्रशिक्षु दिन-रात काम करता है। वह ईंटें बिछाता है, दीवारें बनाता है, और छत लगाता है। जब वह काम पूरा कर लेता है, तो घर खड़ा होता है। वह ढहता नहीं है। निरीक्षक (कंप्यूटर) कहता है, "बहुत अच्छा काम किया! घर संरचनात्मक रूप से मजबूत है।"

यह शोध पत्र इस बारे में है कि इसके बाद क्या होता है।

इस शोध पत्र के लेखकों ने पूछा: "सिर्फ इसलिए कि घर खड़ा है, क्या यह वास्तव में एक अच्छा घर है? क्या इसमें कोई और रह सकता है? क्या वे बाद में आसानी से दूसरी मंजिल जोड़ सकते हैं, या उन्हें पहले दीवारें तोड़नी पड़ेंगी?"

यहाँ उनके प्रयोग का विवरण दिया गया, सरल उपमाओं का उपयोग करते हुए:

प्रयोग: एक "गणित का घर" बनाना

टीम ने एक AI (एक लार्ज लैंग्वेज मॉडल) से एक जटिल गणितीय प्रमेय जिसे ग्रोटेंडिएक का वैनिशिंग थ्योरम (Grothendieck's Vanishing Theorem) कहा जाता है, उसे औपचारिक (formalize) करने के लिए कहा। इस प्रमेय को एक बहुत ही विशिष्ट, उच्च-स्तरीय स्थापत्य चुनौती (architectural challenge) के रूप में समझें।

उन्होंने AI को दिया:

  1. लक्ष्य (प्रमेय का कथन)।
  2. एक पाठ्यपुस्तक प्रमाण (निर्देश)।
  3. एक नियम: "आपको केवल उन्हीं मौजूदा, मानक उपकरणों का उपयोग करना चाहिए जो हमारे पास पहले से मौजूद टूलबॉक्स में हैं (गणित की लाइब्रेरी)।"

चरण 1: "पास" (अवस्था A)
AI ने कड़ी मेहनत की और ऐसा कोड तैयार किया जो बिना किसी त्रुटि के संकलित (compile) हो गया। गणित सॉफ्टवेयर की दुनिया में, त्रुटियों को "सॉरी" (sorry, I couldn't prove this yet - क्षमा करें, मैं इसे अभी सिद्ध नहीं कर सका) कहा जाता है। AI ने "सॉरी" की संख्या को शून्य तक पहुँचाने में सफलता प्राप्त की।

  • परिणाम: घर खड़ा है। कंप्यूटर खुश है।
  • समस्या: एक विशेषज्ञ मानव वास्तुकार (एक गणितज्ञ) ने घर को देखा और कहा, "यह एक आपदा है।"

विशेषज्ञ समीक्षा: क्यों "खड़ा हुआ घर" विफल रहा

मानव विशेषज्ञ ने पाया कि हालांकि घर गिरा नहीं, लेकिन इसे बहुत खराब तरीके से बनाया गया था। यहाँ वे विशिष्ट समस्याएँ दी गई हैं जो उन्हें मिलीं, जिन्हें रोजमर्रा के शब्दों में अनुवादित किया गया है:

1. "कस्टम टूल्स" की समस्या (परिभाषाएँ/Definitions)

  • AI ने क्या किया: AI हर एक छोटे से कार्य के लिए अपने स्वयं के कस्टम उपकरण बनाने लगा। यदि उसे एक दीवार मापने की आवश्यकता थी, तो उसने उस एक दीवार के लिए एक नया, अजीब टेप माप बनाया।
  • यह क्यों बुरा है: एक वास्तविक लाइब्रेरी में, आप मानक उपकरणों का उपयोग करना चाहते हैं जिन्हें हर कोई उपयोग करना जानता हो। यदि AI हर काम के लिए एक कस्टम टूल बनाता है, तो भविष्य के निर्माता उस घर का उपयोग नहीं कर पाएंगे क्योंकि वे AI के अजीब आविष्कारों को चलाना नहीं जानते।
  • फैसला: AI उपकरणों का उपयोग करने में तो बहुत अच्छा था, लेकिन उन्हें डिजाइन करने में बहुत बुरा था। उसने 62 कस्टम परिभाषाएँ बनाईं, और उनमें से 61 बेकार या भ्रमित करने वाली थीं।

2. "बिखरे हुए ब्लूप्रिंट" की समस्या (API डिज़ाइन)

  • AI ने क्या किया: AI ने एक साफ इंटरफेस (यूजर मैनुअल) नहीं बनाया। इसके बजाय, इसने बस दीवारों को खोलकर कच्ची ईंटों को दिखा दिया जब भी किसी को कुछ करने की आवश्यकता होती थी।
  • समाधान: विशेषज्ञ ने AI से एक "यूजर इंटरफेस" (एक API) बनाने के लिए कहा ताकि लोग गणित के जटिल आंतरिक हिस्सों को देखे बिना उसके साथ इंटरैक्ट कर सकें।
  • परिणाम: AI ने एक इंटरफेस तो बनाया, लेकिन वह अस्त-व्यस्त था। इसने वर्तमान प्रमाण के लिए केवल 24 विशिष्ट "नियम" जोड़े, न कि कुछ सुंदर और सामान्य नियम। यह हर एक लाइट बल्ब के लिए एक अद्वितीय, जटिल स्विच लगाने जैसा था, बजाय इसके कि एक मानक लाइट स्विच लगाया जाए।

3. "दूरदर्शिता की कमी" की समस्या (प्रमेय कथन/Theorem Statements)

  • AI ने क्या किया: AI ने ठीक वही सिद्ध किया जो उसे काम पूरा करने के लिए चाहिए था, और उससे अधिक कुछ नहीं। यह एक बढ़ई की तरह था जो बोर्ड को केवल वर्तमान गैप (gap) के फिट होने के लिए काटता है, बजाय इसके कि उसे इस तरह काटे कि उसका उपयोग बाद में अन्य गैप्स के लिए भी किया जा सके।
  • फैसला: AI तत्काल पहेली को हल करने में उत्कृष्ट है, लेकिन वह यह सोचने में बहुत बुरा है कि, "मैं इसे पांच साल बाद किसी और के लिए कैसे उपयोगी बना सकता हूँ?"

"पहले और बाद का" परीक्षण

टीम ने हार नहीं मानी। उन्होंने विशेषज्ञ की प्रतिक्रिया ली और AI को इसे ठीक करने के लिए कहा।

  • AI ने क्या अच्छी तरह से ठीक किया: यह स्थानीय मरम्मत (local repairs) में बहुत अच्छा था। यदि विशेषज्ञ ने कहा, "इस फ़ाइल का नाम बदलें," या "इस विशिष्ट संख्या को बदलें," तो AI ने इसे पूरी तरह से कर दिया। वह गंदगी को साफ कर सकता था।
  • AI क्या ठीक करने में विफल रहा: वह अभी भी यह नहीं समझ सका कि शुरुआत से एक अच्छा घर कैसे डिजाइन किया जाए। समीक्षा के बाद भी, परिभाषाएँ अभी भी बोझिल थीं, और "यूजर इंटरफेस" अभी भी अत्यधिक जटिल था।

बड़ा सबक

शोध पत्र एक सरल, शक्तिशाली विचार के साथ समाप्त होता है:

"अंतरालों को भरना" (कोड को संकलित करना) आसान हिस्सा है।

कठिन हिस्सा डिज़ाइन है।

  • AI एक शानदार राजमिस्त्री (bricklayer) की तरह है: यदि आप उसे बताते हैं कि ईंटें कहाँ रखनी हैं, तो वह ईंटें पूरी तरह से बिछा सकता है।
  • AI एक वास्तुकार (architect) नहीं है: वह यह तय नहीं कर सकता कि घर कैसा दिखना चाहिए, कमरों का प्रवाह कैसा होना चाहिए, या भविष्य के निवासियों को किन उपकरणों की आवश्यकता होगी।

निष्कर्ष:
हमें केवल यह नहीं पूछना चाहिए कि, "क्या AI ने गणित की समस्या को हल किया?" हमें यह पूछना चाहिए, "क्या AI ने कुछ ऐसा बनाया है जिसे अन्य मनुष्य वास्तव में उपयोग कर सकते हैं?"

वर्तमान में, AI पहेली को हल कर सकता है, लेकिन वह लाइब्रेरी नहीं बना सकता। वास्तव में उपयोगी परिणाम प्राप्त करने के लिए, मानव विशेषज्ञ को अभी भी डिज़ाइन और संगठन का भारी काम करने के लिए आगे आना होगा। "कठिन हिस्सा" प्रमेय को सिद्ध करना नहीं है; यह सुनिश्चित करना है कि प्रमाण भविष्य के लिए एक उपहार हो, न कि एक बोझ।

अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?

आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।

Digest आज़माएँ →

इसी तरह के और पेपर

इस विषय के सभी पेपर देखें 🤖 cs.AI →