तकनीकी सारांश: लीन (Lean) के माध्यम से प्रमेय सिद्ध करने के लिए प्रक्रिया-सत्यापित सुदृढीकरण शिक्षण (Process-Verified Reinforcement Learning)

समस्या विवरण

स्वचालित प्रमेय सिद्ध करना (Automated Theorem Proving - ATP) गणितीय प्रमेयों के लिए औपचारिक प्रमाण उत्पन्न करने का लक्ष्य रखता है। जबकि लार्ज लैंग्वेज मॉडल्स (LLMs) ने तर्क संबंधी कार्यों में प्रगति की है, वे आमतौर पर सुदृढीकरण शिक्षण (Reinforcement Learning - RL) के दौरान प्राकृतिक भाषा (Natural Language - NL) या बाइनरी परिणाम पुरस्कारों (सही/गलत) पर निर्भर करते हैं। यह एक अंतराल पैदा करता है:

1. विरल फीडबैक (Sparse Feedback): मानक RL दृष्टिकोण अक्सर केवल एक अंतिम बाइनरी सिग्नल (प्रमाण पास/फेल) का उपयोग करते हैं, जो विरल क्रेडिट असाइनमेंट प्रदान करता है और लंबे तर्क श्रृंखलाओं के माध्यम से मॉडल को निर्देशित करने में संघर्ष करता है।
2. असंरचित बनाम संरचित (Unstructured vs. Structured): प्रतीकात्मक प्रमाण सहायकों (जैसे Lean, Coq, Isabelle) के विपरीत, जो प्रत्येक तर्क चरण के लिए सूक्ष्म, प्रकार-सैद्धांतिक (type-theoretic) सत्यापन प्रदान करते हैं, LLMs को टोकन अनुक्रमों पर प्रशिक्षित किया जाता है जो स्केलर रिवॉर्ड्स (scalar rewards) पर आधारित होते हैं।
3. प्रक्रिया पुरस्कार मॉडल (Process Reward Models - PRMs): हालांकि हालिया कार्य स्टेप-लेवल रिवॉर्ड्स के लिए PRMs का उपयोग करते हैं, वे अक्सर बड़े एनोटेटेड डेटासेट या NL-आधारित CoT पर्यवेक्षण पर निर्भर करते हैं, जिनमें प्रतीकात्मक सत्यापन की कठोर शुद्धता (rigorous soundness) की कमी होती है।

मूल चुनौती यह है कि कैसे बाहरी, संभावित रूप से शोर वाले PRMs या मानव एनोटेशन पर निर्भर रहे बिना, एक प्रतीकात्मक प्रमाण सहायक (Lean) से प्राप्त समृद्ध, संरचित फीडबैक का लाभ उठाकर LLMs को प्रशिक्षित किया जाए।

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

यह शोध पत्र प्रक्रिया-सत्यापित सुदृढीकरण शिक्षण (Process-Verified Reinforcement Learning) का प्रस्ताव करता है, जो एक फ्रेमवर्क है जो लीन (Lean) के प्रतीकात्मक फीडबैक को सीधे ग्रुप रिलेटिव पॉलिसी ऑप्टिमाइजेशन (GRPO) ऑब्जेक्टिव के साथ एकीकृत करता है। यह विधि तीन मुख्य घटकों से मिलकर बनी है:

1. प्रतीकात्मक प्रक्रिया ओरेकल (Symbolic Process Oracle)

लीन (Lean) को केवल एक अंतिम सत्यापनकर्ता (verifier) के रूप में मानने के बजाय, लेखक इसे प्रशिक्षण के दौरान एक 'प्रक्रिया ओरेकल' के रूप में उपयोग करते हैं।

• पार्सिंग (Parsing): जनरेट किए गए प्रमाणों को एब्स्ट्रैक्ट सिंटैक्स ट्री (AST) के आधार पर टैक्टिक्स (tactics) ($T_1, \dots, T_N$) के अनुक्रम में पार्स किया जाता है।
• सत्यापन (Verification): लीन की इलैबोरेशन प्रक्रिया दो प्रकार के सिग्नल प्रदान करती है:
  • परिणाम सिग्नल (Outcome Signal): एक वैश्विक बाइनरी स्कोर $g(Y) \in \{0, 1\}$ जो यह दर्शाता है कि पूरा प्रमाण वैध है या नहीं।
  • प्रक्रिया सिग्नल (Process Signal): प्रत्येक टैक्टिक के लिए सूक्ष्म फीडबैक, जो स्थानीय रूप से सटीक चरणों और पहले त्रुटि के विशिष्ट स्थान की पहचान करता है।

