💬 NLP

OProver: A Unified Framework for Agentic Formal Theorem Proving

OProver, Lean 4 में एजेंटिक औपचारिक प्रमेय प्रमाण (agentic formal theorem proving) के लिए एक एकीकृत ढांचा है जो इटरेटिव प्रूफ रिवीज़न को कंपाइलर फीडबैक और रिट्रीवल के साथ एकीकृत करता है, जो निरंतर प्रीट्रेनिंग, रिपेयर ट्रेजेक्टरीज पर सुपरवाइज्ड फाइन-ट्यूनिंग और कठिन मामलों पर रीइन्फोर्समेंट लर्निंग को संयोजित करने वाले एक नवीन प्रशिक्षण पाइपलाइन के माध्यम से कई बेंचमार्क में अत्याधुनिक प्रदर्शन प्राप्त करता है।

मूल लेखक: David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, Zili Wang

प्रकाशित 2026-05-19

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

CC BY 4.0

मूल लेखक: David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, Zili Wang

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

कल्पना कीजिए कि आप एक बहुत ही कठिन गणितीय पहेली को हल करने की कोशिश कर रहे हैं, लेकिन आपको उसका समाधान Lean 4 नामक एक सख्त, रोबोटिक भाषा में लिखना होगा। यदि आप एक भी छोटी सी टाइपिंग की गलती या तार्किक त्रुटि करते हैं, तो कंप्यूटर (जिसे "कंपाइलर" कहा जाता है) उसे खारिज कर देगा और कहेगा, "नहीं, गलत।"

लंबे समय तक, इन पहेलियों को हल करने वाले AI मॉडल एक छात्र की तरह काम करते थे जो परीक्षा दे रहा हो: वे एक उत्तर का अनुमान लगाते थे, और यदि वह गलत होता, तो वे शून्य से फिर से नया अनुमान लगाते थे। वे वास्तव में यह नहीं समझते थे कि वे क्यों गलत थे, और उन्होंने गलतियों को सुधारने के लिए कंप्यूटर के विशिष्ट फीडबैक का उपयोग नहीं किया।

OProver एक नया सिस्टम है जो खेल बदल देता है। केवल अनुमान लगाने के बजाय, यह एक परफेक्शनिस्ट जासूस (perfectionist detective) की तरह काम करता है जो कभी हार नहीं मानता। यह कैसे काम करता है, इसके लिए सरल उपमाओं का उपयोग किया गया है:

1. "एजेंटिक" जासूस (The Prover)

OProver को केवल एक स्थिर पाठ्यपुस्तक के रूप में नहीं, बल्कि एक ऐसे जासूस के रूप में सोचें जिसके पास एक बहु-चरणीय जांच प्रक्रिया (multi-step investigation process) है।

पुराना तरीका: जासूस एक सिद्धांत लिखता है, जज (कंप्यूटर) कहता है "गलत," और जासूस शुरू से एक पूरी तरह से नया सिद्धांत लिखता है।
OProves का तरीका: जासूस एक सिद्धांत लिखता है। जज कहता है, "आपने यहाँ एक गलती की है: आपने संख्या के गलत प्रकार का उपयोग किया है।" जासूस फिर उस सिद्धांत के उस विशिष्ट भाग को संशोधित (edit) करता है, उसे फिर से जाँचता है, और उसे तब तक परिष्कृत करता रहता है जब तक कि जज यह न कह दे, "सही!"

OProver इस "संशोधित और परिष्कृत" (edit and refine) नृत्य को स्वचालित रूप से करने के लिए प्रशिक्षित है। यह केवल अनुमान नहीं लगाता; यह जज की विशिष्ट शिकायतों को सुनने और उन्हें ठीक करने के लिए प्रशिक्षित होता है।

2. "समाधानों का पुस्तकालय" (Retrieval)

जासूस लिखने से पहले, वे शून्य में काम नहीं करते हैं। वे एक विशाल पुस्तकालय (जिसे रिट्रीवल मेमोरी कहा जाता है) में जाते हैं।

