🤖 machine learning

Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

यह शोध पत्र प्रदर्शित करता है कि चॉइस का अभिगृही (Axiom of Choice) न्यूरल प्रूफ़ एम्बेडिंग्स में एक मापने योग्य ज्यामितीय हस्ताक्षर छोड़ता है—जो निर्भरता ग्राफ (dependency graph) में अभिगृही से दूर जाने पर घटते विसंगति स्कोर (anomaly scores) और पुनर्निर्माण हानि (reconstruction losses) द्वारा अभिलक्षित है—जो लीन 4 (Lean 4) जैसे सिस्टम में रचनात्मक (constructive) और शास्त्रीय (classical) प्रमेय सिद्ध करने के बीच प्रदर्शन के अंतर के साथ सह-संबद्ध है और उसका पूर्वानुमान लगाता है।

मूल लेखक: Rodrigo Mendoza-Smith

प्रकाशित 2026-06-30✓ Author reviewed ⓘ

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

CC BY 4.0

मूल लेखक: Rodrigo Mendoza-Smith

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

कल्पना कीजिए कि Mathlib नामक एक विशाल, प्राचीन पुस्तकालय है। इस पुस्तकालय में लगभग पाँच लाख गणितीय प्रमाण (proofs) हैं, जो 'लीन' (Lean) नामक एक सख्त, कंप्यूटर-पठनीय भाषा में लिखे गए हैं। एक सदी से अधिक समय से, गणितज्ञ इन दो तरीकों में से एक के बारे में बहस कर रहे हैं जिनसे ये प्रमाण बनाए जाते हैं:

रचनात्मक प्रमाण (Constructive Proofs): "लेगो" (Lego) विधि। यदि आप दावा करते हैं कि एक इमारत मौजूद है, तो आपको यह दिखाना होगा कि उसे ईंट-दर-ईंट ठीक कैसे बनाया जाए।
शास्त्रीय प्रमाण (Classical Proofs): "जादुई" (Magic) विधि। आप केवल यह कहकर दावा कर सकते हैं कि एक इमारत मौजूद है कि "यह असंभव है कि वह मौजूद न हो," बिना यह दिखाए कि उसे कैसे बनाया जाए। यह एक नियम पर निर्भर करता है जिसे चॉइस का सिद्धांत (Axiom of Choice) कहा जाता है।

लंबे समय तक, लोगों ने सोचा कि ये केवल दार्शनिक अंतर थे। यह शोध पत्र तर्क देता है कि ये वास्तव में ज्यामितीय अंतर (geometric differences) हैं जिन्हें आप एक मानचित्र पर दो शहरों के बीच की दूरी की तरह माप सकते हैं।

लेखकों ने इसे कैसे खोजा, इसके लिए सरल उपमाओं का उपयोग किया गया है:

1. "जादुई नियम" की गूँज (The "Echo" of the Magic Rule)

लेखकों ने पुस्तकालय को एक विशाल गूँज कक्ष (echo chamber) की तरह माना। उन्होंने एक कंप्यूटर मस्तिष्क (AI) को प्रशिक्षित किया जो केवल "लेगो" (रचनात्मक) प्रमाणों पर आधारित था। AI ने उन प्रमाणों की लय, शैली और संरचना को सीखा। वह एक विशेषज्ञ बन गया कि एक "सामान्य" रचनात्मक प्रमाण कैसा दिखता है।

फिर, उन्होंने उसमें "जादुकी" (शास्त्रीय) प्रमाण डाले।

परिणाम: AI ने केवल यह नहीं कहा कि "यह अलग है।" उसने यह भी मापा कि यह कितना अलग है।
उपमा: कल्पना कीजिए कि आप एक संगीत शिक्षक हैं जो केवल शास्त्रीय पियानो सुनते हैं। यदि आप एक जैज़ (jazz) गीत सुनते हैं, तो आप कह सकते हैं, "यह अजीब लग रहा है।" लेकिन यदि आप एक ऐसा जैज़ गीत सुनते हैं जो 100 साल पहले लिखा गया था, तो वह एक आधुनिक जैज़ गीत की तुलना में कम अजीब लग सकता है, जिसमें एक बहुत ही विशिष्ट, असामान्य वाद्य यंत्र का उपयोग किया गया हो।

