Benchmarking Testing in Automated Theorem Proving

यहाँ जोंगयून किम, होजे हान और सोंग-वोन ह्वांग के शोध पत्र "Benchmarking Testing in Automated Theorem Proving" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

लार्ज लैंग्वेज मॉडल्स (LLMs) की तीव्र प्रगति ने लीन (Lean) जैसे सिस्टम में औपचारिक प्रमाण (formal proofs) उत्पन्न करने की उनकी क्षमता में सुधार किया है। हालाँकि, वर्तमान मूल्यांकन विधियाँ एक गंभीर दोष से ग्रस्त हैं: वे सिंटैक्टिक वैधता (syntactic validity) को सिमेंटिक शुद्धता (semantic correctness) के साथ मिला देती हैं।

• कंपाइलेशन की सीमा (The Limitation of Compilation): मौजूदा बेंचमार्क (जैसे MiniF2F, ProofNet) मुख्य रूप से यह जाँचकर मॉडल्स का मूल्यांकन करते हैं कि उत्पन्न किया गया प्रमेय (theorem) कंपाइल होता है या नहीं। जबकि कंपाइलेशन यह सत्यापित करता है कि कोड सिंटैक्टिक रूप से वैध है और आइसोलेशन में तार्किक रूप से सुसंगत है, यह इस बात की गारंटी नहीं देता कि प्रमेय इच्छित गणितीय अर्थ को पकड़ता है।
• "टॉटोलॉजी" की समस्या (The "Tautology" Problem): एक मॉडल एक तुच्छ टॉटोलॉजी (जैसे $a + b = a + b$) उत्पन्न कर सकता है जो सफलतापूर्वक कंपाइल होती है, लेकिन इच्छित गैर-तुच्छ कथन (जैसे कम्यूटेटिविटी $a + b = b + a$) को सिद्ध करने में विफल रहती है।
• प्रॉक्सी की अपर्याप्तता (Inadequacy of Proxies): सिमेंटिक शुद्धता को मापने के प्रयास मौजूदा अनिश्चित प्रॉक्सी पर निर्भर हैं, जैसे कि मानव-एनोटेटेड संदर्भों के विरुद्ध लेक्सिकल ओवरलैप (BLEU स्कोर) या मैन्युअल निरीक्षण। ये विधियाँ या तो शोर भरी (noisy) हैं, इनमें महंगी मानवीय श्रम की आवश्यकता होती है, या वे सही और गलत सिमेंटिक अर्थों के बीच अंतर करने में विफल रहती हैं।

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

लेखक सॉफ्टवेयर इंजीनियरिंग में इंटीग्रेशन टेस्टिंग (integration testing) से प्रेरित होकर एक प्रतिमान परिवर्तन (paradigm shift) का प्रस्ताव करते हैं। एक प्रमेय का अकेले मूल्यांकन करने के बजाय, वे इसका मूल्यांकन इस आधार पर करते हैं कि यह शेष कोडबेस के साथ कैसे इंटरैक्ट करता है।

मुख्य अवधारणा: थ्योरम टेस्टिंग (T2)

करी-हावर्ड पत्राचार (Curry-Howard correspondence) (जहाँ प्रमाण प्रोग्राम के अनुरूप होते हैं) से प्रेरणा लेते हुए, लेखक एक उत्पन्न प्रमेय को एक फंक्शन के रूप में और उन प्रमेयों को "टेस्ट केस" के रूप में देखते हैं जो उस पर निर्भर हैं।

• डिपेंडेंसी ग्राफ (Dependency Graph): वे एक डिपेंडेंसी ग्राफ का निर्माण करते हैं जहाँ एक लक्षित प्रमेय ($t_{GT}$) के प्रीडेसेसर (परिभाषाएं/लेम्मा जिनका वह उपयोग करता है) और सक्सेसर (प्रमेय जो उसे बुलाते हैं या उस पर निर्मित होते हैं) होते हैं।
• इंटीग्रेशन टेस्टिंग लॉजिक (Integration Testing Logic): यदि एक उत्पन्न प्रमेय ($t_{fl}$) सिमेंटिक रूप से गलत है (उदाहरण के लिए, यह इच्छित गुण के बजाय एक टॉटोलॉजी को परिभाषित करता है), तो कोई भी उत्तराधिकारी (successor) प्रमेय जो उस पर निर्भर है, कंपाइल होने में विफल हो जाएगा।
• कट एलिमिनेशन एनालॉजी (Cut Elimination Analogy): यह प्रक्रिया औपचारिक रूप से कट एलिमिनेशन के तार्किक सिद्धांत पर आधारित है। यदि एक प्रमाण श्रृंखला ($X \to Y \to Z \to W$) विफल हो जाती है जब मध्यवर्ती लेम्मा ($Y$) को एक उत्पन्न उम्मीदवार से बदल दिया जाता है, तो वह उम्मीदवार सिमेंटिक रूप से गलत है।

