💻 computer science

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4

यह शोध पत्र AMBER को प्रस्तुत करता है, जो अनुप्रयुक्त गणित के लिए एक नया Lean 4 बेंचमार्क है जो सत्यापन से पहले स्पष्ट समाधानों के निर्माण पर जोर देता है, जिससे यह पता चलता है कि सामान्य-उद्देश्य वाले रीजनिंग मॉडल विशिष्ट थ्योरम प्रूवर्स (theorem provers) से बेहतर प्रदर्शन करते हैं क्योंकि बाद वाले में "टैक्टिकल ओवरफिटिंग" (tactical overfitting) की प्रवृत्ति होती है जो जटिल निर्देश पालन में बाधा डालती है।

मूल लेखक: Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen

प्रकाशित 2026-02-03

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen

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

कल्पना कीजिए कि आप एक रोबोट को गणित सिखा रहे हैं। लंबे समय तक, हमने इस रोबोट को जो परीक्षण दिए वे इस तरह के थे जैसे उससे पूछना, "क्या इस पहेली का कोई समाधान मौजूद है?" रोबोट "हाँ" कहकर उत्तर दे सकता था, जैसे "मुझे पता है कि यह कहीं न कहीं मौजूद है," बिना कभी उस टुकड़े को वास्तव में खोजे या आपको यह दिखाए कि उसे कैसे जोड़ा जाए।

यह नया शोध पत्र, जिसका शीर्षक "Construction–Verification" (निर्माण-सत्यापन) है, यह तर्क देता है कि अनुप्रयुक्त गणित (applied mathematics - वह गणित जिसका उपयोग पुल बनाने, डिलीवरी रूट को अनुकूलित करने या डेटा का विश्लेषण करने के लिए किया जाता है) के लिए, केवल यह कहना कि "यह मौजूद है" पर्याप्त नहीं है। आपको यह भी चाहिए कि रोबमाट पहले समाधान को वास्तव में बनाए (build), और फिर सिद्ध करे कि वह काम करता है।

यहाँ एक सरल विवरण दिया गया है कि शोधकर्ताओं ने क्या किया और क्या पाया:

1. समस्या: "जादुई छड़ी" बनाम "ब्लूप्रिंट"

पारंपरिक गणितीय परीक्षणों में, एक रोबोट "जादुई छड़ी" (एक गैर-रचनात्मक प्रमाण/non-constructive proof) का उपयोग कर सकता है, समस्या को एक झटके में दूर कर सकता है और घोषित कर सकता है, "एक समाधान मौजूद है!" और आगे बढ़ सकता है।

पुराना तरीका: "मैंने सिद्ध किया कि एक पुल बनाया जा सकता है।" (लेकिन आपको नहीं पता कि इसे कैसे बनाना है)।
नया तरीका (AMBER बेंचमार्क): "यहाँ ब्लूप्रिंट और सामग्रियाँ हैं। पुल का निर्माण करें, और फिर मुझे दिखाएं कि यह गिरता क्यों नहीं है।"

शोधकर्ताओं ने एक नया परीक्षण बनाया जिसे AMBER (Applied Mathematics BEnchmark for Reasoning) कहा जाता है। यह AI को एक सख्त दो-चरणीय वर्कफ़्लो का पालन करने के लिए मजबूर करता है:

निर्माण (Construction): आपको वह कोड या फॉर्मूला लिखना होगा जो वास्तव में उत्तर की गणना करता है।
सत्यापन (Verification): आपको सिद्ध करना होगा कि आपका उत्तर सही है।

उन्होंने AI का चार कठिन क्षेत्रों पर परीक्षण किया:

कॉन्वेक्स एनालिसिस (Convex Analysis): एक घुमावदार घाटी में सबसे निचले बिंदु को खोजना।
ऑप्टिमाइज़ेशन (Optimization): सबसे कुशल योजना बनाना।
न्यूमेरिकल अलजेब्रा (Numerical Algebra): विशाल ग्रिडों में नंबरों की गणना करना।
हाई-डायमेंशनल प्रोबेबिलिटी (High-Dimensional Probability): कई चरों (variables) के साथ परिणामों की भविष्यवाणी करना।