2. "गहराई" का नियम (The "Depth" Law)

लेखकों ने महसूस किया कि सभी "जादुई" प्रमाण समान रूप से जादुई नहीं होते।

उथली गहराई (दूरी 1-2): ये प्रमाण "जादुई नियम" (चॉइस का सिद्धांत) का सीधे उपयोग करते हैं। ये उस अजीब वाद्य यंत्र का उपयोग करने वाले जैज़ गीत की तरह हैं जो बिल्कुल शुरुआत में ही बजता है। AI के लिए, ये बहुत अजीब और "स्थान से बाहर" लगते हैं।
गहरी गहराई (दूरी 9+): ये प्रमाण बहुत पीछे, अन्य लेम्मा (lemmas) की एक लंबी श्रृंखला के भीतर दबे हुए "जादुई नियम" का उपयोग करते हैं। प्रमाण स्वयं बहुत हद तक "लेगो" प्रमाण जैसा दिखता है। AI के लिए, ये लगभग सामान्य लगते हैं।

खोज: यहाँ एक सुचारू ढाल (smooth gradient) मौजूद है। जैसे-जैसे आप "जादुई नियम" के प्रत्यक्ष उपयोग से दूर जाते हैं, प्रमाण एक मानक "लेगो" प्रमाण की तरह दिखने और सुनाई देने लगता है। "अजीबोगरीबपन" धीरे-धीरे कम हो जाता है। लेखक इसे डेप्थ लॉ (Depth Law) कहते हैं।

3. "अजीबोगरीबपन" को मापने के तीन तरीके

शोध पत्र ने इस दूरी को मापने के लिए तीन अलग-अलग "पैमानों" का उपयोग किया, और उन सभी ने एक ही बात कही:

विसंगति स्कोर (The Anomaly Score): यह निकटतम "लेगो" प्रमाण से कितना दूर है? (जैसे एक पियानो नोट से जैज़ नोट की दूरी मापना)।
पुनर्निर्माण हानि (The Reconstruction Loss): यदि AI एक "जादुई" प्रमाण में अगले चरण का अनुमान लगाने की कोशिश करता है, तो क्या वह "लेगो" प्रमाण की तुलना में अधिक गलतियाँ करता है? (जैसे एक शिक्षक वाक्य में अगले शब्द का अनुमान लगाता है; वे "जादुई" वाक्यों के साथ अधिक संघर्ष करते हैं)।
घनत्व जाँच (The Density Check): क्या यह प्रमाण भीड़भाड़ वाले "लेगो" पड़ोस में रह रहा है, या यह खाली "जादुगी" के निर्जन क्षेत्र में खो गया है?

तीनों पैमानों ने एक ही पैटर्न दिखाया: "जादुई" प्रमाण स्रोत के करीब होने पर बहुत विशिष्ट होते हैं, लेकिन जैसे-जैसे आप दूर जाते हैं, वे घुलमिल जाते हैं।

4. "रोबोट सॉल्वर" परीक्षण

शोध पत्र का सबसे व्यावहारिक हिस्सा एक रोबोट है जिसका नाम एसोप (Aesop) है, जो गणित की इन समस्याओं को स्वचालित रूप से हल करने की कोशिश करता है।

समस्या: रोबोट "लेगो" प्रमाणों को हल करने में बहुत अच्छा है (20% सफलता दर) लेकिन "जादुई" प्रमाणों में बहुत बुरा है (केवल 1.5% सफलता दर)। यह ब्लॉक बनाने वाले रोबोट और जादू के मंत्रों से भ्रमित होने वाले रोबोट के बीच के अंतर जैसा है।
ट्विस्ट: लेखकों ने रोबोट की मदद करने के लिए उसे एक "न्यूरल गाइड" (एक स्मार्ट सहायक जो पहला कदम सुझाता है) दिया।
परिणाम: गाइड ने थोड़ी मदद की, लेकिन इसने समस्या को ठीक नहीं किया। रोबोट अभी भी "जादुतिक" प्रमाणों के साथ भारी संघर्ष करता है, भले ही वे "गहरे" हों और "लेगो" जैसे दिखते हों।