T2 बेंचमार्क

लेखकों ने इस मूल्यांकन को सुगम बनाने के लिए एक बड़े पैमाने का बेंचमार्क, T2 बनाया है:

• स्रोत (Source): 5 वास्तविक दुनिया के लीन 4 (Lean 4) रिपॉजिटरी से निकाला गया (बीजगणित, टोपोलॉजी, संख्या सिद्धांत आदि को कवर करता है)।
• पैमाना (Scale): 2,206 समस्याएँ, जिनमें से प्रत्येक को औसतन 41 सक्सेसर प्रमेयों के साथ जोड़ा गया है।
• हार्ड सबसेट (Hard Subset): 389 "हार्ड" समस्याओं का एक उपसमूह जहाँ मॉडल को केवल दिए गए कथन के लिए प्रमाण भरने के बजाय, प्रस्ताव (proposition) और प्रमाण दोनों उत्पन्न करने होते हैं।
• स्वचालन (Automation): निष्कर्षण पाइपलाइन पूरी तरह से स्वचालित है, जिसमें डिपेंडेंसी संरचना के लिए किसी मानव एनोटेशन की आवश्यकता नहीं है। नेचुरल लैंग्वेज (NL) विवरण एक मजबूत LLM (Claude Sonnet 4.5) द्वारा उत्पन्न किए गए थे और एक नमूने के लिए मैन्युअल रूप से सत्यापित किए गए थे।

मीट्रिक: टेस्टिंग एक्यूरेसी (TA)

लेखक टेस्टिंग एक्यूरेसी (TA) को प्राथमिक मूल्यांकन मीट्रिक के रूप में पेश करते हैं:
$$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$$
एक उत्पन्न प्रमेय तभी पास होता है जब इसके सभी आश्रित सक्सेसर प्रमेय सफलतापूर्वक कंपाइल होते हैं, जब मूल प्रमेय को उत्पन्न किए गए प्रमेय से बदल दिया जाता है।

3. प्रमुख योगदान (Key Contributions)

1. T2 बेंचमार्क: औपचारिक प्रमेय सिद्ध करने (formal theorem proving) के लिए पहला बड़े पैमाने का, डिपेंडेंसी-रिच बेंचमार्क जो आइसोलेटेड समस्याओं से आगे बढ़कर वास्तविक दुनिया के रिपॉजिटरी संदर्भों तक जाता है।
2. टेस्टिंग एक्यूरेसी (TA): एक नया, स्वचालित, रेफरेंस-फ्री मीट्रिक जो निर्भर मॉड्यूल के कंपाइलेशन के माध्यम से सिमेंटिक शुद्धता को सीधे सत्यापित करता है।
3. एम्पिरिकल गैप एनालिसिस (Empirical Gap Analysis): 18 अत्याधुनिक मॉडल्स (ओपन और क्लोज्ड-सोर्स दोनों) का व्यापक मूल्यांकन, जो कंपाइलेशन सफलता और सिमेंटिक शुद्धता के बीच एक विशाल अंतर को प्रकट करता है।
4. कॉन्टेक्स्टुअल इनसाइट्स (Contextual Insights): प्रदर्शित किया गया कि सक्सेसर प्रमेयों को कॉन्टेक्स्ट के रूप में प्रदान करना सिमेंटिक शुद्धता में महत्वपूर्ण सुधार करता है, जबकि केवल नेचुरल लैंग्वेज प्रमाण प्रदान करने से ऐसा नहीं होता है।

4. प्रयोगात्मक परिणाम (Experimental Results)

लेखकों ने T2 बेंचमार्क पर 18 मॉडल्स (GPT-5, Claude-Sonnet-4.5, Llama-3.1, और DeepSeek-Prover जैसे विशेष गणित मॉडल्स सहित) का मूल्यांकन किया।