2. आश्चर्य: विशेषज्ञों से बेहतर निकले सामान्यज्ञ (Generalists)

शोधकर्ता उम्मीद कर रहे थे कि जो रोबोट विशेष रूप से "गणित के प्रमाणक" (Math Provers) बनने के लिए प्रशिक्षित किए गए हैं, वे इस परीक्षण में सबको पछाड़ देंगे। वे गलत थे।

विशेषज्ञ (The Specialists - "टैक्टिकल ओवरफिटिंग" का जाल): वे रोबोट जो केवल गणितीय प्रमाणों पर प्रशिक्षित किए गए थे, वे फंस गए। वे केवल चीजों को सिद्ध करने के इतने आदी हो गए थे कि वे चीजों को बनाने के निर्देशों का पालन करना ही भूल गए। यह एक शतरंज के ग्रैंडमास्टर की तरह है जो खेल जीतने में इतना अच्छा है कि वह बोर्ड सेट करना ही भूल गया है। उन्होंने वास्तव में गणना किए बिना ही उत्तर के अस्तित्व को "सिद्ध" करने की कोशिश की, जो इस परीक्षण में विफल रहा।
सामान्यज्ञ (The Generalists - "स्विस आर्मी नाइफ"): वे रोबोट जो सामान्य तर्क (जैसे DeepSeek या GPT) पर प्रशिक्षित किए गए थे, उन्होंने बहुत बेहतर प्रदर्शन किया। क्योंकि वे विभिन्न संदर्भों में जटिल, बहु-चरणीय निर्देशों का पालन करने के आदी हैं, वे यह कहने में बेहतर थे कि, "ठीक है, पहले मुझे इस फंक्शन को परिभाषित करने की आवश्यकता है, फिर मुझे इसे सिद्ध करने की आवश्यकता है।" वे "बस सिद्ध करने" की आदत में नहीं फंसे।

3. यह परीक्षण वास्तव में कैसा दिखता है

शोध पत्र तीन प्रकार की चुनौतियों का वर्णन करता है जिनका सामना AI को करना पड़ा, जो मानक गणितीय परीक्षणों से भिन्न हैं:

मूल्यांकन समस्याएं (Evaluation Problems): "क्या $x$ के लिए कोई संख्या है जो इसे हल करती है?" पूछने के बजाय, परीक्षण पूछता है, "यहाँ $x$ के लिए फॉर्मूला है। इसे कैलकुलेट करने के लिए कोड लिखें।"
एल्गोरिदम डिज़ाइन (Algorithm Design): यह सिद्ध करने के बजाय कि एक लूप काम करता है, AI को खुद वह लूप लिखना होता है। यह एक शेफ से केक बनाया जा सकता है यह सिद्ध करने के बजाय, सटीक रेसिपी और मिश्रण के निर्देश लिखने के लिए कहने जैसा है।
रिप्रेजेंटेशन ट्रांसफॉर्मेशन (Representation Transformation): यह एक अव्यवस्थित, वास्तविक दुनिया की समस्या (जैसे "हम इन बसों को कैसे शेड्यूल करें?") को एक साफ, मानक गणितीय प्रारूप (जैसे "यह एक लीनियर प्रोग्रामिंग समस्या है") में अनुवाद करने जैसा है जिसे कंप्यूटर हल कर सके। AI को केवल एक सॉल्वर के रूप में नहीं, बल्कि एक अनुवादक के रूप में कार्य करना होता है।

4. रोबोट कहाँ विफल हुए

जब शोधकर्ताओं ने देखा कि रोबोट क्यों विफल हुए, तो उन्हें चार मुख्य कारण मिले:

