💬 NLP

Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning

यह शोध पत्र BASE को प्रस्तुत करता है, जो एक बेस-एंड-एडिट पाइपलाइन है जो एक विशेष रीराइटर मॉडल (LEASCRIBE) का लाभ उठाकर एक एकल संभावित उत्तर को औपचारिक रूप देता है और इन-प्लेस एडिटिंग के माध्यम से शेष K-1 औपचारिक कथनों को कुशलतापूर्वक व्युत्पन्न करता है, जिससे लीन-आधारित गणितीय तर्क में उत्तर चयन सटीकता में सुधार करते हुए कम्प्यूटेशनल लागतों को काफी कम किया जाता है।

मूल लेखक: Ji Feng, Zhouxing Shi

प्रकाशित 2026-06-16

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

CC BY 4.0

मूल लेखक: Ji Feng, Zhouxing Shi

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

कल्पना कीजिए कि आप एक शिक्षक हैं जो 8 अलग-अलग गणितीय निबंधों का एक ढेर ग्रेड कर रहे हैं, जो एक बुद्धिमान लेकिन कभी-कभी भ्रमित होने वाले छात्र (AI) द्वारा लिखे गए हैं। प्रत्येक निबंध एक ही समस्या को हल करने की कोशिश करता है, लेकिन वे सभी थोड़े अलग उत्तरों पर पहुँचते हैं। आपका काम यह पता लगाना है कि वास्तव में कौन सा सही है।

परंपरागत रूप से, यह जाँचने के लिए कि उत्तर सही है या नहीं, आप एक अत्यंत कठोर, मशीन-जांच योग्य रोबोट (जिसे Lean कहा जाता है) से प्रत्येक निबंध को एक-एक करके सत्यापित करने के लिए कह सकते हैं। लेकिन यहाँ एक पेच है: रोबोट द्वारा निबंध की जाँच करने से पहले, आपको छात्र की अव्यवस्थित, प्राकृतिक भाषा वाली लिखावट को रोबोट की सख्त, कंप्यूटर-कोड भाषा में अनुवादित करना होगा। यह अनुवाद प्रक्रिया धीमी, महंगी और बहुत अधिक कंप्यूटिंग शक्ति की मांग करने वाली है। यदि आपके पास 8 निबंध हैं, तो आपको 8 महंगी अनुवाद प्रक्रियाओं के लिए भुगतान करना होगा।

यह शोध पत्र एक नया तरीका पेश करता है जिसे BASE (Base-and-Edit) कहा जाता है, जो खेल बदल देता है। सभी 8 निबंधों को शुरू से अनुवादित करने के बजाय, BASE कुछ चतुर करता है:

1. "Base" की खोज

सबसे पहले, सिस्टम निबंधों को उनके आत्मविश्वास के क्रम में देखता है (उस निबंध से शुरू करते हुए जिसे छात्र सबसे अधिक सही मानता है)। यह उनमें से केवल एक को रोबोट की भाषा में अनुवादित करता है और रोबोट से पूछता है, "क्या यह समझ में आता है?"

यदि रोबोट कहता है, "यह एक वैध गणितीय कथन है," तो वह Base बन जाता है।
यदि वह "नहीं" कहता है, तो यह अगले निबंध को आज़माता है।
आमतौर पर, पहली या दूसरी कोशिश सफल हो जाती है। इसलिए, आप केवल एक महंगी अनुवाद प्रक्रिया के लिए भुगतान करते हैं।

2. "Edit" (जादुई ट्रिक)

अब, शेष 7 निबंधों को शुरू से अनुवादित करने के बजाय, BASE महसूस करता है कि वे पहले वाले के लगभग समान हैं। वे एक ही समस्या संरचना साझा करते हैं; बस अंत में उनका नंबर या उत्तर अलग होता है।

पहले अनुवादित निबंध को एक कुकी कटर (cookie cutter) के रूप में सोचें। अन्य 7 निबंध उसी कुकी के आकार के हैं, बस उनमें "फिलिंग" (उत्तर) अलग है।

