CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean
यह शोधपत्र CAM-Bench प्रस्तुत करता है, जो कम्प्यूटेशनल और अनुप्रयुक्त गणित में 1,000 औपचारिक समस्याओं वाला एक नया Lean 4 बेंचमार्क है, जो पाठ्यपुस्तकीय अभ्यासों को अनुकूलित करने के लिए एक डिपेंडेंसी-रिकवरी पाइपलाइन का उपयोग करके और स्थानीय संदर्भ ट्रैकिंग तथा प्रारंभिक प्रमेय अनुप्रयोग की आवश्यकताओं वाले कार्यों पर लार्ज लैंग्वेज मॉडल्स के प्रदर्शन का विश्लेषण करके मौजूदा मूल्यांकनों में इन डोमेन के कम प्रतिनिधित्व को संबोधित करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक बुद्धिमान लेकिन अत्यंत शाब्दिक (literal-minded) रोबोट को गणित सिखाने की कोशिश कर रहे हैं। आपके पास इसे परखने के दो तरीके हैं:
- "उत्तर कुंजी" परीक्षण (The "Answer Key" Test): आप रोबोट को एक गणितीय समस्या देते हैं और वह अंतिम संख्या लिख देता है। यदि संख्या सही है, तो आप उसे एक गोल्ड स्टार देते हैं। वर्तमान में अधिकांश AI गणित परीक्षण इसी तरह काम करते हैं।
- "चरण-दर-चरण" परीक्षण (The "Step-by-Step" Test): आप रोबोट से हर एक तार्किक चरण को विस्तार से लिखने के लिए कहते हैं, जैसे कि किसी पाठ्यपुस्तक में प्रमाण (proof) होता है, और फिर आप यह जाँचते हैं कि क्या हर चरण तार्किक रूप से अटूट है। यह बहुत कठिन है, लेकिन यह साबित करता है कि रोबोट वास्तव में गणित को समझता है, न कि केवल अनुमान लगा रहा है।
यह शोध पत्र एक नया, अत्यंत कठिन "चरण-दर-चरण" परीक्षण पेश करता है जिसे CAM-Bench कहा जाता है।
समस्या: रोबोट केवल "ओलंपियाड" गणित जानता है
वर्तमान में, गणित के लिए अधिकांश AI परीक्षण ओलंपियाड पहेलियों की तरह होते हैं। वे पेचीदा, स्व-निहित पहेलियाँ (जैसे "सिद्ध करें कि यदि X सत्य है, तो Y सत्य है") होती हैं। AI इन मामलों में अच्छा है क्योंकि ये अलग-थलग पड़े तर्क के खेल की तरह होते हैं।
लेकिन वास्तविक दुनिया का गणित—जैसे इंजीनियरिंग, वित्त, या भौतिकी—अलग है। यह आमतौर पर कोई साफ-सुथरी पहेली नहीं होती। यह अधिक से अधिक एक कुकबुक (पाक पुस्तिका) से रेसिपी (विधि) का पालन करने जैसा है।
- रेसिपी (समस्या) यह मान लेती है कि आप पहले से जानते हैं कि "सॉते" (sauté) करने का क्या अर्थ है।
- यह मान लेती है कि आपके पास एक विशिष्ट प्रकार का पैन है (जो अध्याय 3 की एक परिभाषा है)।
- यह मान लेती है कि आप प्याज कैसे काटते हैं (जो अध्याय 1 का एक एल्गोरिदम है)।
यदि आप रोबोट को केवल रेसिपी का अंतिम वाक्य थमा देते हैं ("सूप बनाएं"), तो वह भ्रमित हो जाता है क्योंकि उसके पास वह "स्थानीय संदर्भ" (definitions, tools, previous steps) नहीं है जिसे मूल लेखक ने पहले से ही मौजूद माना था।
CAM-Bench को यह परीक्षण करने के लिए डिज़ाइन किया गया है कि क्या AI इस "कुकबुक शैली" के गणित को संभाल सकता है, विशेष रूप से ऑप्टिमाइज़ेशन (सबसे अच्छा तरीका खोजना), न्यूमेरिकल लीनियर अल्जेब्रा (संख्याओं के विशाल ग्रिड के साथ गणित करना), और न्यूमेरिकल एनालिसिस (समाधानों का अनुमान लगाना) जैसे क्षेत्रों में।
समाधान: "संदर्भ जासूस" पाइपलाइन (The "Context Detective" Pipeline)
लेखकों ने केवल पाठ्यपुस्तकों से समस्याएं उठाकर AI को नहीं दीं। उन्होंने समस्याओं को तैयार करने के लिए एक परिष्कृत पाइपलाइन (एक फैक्ट्री लाइन) बनाई है। इसे एक संदर्भ जासूस (Context Detective) के रूप में सोचें:
- कच्चा सुराग (The Raw Clue): वे एक अव्यवस्थित पाठ्यपुस्तक अभ्यास से शुरू करते हैं जो कहता है, "समस्या 16.76 को हल करने के लिए एल्गोरिदम 16.4 का उपयोग करें।"
- जासूसी कार्य (The Detective Work): पाइपलाइन वापस किताब में जाती है ताकि यह पता लगाया जा सके कि "एल्गोरिदम 16.4" वास्तव में क्या है। यह उन परिभाषाओं, सूत्रों और धारणाओं को खोज निकालती है जो पिछले अध्यायों में छिपी हुई हैं।
- पुनर्निर्माण (The Reconstruction): यह इन बिखरे हुए टुकड़ों को एक साथ जोड़कर एक बड़ा, स्व-निहित "अनौपचारिक प्रमेय" (informal theorem) बनाती है। यह एक ऐसी रेसिपी को फिर से लिखने जैसा है जिसमें लिखा है "गुप्त सॉस डालें" और उसे बदलकर "टमाटर, तुलसी और लहसुन से बनी सॉस डालें" कर दिया गया है।
- अनुवाद (The Translation): अंत में, यह इस साफ, स्व-निहित कहानी को Lean में अनुवादित करती है, जो एक सख्त कंप्यूटर भाषा है और एक अत्यंत सूक्ष्म (pedantic) गणित शिक्षक की तरह व्यवहार करती है। यदि इसके तर्क में एक भी छोटी सी कमी होती है, तो Lean इसे अस्वीकार कर देता है।
परिणाम: AI "कुकबुक" में फंसा हुआ है
लेखकों ने इस नए बेंचमार्क पर दुनिया के सबसे स्मार्ट AI मॉडल का परीक्षण किया। यहाँ क्या हुआ:
- "उत्तर कुंजी" का अंतर (The "Answer Key" Gap): AI मॉडल सामान्य अंग्रेजी में समस्याओं को हल करने में काफी अच्छे थे (सही उत्तर प्राप्त करना)। लेकिन जब उन्हें Lean (एक सख्त भाषा) में प्रमाण लिखना था, तो उनकी सफलता दर तेजी से गिर गई।
- उपमा: यह ऐसा है जैसे AI आपसे बातचीत में केक बनाने का तरीका बता सकता है, लेकिन यदि आप उसे एक ऐसे रोबोट के लिए निर्देश लिखने के लिए कहें जो कुछ भी अनुमान नहीं लगा सकता, तो वह रसोई जला देगा।
- "स्थानीय संदर्भ" की विफलता (The "Local Context" Failure): AI बार-बार "स्थानीय नियमों" को भूल जाता था। वह ऐसे टूल का उपयोग करने की कोशिश करता जो वर्तमान अध्याय में मौजूद नहीं था, या वह एक छोटी सी धारणा (जैसे "संख्या सकारात्मक होनी चाहिए") को छोड़ देता जो पाठ्यपुस्तक ने उस विशिष्ट वाक्य में स्पष्ट रूप से नहीं लिखी थी लेकिन निहित की थी।
- "लंबी श्रृंखला" की समस्या (The "Long Chain" Problem): वास्तविक गणितीय समस्याओं के लिए अक्सर छोटे चरणों की एक लंबी श्रृंखला की आवश्यकता होती है (जैसे ईंट-दर-ईंट घर बनाना)। AI मॉडल अक्सर श्रृंखला के बीच में ही भटक जाते थे, यह भूल जाते थे कि वे क्या बना रहे हैं या लंबे समय के लक्ष्य पर नियंत्रण खो देते थे।
"एजेंट" अपग्रेड (The "Agent" Upgrade)
शोधकर्ताओं ने एक अधिक उन्नत तरीका भी आजमाया जहाँ AI एक टूलबॉक्स के साथ एक मानव जासूस की तरह कार्य करता है। केवल उत्तर का अनुमान लगाने के बजाय, AI को अनुमति है:
- गलती होने पर कंप्यूटर (Lean) से मदद मांगना।
- अपने काम की स्वयं जाँच करना।
- त्रुटि संदेश (error message) के आधार पर फिर से प्रयास करना।
यह "एजेंट" दृष्टिकोण बहुत बेहतर रहा, जिसने सफलता दर को दोगुना कर दिया। हालाँकि, यह अभी भी पूर्णता से बहुत दूर था, और इसे चलाने के लिए बहुत अधिक "मस्तिष्क शक्ति" (कंप्यूटर टोकन) की आवश्यकता थी।
निष्कर्ष (The Bottom Line)
CAM-Bench दिखाता है कि जबकि AI गणितीय पहेलियों को हल करने में अच्छा हो रहा है, यह अभी भी उस अनुप्रयुक्त गणित (applied math) के लिए संघर्ष कर रहा है जिसके लिए संदर्भ समझने, स्थानीय नियमों को याद रखने और चरण-दर-चरण तार्किक तर्क बनाने की आवश्यकता होती है।
लेखक निष्कर्ष निकालते हैं कि AI को वास्तविक दुनिया के गणित के लिए वास्तव में विश्वसनीय बनाने के लिए, हमें इसे अलग-थलग पड़ी पहेलियों पर टेस्ट करना बंद करना होगा और इसे इन जटिल, संदर्भ-प्रधान "कुकबुक" समस्याओं पर टेस्ट करना शुरू करना होगा। वर्तमान मॉडल उन छात्रों की तरह हैं जो उत्तर रटने में तो माहिर हैं लेकिन अभी तक ज़मीन से घर बनाना नहीं सीख पाए हैं।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।