भ्रम/हैलुसिनेशन (Hallucinations - 47%): रोबोटों ने ऐसे गणितीय प्रमेय या लाइब्रेरी के नाम बना दिए जो वास्तव में मौजूद नहीं थे। वे आत्मविश्वास से भरे लग रहे थे लेकिन तथ्य गढ़ रहे थे।
औपचारिकता त्रुटियां (Formalization Errors - 33%): वे सही गणितीय अवधारणाओं को जानते थे लेकिन उन्हें सख्त कंप्यूटर भाषा (Lean 4) में सही ढंग से अनुवादित नहीं कर सके।
हार मान लेना (Giving Up - 15%): उन्होंने कोड शुरू किया लेकिन उसे अधूरा छोड़ दिया, कठिन हिस्से को पूरा करने के बजाय "सॉरी" (एक प्लेसहोल्डर) लिख दिया।
टाइपो (Typos - 5%): साधारण फॉर्मेटिंग की गलतियाँ।

निष्कर्ष

शोध पत्र निष्कर्ष निकालता है कि AI को वास्तव में उपयोगी प्रयुक्त गणित (applied math) के लिए बनाने हेतु, हम केवल इसे "प्रूफ मशीन" के रूप में प्रशिक्षित नहीं कर सकते। हमें ऐसे सिस्टम चाहिए जो पहले समाधानों को बना सकें और फिर उनका सत्यापन कर सकें। वर्तमान में, सामान्य-उद्देश्य वाले AI मॉडल इस "निर्माण" कार्य में विशेष गणित मॉडल की तुलना में बेहतर हैं, क्योंकि विशेषज्ञ सोचने के मामले में बहुत अधिक कठोर (rigid) हो गए हैं।

शोधकर्ता सुझाव देते हैं कि भविष्य के AI को एक हाइब्रिड होना चाहिए: चीजें बनाने के लिए जटिल निर्देशों का पालन करने के लिए पर्याप्त स्मार्ट, और यह सिद्ध करने के लिए पर्याप्त सटीक कि वे सही हैं।

तकनीकी सारांश: कंस्ट्रक्शन-वेरिफिकेशन: लीन 4 (Lean 4) में अनुप्रयुक्त गणित को औपचारिक बनाने के लिए एक बेंचमार्क

1. समस्या विवरण

स्वचालित प्रमेय सिद्ध करने (automated theorem proving) के वर्तमान बेंचमार्क, जैसे कि MiniF2F और ProofNet, मुख्य रूप से घोषणात्मक प्रस्तावों (declarative propositions) के तार्किक सत्यापन पर केंद्रित हैं (अर्थात, समाधान के अस्तित्व को सिद्ध करना)। यह प्रतिमान अनुप्रयुक्त गणित (applied mathematics) के लिए अपर्याप्त है, जहाँ प्राथमिक उद्देश्य अक्सर केवल अस्तित्व के प्रमाण के बजाय ठोस मान (concrete values), निष्पादनीय एल्गोरिदम, या संरचनात्मक रूपांतरण प्राप्त करना होता है।

मौजूदा डेटासेट इस क्षेत्र में दो महत्वपूर्ण सीमाओं से ग्रस्त हैं:

स्कोप गैप (Scope Gap): उनमें स्नातक स्तर और उच्चतर अनुप्रयुक्त गणित का कवरेज नहीं है, जिसमें कॉनवेक्स एनालिसिस (convex analysis), ऑप्टिमाइज़ेशन, न्यूमेरिकल अलजेब्रा और हाई-डायमेंशनल प्रोबेबिलिटी शामिल हैं।
कंस्ट्रक्टिव डेफिसिट (Constructive Deficit): वे "निर्माण-सत्यापन" (construction-verification) वर्कफ़्लो को लागू करने में विफल रहते हैं। अनुप्रयुक्त गणित में, एक मॉडल को अपने correctness को सिद्ध करने से पहले एक समाधान (जैसे, एक एल्गोरिदम या एक विशिष्ट मान) को स्पष्ट रूप से संश्लेषित (synthesize) करना चाहिए। वर्तमान बेंचमार्क मॉडलों को गैर-रचनात्मक टैक्टिक्स (non-constructive tactics) का उपयोग करके इसे बायपास करने की अनुमति देते हैं (उदाहरण के लिए, विशिष्ट इष्टतम की गणना करने के बजाय 'एक्सट्रीम वैल्यू थ्योरम' के माध्यम से अस्तित्व को सिद्ध करना), जिससे मॉडल की कम्प्यूटेशनल रीजनिंग करने की क्षमता का गलत चित्रण होता है।