सरल संपादन (Simple Edits): यदि उत्तर बिल्कुल उसी तरह लिखा गया है (जैसे, "5"), तो BASE बस संख्या को बदल देता है।
स्मार्ट संपादन (Smart Edits - LEANSCRIBE): कभी-कभी छात्र उत्तर को अजीब तरीके से लिखता है (जैसे, "13 के वर्गमूल का 3 गुना")। रोबोट ने इसे एक जटिल कोड ब्लॉक के रूप में अनुवादित किया होगा। BASE एक विशेष सहायक मॉडल जिसका नाम LEANSCRIBE है, का उपयोग यह पता लगाने के लिए करता है कि वह जटिल कोड ब्लॉक ठीक कहाँ है और उसे नए उत्तर के कोड के साथ कैसे बदला जाए। यह एक मास्टर शेफ की तरह है जो पूरी रेसिपी को खराब किए बिना ठीक जानता है कि किस सामग्री को बदलना है।

परिणाम: एक "पारेटो सुधार" (Pareto Improvement)

शोध पत्र दावा करता है कि यह विधि एक "पारेटो सुधार" है, जो एक फैंसी तरीका है यह कहने का कि: "हमें बेहतर परिणाम मिले जबकि हमने कम पैसा खर्च किया।"

सस्ता: 8 अनुवादों के लिए भुगतान करने के बजाय, वे 1 अनुवाद और 7 सस्ते संपादनों के लिए भुगतान करते हैं। यह लागत को लगभग 5 गुना (विशेष रूप से, औसतन 5.4x) कम कर देता है।
अधिक सटीक: आश्चर्यजनक रूप से, इस विधि ने शून्य से शुरू करके प्रत्येक की जाँच करने की तुलना में सही उत्तर अधिक बार खोजा। क्यों? क्योंकि "Base" का पुन: उपयोग करके जिसे रोबोट ने पहले ही स्वीकृत कर लिया था, यह सिस्टम उन गलतियों से बचता है जो एक नए, बिखरे हुए निबंध को शुरू से अनुवादित करने पर होती हैं। यह एक घर के प्रमाणित, मजबूत ब्लूप्रिंट का उपयोग करने और फिर केवल पेंट का रंग बदलने जैसा है, बजाय इसके कि हर बार एक नया घर बनाने की कोशिश की जाए।

मुख्य निष्कर्ष (The Bottom Line)

लेखकों ने एक ऐसा सिस्टम बनाया है जो एक ही गणितीय समस्या को बार-बार पुन: अनुवादित करने में समय बर्बाद करना बंद कर देता है। यह एक "अच्छा" संस्करण ढूंढता है, उसे लॉक करता है, और फिर बाकी के लिए बस उत्तर में मामूली बदलाव करता है। यह गणित के उत्तरों की जाँच करना AI के लिए तेज़, सस्ता और आश्चर्यजनक रूप से अधिक विश्वसनीय बनाता है।

उन्होंने क्या दावा नहीं किया:

उन्होंने यह नहीं कहा कि यह AI के गणित कौशल को ठीक करता है; यह केवल एक सूची में से सबसे अच्छा उत्तर चुनने में मदद करता है।
उन्होंने यह दावा नहीं किया कि यह हर प्रकार की समस्या के लिए काम करता है (केवल उन समस्याओं के लिए जहाँ उत्तर संरचनात्मक रूप से समान दिखते हैं)।
उन्होंने स्वीकार किया कि जबकि "अनुवाद" की जाँच की जाती है, अंतिम "प्रमाण" (चरण-दर-चरण तर्क) अभी भी वर्तमान रोबोटों के लिए जल्दी से करना कठिन है, इसलिए वे पहले यह जाँचने पर ध्यान केंद्रित करते हैं कि क्या उत्तर रोबोट की भाषा में सही दिखता है।

तकनीकी सारांश: एक बार औपचारिक बनाना, शेष को संपादित करना (BASE)

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

