FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
यह शोध पत्र FormalRewardBench प्रस्तुत करता है, जो 250 विशेषज्ञ-क्यूरेटेड प्राथमिकता युग्मों (preference pairs) का उपयोग करके औपचारिक प्रमेय सिद्ध करने (formal theorem proving) में रिवॉर्ड मॉडल्स के मूल्यांकन के लिए पहला बेंचमार्क है, जो यह प्रकट करता है कि फ्रंटियर LLMs प्रमाण गुणवत्ता मूल्यांकन में विशिष्ट थ्योरम प्रोवर्स से बेहतर प्रदर्शन करते हैं और विभिन्न इंजेक्ट की गई त्रुटियों से सही प्रमाणों को अलग करने में वर्तमान मॉडल्स की सीमाओं को उजागर करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक रोबोट को गणित की समस्याएँ हल करना सिखा रहे हैं। रोबोट को सीखने के लिए प्रेरित करने हेतु, आपको उसे बताना होगा कि वह कब सही है और कब गलत।
लंबे समय से, इन रोबोटों (जिन्हें "न्यूरल थ्योरम प्रूवर" कहा जाता है) को सिखाने का मानक तरीका एक सरल ट्रैफिक लाइट सिस्टम रहा है:
- हरी बत्ती: प्रमाण (proof) एकदम सटीक है।
- लाल बत्ती: प्रमाण गलत है।
यह अच्छी तरह काम करता है क्योंकि "ट्रैफिक लाइट" वास्तव में एक कंप्यूटर प्रोग्राम है जो 100% सटीकता के साथ गणित की जाँच करता है। लेकिन इसमें एक बड़ी समस्या है: यह बहुत ही सीमित (sparse) है। यदि रोबोट एक कठिन समस्या का 99% हिस्सा हल कर लेता है लेकिन अंत में एक छोटी सी गलती कर देता है, तो उसे लाल बत्ती मिलती है। उसे उस 99% के लिए कोई श्रेय नहीं मिलता जो उसने सही किया था। यह ऐसा है जैसे किसी छात्र को एक प्रश्न गलत होने पर पूरे टेस्ट में "F" ग्रेड मिल जाए, बिना बाकी के काम पर कोई फीडबैक दिए। रोबोट भ्रमित हो जाता है और उसे समझ नहीं आता कि सुधार कैसे किया जाए।
इसे ठीक करने के लिए, शोधकर्ता एक रिवॉर्ड मॉडल (Reward Model) सिखाना चाहते हैं। इसे एक मानव-समान शिक्षक के रूप में सोचें जो एक प्रमाण को देख सकता है और कह सकता है, "आपने यहाँ बहुत अच्छा किया, लेकिन वहाँ आपने गलती की," और पास या फेल बताने के बजाय 0 से 100 तक का स्कोर दे सकता है।
समस्या: आप कैसे जानेंगे कि आपका "मानव-समान शिक्षक" (रिवॉर्ड मॉडल) वास्तव में ग्रेड देने में कितना अच्छा है?
आमतौरता पर, एक शिक्षक को परखने के लिए, आपको उन्हें हफ्तों तक कक्षा में पढ़ाने के लिए रखना होगा और देखना होगा कि छात्र सुधरते हैं या नहीं। यह महंगा और धीमा है।
समाधान: FormalRewardBench
लेखकों ने इन "शिक्षक" रोबोटों के लिए एक मानकीकृत ग्रेडिंग परीक्षा बनाई है। वे इसे FormalRewardBench कहते हैं।
यहाँ बताया गया है कि उन्होंने इस परीक्षा को कैसे बनाया:
- स्रोत सामग्री: उन्होंने 250 वास्तविक, कठिन गणितीय समस्याओं को लिया (इंटरनेशनल मैथ ओलंपियाड जैसी प्रतियोगिताओं से) जिन्हें Lean 4 नामक एक सख्त कंप्यूटर भाषा में अनुवादित किया गया है।
- जाल (The Trap): प्रत्येक सही प्रमाण के लिए, उन्होंने एक सुपर-स्मार्ट AI का उपयोग करके पाँच अलग-अलग प्रकार के नकली, गलत प्रमाण तैयार किए। ये केवल स्पष्ट टाइपो नहीं थे; ये चालाक जाल थे जिन्हें रोबोट को बेवकूफ बनाने के लिए डिज़ाइन किया गया था।
- द सर्जिकल स्ट्राइक (The Surgical Strike): सिर्फ एक छोटा सा अक्षर या नंबर बदल देना जो तर्क को तोड़ देता है।
- द स्मूथ टॉकर (The Smooth Talker): लंबे, आत्मविश्वास से भरे स्पष्टीकरण जोड़ना जो सही लगते हैं लेकिन वास्तव में गलत होते हैं।
- द इम्पोस्टर (The Imposter): समाधान को पायथन (Python) कोड में लिखना (जो कंप्यूटर के लिए काम करता है) बजाय आवश्यक गणितीय भाषा (Lean) के।
- द कन्फ्यूज्ड स्टूडेंट (The Confused Student): सही उपकरणों का उपयोग करना लेकिन उन्हें गलत धारणाओं पर लागू करना।
- द वर्डी नॉनसेंस (The Wordy Nonsense): एक ऐसा प्रमाण लिखना जो अविश्वसनीय रूप से लंबा और जटिल है लेकिन मौलिक रूप से त्रुटिपूर्ण है।
परीक्षण:
उन्होंने विभिन्न AI मॉडलों को एक जोड़े प्रमाणों (एक असली, एक नकली) को देखने और सही वाले को चुनने के लिए कहा। उन्होंने चार प्रकार के "जजों" का परीक्षण किया:
- सुपर-जीनियस (Frontier LLMs): विशाल, सामान्य-उद्देश्य वाले AI मॉडल (जैसे Claude Opus या GPT-5)।
- प्रोफेशनल ग्रेडर्स (Judge LLMs): वे मॉडल जिन्हें विशेष रूप से बेहतर उत्तर चुनने के लिए प्रशिक्षित किया गया है।
- गणित के माहिर (General-Purpose LLMs): वे मॉडल जिन्हें गणित और कोड पर भारी प्रशिक्षण दिया गया है।
- प्रूफ स्पेशलिस्ट (Theorem Provers): वे मॉडल जो विशेष रूप से गणितीय प्रमाण बनाने के लिए बनाए गए हैं।
चौंकाने वाले परिणाम:
शोध में एक आश्चर्यजनक मोड़ सामने आया:
- विशेषज्ञ विफल रहे: वे मॉडल जो प्रमाण लिखने में सबसे अच्छे हैं (प्रूफ स्पेशलिस्ट), वे प्रमाणों को ग्रेड देने में सबसे खराब थे। उनका स्कोर लगभग 24% था (अनुमान लगाने से भी कम बेहतर)। यह सच है कि घर बनाना जानने का मतलब यह नहीं है कि आप उसमें दरारें ढूंढने के लिए निरीक्षण करना जानते हैं।
- जनरलिस्ट जीते: "सुपर-जीनियस" (सामान्य AI मॉडल) नकली प्रमाणों को पकड़ने में सबसे अच्छे थे, जिनका स्कोर लगभग 60% था।
- "स्मूथ टॉकर" का जाल: कई मॉडल "वर्डी नॉनसेंस" या "स्मूथ टॉकर" वाले प्रमाणों से आसानी से धोखा खा गए। वे लंबे स्पष्टीकरणों को पसंद करते थे भले ही गणित गलत हो।
निष्कर्ष:
पेपर यह निष्कर्ष निकालता है कि एक प्रमाण बनाने में अच्छा होना स्वचालित रूप से उसे मूल्यांकन करने में अच्छा होने का प्रमाण नहीं है। गणितज्ञों की मदद करने के लिए बेहतर AI बनाने के लिए, हमें मॉडलों को विशेष रूप से "क्रिटिक" या "जज" बनने के लिए प्रशिक्षित करने की आवश्यकता है, न कि केवल "निर्माता" के रूप में।
लेखकों ने इस परीक्षा (FormalRewardBench) को सार्वजनिक रूप से जारी किया है ताकि अन्य शोधकर्ता अपने स्वयं के "शिक्षक" रोबोटों का परीक्षण कर सकें और देख सकें कि क्या वे वास्तव में त्रुटियों को पहचानने में बेहतर हो रहे हैं।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।