🤖 machine learning

VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

यह शोध पत्र VERITAS को प्रस्तुत करता है, जो एक ज़ीरो-शॉट फ्रेमवर्क है जो दो-चरणीय बेस्ट-ऑफ-एन (Best-of-N) और क्रिटिक-गाइडेड एमसीटीएस (critic-guided MCTS) प्रोटोकॉल के माध्यम से समृद्ध वेरीफायर संकेतों को वापस खोज प्रक्रिया में रूट करके औपचारिक प्रमेय सिद्ध करने (formal theorem proving) को बेहतर बनाता है, जिससे miniF2F और एक नए कॉम्बिनेटरिक्स डेटासेट जैसे बेंचमार्क पर अत्याधुनिक प्रदर्शन प्राप्त होता है।

मूल लेखक: Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

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

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

CC BY 4.0

मूल लेखक: Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

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

कल्पना कीजिए कि आप एक बहुत ही कठिन पहेली को हल करने की कोशिश कर रहे हैं, जैसे कि कोई जटिल गणितीय समस्या, लेकिन आप इसे AI सहायकों की एक टीम के साथ मिलकर कर रहे हैं। आमतौर पर, जब ये AI सहायक किसी समस्या को हल करने की कोशिश करते हैं, तो वे एक समाधान का अनुमान लगाते हैं, जाँचते हैं कि क्या वह काम करता है, और यदि वह विफल हो जाता है, तो उन्हें केवल एक साधारण "नहीं, फिर से प्रयास करें" का संकेत मिलता है। वे इस बात के सभी विवरणों को फेंक देते हैं कि वह क्यों विफल हुआ।

VERITAS एक नया सिस्टम है जो खेल बदल देता है। केवल "नहीं" कहने के बजाय, यह उन विशिष्ट कारणों को सुनता है कि प्रमाण क्यों विफल हुआ और उन कारणों का उपयोग अगले अनुमान को निर्देशित करने के लिए करता है। इसे एक जासूस की तरह समझें जो केवल यह नहीं कहता कि "संदेश निर्दोष है," बल्कि यह कहता है, "संदेश निर्दोष है क्योंकि वह शाम 5 बजे दुकान पर था, इसलिए चलिए किसी ऐसे व्यक्ति को ढूँढते हैं जो उस दुकान पर था।"

VERITAS कैसे काम करता है, यहाँ इसके सरल भाग दिए गए हैं:

1. चार विशेषज्ञों की टीम

VERITAS केवल एक AI मस्तिष्क पर निर्भर नहीं है। यह चार विशिष्ट "एजेंटों" का उपयोग करता है जो एक-दूसरे से बात करते हैं:

रणनीतिकार (The Strategist): समस्या को हल करने की कोशिश करने से पहले, यह एजेंट एक उच्च-स्तरीय योजना तय करता है (जैसे, "आइए इसे मामलों में विभाजित करने का प्रयास करें" या "आइए विरोधाभास द्वारा इसे सिद्ध करने का प्रयास करें")। यह खोज को सीमित करता है ताकि टीम बुरे विचारों पर समय बर्बाद न करे।
पुनर्प्राप्तकर्ता (The Retriever): यह एजेंट एक लाइब्रेरियन की तरह है। यह जल्दी से सही संदर्भ पुस्तकें (गणितीय नियम और लेम्मा) खोज लेता है जो वर्तमान चरण को हल करने में मदद कर सकती हैं।
व्यूह रचनाकार (The Tactician): यह मुख्य कार्यकर्ता है। यह प्रमाण के वास्तविक चरणों को लिखने का प्रयास करता है। महत्वपूर्ण रूप से, यह पहले के विफल प्रयासों की एक सूची को देखता है। यदि पिछला प्रयास इसलिए विफल हुआ क्योंकि उसने नियम के लिए गलत नाम का उपयोग किया था, तो टैक्टिशियन को बताया जाता है, "उस नाम का दोबारा उपयोग न करें; यहाँ त्रुटि संदेश है।"
आलोचक (The Critic): यह एजेंट एक कोच की तरह कार्य करता है। यह प्रगति पर नज़र रखता है और गणित की जाँच करने वाले कंप्यूटर के आधार पर कहता है, "आप करीब पहुँच रहे हैं," या "आप गलत रास्ते पर जा रहे हैं।"

2. दो-चरणीय गेम प्लान

यह कुशलता के लिए दो अलग-अलग राउंड में खेल खेलता है:

चरण 1: "त्वरित स्वीप" (Best-of-N)
टीम समाधान के 5 त्वरित, स्वतंत्र अनुमान लगाती है। यदि उनमें से कोई भी काम कर जाता है, तो बहुत अच्छा! वे तुरंत रुक जाते हैं। यह तेज़ है और "आसान" समस्याओं को संभालता है।
चरण 2: "गहन गोता" (Critic-Guided Search)
यदि त्वरित स्वीप विफल रहता है, तो सिस्टम अधिक सावधानीपूर्वक मोड में स्विच करता है। यह चरण 1 से सभी गलतियों को लेता है और उन्हें टैक्टिशियन में "नकारात्मक उदाहरणों" के रूप में वापस फीड करता है।
- उपमा: कल्पना कीजिए कि आप एक बंद दरवाजे को खोलने की कोशिश कर रहे हैं। चरण 1 में, आप जल्दी से 5 अलग-अलग चाबियाँ आज़माते हैं। कोई भी काम नहीं करती। चरण 2 में, केवल यादृच्छिक चाबियाँ आज़माने के बजाय, आप उन 5 चाबियों को देखते हैं जो ताले में फंस गईं, नोट करते हैं कि वे ठीक कैसे फंसीं, और उस जानकारी का उपयोग करके एक नई चाबी बनाते हैं जो ताले के विशिष्ट आकार में फिट बैठती है।

3. यह क्यों मायने रखता है: "कॉम्बिनेटोरिक्स" (Combinatorics) की समस्या

पेपर ने इन दो प्रकार की गणितीय समस्याओं पर इसका परीक्षण किया।

मानक गणितीय समस्याएं: VERITAS ने पिछले तरीकों की तुलना में अधिक मानक समस्याएं हल कीं (40.6% बनाम 36.9%)।
कॉम्बिनेटोरिक्स (गिनती वाली समस्याएं): यहाँ VERITAS वास्तव में चमक उठा। इन समस्याओं में, आपको अक्सर गणित के नियमों के बहुत विशिष्ट, सटीक नामों का उपयोग करने की आवश्यकता होती है।
- समस्या: मानक AI अनुमान अक्सर उन नियमों के नाम "भ्रमित" (hallucinate) करते हैं जो अस्तित्व में नहीं हैं। यदि कोई AI नकली नियम का नाम अनुमान लगाता है, तो एक मानक सिस्टम केवल "विफल" कहता है और आगे बढ़ जाता है।
- VERITAS का समाधान: क्योंकि VERITAS विशिष्ट त्रुटि संदेश ("Unknown constant 'X'") पढ़ता है, यह वास्तविक समय में सीख जाता है कि "X" मौजूद नहीं है। यह वास्तविक नाम खोजने तक इसे बार-बार सुधारता है।
- परिणाम: इन कठिन गिनती वाली समस्याओं पर, मानक अनुमान वास्तव में जितना अधिक प्रयास करता है, उतना ही खराब होता जाता है (क्योंकि यह बार-बार नकली नाम बनाता रहता है)। VERITAS बेहतर होता गया क्योंकि इसने अपनी गलतियों से सीखा।

4. "मोनोटोनिसिटी" (Monotonicity) की गारंटी

लेखकों ने यह सुनिश्चित किया कि VERITAS पहले से पाया गया समाधान कभी न खोए।

गारंटी: यदि "त्वरित स्वीप" (चरण 1) किसी समस्या को हल कर देता है, तो VERITAS उस समाधान को रखता है और उसे नहीं छेड़ता। "गहन गोता" (चरण 2) केवल उन समस्याओं पर काम करता है जिन्हें पहला चरण हल नहीं कर सका।
महत्व: यह साबित करता है कि VERITAS द्वारा प्राप्त की गई कोई भी अतिरिक्त सफलता विशेष रूप से स्मार्ट, फीडबैक-संचालित खोज से आती है, न कि केवल अधिक यादृच्छिक अनुमान लगाने से।

5. "बैच" (Batch) ट्रिक

पेपर में एक चतुर इंजीनियरिंग ट्रिक यह है कि वे उत्तरों की जाँच कैसे करते हैं।

पुराना तरीका: एक अनुमान की जाँच करें, कंप्यूटर के "नहीं" कहने का इंतज़ार करें, अगली जाँच करें, इंतज़ार करें, अगली जाँच करें... यह धीमा है।
VERITAS का तरीका: वे 6 अनुमानों को एक ही फ़ाइल में पैक करते हैं और कंप्यूटर से उन सभी को एक साथ जाँचने के लिए कहते हैं। यह सिस्टम को 10 से 20 गुना तेज़ बनाता है, जिससे बहुत समय और पैसा बचता है।