2. कार्यप्रणाली (Methodology)

कंस्ट्रक्शन-वेरिफिकेशन फ्रेमवर्क

लेखक लीन 4 (Lean 4) में एक औपचारिककरण प्रतिमान (formalization paradigm) प्रस्तावित करते हैं जो संरचनात्मक रूप से एक दो-चरणीय वर्कफ़्लो को लागू करता है: निर्माण (Construction) और उसके बाद सत्यापन (Verification)। यह फ्रेमवर्क एजेंटों को गैर-रचनात्मक शॉर्टकट का लाभ उठाने से रोकता है क्योंकि यह प्रमाणों से पहले स्पष्ट परिभाषाओं की मांग करता है। यह फ्रेमवर्क अनुप्रयुक्त गणित के तीन विशिष्ट श्रेणियों को संबोधित करता है:

इवैल्यूएशन प्रॉब्लम्स (Evaluation Problems): $\exists x, Q(x)$ को सिद्ध करने के बजाय, एजेंट को एक फंक्शन def x (V) := ... को परिभाषित करना होगा जो पैरामीटर्स $V$ के आधार पर समाधान $x(V)$ की गणना करता है, और फिर एक थ्योरम $Q(x(V), V)$ को सिद्ध करना होगा। फंक्शन सिग्नेचर इनपुट को कच्चे पैरामीटर्स तक सख्ती से सीमित करता है, जिससे मॉडल को निर्माण के लिए लक्षित गुण (target property) का उपयोग करके "चीटिंग" करने से रोका जा सके।
एल्गोरिदम डिज़ाइन प्रॉब्लम्स (Algorithm Design Problems): एजेंट को एक पुनरावर्ती फंक्शन (recursive function) को परिभाषित करना होगा जो एक पुनरावृत्ति प्रक्रिया (जैसे, ग्रेडिएंट डिसेंट) का प्रतिनिधित्व करता है। कार्य में $(n+1)$ -वें चरण के लिए ट्रांजिशन नियम (लूप बॉडी) को भरना शामिल है, और उसके बाद अभिसरण (convergence) या मोनोटोनिसिटी (monotonicity) जैसे गुणों का प्रमाण देना है।
रिप्रेजेंटेशन ट्रांसफॉर्मेशन (Representation Transformation): एजेंट को एक कच्चे समस्या उदाहरण को एक लक्षित कैनोनिकल फॉर्म (जैसे, एक ग्राफ कट समस्या को स्पेक्ट्रल क्लस्टरिंग फॉर्मूलेशन में बदलना) के रूप में मॉडल करना होगा। इसमें नया डोमेन, बाधाएं (constraints) और ऑब्जेक्टिव फंक्शन को परिभाषित करना, और स्रोत एवं लक्ष्य समस्याओं के बीच एक रिलैक्सेशन या समानता संबंध को सिद्ध करना शामिल है।
थ्योरम प्रूविंग (Theorem Proving): शुद्ध तार्किक तर्क क्षमताओं को मापने के लिए पारंपरिक निगमनात्मक कार्यों का एक बेसलाइन सबसेट शामिल किया गया है।

बेंचमार्क क्यूरेशन (AMBER)

लेखक AMBER (Applied Mathematics BEnchmark for Reasoning) पेश करते हैं, जो चार मुख्य डोमेन में फैला हुआ है:

कॉनवेक्स एनालिसिस (Convex Analysis)
ऑप्टिमाइज़ेशन (Optimization)
न्यूमेरिकल अलजेब्रा (Numerical Algebra)
हाई-डायमेंशनल प्रोबेबिलिटी (High-Dimensional Probability)

