तकनीकी सारांश: पाइथागोरस-प्रूवर (Pythagoras-Prover)

समस्या विवरण

आधुनिक लीन (Lean) प्रमेय प्रूवर (theorem provers) ने मजबूत प्रदर्शन हासिल किया है, लेकिन वे भारी प्रशिक्षण और अनुमान गणना (inference compute) पर निर्भर करते हैं, जिसके लिए अक्सर फ्रंटियर-स्केल मॉडल्स (सैकड़ों अरब पैरामीटर्स) या व्यापक खोज, स्व-सुधार (self-correction) और बड़े सैंपलिंग बजट जैसी गणनात्मक रूप से गहन अनुमान प्रक्रियाओं की आवश्यकता होती है। यह निर्भरता सत्यापित प्रमाण डेटा (verified proof data) की कमी और औपचारिक प्रमाण खोज के लिए आवश्यक लंबे तर्क पथों (reasoning traces) के कारण है, जो सुपरवाइज्ड फाइन-ट्यूनिंग (SFT) और सैंपलिंग को महंगा बना देते हैं। फलस्वरूप, छोटे ओपन-सोर्स प्रूवर्स और उनके सबसे बड़े समकक्षों के बीच एक महत्वपूर्ण अंतर मौजूद है, जो उन शोधकर्ताओं और चिकित्सकों के लिए पहुंच को सीमित करता है जिनके पास विशाल कंप्यूट संसाधन नहीं हैं।

कार्यप्रणाली

लेखक पाइथागोरस-प्रूवर (Pythagoras-Prover) का परिचय देते हैं, जो लीन 4 (Lean 4) का एक कंप्यूट-कुशल ओपन-सोर्स प्रमेय प्रूवर परिवार है। यह दृष्टिकोण कच्चे मॉडल स्केल के बजाय एक चरणबद्ध, कंप्यूट-मितव्ययी (compute-frugal) डेटा पाइपलाइन और प्रशिक्षण रणनीति पर निर्भर करता है।

1. डेटा निर्माण और पाठ्यक्रम शिक्षण (Curriculum Learning)

प्रशिक्षण कॉर्पस को तीन कठिनाई स्तरों (आसान, मध्यम, कठिन) में बनाया गया है, जो सभी शुद्धता सुनिश्चित करने के लिए लीन टाइप-चेकर द्वारा नियंत्रित हैं:

• आसान और मध्यम स्तर: इन्हें "थ्योरम प्रूवर एज़ अ जज" (Theorem Prover as a Judge) से प्रेरित एक तीन-चरणीय पाइपलाइन के माध्यम से उत्पन्न किया गया है, जहाँ DART-Math-Hard, DeepScaleR और OpenR1-Math जैसे डेटासेट से प्राकृतिक भाषा की समस्याओं को लीन कथनों (statements) में ऑटोफॉर्मलाइज (autoformalize) किया गया है। विफल प्रमाणों का विश्लेषण किया जाता है, और एक रूब्रिक-निर्देशित डिस्टिलेशन (rubric-guided distillation) प्रक्रिया विशिष्ट त्रुटि श्रेणियों (जैसे, टैक्टिक विफलताएं, टाइप मिसमैच) को लक्षित करने वाले सरलीकृत सिंथेटिक वेरिएंट उत्पन्न करती है। यह प्रक्रिया ऑटोफॉर्मलाइजेशन सफलता दर में 30% सापेक्ष सुधार प्रदान करती है।
• कठिन स्तर: इसे Big-Math-RL-Verified से प्रतियोगिता-स्तर की समस्याओं (Olympiads, AIME, AMC) से लिया गया है। आसान स्तरों के विपरीत, इन्हें सुदृढीकरण शिक्षण (reinforcement learning - RL) के लिए उनकी कठिनाई बनाए रखने हेतु सरल नहीं बनाया गया है।
• करिकुलम SFT: मॉडल्स को एक कठिनाई-क्रमित पाठ्यक्रम (आसान $\to$ मध्यम $\to$ कठिन) के साथ LoRA (लो-रैंक अडैप्टेशन) का उपयोग करके प्रशिक्षित किया जाता है ताकि पैरामीटर दक्षता बनी रहे। 8k-टोकन संदर्भ बजट को प्रबंधित करने के लिए SFT के दौरान एक डायनेमिक प्रूफ-रीजनिंग फ़िल्टरिंग स्कीम लागू की जाती है: यदि रीजनिंग चेन और प्रमाण सीमा से अधिक हो जाता है, तो प्रमाण को रखते हुए रीजनिंग को हटा दिया जाता है; यदि केवल प्रमाण ही सीमा से अधिक हो जाता है, तो उस इंस्टेंस को त्याग दिया जाता है।

