MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

कल्पना कीजिए कि आप एक अत्यंत बुद्धिमान लेकिन थोड़े अनाड़ी रोबोट को शुद्ध तर्क की भाषा बोलना सिखाने की कोशिश कर रहे हैं। यह रोबोट, जो एक लार्ज लैंग्वेज मॉडल (LLM) है, कहानियाँ पढ़ने, कविताएँ लिखने और सामान्य अंग्रेजी में गणित की पहेलियाँ हल करने में अद्भुत है। लेकिन एक पेच है: किसी गणितीय प्रमेय (theorem) को पूर्ण निश्चितता के साथ सिद्ध करने के लिए, आप केवल शब्दों का उपयोग नहीं कर सकते; आपको इसे 'लीन 4' (Lean 4) नामक एक अत्यंत सख्त कंप्यूटर भाषा में लिखना होगा। लीन 4 को एक उच्च-सुरक्षा वाली तिजोरी की तरह समझें जहाँ हर एक शब्द, प्रतीक और नियम सटीक होना चाहिए, अन्यथा तिजोरी का दरवाजा नहीं खुलेगा। समस्या यह है कि रोबोट गणित तो जानता है, लेकिन वह उस विशिष्ट "नियम पुस्तिका" (जिसे Mathlib कहा जाता है) को नहीं जानता जिसका लीन 4 उपयोग करता है। यह वैसा ही है जैसे किसी ऐसे शेफ से पूछना जो एक बेहतरीन स्टेक बनाना जानता है, लेकिन उसे एक ऐसी रेसिपी का पालन करने के लिए कहना जो एक ऐसी भाषा में लिखी गई है जिसे उसने पहले कभी नहीं देखा, और जिसमें ऐसे सामग्रियाँ हैं जिनके नाम भी उसे नहीं पता। वह अनुमान लगा सकता है, लेकिन उसके गलत होने की संभावना अधिक है।

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

MathForm के पीछे के शोधकर्ताओं ने महसूस किया कि रोबोट को औपचारिक गणित की भाषा में पूर्ण रूप से बोलने के लिए सक्षम बनाने हेतु, आप केवल उसे एक ड्राफ्ट लिखने और फिर बेहतर होने की उम्मीद करने के लिए नहीं छोड़ सकते। उन्होंने रोबोट के कार्यप्रवाह (workflow) को ठीक करने के लिए एक तीन-चरणीय असेंबली लाइन बनाई। सबसे पहले, रोबोट द्वारा कोड की एक भी पंक्ति लिखने से पहले, एक "रिसर्चर" (Researcher) एजेंट उस विशिष्ट समस्या के लिए रोबले की आवश्यकता वाले सटीक परिभाषाओं और नियमों को खोजने के लिए विशाल Mathlib लाइब्रेरी को स्कैन करता है। यह शेफ को चाकू उठाने से पहले ही "स्टेक" के लिए विशिष्ट कुकबुक पेज देने जैसा है। दूसरा, रोबोट अपना कोड लिखता है, और फिर एक "इंस्पेक्टर" (Inspector) उसकी जाँच करता है। यदि कोड में सिंटैक्स त्रुटि है (जैसे कॉमा गायब होना), तो इंस्पेक्टर उस ओर इशारा करता है। यदि कोड संकलित (compile) हो जाता है लेकिन उसका अर्थ गलत निकलता है (जैसे यह कहना कि "सभी संख्याएँ" जबकि समस्या का अर्थ केवल "धनात्मक संख्याएँ" था), तो इंस्पेक्टर उस अर्थ संबंधी त्रुटि (semantic error) को समझाता है। तीसरा, हार मानने के बजाय, रोबोट इस फीडबैक का उपयोग करके अपने कोड को फिर से लिखता है। वह इस "लिखो-जाँचो-सुधारो" चक्र के माध्यम से तब तक लूप में रहता है जब तक कि कोड सटीक न हो जाए।

इस चतुर लूप का उपयोग करते हुए, टीम ने एक विशाल नया डेटासेट FormalVerse बनाया, जिसमें लगभग 3,67,000 सत्यापित गणितीय उदाहरण शामिल हैं। इसके बाद उन्होंने एक नए मॉडल, MathForm-8B को इस डेटा पर प्रशिक्षित किया। परिणाम आश्चर्यजनक थे: यह अपेक्षाकृत छोटा मॉडल (8 बिलियन पैरामीटर्स) उन बहुत बड़े, विशिष्ट मॉडलों (32 बिलियन पैरामीटर्स) की तुलना में गणित को औपचारिक रूप देने में बेहतर बन गया जो पुराने "अनुमान लगाओ और आशा करो" वाले तरीकों पर निर्भर थे। छह अलग-अलग कठिन गणित परीक्षणों पर, MathForm-8B ने "कंसिस्टेंसी चेक" (Consistency Check) को लगभग 72.4% बार सफलतापूर्वक पास किया (जिसका अर्थ है कि कोड वास्तव में वही था जो मानव समस्या में कहा गया था), और पिछले सर्वश्रेष्ठ मॉडलों को पीछे छोड़ दिया। यहाँ तक कि सबसे कठिन, अमूर्त बीजगणित (abstract algebra) की समस्याओं पर भी, इसने अपने बड़े प्रतिद्वंद्वियों को काफी पीछे छोड़ दिया। यह शोध पत्र सुझाव देता है कि मॉडल को जानकारी खोजने के लिए सही उपकरण देने और उसे अपनी गलतियों से सीखने का अवसर देकर, आपको गणित का जीनियस बनने के लिए एक विशाल मस्तिष्क की आवश्यकता नहीं है; आपको बस एक स्मार्ट वर्कफ़्लो की आवश्यकता है।