सारांश

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

तकनीकी सारांश: VERITAS: ज़ीरो-शॉट औपचारिक प्रमेय प्रमाणन के लिए वेरीफायर-निर्देशित प्रमाण खोज (Verifier-Guided Proof Search)

समस्या विवरण

वर्तमान LLM-आधारित औपचारिक प्रमेय प्रुवर (formal theorem provers) आमतौर पर औपचारिक वेरीफायर (जैसे Lean 4) से प्राप्त समृद्ध, संरचित संकेतों को एक बाइनरी पास/फेल परिणाम में संकुचित कर देते हैं। वेरीफायर सिंटैक्स त्रुटियों, टाइप मिसमैच, आंशिक लक्ष्य प्रगति और प्रमाण पूर्णता स्थिति सहित विस्तृत फीडबैक प्रदान करता है। हालाँकि, मानक पाइपलाइन इन मध्यवर्ती आर्टिफैक्ट्स को छोड़ देती है, उन्हें स्केलर रिवॉर्ड्स में सारांशित कर देती है या पूरी तरह से त्याग देती है। यह खोज एल्गोरिदम को उस जानकारी को "पुनः सीखने" के लिए मजबूर करता है जो वेरीफायर पहले से ही स्पष्ट रूप से प्रदान कर चुका है, जो कि उन प्रमाणों के लिए विशेष रूप से महंगा हो जाता है जिनमें निर्भर टैक्टिक्स (dependent tactics) की श्रृंखलाओं की आवश्यकता होती है जहाँ प्रत्येक चरण की शुद्धता पिछले चरण के प्रभाव पर टिकी होती है।

कार्यप्रणाली: VERITAS फ्रेमवर्क

VERITAS एक ज़ीरो-शॉट फ्रेमवर्क है जिसे हर वेरीफायर सिग्नल को प्रमाण जनरेशन प्रक्रिया में वापस रूट करने के लिए डिज़ाइन किया गया है। यह एक साझा 'प्रूफ स्टेट' और एक दो-चरणीय खोज प्रोटोकॉल द्वारा समन्वित चार-एजेंट आर्किटेक्चर का उपयोग करता है।

1. चार विशिष्ट एजेंट

सभी एजेंट एक साझा ProofState पर कार्य करते हैं जिसमें प्रमेय, वर्तमान लक्ष्य, परिकल्पनाएँ (hypotheses), टैक्टिक इतिहास और Lean से चार संरचित संकेत शामिल हैं:

स्ट्रैटेजिस्ट (Strategist): प्रूफ स्टेट को छह उच्च-स्तरीय रणनीतियों (direct, induction, contradiction, cases, rewrite, apply_lemma) में से एक में मैप करता है और गहराई (depth) का अनुमान लगाता है, जिससे खोज को एक प्रासंगिक सबस्पेस तक सीमित किया जा सके।
रिट्रीवर (Retriever): लक्ष्य टोकन, लेम्मा नाम और सिग्नेचर के विरुद्ध कीवर्ड ओवरलैप को स्कोर करके प्रासंगिक Mathlib प्रिमिसिस (premises) को सामने लाता है।
क्रिटिक (Critic): एक हल्का मॉडल जो आंशिक प्रूफ स्टेट्स को स्कोर करता है, अगले टैक्टिक्स का सुझाव देता है और छंटनी (pruning) की सिफारिश करता है। यह MCTS में रैंडम रोलआउट्स के स्थान पर एक वैल्यू एस्टीमेट का उपयोग करता है जो Lean के चार-तरफा फीडबैक को एकीकृत करता है।
टैक्टिशियन (Tactician): रणनीति, रिट्रीव किए गए प्रिमिसिस, क्रिटिक मार्गदर्शन और विशेष रूप से, पिछले विफल टैक्टिक्स की एक सूची (जिनमें उनके विशिष्ट Lean एरर मैसेज नेगेटिव उदाहरण के रूप में इंजेक्ट किए गए हैं) की स्थिति में $K$ टैक्टिक कैंडिडेट जेनरेट करता है।

2. मॉनोटोनिसिटी गारंटी के साथ दो-चरणीय प्रोटोकॉल

फ्रेमवर्क एक रूढ़िवादी दो-चरणीय प्रोटोकॉल का उपयोग करता है ताकि यह सुनिश्चित किया जा सके कि लाभ फीडबैक-संचालित खोज के कारण ही हैं:

चरण 1 (Best-of-N): एक मानक Best-of-N स्वीप (जैसे, $N=5$ ) एक सिंगल बैच में टैक्टिक्स जेनरेट करता है। यदि कोई भी सफल होता है, तो प्रमेय तुरंत हल हो जाता है।
चरण 2 (Critic-Guided MCTS): केवल तभी सक्रिय होता है जब चरण 1 विफल हो जाता है। चरण 1 के विफलताओं के सेट (टैक्टिक्स और उनके एरर्स) को टैक्टिशियन के सिस्टम प्रॉम्प्ट में नेगेटिव उदाहरण के रूप में इंजेक्ट किया जाता है। क्रिटिक एक मोंटे कार्लो ट्री सर्च (MCTS) को निर्देशित करता है जहाँ:
- सिलेक्शन (Selection): क्रिटिक के वैल्यू और स्ट्रैटेजी अलाइनमेंट को शामिल करने वाला एक विस्तारित UCB फॉर्मूला उपयोग करता है।
- एक्सपेंशन (Expansion): एजेंट क्रमवार चलते हैं; उम्मीदवारों को बैच्ड लीन वैलिडेशन (Batched Lean Validation) ट्रिक के माध्यम से मान्य किया जाता है।
- सिमुलेशन (Simulation): रैंडम रोलआउट्स के स्थान पर क्रिटिक के वैल्यू का उपयोग करता है जो संरचित संकेतों ( $\sigma_A$ सिंटैक्स, $\sigma_B$ टाइप, $\sigma_C$ प्रोग्रेस, $\sigma_D$ कम्पलीशन) द्वारा संवर्धित है।
- बैकप्रोपैगेशन (Backpropagation): बाइनरी विन/लॉस के बजाय संरचित संकेतों को ऊपर की ओर ले जाता है, जिससे आंशिक प्रगति के लिए क्रेडिट सुरक्षित रहता है।

बैच्ड लीन वैलिडेशन: प्रत्येक एक्सपेंशन के लिए $K$ बार Lean को कॉल करने के बजाय, उम्मीदवारों को एक सिंगल .lean फाइल में प्राइवेट थीोरम्स के रूप में संकलित किया जाता है और एक ही कॉल में मान्य किया जाता है। यह सत्यापन लागत को $O(K)$ से घटाकर $O(1)$ कर देता है, जिससे $\sim10\times$ की गति वृद्धि होती है।

मॉनोटोनिसिटी (Monotonicity): यह प्रोटोकॉल गारंटी देता है कि अंतिम हल किए गए प्रमेयों का सेट चरण 1 द्वारा हल किए गए प्रमेयों का सुपरसेट है ( $S \supseteq S_1$ )। यह फीडबैक-संचालित खोज के योगदान को अलग करता है, यह सुनिश्चित करता है कि कोई भी अतिरिक्त समाधान सख्ती से चरण 2 के कारण है।

मुख्य योगदान

ज़ीरो-शॉट फोर-एजेंट फ्रेमवर्क: एक ऐसा सिस्टम जो बिना किसी ट्रेस फाइन-ट्यूनिंग के, संरचित Lean फीडबैक (सिंटैक्स, टाइप, प्रोग्रेस, कम्पलीशन) को हर जनरेशन निर्णय में रूट करता है।
दो-चरणीय प्रोटोकॉल: एक Best-of-N $\to$ Critic-MCTS डिज़ाइन जिसमें एक आंतरिक मॉनोटोनिसिटी गारंटी है जो फीडबैक-संचालित खोज के योगदान का स्पष्ट श्रेय (attribution) देती है।
दक्षता अनुकूलन (Efficiency Optimization): एक बैच्ड लीन वैलिडेशन ट्रिक जो सत्यापन ओवरहेड को लगभग $10\times$ कम कर देती है।
VERITAS-CombiBench: Lean 4 में 55 लेखक-सत्यापित, कठिन कॉम्बिनेटरिक्स प्रमेयों का एक नया बेंचमार्क, जिसे अनगाइडेड सैंपलिंग की सीमाओं को उजागर करने के लिए जारी किया गया है।
एट्रीब्यूशन एनालिसिस: इस बात का अनुभवजन्य प्रमाण कि 11 miniF2F प्रमेय विशेष रूप से MCTS चरण द्वारा हल किए जाible थे, जिन्हें फ्लैट सैंपलिंग नहीं छू सका था।

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

प्रयोग miniF2F (244 प्रमेय) और VERITAS-CombiBench (55 प्रमेय) पर किए गए।