• सिमेंटिक गैप (The Semantic Gap):

  • कंपाइलेशन एक्यूरेसी (Compilation Accuracy): मॉडल्स ने उच्च कंपाइलेशन दर प्राप्त की (जैसे, पूर्ण सेट पर Claude-Sonnet-4.5: 80.3%)।
  • टेस्टिंग एक्यूरेसी (TA): उन्हीं मॉडल्स ने काफी कम TA स्कोर प्राप्त किया (जैसे, पूर्ण सेट पर Claude-Sonnet-4.5: 38.9%; हार्ड सेट पर 4.5%)।
  • फॉल्स पॉजिटिव्स (False Positives): परीक्षण किए जाने पर 93.1% तक कंपिलेबल प्रमेय सिमेंटिक रूप से गलत पाए गए।

• मौजूदा मीट्रिक्स की विफलता (Failure of Existing Metrics):

  • BLEU: उच्च लेक्सिकल समानता (BLEU स्कोर) ने सिमेंटिक शुद्धता के साथ लगभग कोई सहसंबंध नहीं दिखाया (कोरिलेशन: 0.123)। मॉडल टेक्स्टुअली समान लेकिन तार्किक रूप से गलत प्रमाण उत्पन्न कर सकते हैं।
  • विशेषज्ञ मॉडल (Specialized Models): विशेष रूप से प्रमेय सिद्ध करने के लिए फाइन-ट्यून किए गए मॉडल्स ने अक्सर उच्च कंपाइलेशन दर प्राप्त की लेकिन TA पर सामान्य-उद्देश्य वाले मॉडल्स के समान या उससे खराब प्रदर्शन किया, जो यह सुझाव देता है कि वे सिमेंटिक्स के बजाय सिंटैक्स पर ओवरफिट होते हैं।

• कॉन्टेक्स्ट का प्रभाव (Impact of Context):

  • सक्सेसर प्रमेयों को इनपुट कॉन्टेक्स्ट के रूप में प्रदान करने से लगातार TA में सुधार हुआ (जैसे, Claude-Sonnet-4.5 के लिए +4.9%)।
  • बिना सक्सेसरों के केवल NL प्रूफ प्रदान करने से प्रदर्शन में सुधार नहीं हुआ और कभी-कभी यह घट भी गया।
  • फ्यू-शॉट प्रॉम्प्टिंग और इटरेटिव रिफाइनमेंट (कंपाइलर फीडबैक का उपयोग करके) ने हार्ड सेट पर नगण्य सुधार दिखाया, जो यह दर्शाता है कि कठिनाई केवल टास्क फॉर्मेटिंग में नहीं, बल्कि गहरे सिमेंटिक रीजनिंग में है।

5. महत्व और निष्कर्ष (Significance and Conclusion)

यह शोध पत्र ऑटोमेटेड थ्योरम प्रूविंग (ATP) के मूल्यांकन को मौलिक रूप से चुनौती देता है।

• सफलता को फिर से परिभाषित करना: यह सिद्ध करता है कि "कंपाइलेशन" प्रमेय जनरेशन के लिए एक आवश्यक लेकिन अपर्याप्त शर्त है। एक मॉडल सिंटैक्टिक रूप से परफेक्ट हो सकता है लेकिन सिमेंटिक रूप से बेकार।
• विश्वसनीयता (Trustworthiness): T2 बेंचमार्क और TA मीट्रिक यह आकलन करने का एक कठोर, स्वचालित तरीका प्रदान करते हैं कि क्या एक LLM वास्तव में गणितीय अवधारणाओं को समझता है या केवल सिंटैक्टिक रूप से वैध कोड का भ्रम (hallucination) पैदा कर रहा है।
• भविष्य की दिशा: यह कार्य सुझाव देता है कि भविष्य के ATP सिस्टम को आइसोलेटेड पहेलियों को हल करने के बजाय मौजूदा कोडबेस में एकीकृत होने की उनकी क्षमता (डिपेंडेंसी-अवेयर जनरेशन) पर मूल्यांकित किया जाना चाहिए। यह भी रेखांकित करता है कि जनरेशन के दौरान मॉडल को "टेस्ट सूट" (सक्सेसर प्रमेय) प्रदान करना सिमेंटिक अलाइनमेंट में सुधार करने के लिए एक महत्वपूर्ण रणनीति है।

संक्षेप में, यह शोध पत्र तर्क देता है कि इंटीग्रेशन टेस्टिंग औपचारिक गणित के लिए LLMs के मूल्यांकन में गायब कड़ी है, जो यह प्रकट करती है कि वर्तमान अत्याधुनिक मॉडल प्रमेय सिद्ध करने में विश्वसनीय सिमेंटिक शुद्धता प्राप्त करने से बहुत दूर हैं।