जैसे-जैसे बड़े भाषा मॉडल (LLMs) गणितीय तर्क (mathematical reasoning) में अधिक रूप से लागू किए जा रहे हैं, वे अक्सर एक ही समस्या के लिए कई अलग-अलग तर्क पथ और संभावित उत्तर उत्पन्न करते हैं। एक महत्वपूर्ण चुनौती उत्तर चयन (answer selection) में आती है: टेस्ट-टाइम स्केलिंग के दौरान ग्राउंड-ट्रुथ लेबल तक पहुँच के बिना यह सत्यापित कैसे किया जाए कि कौन सा उम्मीदवार सही है।

जबकि मौजूदा दृष्टिकोण जैसे मेजॉरिटी वोटिंग या सीखे गए रिवॉर्ड मॉडल सांख्यिकीय संकेत प्रदान करते हैं, उनमें औपचारिक गारंटी का अभाव होता है। हाल के कार्यों ने उम्मीदवारों को सत्यापित करने के लिए औपचारिक प्रमाण सहायकों (विशेष रूप से Lean 4) का लाभ उठाया है। इस प्रतिमान (paradigm) में, एक "ऑटोफॉर्मलाइज़र" (autoformalizer) समस्या और एक संभावित उत्तर को एक लीन (Lean) प्रमेय कथन में अनुवादित करता है जो उत्तर की शुद्धता का दावा करता है। फिर एक प्रवर (prover) इस कथन को सत्यापित करने का प्रयास करता है।

हालाँकि, एक महत्वपूर्ण बाधा मौजूद है: $K$ संभावित उत्तरों को सत्यापित करने के लिए, ऑटोफॉर्मलाइज़र को $K$ बार स्वतंत्र रूप से बुलाया जाना चाहिए। यह $\Theta(K)$ का कम्प्यूटेशनल खर्च उठाता है, जो नमूनों की संख्या के साथ रैखिक रूप से बढ़ता है। लेखक देखते हैं कि एक एकल समस्या के लिए, $K$ औपचारिक कथन लगभग समान होते हैं, जो एक ही समस्या संरचना साझा करते हैं और केवल उत्तर अभिव्यक्ति (answer expression) में भिन्न होते हैं। मुख्य समस्या यह है कि चयन सटीकता से समझौता किए बिना औपचारिककरण लागत को $\Theta(K)$ से $\Theta(1)$ तक कैसे कम किया जाए।

2. कार्यप्रणाली: BASE पाइपलाइन

लेखक BASE (बेस-एंड-सबस्टिट्यूट-एडिट) प्रस्तावित करते हैं, जो एक एकल "बेस" उम्मीदवार को औपचारिक बनाने और शेष $K-1$ कथनों को स्थानीयकृत संपादन (localized editing) के माध्यम से प्राप्त करने के लिए डिज़ाइन की गई एक पाइपलाइन है।

2.1 बेस डिस्कवरी (Base Discovery)

पाइपलाइन एक अपस्ट्रीम सॉल्वर के साथ शुरू होती है जो $K$ संभावित उत्तरों की एक रैंक की गई सूची उत्पन्न करता है, $S(x) = (a_1, \dots, a_K)$ , जो सॉल्वर के आत्मविश्वास द्वारा क्रमबद्ध है।

सिस्टम रैंक क्रम में उम्मीदवारों के माध्यम से पुनरावृत्ति करता है।
प्रत्येक उम्मीदवार $a_i$ के लिए, यह समस्या-उत्तर युग्म $(x, a_i)$ को एक लीन कथन $F_i$ में औपचारिक बनाने का प्रयास करता है।
प्रक्रिया उस पहले उम्मीदवार $a_b$ पर रुक जाती है जिसका औपचारिककरण $F_b$ लीन में सफलतापूर्वक टाइप-चेक (type-checks) होता है।
$F_b$ बेस फॉर्मलाइजेशन बन जाता है, और $a_b$ बेस उत्तर बन जाता है।
यदि कोई भी उम्मीदवार टाइप-चेक नहीं होता है, तो सिस्टम शीर्ष-रैंक वाले उम्मीदवार $a_1$ पर वापस चला जाता है।

2.2 प्रतिस्थापन कैस्केड (Substitution Cascade)