बड़ी सीख: भले ही "जादुकी" प्रमाण स्रोत से दूर होने पर अधिक और अधिक "लेगो" प्रमाणों जैसे दिखने लगें, फिर भी रोबोट सॉल्वर उन्हें कठिन के रूप में ही देखता है। यह सुझाव देता है कि "जादुतिक" नियम प्रमाण पर एक स्थायी, अदृश्य निशान छोड़ देता है जो वर्तमान कंप्यूटरों के लिए उन्हें हल करना कठिन बना देता है, चाहे वह सतह पर कितना भी "सामान्य" क्यों न दिखे।

सारांश

यह शोध पत्र सिद्ध करता है कि चॉइस का सिद्धांत (Axiom of Choice) केवल एक दार्शनिक विचार नहीं है; यह गणितीय प्रमाणों पर एक मापने योग्य, ज्यामितीय छाप छोड़ता है।

नियम का सीधा उपयोग AI के लिए प्रमाणों को बहुत "विदेशी" बना देता है।
अप्रत्यक्ष उपयोग उन्हें अधिक "सामान्य" बनाता है।
हालाँकि, भले ही वे "सामान्य" दिखें, फिर भी स्वचालित सॉल्वर शुद्ध रचनात्मक प्रमाणों की तुलना में उनके साथ काफी अधिक संघर्ष करते हैं।

यह पता लगाने जैसा है कि "जादुई ईंटों" से बना घर बाहर से देखने में बिल्कुल "सामान्य ईंटों" से बने घर जैसा लग सकता है, लेकिन यदि आप एक मानक टूलकिट के साथ उसकी मरम्मत करने की कोशिश करते हैं, तो जादुई ईंटें अभी भी समस्या पैदा करती हैं।

तकनीकी सारांश: न्यूरल प्रूफ एम्बेडिंग्स में चॉइस के सिद्धांत (Axiom of Choice) के ज्यामितीय माप

समस्या विवरण

चॉइस का सिद्धांत (Axiom of Choice - AC) ऐतिहासिक रूप से गणितीय आधारों को शास्त्रीय (classical) और रचनात्मक (constructive) समूहों में विभाजित करता रहा है, जो कि एक ऐसा अंतर है जो मुख्य रूप से दार्शनिक और पद्धतिगत बना हुआ है। जहाँ शास्त्रीय प्रमाण AC द्वारा अनुमत गैर-रचनात्मक शॉर्टकट्स का उपयोग करते हैं, वहीं रचनात्मक प्रमाण स्पष्ट साक्ष्यों (witnesses) की आवश्यकता रखते हैं, लेकिन यह स्पष्ट नहीं था कि क्या ये दोनों प्रतिमान केवल स्वयंसिद्ध निर्भरता से परे संरचनात्मक रूप से भिन्न हैं। यह शोध जांचता है कि क्या चॉइस का सिद्धांत औपचारिक प्रमाणों के स्थान में, विशेष रूप से Lean 4 Mathlib लाइब्रेरी के भीतर, एक मापने योग्य "ज्यामितीय हस्ताक्षर" (geometric signature) छोड़ता है, और क्या इस हस्ताक्षर के न्यूरल थ्योरम प्रूवर्स के लिए परिचालन संबंधी परिणाम होते हैं।

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

डेटा विभाजन और निर्भरता ट्रैकिंग

