TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
यह शोधपत्र TaoBench प्रस्तुत करता है, जो टेरेन्स ताओ की *Analysis I* से व्युत्पन्न एक नवीन बेंचमार्क है जो विशेष गणितीय संरचनाओं पर स्वचालित प्रमेय प्रुवरों (automated theorem provers) का मूल्यांकन करता है, जो मानक MathLib समस्याओं की तुलना में प्रदर्शन में 26% की महत्वपूर्ण गिरावट को प्रकट करता है और यह रेखांकित करता है कि वर्तमान प्रणालियों की प्राथमिक सीमा कार्यों की अंतर्निहित कठिनाई के बजाय विभिन्न परिभाषात्मक ढांचों (definitional frameworks) में सामान्यीकरण करने की उनकी अक्षमता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
यहाँ TAOBENCH पेपर का सरल भाषा और रचनात्मक उपमाओं (analogies) का उपयोग करके दिया गया विवरण है।
मुख्य विचार: "विशेषज्ञ शेफ" की समस्या
कल्पना कीजिए कि आपने एक विश्व स्तरीय शेफ (एक AI) को अद्भुत भोजन पकाना सिखाया है, लेकिन आपने उसे केवल एक विशिष्ट कुकबुक (जिसे MathLib कहा जाता है) का उपयोग करके ही सिखाया है। इस कुकबुक के बहुत विशिष्ट नियम हैं: यह टमाटर को "लाल फल" कहता है, एक विशेष प्रकार के चाकू का उपयोग करता है, और व्यंजनों को रंग के आधार पर व्यवस्थित करता है।
क्योंकि शेफ ने इस किताब के साथ बहुत अभ्यास किया है, इसलिए वे कुछ ही सेकंड में एक बेहतरीन टमाटर सलाद बना सकते हैं। वे इस किताब का पालन करने में जीनियस हैं।
समस्या:
अब, कल्पना कीजिए कि आप इस शेफ से बिल्कुल वही सलाद बनाने के लिए कहते हैं, लेकिन इस बार आप उन्हें एक अलग कुकबुक देते हैं (जो प्रसिद्ध गणितज्ञ टेरेंस ताओ द्वारा लिखी गई है)। इस नई किताब में:
- टमाटर को "लाल बेरी" कहा जाता है।
- चाकू को अलग तरीके से पकड़ा जाता है।
- व्यंजनों को दिन के समय के आधार पर व्यवस्थित किया गया है।
भले ही सामग्री और अंतिम व्यंजन बिल्कुल वही हैं, शेफ ठिठक जाते हैं। वे नए नामों और नई व्यवस्था से भ्रमित हो जाते हैं। वे यह नहीं समझ पाते कि शुरुआत कैसे करें क्योंकि वे पुराने नियमों के इतने आदी हो चुके हैं।
शोधकर्ताओं की खोज:
शोधकर्ताओं ने इस बात को साबित करने के लिए TAOBENCH नामक एक परीक्षण बनाया। उन्होंने टेरेंस ताओ की पाठ्यपुस्तक से 150 गणितीय समस्याएं लीं, जो "शून्य से" (from-scratch) परिभाषाओं का उपयोग करती हैं (जैसे संख्याओं और सेटों जैसी अवधारणाओं को बुनियादी स्तर से बनाना)।
इसके बाद, उन्होंने उन्हीं समस्याओं का एक "अनुवाद" मानक MathLib भाषा में किया, जिससे AI शेफ परिचित हैं।
परिणाम:
- मानक MathLib समस्याओं पर: AI शेफ ने उनमें से लगभग 70% को हल किया। वे अपने सहज क्षेत्र (element) में थे।
- ताओ (नई भाषा) की समस्याओं पर: वही AI शेफ केवल लगभग 44% को हल कर पाए।
सीख:
AI गणित में बुरा नहीं है। यह बस अनुकूलन (adapting) करने में बुरा है। इसने मानक लाइब्रेरी की "बोली" को इतनी अच्छी तरह से याद कर लिया है कि यह एक नई, लेकिन गणितीय रूप से समान रूप से ढाँचे (framework) में बात नहीं कर सकता।
उन्होंने यह कैसे किया: "एजेंटिक पाइपलाइन" (Agentic Pipeline)
इस परीक्षण को बनाना कठिन था। आप किसी गणित की समस्या को सीधे कंप्यूटर में कॉपी-पेस्ट नहीं कर सकते; कंप्यूटर को समझने के लिए एक पूरे "रसोईघर" (परिभाषाएं, उपकरण और नियम) की आवश्यकता होती है।
शोधकर्ताओं ने भारी काम को संभालने के लिए एक रोबोट टीम (एजेंटिक पाइपलाइन) बनाई:
- लाइब्रेरियन (The Librarian): इसने विशाल पाठ्यपुस्तक में जाकर ठीक वही परिभाषाएँ ढूँढीं जिनकी एक विशिष्ट समस्या को आवश्यकता थी, और बाकी सब को अनदेखा कर दिया।
- अनुवादक (The Translator): इसने "ताओ" संस्करण की समस्या को "MathLib" संस्करण में फिर से लिखने का प्रयास किया।
- संपादक (The Editor): इसने जाँच की कि क्या अनुवाद गणितीय रूप से वास्तव में सही था। यदि अनुवाद के दौरान रोबोट ने समस्या का अर्थ बदल दिया, तो संपादक ने उसे खारिज कर दिया और दोबारा प्रयास किया।
इससे यह सुनिश्चित हुआ कि जब AI ताओ संस्करण पर विफल हुआ, तो वह इसलिए नहीं था क्योंकि समस्या कठिन थी, बल्कि इसलिए क्योंकि भाषा अलग थी।
यह क्यों महत्वपूर्ण है: "वास्तविक दुनिया" का अंतर
हमें इससे क्या फर्क पड़ता है कि एक AI कुकबुक बदल नहीं सकता?
वास्तविक दुनिया में, गणित अन्वेषणात्मक (exploratory) है। जब गणितज्ञ कुछ नया खोजते हैं, तो उन्हें अक्सर अपनी स्वयं की परिभाषाएँ और नियम बनाने पड़ते हैं क्योंकि मानक "कुकबुक्स" में वे मौजूद नहीं होते।
- वर्तमान AI: एक ऐसे शेफ की तरह जो केवल तभी खाना बना सकता है जब आप उसे वही सटीक कुकबुक दें जिस पर उसने प्रशिक्षण लिया है। यदि आप उनसे एक नई रेसिपी बनाने या एक नए घटक का उपयोग करने के लिए कहते हैं, तो वे विफल हो जाते हैं।
- लक्ष्य: हम चाहते हैं कि AI एक अनुसंधान भागीदार (research partner) बन सके। हम चाहते हैं कि AI एक नई, अजीब परिभाषा को देख सके, उसे समझ सके और प्रमेय (theorems) सिद्ध करने में मदद कर सके, भले ही उसने पहले कभी उस विशिष्ट "बोली" को न देखा हो।
निष्कर्ष:
यह पेपर दिखाता है कि वर्तमान "स्टेट-ऑफ-द-आर्ट" AI प्रमेय सिद्ध करने वाले वास्तव में काफी नाजुक हैं। वे अत्यधिक विशिष्ट (over-specialized) हैं। वे एक विशिष्ट कमरे (MathLib) में पहेलियाँ सुलझाने में महान हैं, लेकिन यदि आप फर्नीचर को थोड़ा सा भी बदल दें (परिभाषाएं बदल दें), तो वे खो जाते हैं।
TAOBENCH इन AI के लिए एक नया जिम है। यह उन्हें लचीला बनना सिखाने के लिए मजबूर करता है, ताकि वे अंततः मनुष्यों के वास्तविक, अत्याधुनिक अनुसंधान में मदद कर सकें जहाँ नियम अभी तक लिखे नहीं गए हैं।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।