एक बार एक वैध बेस $F_b$ स्थापित हो जाने के बाद, सिस्टम अन्य उम्मीदवारों को दर्शाने के लिए $F_b$ में इन-प्लेस संपादन करके शेष $K-1$ कथन उत्पन्न करता है। इसे दो-स्तरीय कैस्केड द्वारा संभाला जाता है:

टियर 1 (R1): नियम-आधारित प्रत्यक्ष स्थानीयकरण (Rule-Based Direct Localization)
- सिस्टम एक "गेटेड रीजन" (टिप्पणियों/हेडर को छोड़कर प्रमेय बॉडी) के भीतर सटीक स्ट्रिंग मिलान के माध्यम से $F_b$ में उत्तर अभिव्यक्ति को खोजने का प्रयास करता है।
- यदि एक अद्वितीय मिलान मिलता है, तो सिस्टम उत्तर स्ट्रिंग का सीधा प्रतिस्थापन (direct substitution) करता है।
- यदि कई मिलान होते हैं, तो एक छोटा विसंगति निवारण मॉडल (disambiguation model) सही स्लॉट का चयन करता है।
- यह टियर कुशल है लेकिन तब विफल हो जाता है जब ऑटोफॉर्मलाइज़र उत्तर को वर्बैटिम स्ट्रिंग (जैसे कि एक टुपल (3, 5) जिसे अलग-अलग बाइंडिंग्स के रूप में एनकोड किया गया हो या एक Prod वैल्यू) के बजाय विविध सिंटैक्टिक रूप में एनकोड करता है।
टियर 2 (R2): LEANSCRIBE (सीखा हुआ रीराइटर)
- उन मामलों के लिए जहाँ R1 विफल हो जाता है, सिस्टम LEANSCRIBE को बुलाता है, जो एक विशेष फाइन-ट्यून्ड LLM है।
- इनपुट: समस्या $x$ , बेस फॉर्मलाइजेशन $F_b$ , और बेस उत्तर $a_b$ ।
- आउटपुट:
  - एक लोकल ब्लॉक $s$ : $F_b$ का एक निरंतर खंड जिसमें उत्तर-निर्भर अभिव्यक्ति शामिल है।
  - एक फिल फंक्शन $f$ : एक हल्का पायथन फंक्शन जो किसी भी अनौपचारिक उत्तर $a_i$ को $s$ को बदलने वाली संगत लीन अभिव्यक्ति में मैप करता है।
- निष्पादन: LEANSCRIBE प्रति समस्या एक बार चलता है। जनरेट किया गया फंक्शन $f$ को शेष सभी $K-1$ उम्मीदवारों $a_i$ पर लागू किया जाता है ताकि उनके औपचारिक कथन $F_i = f(a_i)$ बनाए जा सकें। यह मॉडल कॉल की लागत को सभी $K-1$ उम्मीदवारों में फैला देता है (amortize करता है)।

2.3 सत्यापन और चयन (Verification and Selection)

पाइपलाइन प्राथमिक चयन संकेत के रूप में स्टेटमेंट-लेवल टाइप-चेकिंग पर निर्भर करती है।

एक उम्मीदवार को तब "सत्यापित" माना जाता है यदि उसका औपचारिक कथन $F_i$ लीन में टाइप-चेक होता है (अर्थात, एक सुव्यवस्थित प्रस्ताव/proposition है)।
सिस्टम उच्चतम-रैंक वाले उम्मीदवार $a_j$ का चयन करता है ऐसा कि $F_j$ टाइप-चेक हो।
यदि कोई भी उम्मीदवार टाइप-चेक नहीं होता है, तो यह शीर्ष-रैंक वाले उम्मीदवार $a_1$ पर वापस चला जाता है।
लेखक नोट करते हैं कि जबकि प्रूफ-लेवल सत्यापन (प्रूवर चलाना) अधिक कठोर है, वर्तमान प्रोवर्स का पास@1 दर कम है, जिससे बजट-बाधित सेटिंग में चयन के लिए स्टेटमेंट-लेवल टाइप-चेकिंग एक अधिक व्यावहारिक संकेत बन जाता है।

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

