MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries
यह शोध पत्र MathlibPR को प्रस्तुत करता है, जो वास्तविक Lean/Mathlib4 पुल रिक्वेस्ट इतिहास से प्राप्त एक बेंचमार्क है, जिसका उद्देश्य LLMs और एजेंटों की मर्ज-तैयार योगदानों से गैर-मर्ज किए गए योगदानों के बीच अंतर करने की क्षमता का मूल्यांकन करना है, जो उनकी वर्तमान संघर्षों को प्रकट करता है और रिव्यूअर असिस्टेंट और रिवॉर्ड मॉडल विकसित करने के लिए इस बेंचमार्क की क्षमता को उजागर करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि गणित की एक विशाल, जीवित लाइब्रेरी है जिसे Mathlib कहा जाता है। यह केवल एक किताब नहीं है; यह एक विशाल, साझा निर्माण स्थल है जहाँ गणितज्ञ और कंप्यूटर वैज्ञानिक गणित का एक पूर्ण, त्रुटिहीन आधार बनाने के लिए काम कर रहे हैं। इस लाइब्रेरी को सुरक्षित और उपयोगी बनाए रखने के लिए, कोड का हर नया हिस्सा (जिसे "पुल रिक्वेस्ट" या PR कहा जाता है) दो परीक्षणों से गुजरना चाहिए:
- "क्या यह काम करता है?" वाला परीक्षण: क्या कोड बिना क्रैश हुए वास्तव में चलता है? (यह कंप्यूटर द्वारा जांचा जाता है)।
- "क्या यह एक अच्छा नागरिक है?" वाला परीक्षण: क्या कोड लाइब्रेरी के बाकी हिस्सों के साथ मेल खाता है? क्या इसे सही शैली (style) में लिखा गया है? क्या यह दूसरों के उपयोग के लिए पर्याप्त स्पष्ट है? (यह मनुष्यों द्वारा जांचा जाता है)।
लंबे समय से, आर्टिफिशियल इंटेलिजेंस (AI) पहले परीक्षण में बहुत अच्छा रहा है। यह ऐसा कोड लिख सकता है जो पूरी तरह से चलता है। लेकिन दूसरा परीक्षण—मानवीय समीक्षा (human review)—एक बाधा बन गया है। सबमिशन बहुत अधिक हैं, और उन कोडों की जांच करने के लिए पर्याप्त मानव समीक्षक नहीं हैं जो यह देख सकें कि क्या वह कोड लाइब्रेरी में शामिल करने के लिए वास्तव में तैयार है।
यह शोध पत्र एक सरल प्रश्न पूछता है: क्या AI समीक्षक बनना सीख सकता है? क्या एक AI कोड के उस हिस्से को देख सकता है जो पहले से ही काम कर रहा है और यह तय कर सकता है कि क्या वह "मर्ज-रेडी" (सम्मिलित करने के लिए तैयार) है या उसे और काम की आवश्यकता है?
यह जानने के लिए, लेखकों ने एक नया परीक्षण बनाया जिसे MATHLIBPR कहा जाता है।
प्रयोग: कोड के लिए एक "ब्लाइंड टेस्ट"
सोचिए कि MATHLIBPR एक नई रेसिपी के लिए "ब्लाइंड टेस्ट" की तरह है।
- सेटअप: शोधकर्ताओं ने Mathlib लाइब्रेरी के वास्तविक इतिहास का उपयोग किया। उन्होंने हजारों कोड सबमिशन एकत्र किए जो पहले ही "क्या यह काम करता है?" वाले परीक्षण को पास कर चुके थे (वे सफलतापूर्वक कंपाइल हुए थे)।
- चुनौती: उन्होंने ये कोड स्निपेट्स विभिन्न AI मॉडलों (जैसे DeepSeek, Qwen और अन्य) को दिए और पूछा: "क्या यह लाइब्रेरी में प्रकाशित करने के लिए तैयार है, या इसे सुधार के लिए वापस भेजा जाना चाहिए?"
- पकड़ (The Catch): AI को अंतिम परिणाम का पता नहीं था। वह मानव समीक्षकों से यह नहीं पूछ सकता था, "क्या आपको यह पसंद आया?" उसे केवल कोड के आधार पर निर्णय लेना था, ठीक वैसे ही जैसे एक मानव समीक्षक करेगा।
उन्होंने AI का तीन चरणों में परीक्षण किया, जिसमें उसे अधिक से अधिक सुराग दिए गए:
- चरण 1: केवल कोड परिवर्तन और कुछ स्टाइल गाइड।
- चरण 2: कोड और स्वचालित "लिंटिंग" त्रुटियों (जैसे कोड के लिए स्पेल-चेकर) की एक सूची।
- चरण 3: कोड, त्रुटियाँ, और लेखक का विवरण कि वे क्या करने की कोशिश कर रहे थे।
परिणाम: AI अटक गया
परिणाम आश्चर्यजनक और AI समुदाय के लिए थोड़े निराशाजनक थे।
- AI अंतर नहीं बता सका। सभी अतिरिक्त सुरागों के बावजूद, AI मॉडल उस कोड के बीच अंतर करने में संघर्ष करते रहे जो अंततः स्वीकार किया गया था और जिसे खारिज कर दिया गया था या सुधार के लिए वापस भेजा गया था।
- "हाँ" का पूर्वाग्रह (The "Yes" Bias): अधिकांश AI बहुत आशावादी थे। वे यह कहने की ओर झुके कि, "हाँ, यह बहुत बढ़िया है!" भले ही कोड अव्यवस्थित था या लाइब्रेरी की शैली में फिट नहीं बैठता था। उन्होंने शायद ही कभी कहा, "नहीं, इसमें काम करने की आवश्यकता है।"
- "मुझे नहीं पता" का विकल्प: कुछ मॉडल, कठिन निर्णय का सामना करते समय, बस कह देते थे, "मुझे यकीन नहीं है।" हालांकि यह ईमानदार था, लेकिन यह लाइब्रेरी को आगे बढ़ने में मदद नहीं करता है।
- अधिक संदर्भ (Context) से ज्यादा मदद नहीं मिली। AI को अधिक जानकारी देने (जैसे लेखक का इरादा या स्वचालित त्रुटि रिपोर्ट) से सही निर्णय लेने की उसकी क्षमता में कोई खास सुधार नहीं हुआ।
एक दिलचस्प खोज यह थी कि भले ही AI ने एक ही प्रोजेक्ट को दो अलग-अलग समय पर देखा हो (एक बार जब वह अव्यवस्थित था, और एक बार जब वह ठीक और स्वीकृत हो गया था), वह अक्सर यह नहीं पहचान सका कि कौन सा संस्करण "बेहतर" था। यह एक छात्र की तरह था जो उस विषय पर परीक्षा दे रहा है जिसका उसने अध्ययन किया है, लेकिन वह एक कच्चे ड्राफ्ट और अंतिम निबंध के बीच के अंतर को पहचानने में विफल रहा।
यह क्यों महत्वपूर्ण है
शोध पत्र निष्कर्ष निकालता है कि जबकि AI कोड लिखने में उत्कृष्ट है जो काम करता है, यह वर्तमान में कोड की समीक्षा करने में बहुत खराब है कि क्या वह एक उच्च-गुणवत्ता वाली लाइब्रेरी का हिस्सा बनने के योग्य है।
लेखक यह नहीं कह रहे हैं कि AI को मानव समीक्षकों की जगह लेनी चाहिए। इसके बजाय, वे इस बेंचमार्क (MATHLIBPR) को एक शुरुआती बिंदु के रूप में देखते हैं। यह भविष्य के AI सिस्टम को बेहतर "सहायक समीक्षक" बनने के लिए प्रशिक्षित करने के लिए एक उपकरण है। लक्ष्य एक ऐसा AI बनाना है जो स्पष्ट शैली संबंधी समस्याओं या लुप्त दस्तावेज़ों को पकड़कर मनुष्यों की मदद कर सके, जिससे एक पहली रक्षा पंक्ति (first line of defense) बन सके ताकि मानव समीक्षक काम के सबसे कठिन और रचनात्मक हिस्सों पर ध्यान केंद्रित कर सकें।
संक्षेप में: AI एक बेहतरीन निर्माता है, लेकिन फिलहाल, वह एक बहुत बुरा निरीक्षक (inspector) है। यह शोध पत्र यह मापने के लिए पहला वास्तविक परीक्षण प्रदान करता है कि वह कितना खराब है, ताकि हम उसे बेहतर करना सिखा सकें।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।