यदि जासूस त्रिभुजों (triangles) के बारे में एक पहेली हल करने की कोशिश कर रहा है, तो पुस्तकालय तुरंत उन शीर्ष 5 सर्वश्रेष्ठ प्रमाणों (proofs) को निकाल लेता है जो अन्य जासूसों ने सफलतापूर्वक हल किए थे।
OProver इन "चीट शीट्स" को पढ़ता है ताकि देख सके कि अन्य लोगों ने समान समस्याओं को कैसे हल किया, और उनके रणनीतियों का उपयोग एक मार्गदर्शक के रूप में करता है। यह जासूस को सामान्य जाल से बचने में मदद करता है।

3. "स्व-सुधार चक्र" (The Training)

यह सबसे जादुई हिस्सा है। आमतौर पर, AI मॉडल को डेटा के एक निश्चित सेट पर प्रशिक्षित किया जाता है और फिर अकेला छोड़ दिया जाता है। OProver अलग है; इसमें एक स्व-सुधार चक्र (self-improving cycle) है।

चरण 1: OProver कई पहेलियों को हल करने की कोशिश करता है।
चरण 2: जब वह सफल होता है, तो वह उस समाधान को पुस्तकालय में सहेज लेता है ताकि भविष्य की समस्याओं के लिए उसका उपयोग "चीट शीट" के रूप में किया जा सके।
चरण 3: जब वह विफल होता है, तो वह विफलता की पूरी कहानी सहेजता है—कि कैसे वह विफल हुआ, कंप्यूटर ने क्या कहा, और उसने अंततः इसे कैसे ठीक किया।
चरण 4: सिस्टम इन "विफलता की कहानियों" का उपयोग खुद को बेहतर बनाने के लिए सीखने के रूप में करता है।

यह एक ऐसे छात्र की तरह है जो, हर परीक्षा के बाद, न केवल सही उत्तर याद रखता है, बल्कि यह भी लिखता है कि वे प्रश्न गलत क्यों हुए और उन नोट्स को अपने अध्ययन गाइड में जोड़ देता है। समय के साथ, छात्र स्मार्ट होता जाता है, और अध्ययन गाइड अधिक घनी और अधिक सहायक होती जाती है।

4. परिणाम: एक सुपर-स्टूडेंट

इस सिस्टम का परीक्षण पांच अलग-अलग "मैथ ओलंपियाड" (हाई स्कूल स्तर से लेकर बहुत कठिन विश्वविद्यालय प्रतियोगिताओं तक) पर किया गया।

उपलब्धि: OProver (विशेष रूप से 32-बिलियन-पैरामीटर वाला संस्करण) सभी ओपन-सोर्स AI प्रोवर्स में शीर्ष प्रदर्शन करने वाला बन गया। इसने किसी भी अन्य समान सिस्टम की तुलना में अधिक समस्याओं को सही ढंग से हल किया, यहाँ तक कि बहुत बड़े मॉडलों को भी पीछे छोड़ दिया।
यह क्यों मायने रखता है: इसने सिद्ध किया कि AI को फीडबैक सुनने, पिछले समाधानों को देखने और अपने काम को बार-बार सुधारने की क्षमता देना, केवल उसे अनुमान लगाने में बड़ा या स्मार्ट बनाने से कहीं अधिक शक्तिशाली है।

सारांश में

OProver एक गणित हल करने वाला AI है जो केवल "अनुमान और जाँच" (guess and check) नहीं करता है। यह एक सहयोगात्मक शिक्षार्थी (collaborative learner) है जो:

पहले समान हल की गई समस्याओं को ढूँढता है।
एक प्रमाण लिखता है।
कंप्यूटर के विशिष्ट त्रुटि संदेशों को सुनता है।
उन त्रुटियों को ठीक करने के लिए अपने काम को संशोधित करता है।
तब तक दोहराता है जब तक कि वह सफल न हो जाए, फिर अगले समय के लिए सबक सहेज लेता है।

विफलता को सीखने के अवसर में बदलकर और यह रिकॉर्ड रखकर कि क्या काम करता है, OProver आज औपचारिक रूप से गणितीय प्रमेयों (mathematical theorems) को सिद्ध करने वाला सबसे अच्छा ओपन-सोर्स AI बन गया है।

तकनीकी सारांश: OProver: एजेंटिक औपचारिक प्रमेय सिद्ध करने के लिए एक एकीकृत ढांचा (A Unified Framework for Agentic Formal Theorem Proving)