लेखक Classical.choice पर स्वयंसिद्ध निर्भरता को ट्रैक करने के लिए Lean 4 के कर्नेल-स्तरीय ट्रैकिंग का उपयोग करते हैं ताकि Mathlib लाइब्रेरी को विभाजित किया जा सके, जिसमें 471,260 मशीन-प्रमाणित घोषणाएँ शामिल हैं। डिपेंडेंसी ग्राफ पर ब्रैडथ-फर्स्ट सर्च (breadth-first search) करके, वे घोषणाओं को दो सेटों में वर्गीकृत करते हैं:

शास्त्रीय प्रमाण (Classical Proofs): वे जो पारगमन रूप से (transitively) Classical.choice पर निर्भर हैं।
रचनात्मक प्रमाण (Constructive Proofs): वे जो उस पर निर्भर नहीं हैं।

एक शास्त्रीय प्रमाण की "दूरी" को उस प्रमाण से Classical.choice तक की सबसे छोटी निर्भरता श्रृंखला की लंबाई के रूप में परिभाषित किया गया है। यह एक ऐसा स्तरीकृत (stratified) डेटासेट बनाता है जहाँ प्रमाणों को स्वयंसिद्ध से उनकी गहराई के आधार पर समूहीकृत किया जाता है। अध्ययन 2 से 200 चरणों वाले टैक्टिक ट्रेसेस (tactic traces) के साथ 42,355 प्रमेयों (31,144 शास्त्रीय, 11,211 रचनात्मक) की एक फ़िल्टर की गई आबादी पर केंद्रित है।

लेबल-मुक्त प्रतिनिधित्व शिक्षण (Label-Free Representation Learning)

इन प्रमाणों के ज्यामितीय गुणों को बिना किसी पूर्वाग्रह के मापने के लिए, लेखक विशेष रूप से रचनात्मक प्रमाणों पर एक स्व-पर्यवेक्षित डीनॉइजिंग ऑटोएनकोडर (self-supervised denoising autoencoder) को प्रशिक्षित करते हैं।

इनपुट: प्रमाणों को टैक्टिक हेड्स (जैसे, intro, rw, simp) के अनुक्रमों के रूप में दर्शाया जाता है, जहाँ विशिष्ट तर्कों को हटा दिया जाता है ताकि प्रमाण संरचना पर ध्यान केंद्रित किया जा सके।
आर्किटेक्चर: एक 4-लेयर ट्रांसफॉर्मर एनकोडर को 2-लेयर डिकोडर के साथ जोड़ा गया है। मॉडल को इनपुट अनुक्रम से मास्क किए गए टैक्टिक टोकन (20% भ्रष्टाचार/corruption) को पुनर्गठित करने के लिए प्रशिक्षित किया जाता है।
एम्बेडिंग (Embedding): प्रमाण एम्बेडिंग एनकोडर की हिडन स्टेट्स (पैडिंग को छोड़कर) का माध्य (mean) है, जिसे यूनिट स्फीयर पर सामान्यीकृत (normalized) किया गया है।
लेबल-मुक्त बाधा: एनकोडर प्रशिक्षण, शब्दावली निर्माण या हाइपरपैरामीटर चयन के दौरान कभी भी शास्त्रीय प्रमाणों को नहीं देखता है। शास्त्रीय प्रमाण केवल एक होल्ड-आउट आबादी के रूप में कार्य करते हैं।

ज्यामितीय माप

शास्त्रीय प्रमाणों के रचनात्मक प्रशिक्षण वितरण से विचलन को मापने के लिए तीन पूरक मेट्रिक्स का उपयोग किया जाता है:

विसंगति स्कोर (Anomaly Score - k-NN): $k$ -निकटतम रचनात्मक पड़ोसियों से यूक्लिडियन दूरी।
पुनर्गठन हानि (Reconstruction Loss): शास्त्रीय प्रमाण में मास्क किए गए टोकन की भविष्यवाणी करने का प्रयास करते समय होने वाला क्रॉस-एन्ट्रॉपी लॉस।
घनत्व-सुपरलेवल कंटेनमेंट (Density-Superlevel Containment): रचनात्मक प्रशिक्षण वितरण द्वारा परिभाषित उच्च-घनत्व क्षेत्र (superlevel set) के बाहर गिरने वाले शास्त्रीय प्रमाणों का अंश।