2. ऑगमेंटेड लीन फॉर्मलाइजेशन (ALF) और स्व-डिस्टिलेशन (Self-Distillation)

लीन सत्यापन थ्रूपुट (verification throughput) की बाधा को दूर करने के लिए, लेखक ऑगमेंटेड लीन फॉर्मलाइजेशन (ALF) पेश करते हैं।

• तंत्र: ALF सत्यापित सीड इंस्टेंसेस पर पांच संरचित उत्परिवर्तन ऑपरेटरों (सरलीकरण, सामान्यीकरण, लेम्मा प्रस्ताव, प्रूफ-स्टेप डिकम्पोजिशन, रीफॉर्मुलेशन) को लागू करता है।
• दक्षता: प्रत्येक उत्परिवर्तित इंस्टेंस को लीन के साथ सत्यापित करने के बजाय (जो गणनात्मक रूप से निषेधात्मक है), ALF एक हल्के स्टेटमेंट-अलाइनमेंट चेक का उपयोग करता है। यह सत्यापित करता है कि उत्पन्न प्रमाण उत्परिवर्तित कथन को संदर्भित करता है, जिससे पूर्ण संकलन (compilation) के बिना संरचनात्मक वैधता सुनिश्चित होती है।
• स्व-डिस्टिलेशन: पोस्ट-RL मॉडल इन उत्परिवर्तित कथनों के लिए प्रमाण उत्पन्न करता है। यह प्रति-इंस्टेंस सत्यापन की आवश्यकता के बिना कॉर्पस को लगभग 2.5$\times$ (~2M इंस्टेंसेस तक) विस्तारित करता है। इस विस्तारित कॉर्पस का उपयोग निरंतर SFT और एक डिफ्यूजन-आधारित प्रूवर को प्रशिक्षित करने के लिए किया जाता है।

3. मॉडल आर्किटेक्चर

यह परिवार दो पीढ़ी-परिवर्तन (generation paradigms) को कवर करता है:

• ऑटोरिग्रेसिव प्रूवर्स (Autoregressive Provers): उपरोक्त पाइपलाइन के साथ प्रशिक्षित 4B और 32B पैरामीटर मॉडल।
• डिफ्यूजन-आधारित प्रूवर: Pythagoras-Prover-Diffusion-4B, लीन के लिए पहला प्रूफ-ऑफ-कांसेप्ट डिफ्यूजन-आधारित प्रमेय प्रूवर है। यह टैक्टिक-आधारित मास्किंग का उपयोग करता है, जहाँ पूरे लीन टैक्टिक्स को व्यक्तिगत टोकन के बजाय इकाइयों के रूप में मास्क और डिनोइज़ (denoise) किया जाता है, जिससे डिनोइजिंग ऑब्जेक्टिव को डिस्क्रीट रीजनिंग स्टेप्स के साथ संरेखित किया जाता है।

4. सुदृढीकरण शिक्षण (Reinforcement Learning - RL)

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

मुख्य योगदान

1. कंप्यूट-कुशल प्रूवर्स: लीन प्रूवर्स का एक परिवार (4B, 32B, और एक 4B डिफ्यूजन मॉडल) जो इस धारणा को चुनौती देता है कि मजबूत औपचारिक तर्क के लिए फ्रंटियर-स्केल मॉडल्स की आवश्यकता होती है।
2. ALF डेटा पाइपलाइन: एक संरचित उत्परिवर्तन योजना जो प्रति-इंस्टेंस लीन सत्यापन के बजाय हल्के सैनिटी चेक का उपयोग करके सत्यापित कॉर्पस को ~2.5$\times$ विस्तारित करती है, जिससे कॉर्पस विस्तार को सत्यापन थ्रूपुट से अलग किया जा सकता है।
3. MiniF2F-ALF बेंचमार्क: MiniF2F-Test सेट पर ALF उत्परिवर्तन लागू करके बनाया गया एक कंटैमिनेशन-सेंसिटिव परटर्बेशन बेंचमार्क। यह मूल्यांकन करने के लिए एक स्ट्रेस टेस्ट के रूप में कार्य करता है कि क्या मॉडल सटीक बेंचमार्क रिकॉल पर निर्भर करते हैं या उनमें हस्तांतरणीय प्रमाण व्यवहार (transferable proof behaviors) हैं।
4. प्रथम डिफ्यूजन थ्योरम प्रूवर: लीन के लिए एक व्यवहार्य डिफ्यूजन-आधारित प्रूवर, जो यह प्रदर्शित करता है कि पुनरावृत्त परिशोधन (iterative refinement) एक व्यवहार्य डिकोडिंग रणनीति है, हालांकि वर्तमान संदर्भ लंबाई की सीमाएँ मौजूद हैं।

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