समस्या विवरण

औपचारिक प्रमेय सिद्ध करने (formal theorem proving) के क्षेत्र में हालिया प्रगति, विशेष रूप से Lean 4 इकोसिस्टम के भीतर, MiniF2F और PutnamBench जैसे बेंचमार्क पर प्रदर्शन में सुधार करने के लिए बड़े पैमाने पर प्रमाण निर्माण (proof generation) और सत्यापनकर्ता-जागरूक प्रशिक्षण (verifier-aware training) का लाभ उठाती है। हालाँकि, एक महत्वपूर्ण सीमा बनी हुई है: एजेंटिक सिद्ध करने की क्षमताएं (रिट्रीवल, कंपाइलर फीडबैक, और पुनरावृत्ति सुधार/iterative repair) आमतौर पर एक निश्चित प्रवर (prover) पर लागू किए गए इन्फरेंस-टाइम ह्यूरिस्टिक्स (inference-time heuristics) के रूप में मानी जाती हैं, न कि प्रशिक्षण प्रक्रिया में एकीकृत सीखे गए नीतियों (learned policies) के रूप में।

यह एक प्रशिक्षण-अनुमान विसंगति (train-inference mismatch) पैदा करता है। वे मॉडल जो मुख्य रूप से अंतिम, सफल प्रमाणों पर प्रशिक्षित होते हैं, उन्हें परिनियोजन (deployment) के दौरान उन वितरणों (distributions) में कंपाइलर फीडबैक और रिट्रीव किया गया संदर्भ मिलता है, जिनके लिए वे अनुकूलित नहीं किए गए थे। इसके अलावा, मौजूदा औपचारिक कॉर्पोरा (corpora) केवल अंतिम उत्पादों (कथन और सत्यापित प्रमाण) पर ध्यान केंद्रित करते हैं, और बहु-चरण इंटरैक्शन इतिहास (multi-round interaction histories)—विफल प्रयास, रिट्रीव किया गया संदर्भ, और कंपाइलर डायग्नोस्टिक्स—को छोड़ देते हैं, जो प्रमाणों की मरम्मत करने के सीखने के लिए आवश्यक हैं। फलस्वरूप, व्यावहारिक रूप से प्रमाण सुधार (proof repair) को चलाने वाले पर्यवेक्षण संकेत (supervision signal) का उपयोग प्रशिक्षण में काफी हद तक अनैतिक रहता है।

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

यह शोध पत्र OProver प्रस्तुत करता है, जो एक एकीकृत ढांचा है जो रिट्रीवल, कंपाइलर फीडबैक, और पुनरावृत्ति सुधार (iterative repair) को एक सह-विकासवादी प्रशिक्षण पाइपलाइन (co-evolutionary training pipeline) के माध्यम से सीधे प्रवर की नीति (policy) में एकीकृत करता है।

1. OProver ढांचा

OProver प्रमेय सिद्ध करने को एक सीमित, बहु-चरण परिशोधन लूप (bounded, multi-round refinement loop) के रूप में मानता है। प्रत्येक दौर $t$ में, नीति $\pi$ एक संक्षिप्त अवस्था $X_t = (s, R_t, p_{t-1}, f_{t-1})$ पर आधारित होती है, जहाँ:

$s$ : लक्षित प्रमेय कथन (target theorem statement)।
$R_t$ : मेमोरी $M$ से शीर्ष- $k$ रिट्रीव किए गए कंपाइलर-सत्यापित प्रमाण।
$p_{t-1}$ : पिछला प्रमाण प्रयास।
$f_{t-1}$ : Lean 4 सत्यापनकर्ता (verifier) से प्राप्त कच्चा टेक्स्टुअल कंपाइलर फीडबैक (डायग्नोस्टिक्स)।

नीति एक संशोधित प्रयास $p_t$ उत्पन्न करती है। यदि सत्यापन विफल हो जाता है, तो कच्चा फीडबैक अगले दौर के लिए नीति को वापस भेज दिया जाता है। महत्वपूर्ण रूप से, नीति केवल सबसे हालिया प्रयास और फीडबैक पर आधारित होती है, जिससे स्थानीय सुधार संकेतों को सुरक्षित रखते हुए अवस्था को संक्षिप्त रखा जा सके।