डेटा स्रोत और कठिनाई: समस्याएं शास्त्रीय पाठ्यपुस्तकों (जैसे, Boyd & Vandenberghe, Vershynin) से ली गई हैं और कठिनाई के आधार पर वर्गीकृत की गई हैं (आसान: मानक अभ्यास; कठिन: PhD क्वालिफाइंग एग्जाम स्तर)।
औपचारिककरण और सत्यापन: 50 समस्याओं को अनुभवी लीन (Lean) उपयोगकर्ताओं द्वारा औपचारिक रूप किया गया था। सत्यापन में दो चरणों वाली प्रक्रिया शामिल थी: एक LLM-आधारित सिमेंटिक चेक और उसके बाद मूल गणितीय कथनों के साथ सख्त संरेखण सुनिश्चित करने के लिए मैथलिब (Mathlib) योगदानकर्ताओं द्वारा कठोर मैनुअल क्रॉस-वैलिडेशन।
जटिलता मेट्रिक्स: बेंचमार्क को उच्च सिमेंटिक डिपेंडेंसी डेंसिटी (semantic dependency density) द्वारा पहचाना जाता है। डिपेंडेंसी ग्राफ विश्लेषण ( $k=3$ ) का उपयोग करते हुए, AMBER औसतन 164.21 की डिपेंडेंसी डेंसिटी प्रदर्शित करता है, जो MiniF2F (29.72), ProofNet (33.95), और FATE (53.14) की तुलना में काफी अधिक है, जो जटिल गणितीय अवधारणाओं को रिट्रीव करने और उन पर तर्क करने की गहरी आवश्यकता को दर्शाता है।

3. प्रमुख योगदान

प्रतिमान परिवर्तन (Paradigm Shift): यह पेपर अस्तित्व संबंधी प्रस्तावों (existential propositions) को सत्यापित करने से लेकर रचनात्मक समाधानों को संश्लेषित करने की ओर बदलाव का प्रस्ताव देता है, जो औपचारिक कार्यों को अनुप्रयुक्त गणित की कम्प्यूटेशनल अंतर्दृष्टि के साथ संरेखित करता है।
AMBER बेंचमार्क: विभिन्न कठिनाई स्तरों के साथ मुख्य अनुप्रयुक्त डोमेन को कवर करने वाला एक व्यापक डेटासेट, जिसमें केवल थ्योरम प्रूविंग ही नहीं, बल्कि एल्गोरिदम डिज़ाइन और रिप्रेजेंटेशन ट्रांसफॉर्मेशन जैसे जटिल कार्य भी शामिल हैं।
औपचारिककरण पैटर्न (Formalization Patterns): मूल्यांकन, एल्गोरिदम डिज़ाइन और रिप्रेजेंटेशन ट्रांसफॉर्मेशन के लिए विशेष लीन 4 टेम्प्लेट्स जो गैर-रचनात्मक तर्क के विरुद्ध सख्त सिंटैक्टिक बाधाएं लागू करते हैं।
अनुभवजन्य विश्लेषण (Empirical Analysis): एक व्यवस्थित मूल्यांकन जो वर्तमान न्यूरो-सिम्बोलिक सिस्टम में एक मौलिक ट्रेड-ऑफ को प्रकट करता है: स्थानीय टैक्टिकल दक्षता (विशेषज्ञ प्रूवर) और उच्च-स्तरीय एल्गोरिद्मिक संश्लेषण (सामान्य मॉडल) के बीच तनाव।

4. प्रयोगात्मक परिणाम

मॉडल प्रदर्शन

लेखकों ने विविध मॉडलों का मूल्यांकन किया, जिनमें सामान्य-उद्देश्य वाले रीजनिंग एजेंट (DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro) और विशेष थ्योरम प्रूवर (Goedel Prover-32B, Kimina Prover-72B) शामिल हैं।