2. क्रेडिट असाइनमेंट रणनीति (Credit Assignment Strategy)

प्रतीकात्मक फीडबैक और टोकन-लेवल RL के बीच के अंतर को पाटने के लिए, लेखक विशिष्ट असाइनमेंट नियम पेश करते हैं:

• प्रथम-त्रुटि प्रसार (First-Error Propagation): यदि एक टैक्टिक $T_j$ विफल हो जाता है, तो सभी आगामी टैक्टिक्स ($T_k$ जहाँ $k \ge j$) को त्रुटिपूर्ण माना जाता है। यह प्रमाणों की कारण संबंधी प्रकृति को दर्शाता: एक अमान्य प्रीफिक्स पूरी आगामी तर्क श्रृंखला को अमान्य कर देता है।
• टैक्टिक-स्तरीय स्कोरिंग ($\phi$):
  • यदि प्रमाण पास हो जाता है ($g(Y)=1$), तो सभी टैक्टिक्स को सकारात्मक स्कोर (1) प्राप्त होता है।
  • यदि प्रमाण विफल हो जाता ($g(Y)=0$):
    • पहली त्रुटि से पहले के टैक्टिक्स को आंशिक स्कोर ($d_1$) प्राप्त होता है।
    • पहली त्रुटिपूर्ण टैक्टिक और उसके बाद के सभी को दंड स्कोर ($d_2$) प्राप्त होता है।
• टोकन-स्तरीय मैपिंग (Token-Level Mapping): टैक्टिक-स्तरीय एडवांटेज को प्रत्येक टैक्टिक के केवल पहले टोकन (कीवर्ड, जैसे intro, apply) को सौंपा जाता है। यह उस सिमेंटिक निर्णय बिंदु के साथ संरेखित होता जहाँ प्रमाण रणनीति निर्धारित की जाती है।

3. RL ऑब्जेक्टिव (GRPO एकीकरण)

यह फ्रेमवर्क आउटकम और प्रोसेस एडवांटेज को एक एकल GRPO ऑब्जेक्टिव में जोड़ता है:

• आउटकम एडवांटेज ($A_{outcome}$): वैश्विक पास/फेल स्थिति के आधार पर ग्रुप मीन (group mean) के सापेक्ष गणना की जाती है।
• प्रोसेस एडवानाेज ($A_{process}$): टैक्टिक-लेवल स्कोर के आधार पर गणना की जाती है, जिसे समस्या की कठिनाई को ध्यान में रखने के लिए ग्रुप के औसत आउटकम रिवॉर्ड द्वारा सामान्यीकृत (normalized) किया जाता है।
• संयुक्त एडवांटेज (Combined Advantage): प्रतिक्रिया $i$ में टैक्टिक $j$ के पहले टोकन के लिए टोकन $t$ हेतु:
  $$A_{i,t} = A_{outcome, i, t} + A_{process, i, j}$$
  गैर-प्रथम टोकनों के लिए, केवल आउटकम एडवांटेज लागू होता है। यह फॉर्मूलेशन वैल्यू मॉडल या सहायक PRM की आवश्यकता को समाप्त करता है, और पूरी तरह से सत्यापनकर्ता के ग्राउंड ट्रुथ (ground truth) पर निर्भर करता है।

मुख्य योगदान

1. प्रतीकात्मक फीडबैक का औपचारिकीकरण: लेखक लीन के टैक्टिक-लेवल फीडबैक को स्केलर ट्रेनिंग सिग्नल्स में औपचारिक रूप देते हैं, जिससे प्राकृतिक भाषा मार्गदर्शन के बिना सूक्ष्म, टोकन-लेवल क्रेडिट असाइनमेंट सक्षम होता है।
2. प्रतीकात्मक सत्यापन-निर्देशित RL: वे आउटकम और टैक्टिक-लेवल रिवॉर्ड्स को सीधे लीन से प्राप्त करके एक RL फ्रेमवर्क में एकीकृत करते हैं, जो सघन (dense) और सत्यापन योग्य क्रेडिट असाइनमेंट प्रदान करता है।
3. स्थिर बेंचमार्क सुधार: दृष्टिकोण MiniF2F और ProofNet बेंचमार्क पर निरंतर सुधार प्रदर्शित करता है, जो बाहरी PRMs या NL नोटेशन के बिना आउटकम-ओनली RL और वैनिला बेसलाइन्स से बेहतर प्रदर्शन करता है।

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