2. OProofs: एक एकीकृत प्रशिक्षण कॉर्पस

इस ढांचे को समर्थन देने के लिए, लेखक OProofs का निर्माण करते हैं, जो विशेष रूप से एजेंटिक सिद्ध करने के लिए डिज़ाइन किया गया एक बड़े पैमाने का कॉर्पस है। पूर्ववर्ती डेटासेट्स के विपरीत, जो केवल अंतिम प्रमाणों को सुरक्षित रखते हैं, OProofs शामिल किए गए विस्तृत पथों (trajectories) को रिकॉर्ड करता है:

रिट्रीव किया गया संदर्भ।
विफल प्रयास।
कच्चा कंपाइलर फीडबैक।
आगामी सुधार (subsequent repairs)।

OProofs तीन स्रोतों से बनाया गया है: सार्वजनिक Lean संसाधन, बड़े पैमाने पर प्रमाण संश्लेषण (ऑटोफॉर्मलाइजेशन + सत्यापन), और OProver के अपने एजेंटिक सिद्ध करने के ट्रेस। इसमें 1.77M अद्वितीय Lean कथन और 6.86M कंपाइलर-सत्यापित प्रमाण, साथ ही 1.07M एजेंटिक ट्रेजेक्टरीज शामिल हैं।

3. सह-विकासवादी प्रशिक्षण पाइपलाइन (Co-Evolutionary Training Pipeline)

प्रशिक्षण प्रक्रिया एक पुनरावृत्ति लूप (एल्गोरिदम 1) का अनुसरण करती है जहाँ प्रवर और कॉर्पस सह-विकसित होते हैं:

निरंतर प्री-ट्रेनिंग (CPT): एक बेस मॉडल को Lean कोड, गणित, और लॉन्ग-कॉन्टेक्स्ट रीजनिंग डेटा के मिश्रण पर प्रशिक्षित किया जाता है ताकि OProver-Base बनाया जा सके।
पुनरावृत्ति पोस्ट-ट्रेनिंग:
- एजेंटिक रोलआउट्स (Agentic Rollouts): वर्तमान नीति एक प्रमेय पूल पर बहु-चरण सिद्धिंग करती है, वर्तमान मेमोरी $M_k$ से रिट्रीव करती है और Lean कंपाइलर के साथ सत्यापित करती है।
- डेटा संग्रह: नए सत्यापित प्रमाणों को कॉर्पस में जोड़ा जाता है और रिट्रीवल मेमोरी में इंडेक्स किया जाता है। विफल प्रयासों और सफल सुधारों को दौर-स्तर के उदाहरणों $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$ में विभाजित किया जाता है।
- **सुपरवाइज्ड फाइन-ट्यूनिंग (SFT): एकत्र किए गए सुधार उदाहरणों का उपयोग करके मॉडल को अपडेट किया जाता है।
- रीइन्फोर्समेंट लर्निंग (RL): कठिन अनसुलझे मामलों के लिए ग्रुप सीक्वेंस पॉलिसी ऑप्टिमाइज़ेशन (GSPO) लागू किया जाता है, जिसमें सत्यापन सफलता और फॉर्मेट शुद्धता पर आधारित रिवॉर्ड सिग्नल का उपयोग किया जाता है।
- पुनरावृत्ति (Recirculation): अपडेट किया गया कॉर्पस और मेमोरी अगले इटरेशन में फीड होती है, जिससे नीति अपने स्वयं के बेहतर प्रमाणों से सीख सकती है।

मुख्य योगदान