परिचालन मूल्यांकन

अध्ययन दो प्रणालियों का उपयोग करके थ्योरम सिद्ध करने के प्रदर्शन पर इन ज्यामितीय निष्कर्षों के प्रभाव का मूल्यांकन करता है:

aesop: एक प्रतीकात्मक बेस्ट-फर्स्ट सर्च प्रूवर।
हाइब्रिड (ReProver + aesop): एक न्यूरल-निर्देशित दृष्टिकोण जहाँ एक टैक्टिक जनरेटर पहला कदम प्रस्तावित करता है, जिसके बाद aesop चलता है।

मुख्य परिणाम

गहराई का नियम (The Depth Law)

प्राथमिक निष्कर्ष एक "डेप्थ लॉ" का अस्तित्व है: Classical.choice से दूरी के साथ शास्त्रीय और रचनात्मक प्रमाणों के बीच ज्यामितीय अंतर अनुमानित रूप से घटता है।

उथले स्तरों पर तीव्र अलगाव: गहराई 2 (सीधे शास्त्रीय लेम्मा का उपयोग करने वाले प्रमाण) पर, अलगाव मजबूत है। k-NN विसंगति स्कोर एक AUC 0.847 प्राप्त करता है, पुनर्गठन हानि रचनात्मक बेसलाइन से 34.5% अधिक है, और 43% शास्त्रीय प्रमाण रचनात्मक 90% घनत्व क्षेत्र के बाहर गिरते हैं।
अस्पष्टता की ओर क्षय: जैसे-जैसे गहराई बढ़ती है, मेट्रिक्स रचनात्मक बेसलाइन की ओर अभिसरित (converge) होते हैं। गहराई 9+ तक, तीनों मेट्रिक्स चांस स्तरों (AUC $\approx$ 0.5, लॉस $\approx$ बेसलाइन, कंटेनमेंट $\approx$ 90%) के करीब पहुँच जाते हैं, जिससे गहरे शास्त्रीय प्रमाण रचनात्मक प्रमाणों से ज्यामितीय रूप से अविभेद्य हो जाते हैं।
एक-पैरामीटर मिश्रण नियम (One-Parameter Mixture Law): लेखक इस ग्रेडिएंट को दो वितरणों के मिश्रण के रूप में मॉडल करते हैं: एक रचनात्मक वितरण $P$ और एक सीधे-शास्त्रीय वितरण $R$ । गहराई- $d$ वितरण $Q_d$ को $Q_d = (1 - \lambda_d)P + \lambda_d R$ के रूप में मॉडल किया गया है, जहाँ $\lambda_d$ एक मिश्रण भार है जो गहराई के साथ घटता है। सामान्यीकृत होने पर तीनों अलग-अलग माप एक ही वक्र (curve) पर सिमट जाते हैं, जो एक एक-पैरामीटर नियम का समर्थन करते हैं।

मजबूती नियंत्रण (Robustness Controls)

सिग्नल कई संभावित भ्रमों (confounds) के विरुद्ध मजबूत है:

कीवर्ड्स: स्पष्ट शास्त्रीय टैक्टिक मार्कर (जैसे, classical, by contra) को हटाने से गहराई-2 का AUC केवल थोड़ा (0.847 से 0.754) कम होता है, जो दर्शाता है कि सिग्नल संरचनात्मक है, न कि केवल शाब्दिक।
लंबाई: प्रमाण की लंबाई के लिए एम्बेडिंग्स को रेसिडुअलाइज (residualize) करने से भी ग्रेडिएंट समाप्त नहीं होता है।
लेखक/फ़ाइल/विषय: लेखक, फ़ाइल और गणितीय उप-क्षेत्र को नियंत्रित करने वाले मिक्स-इफेक्ट्स मॉडल पुष्टि करते हैं कि सिग्नल विशिष्ट संदर्भों के भीतर बना रहता है।
कथन बनाम प्रमाण: थ्योरम कथन (statements) में थ्योरम प्रमाणों (proofs) की तुलना में बहुत कमजोर गहराई ग्रेडिएंट दिखता है (कथन का AUC 0.604 कुल मिलाकर है बनाम प्रमाण का AUC 0.675 कुल मिलाकर), जो पुष्टि करता है कि सिग्नल मुख्य रूप से कम्पोजिशनल (प्रमाण संरचना) है, न कि विषयगत (थ्योरम सामग्री)।
स्वयंसिद्ध विशिष्टता: हालांकि propext और Quot.sound भी गहराई ग्रेडिएंट दिखाते हैं, Classical.choice सबसे तीव्र ग्रेडिएंट उत्पन्न करता है, जो शास्त्रीय तर्क के साथ एक अद्वितीय परिचालन जुड़ाव का सुझाव देता है।

परिचालन परिणाम

ज्यामितीय सिग्नेचर प्रूवर के प्रदर्शन के साथ सह-संबंध रखता है:

aesop की विफलता: aesop 20.0% रचनात्मक प्रमेयों को हल करता है लेकिन केवल 1.5% शास्त्रीय प्रमेयों को (एक 13 $\times$ का अंतर)। ज्यामितीय सिग्नल के विपरीत, यह परिचालन अंतर गहराई के साथ सुचारू नहीं होता है; शास्त्रीय प्रमाण स्वयंसिद्ध से उनकी दूरी के बावजूद aesop के लिए कठिन बने रहते हैं।
न्यूरल मार्गदर्शन: एक न्यूरल टैक्टिक जनरेटर (ReProver) जोड़ने से अंतर लगभग 5 $\times$ (22.0% बनाम 4.5%) तक कम हो जाता है, लेकिन यह पूरी तरह समाप्त नहीं होता है।
पूर्वानुमान शक्ति: ज्यामितीय विसंगति स्कोर प्रमाण लंबाई अकेले की तुलना में aesop की विफलता का बेहतर पूर्वानुमान लगाता है (विसंगति स्कोर जोड़ने पर AUC 0.766 से बढ़कर 0.841 हो जाता है)।

महत्व और दावे

यह शोध दावा करता है कि यह प्रमाण स्थान में चॉइस के सिद्धांत का मापने योग्य ज्यामितीय सहसंबंध प्रदान करने वाला पहला अनुभवजन्य प्रमाण है। लेखक तर्क देते हैं कि:

संरचनात्मक अंतर: शास्त्रीय/रचनात्मक विभाजन केवल एक दार्शनिक रुख नहीं है, बल्कि प्रमाण संरचना का एक संरचनात्मक गुण है जो न्यूरल एम्बेडिंग्स में दिखाई देता है।
परिचालन प्रासंगिकता: यह ज्यामितीय हस्ताक्षर केवल एक अमूर्त जिज्ञासा नहीं है; यह स्वचालित थ्योरम प्रूवर्स के प्रदर्शन का पूर्वानुमान लगाता है। "डेप्थ लॉ" यह सुझाव देता है कि जैसे-जैसे प्रमाण स्वयंसिद्ध से दूर जाते हैं, वे संरचनात्मक रूप से रचनात्मक प्रमाणों के अधिक समान होते जाते हैं, फिर भी aesop जैसे प्रतीकात्मक प्रूवर्स के लिए परिचालन बाधा Classical.choice की उपस्थिति के प्रति विशिष्ट बनी रहती है।
पद्धतिगत योगदान: यह कार्य प्रदर्शित करता है कि एक एकल वर्ग (रचनात्मक प्रमाणों) पर लेबल-मुक्त, स्व-पर्यवेक्षित शिक्षण, एक रखे गए वर्ग (शास्त्रीय प्रमाणों) की संरचनात्मक सीमाओं को प्रकट कर सकता है, जो मेटा-गणितीय विश्लेषण के लिए एक नया उपकरण प्रदान करता है।

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