कुल कठिनाई: सभी मॉडलों में प्रदर्शन उल्लेखनीय रूप से कम है। "Hard" सबसेट पर, लगभग सभी मॉडलों के लिए सफलता दर शून्य के करीब है।
सामान्य बनाम विशेष (General vs. Specialized): शुद्ध गणित बेंचमार्क के रुझान के विपरीत, सामान्य-उद्देश्य वाले रीजनिंग मॉडल लगातार विशेष थ्योरम प्रूवर से बेहतर प्रदर्शन करते हैं।
- Pass@16 (Full AMBER): सामान्य मॉडलों ने 4.50%–6.00% हासिल किया, जबकि विशेष प्रूवर ने 4.00% हासिल किया।
- Pass@16 (Hard Subset): सामान्य मॉडलों ने 0%–0% (Easy सबसेट्स में कुछ भिन्नता के साथ) हासिल किया, जबकि विशेष प्रूवर भी काफी संघर्ष करते रहे।
एब्लेशन स्टडी (Ablation Study): कंस्ट्रक्शन-वेरिफिकेशन प्रॉम्प्ट रणनीति ने 100-समस्याओं के सबसेट पर 8% सफलता दर प्राप्त की, जो मानक कोड कंप्लीशन (6%) और पारंपरिक प्रूफ-ओनली प्रॉम्प्ट्स (5%) से बेहतर थी। प्रूफ-ओनली प्रॉम्प्ट्स अक्सर मॉडलों को गैर-रचनात्मक शॉर्टकट (जैसे, Classical.choice) का उपयोग करने के लिए प्रेरित करते हैं।

त्रुटि विश्लेषण (Error Analysis)

DeepSeek-R1 मॉडल के 3,189 त्रुटि संदेशों के विश्लेषण से पता चला:

हैलुसिनेशन (Hallucination) (47.3%): सबसे आम विफलता मोड, जहाँ मॉडल गैर-मौजूद थ्योरम या परिभाषाओं (जैसे, convexHull eq sInter) का आह्वान करते हैं।
औपचारिककरण सक्षमता (Formalization Competence) (32.7%): वैध टैक्टिक्स का गलत अनुप्रयोग या साइड-कंडीशन्स को पूरा करने में विफलता।
अपूर्ण आउटपुट (Incomplete Outputs) (15.2%): पूरी तरह से निष्पादनीय कोड प्रदान करने में विफलता, जो अक्सर जटिल इंडक्टिव स्टेप्स में sorry प्लेसहोल्डर्स छोड़ देते हैं।
फॉर्मेटिंग/सिंटैक्स (Formatting/Syntax) (4.8%): बुनियादी मार्कडाउन या सिंटैक्स त्रुटियां।

5. महत्व और दावे

यह पेपर दावा करता है कि ऑटोमेटेड फॉर्मलाइजेशन का वर्तमान परिदृश्य "टैक्टिकल ओवरफिटिंग" (tactical overfitting) नामक घटना का सामना कर रहा है। प्रूफ कॉर्पोरा पर व्यापक रूप से फाइन-ट्यून किए गए विशेष मॉडल, अपनी सामान्य इंस्ट्रक्शन-फॉलोइंग क्षमताओं को खोते हुए प्रतीत होते हैं। वे हर संरचनात्मक चुनौती को एक शुद्ध थ्योरम-प्रूविंग कार्य के रूप में देखते हैं, और अक्सर अनुप्रयुक्त गणित की बहु-चरणीय आवश्यकताओं (जैसे, एक फंक्शन को सिद्ध करने से पहले उसे परिभाषित करना) को अनदेखा कर देते हैं।

इसके विपरीत, सामान्य-उद्देश्य वाले मॉडल वह बहुमुखी प्रतिभा बनाए रखते हैं जो अनौपचारिक इरादे और औपचारिक सिंटैक्स के बीच सेतु बनाने के लिए आवश्यक है, और सत्यापन चरण में प्रवेश करने से पहले गणितीय वस्तुओं को सफलतापूर्वक संश्लेषित करते हैं। लेखक निष्कर्ष निकालते हैं कि अनुप्रत्त गणित के दायरे को आगे बढ़ाने के लिए शुद्ध प्रूफ सर्च से आगे बढ़कर ऐसे न्यूरो-सिम्बोलिक सिस्टम की आवश्यकता है जो उच्च-स्तरीय एल्गोरिद्मिक रीजनिंग को कठोर औपचारिक सत्यापन के साथ एकीकृत करते हों। AMBER बेंचमार्क केवल तार्किक वैधता के बजाय रचनात्मक संश्लेषण की मांग करने वाले मानक प्रदान करके, औपचारिक अनुप्रयुक्त गणित के विस्तार के लिए भविष्य के अनुसंधान के लिए एक आधार के रूप में कार्य करता है।