एजेंटिक सिद्धिंग के लिए एकीकृत ढांचा: OProver रिट्रीवल, फीडबैक, और पुनरावृत्ति सुधार को एक एकल सीखी गई नीति में एकीकृत करता है, जो प्रशिक्षण-अनुमान विसंगति को समाप्त करता है। यह मॉडल को इन संकेतों को एक बाहरी ह्यूरिस्टिक के बजाय अपनी मूल रणनीति के हिस्से के रूप में उपयोग करने के लिए प्रशिक्षित करता है।
OProofs कॉर्पस: एक बड़े पैमाने का कॉर्पस (1.77M कथन, 6.86M प्रमाण) का निर्माण जो विफल प्रयासों और कच्चे कंपाइलर फीडबैक सहित बहु-टर्न इंटरैक्शन इतिहास को स्पष्ट रूप से सुरक्षित रखता है, जिससे वह पर्यवेक्षण उपलब्ध हुआ जो पहले औपचारिक डेटासेट्स में अनुपलब्ध था।
सह-विकास पाइपलाइन: एक प्रशिक्षण पद्धति जहाँ प्रवर नया डेटा (सत्यापित प्रमाण और सुधार ट्रेजेक्टरीज) उत्पन्न करता है जिसे तुरंत प्रशिक्षण कॉर्पस और रिट्रीवल मेमोरी में समाहित किया जाता है, जिससे एक स्व-सुधार लूप बनता है।
स्टेट-ऑफ-द-आर्ट प्रदर्शन: OProver ओपन-वेट होल-प्रूफ प्रवर्स में शीर्ष-स्तरीय परिणाम प्राप्त करता है, यह प्रदर्शित करते हुए कि एजेंटिक रिफाइनमेंट रणनीतियाँ काफी बड़े मॉडलों से बेहतर प्रदर्शन कर सकती हैं।

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

OProver का मूल्यांकन पांच Lean 4 बेंचमार्क पर किया गया: MiniF2F, MathOlympiadBench, ProofNet, ProverBench, और PutnamBench।

प्रदर्शन: OProver-32B मॉडल ने तीन बेंचमार्क (MiniF2F: 93.3%, ProverBench: 58.2%, PutnamBench: 11.3%) पर सर्वश्रेष्ठ Pass@32 स्कोर प्राप्त किया और अन्य दो पर दूसरा सर्वश्रेष्ठ स्थान (MathOlympiad: 22.8%, ProofNet: 33.2%) प्राप्त किया।
दक्षता: OProver-32B (32B पैरामीटर्स) ने अधिकांश बेंचमार्क पर 671B DeepSeek-Prover-V2 और 560B LongCat-Flash-Prover (TIR के साथ) को पछाड़ दिया, जबकि इसके पैरामीटर्स काफी कम थे। यहाँ तक कि इसका 8B वेरिएंट भी सभी बेंचमार्क में 32B Goedel-Prover-V2 से बेहतर रहा।
टेस्ट-टाइम स्केलिंग: कंप्यूट बजट (अधिक सैंपल या रिफाइनमेंट राउंड) के बढ़ने के साथ प्रदर्शन लगातार सुधरता गया, हालांकि इसमें घटते प्रतिफल (diminishing returns) देखे गए। रिफाइनमेंट डेप्थ और सैंपलिंग विड्थ के बीच इष्टतम आवंटन बेंचमार्क की कठिनाई के अनुसार भिन्न था।
एब्लेशन स्टडीज (Ablation Studies): मल्टी-टर्न कंपाइलर फीडबैक को हटाने से सबसे महत्वपूर्ण प्रदर्शन गिरावट आई, जो पुष्टि करती है कि पुनरावृत्ति परिशोधन (iterative refinement) लाभों का प्राथमिक चालक है। रिट्रीवल ऑग्मेंटेशन को हटाने से भी निरंतर, हालांकि छोटे, ड्रॉप देखे गए, जो रिट्रीवल ग्राउंडिंग के पूरक मूल्य को उजागर करते हैं।

महत्व और दावे

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

लेखक इस बात पर जोर देते हैं कि प्रदर्शन में वृद्धि केवल मॉडल स्केल का परिणाम नहीं है, बल्कि रिट्रीवल-ऑगमेंटेड ग्राउंडिंग और कंपाइलर-गाइडेड इटरेटिव रिफाइनमेंट के बीच तालमेल से उपजी है। OProver नीति और OProofs कॉर्पस का सह-विकास सिस्टम को अपने स्वयं के सफल और असफल प्रयासों से सीखकर अपनी सिद्ध करने की क्षमताओं में निरंतर सुधार करने की अनुमति देता है, जो औपचारिक तर्क प्रणालियों (formal reasoning systems) के प्रशिक्षण के लिए एक नया प्रतिमान स्थापित करता है।