MiniF2F-Test, PutnamBench, और MiniF2F-ALF पर मूल्यांकन किया गया:

• MiniF2F-Test (Pass@32):
  • Pythagoras-Prover-4B ने 86.1% प्राप्त किया, जो DeepSeek-Prover-V2-671B (82.4%) को पछाड़ते हुए लगभग 167$\times$ छोटा है। यह Goedel-Prover-V2-8B (84.6%) और Kimina-Prover-70B (84.0%) से भी बेहतर है।
  • Pythagoras-Prover-32B ने 89.8% प्राप्त किया, जो बिना स्व-सुधार (self-correction) वाले सभी ओपन-सोर्स प्रूवर्स में अग्रणी है।
• MiniF2F-Test (Pass@2048):
  • Pythagoras-Prover-32B ने 93.03% तक पहुँचकर, बिना स्व-सुधार वाले सभी न्यूरल लीन प्रूवर्स के लिए एक नया स्टेट-ऑफ-द-आर्ट स्थापित किया, जिसने Goedel-Prover-V2-32B (Pass@8192 पर 92.2%) को एक चौथाई सैंपलिंग बजट के साथ पीछे छोड़ दिया।
• PutnamBench:
  • Pythagoras-Prover-32B ने Pass@2048 पर 672 में से 93 समस्याओं को हल किया, जो सबसे मजबूत ओपन-सोर्स परिणाम है, जो Goedel-Prover-V2 (स्व-सुधार के साथ Pass@184 पर 86) से बेहतर है।
• MiniF2F-ALF (Robustness):
  • सभी मूल्यांकित मॉडल्स इस परटर्ब्ड बेंचमार्क पर गिरावट दिखाते हैं, जो पुष्टि करता है कि मूल स्प्लिट पर उच्च सटीकता संरचनात्मक वेरिएंट के प्रति मजबूती की गारंटी नहीं देती है।
  • Pythagoras-Prover-32B सबसे मजबूत (85.0%) बना हुआ है, और Pythagoras-Prover-4B (83.2%) Goedel-Prover-V2-32B (83.6%) के बराबर प्रदर्शन करता है, और कम गिरावट दिखाता है।
• डिफ्यूजन दक्षता (Diffusion Efficiency):
  • Pythagoras-Prover-Diffusion-4B MiniF2F-Test पर 63.25% Pass@32 प्राप्त करता है। अपने ऑटोरिग्रेसिव समकक्ष की तुलना में कम सटीक होने के बावजूद, यह 2.58$\times$ तेज़ (10.56 बनाम 4.10 टोकन/सेकंड) प्रमाण उत्पन्न करता है, जो उच्च थ्रूपुट-प्रति-GPU-सेकंड प्रदान करता है।

महत्व और दावे

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

विशेष रूप रूप से, लेखक रेखांकित करते हैं:

• दक्षता: Pythagoras-Prover-4B एक 671B-पैरामीटर मॉडल से बेहतर प्रदर्शन करता है, जो यह सुझाव देता है कि प्रस्तावित प्रशिक्षण रेसिपी छोटे-मॉडल व्यवस्थाओं में आसानी से स्थानांतरित हो सकती है जहाँ बिलियन-स्केल बेसलाइन्स अव्यावहारिक हैं।
• मजबूती (Robustness): प्रशिक्षण के दौरान ALF उत्परिवर्तन का उपयोग कथन-स्तरीय परटर्बेशन के प्रति मजबूती में सुधार करता है, जैसा कि अन्य बेसलाइन्स की तुलना में MiniF2F-ALF पर कम प्रदर्शन गिरावट से सिद्ध होता है।
• नए प्रतिमान (New Paradigms): एक डिफ्यूजन-आधारित प्रूवर का परिचय एक प्रारंभिक आधार स्थापित करता है, जो पुनरावृत्त परिशोधन (iterative refinement) के लिए एक पूरक दिशा खोलता है, जहाँ प्रूवर्स की तुलना केवल सटीकता से नहीं, बल्कि थ्रूपुट और प्रमाण-प्रति-GPU-सेकंड से की जा सकती है।

लेखक निष्कर्ष निकालते हैं कि "कंप्यूट-फ्रगल" डेटा पाइपलाइन इन परिणामों का प्राथमिक चालक है, जो व्यावहारिक कंप्यूट बजट के तहत अत्याधुनिक प्रदर्शन को सक्षम बनाती है।