प्रयोग STP-Lean और DeepSeek-Prover-V1.5 (7B मॉडल्स) का उपयोग करके MiniF2F-Test और ProofNet-Test बेंचमार्क पर किए गए।

• प्रदर्शन लाभ (Performance Gains):
  • STP-Lean: प्रस्तावित विधि ने MiniF2F pass@64 में +2.5% (56.7% से 59.2% तक) और ProofNet pass@32 में +1.4% का सुधार किया।
  • DeepSeek-Prover-V1.5: सभी सेटिंग्स में निरंतर, हालांकि मामूली सुधार देखे गए।
• बेसलाइन्स के साथ तुलना:
  • इसने "Outcome-only" GRPO को पछाड़ दिया, जो अस्थिरता दिखाता है और कुछ कॉन्फ़िगरेशन में ProofNet पर सुधार करने में विफल रहा।
  • इसने मजबूत ट्री-सर्च बेसलाइन्स (जैसे InternLM2.5-StepProver, DeepSeek-Prover-RL+RMaxTS) के मुकाबले प्रतिस्पर्धी परिणाम प्राप्त किए, जबकि भारी इन्फरेंस-टाइम सर्च बजट के बिना सिंगल-शॉट जनरेशन दृष्टिकोण का उपयोग किया।
• एब्लेशन अध्ययन (Ablation Studies):
  • टोकन असाइनमेंट: क्रेडिट को टैक्टिक के पहले टोकन को सौंपने से पूरे टोकन या अंतिम टोकन में वितरित करने की तुलना में सबसे स्थिर परिणाम मिले।
  • प्रथम-त्रुटि प्रसार: इस नियम को हटाने से प्रदर्शन काफी गिर गया, जो पुष्टि करता है कि त्रुटि के बाद के चरणों को अमान्य मानने की आवश्यकता है।
  • टाइमआउट: 15-सेकंड का सत्यापन टाइमआउट सबसे अच्छा संतुलन प्रदान करता है, जो वैध जटिल प्रमाणों को खारिज किए बिना संक्षिप्त प्रमाणों को प्रोत्साहित करता है।

महत्व और दावे

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

अध्ययन रेखांकित करता है कि:

• सघन, सत्यापन योग्य सिग्नल: प्रोवर के अपने एरर लॉग्स और इलैबोरेशन ट्री का उपयोग करना एक सुदृढ़, सघन रिवॉर्ड सिग्नल प्रदान करता है जो विरल बाइनरी आउटकम या सीखे गए PRMs से बेहतर है।
• स्थिरता: ग्लोबल आउटकम रिवॉर्ड्स और लोकल टैक्टिक रिवॉर्ड्स का संयोजन प्रशिक्षण को स्थिर करता है, जिससे टैक्टिक-ओनली ट्रेनिंग में देखी गई समयपूर्व अभिसरण (premature convergence) और आउटकम-ओनली ट्रेनिंग की विरलता की समस्याओं को रोका जा जाता है।
• दक्षता: यह दृष्टिकोण ट्री सर्च के कम्प्यूटेशनल ओवरहेड या अलग PRMs के डेटा आवश्यकताओं के बिना अत्याधुनिक या प्रतिस्पर्धी प्रदर्शन प्राप्त करता है।

लेखक अपनी सीमाओं के संबंध में विनम्र रहते हैं, यह नोट करते हुए कि उनकी विधि सीखा गया एडवांटेज एस्टिमेटर होने के बजाय निश्चित रिवॉर्ड स्कोर ($d_1, d_2$) पर निर्भर करती है और वर्तमान में गैर-CoT, शुद्ध लीन प्रमाणों पर केंद्रित है, जिससे लंबे रूप वाले प्राकृतिक भाषा तर्क के लिए रिवॉर्ड डिजाइन का प्रश्न खुला रह जाता है।