BASE पाइपलाइन: एक सत्यापित बेस स्टेटमेंट को साझा करके एकल सत्यापित बेस स्टेटमेंट के माध्यम से ऑटोफॉर्मलाइज़र लागत को $\Theta(K)$ से $\Theta(1)$ तक कम करने वाला पहला कार्य।
LEANSCRIBE मॉडल: एक सीखा हुआ रीराइटर जिसे उत्तर-निर्भर ब्लॉक्स को स्थानीयकृत करने और पुन: प्रयोज्य एडिट फंक्शन बनाने के लिए प्रशिक्षित किया गया है, जो उन विविध सिंटैक्टिक एनकोडिंग को संभालता है जिन्हें नियम-आधारित प्रतिस्थापन नहीं संभाल सकता।
पेरेटो सुधार (Pareto Improvement): यह विधि सभी परीक्षण कॉन्फ़िगरेशन में उच्च चयन सटीकता प्राप्त करते हुए कम्प्यूटेशनल लागत को काफी कम करती है।

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

लेखकों ने चार बेंचमार्क (MATH-500, OlympiadBench, AMC-AIMO, AIME 2024) पर तीन अलग-अलग अपस्ट्रीम सॉल्वर (Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B) का उपयोग करके $K=8$ उम्मीदवारों के साथ BASE का मूल्यांकन किया।

सटीकता (Accuracy): BASE ने स्वतंत्र फॉर्मलाइजेशन की तुलना में सभी 12 (डेटासेट, सॉल्वर) कॉन्फ़िगरेशन में चयन सटीकता (Acc) में सुधार किया, जिसमें लाभ +0.7 से +23.3 प्रतिशत अंक तक रहा।
मजबूती (Robustness): "गोल्ड-आंसर पास" दर (GT-pass)—वे समस्याएँ जहाँ सही उत्तर का कथन टाइप-चेक होता है—काफी बढ़ गई (33.3 अंक तक), जो कई मामलों में 96–100% तक पहुँच गई। यह इंगित करता है कि एक सत्यापित बेस को साझा करने से सही उत्तर का औपचारिककरण अधिक मजबूत हो जाता है।
लागत दक्षता (Cost Efficiency): $K=8$ पर, BASE ने ऑटोफॉर्मलाइज़र कॉल्स की संख्या को लगभग 5.4× कम कर दिया (औसत कमी 4.7–6.5×)। लागत $\Theta(K)$ के बजाय $\Theta(1)$ के रूप में स्केल करती है।
एब्लेशन (Ablation): केवल नियम-आधारित प्रतिस्थापन (R1) पर निर्भर करते हुए सीखा हुआ रीराइटर (LEANSCRIBE) हटाने से उम्मीदवार कवरेज में महत्वपूर्ण गिरावट (8–22 प्रतिशत अंक) आई, जो विविध सिंटैक्टिक एनकोडिंग को संभालने के लिए सीखे गए घटक की आवश्यकता को प्रदर्शित करता है।
प्रूफ-लेवल विश्लेषण: भले ही एक प्रूवर (DeepSeek-Prover-V2) का उपयोग किया गया हो, BASE ने 12 में से 11 कॉन्फ़िगरेशन में प्रूफ-लेवल सटीकता में सुधार किया, जो बताता है कि बेहतर-संरचित औपचारिक कथन डाउनस्ट्रीम प्रोवर्स की सहायता करते हैं।

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

लेखक दावा करते हैं कि BASE लीन-आधारित उत्तर चयन के लिए एक पेरेटो सुधार (Pareto improvement) का प्रतिनिधित्व करता है। एक बार औपचारिक बनाने और शेष को संपादित करने से, यह विधि साथ ही:

लागत कम करती है: औपचारिक सत्यापन के अनुमान (inference) लागत को काफी कम करती है, जिससे बड़े $K$ के साथ टेस्ट-टाइम स्केलिंग अधिक व्यवहार्य हो जाती है।
सटीकता में सुधार करती है: सही उत्तर चुनने की विश्वसनीयता को बढ़ाती है, क्योंकि साझा, सत्यापित स्कैफोल्ड का उपयोग करने से सही उम्मीदवार के लिए ऑटोफॉर्मलाइज़र की भिन्नता और विफलता दर कम हो जाती है।

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

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