miniF2F प्रदर्शन: VERITAS ने 40.6% सॉल्व रेट (99/244) प्राप्त किया, जो स्वतंत्र Best-of-5 बेसलाइन (36.9%) और एक हैंडक्राफ्टेड पोर्टफोलियो (26.2%) से बेहतर है।
- चरण 2 ने 11 अद्वितीय समाधानों में योगदान दिया जिन्हें फ्लैट सैंपलिंग प्राप्त नहीं कर सका, मुख्य रूप से उन समस्याओं पर जिनमें 2-4 निर्भर टैक्टिक्स की आवश्यकता थी।
- "हार्ड" नॉन-सोरी (non-sorry) समस्याओं पर, VERITAS ने 28.9% प्राप्त किया, जबकि Best-of-5 ने 25.9% प्राप्त किया।
VERITAS-CombiBench प्रदर्शन: इस बेंचमार्क ने अनगाइडेड सैंपलिंग की विफलता को उजागर किया। Best-of-5 ने केवल 1.8% प्राप्त किया, जो पोर्टफोलियो (3.6%) से भी कम था क्योंकि LLMs ने गलत Mathlib लेम्मा नामों का भ्रम (hallucination) पैदा किया। VERITAS ने लीन के एरर फीडबैक का उपयोग करके इन नामों को पुनरावृत्ति (iteratively) से सुधार कर 7.3% तक पहुँच बनाया।
दक्षता: VERITAS इन्फरेंस-ओनली विधियों के लिए पारेटो फ्रंटियर (Pareto frontier) पर हावी है, जो प्रति प्रमेय $\sim27$ लीन कॉल्स के साथ 40.6% सॉल्व रेट प्राप्त करता है, जिसकी API लागत $\sim\$ 150$ प्रति स्वीप है।
विफलता मोड (Failure Modes): विश्लेषण से पता चला कि 32% विफलताएं सिंटैक्स-स्तर (गलत नाम) की थीं, 17% टाइप-करेक्ट लेकिन गलत थीं, और 10% "नियर-मिस" (आंशिक लक्ष्य प्रगति) थे जहाँ क्रिटिक उच्च-मूल्य वाला मार्गदर्शन प्रदान कर सकता था।

महत्व और दावे

यह पेपर एक सामान्य डिज़ाइन सिद्धांत प्रतिपादित करता है: जब एक नियतात्मक वेरीफायर (deterministic verifier) संरचित मध्यवर्ती संकेत उत्सर्जित करता है, तो उन्हें जनरेशन में वापस डालने से LLM की क्षमता अतिरिक्त सैंपलिंग करने की तुलना में बहुत अधिक बढ़ जाती है।

VERITAS सिद्ध करता है कि:

वेरीफायर सिग्नल्स एक स्टेट के रूप में: नियतात्मक वेरीफायर संकेत केवल अंतिम जाँच नहीं, बल्कि इन्फरेंस-टाइम स्टेट के रूप में भी काम कर सकते हैं।
घटकों की सिनर्जी: जनरेशन या सर्च कंपोनेंट को अलग-अलग स्केल करने की तुलना में वेरीफायर को मजबूती से जोड़ना अधिक प्रभावी है।
पुनरावृत्ति सुधार (Iterative Correction): सटीक लेम्मा रिट्रीवल वाले डोमेन (जैसे कॉम्बिनेटरिक्स) के लिए, लीन एरर फीडबैक से होने वाला पुनरावृत्ति सुधार फ्लैट सैंपलिंग से बेहतर है, जो अक्सर लेक्सिकल रूप से गलत नामों का भ्रम पैदा करता है।

लेखकों का निष्कर्ष है कि हालांकि VERITAS, IMO-स्तर की रचनात्मकता या इंटरैक्टिव लेटेंसी का इलाज नहीं है, इसका प्राथमिक योगदान रूटिंग (routing) है: चरण 1 में आसान प्रमाणों को कुशलतापूर्वक एकत्र करना और चरण 2 में केवल वहीं कंप्यूटेशनल बजट खर्च करना जहाँ वेरीफायर की विफलताएं अगले टैक्टिक के लिए मार्गदर्शन कर सकें। भविष्य के कार्य के रूप में रिट्रीवल में सुधार, सस्ते क्रिटिक्स बनाना और शेष कठिन समस्याओं तक इस सिद्धांत को स्केल करने के लिए चरण 2 ट्रेसेस को डिस्टिल करना पहचाना गया है।