← नवीनतम पेपर
💻 computer science

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

यह शोध पत्र Continuous-Eris को प्रस्तुत करता है, जो Rocq प्रूफ असिस्टेंट में कार्यान्वित एक हायर-ऑर्डर सेपरेशन लॉजिक है, ताकि गॉसियन और लाप्लास जैसे निरंतर वितरणों (continuous distributions) के लिए सटीक सैंपलिंग एल्गोरिदम की शुद्धता को औपचारिक रूप से सत्यापित किया जा सके, जो फ्लोटिंग-पॉइंट सन्निकटन (floating-point approximations) की सुरक्षा और सटीकता संबंधी सीमाओं को संबोधित करता है।

मूल लेखक: Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti

प्रकाशित 2026-05-14
📖 7 मिनट में पढ़ें🧠 गहराई से पढ़ें
CC BY 4.0

मूल लेखक: Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti

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

कल्पना कीजिए कि आप एक केक बनाने की कोशिश कर रहे हैं, लेकिन एक मानक मापने वाले कप के बजाय, आपको हर सामग्री को एक बाल्टी से एक छोटे कप में पानी डालकर मापना है, वह भी एक बार में केवल एक बूंद करके। यदि आप 100 बूंदों के बाद रुक जाते हैं, तो यह मात्रा का एक अनुमान (approximation) है। यदि आप 1,000 बूंदों के बाद रुकते हैं, तो यह और भी करीब है। लेकिन यदि आप किसी भी बिंदु पर रुकते हैं, तो तकनीकी रूप से आपने एक छोटी सी गलती की है क्योंकि आपने सटीक मात्रा प्राप्त नहीं की थी।

कंप्यूटर विज्ञान की दुनिया में, यह बिल्कुल वही होता है जो कंप्यूटर तब करते हैं जब वे वास्तविक संख्याओं (जैसे 3.14159...) को संभालते हैं। वे "फ्लोटिंग-पॉइंट नंबरों" का उपयोग करते हैं, जो उन 100-बूंदों वाले अनुमानों की तरह होते हैं। अधिकांश चीजों के लिए, यह ठीक है। लेकिन संवेदनशील कार्यों के लिए—जैसे चिकित्सा अध्ययनों या वित्तीय रिकॉर्ड में निजी डेटा की सुरक्षा करना—वे छोटी "राउंडिंग त्रुटियां" (rounding errors) बड़े सुरक्षा लीक का कारण बन सकती हैं।

यह शोध पत्र इस समस्या को ठीक करने का एक नया तरीका पेश करता है। लेखकों ने Continuous-Eris नामक एक उपकरण बनाया है जो प्रोग्रामर्स को यह सिद्ध करने में मदद करता है कि उनका कोड निरंतर वितरण (continuous distributions) (जैसे 0 और 1 के बीच एक पूरी तरह से यादृच्छिक संख्या चुनना) से सटीक सैंपलिंग (exact sampling) कर रहा है, और वह भी बिना किसी राउंडिंग एरर के।

उन्होंने इसे कैसे किया, इसके लिए कुछ रचनात्मक उपमाओं का उपयोग किया गया है:

1. समस्या: "आलसी" शेफ (The "Lazy" Chef)

आमतौर पर, 0 और 1 के बीच एक यादृच्छिक संख्या प्राप्त करने के लिए, एक कंप्यूटर पूरे अनंत अनुक्रम (infinite sequence) (जैसे 0.101101...) को एक साथ उत्पन्न करने का प्रयास कर सकता है। लेकिन यह असंभव है; आप एक अनंत सूची नहीं लिख सकते।

इसके बजाय, लेखक एक "आलसी" दृष्टिकोण का उपयोग करते हैं। कल्पना कीजिए कि एक शेफ प्याज की परत दर परत छील रहा है, लेकिन केवल तभी जब आप उससे मांगते हैं।

  • कोड: प्रोग्राम U (Uniform) तुरंत पूरी संख्या उत्पन्न नहीं करता है। यह केवल एक खाली सूची बनाता है।
  • अनुरोध: जब आप पहले कुछ अंकों के लिए पूछते हैं (एक फ़ंक्शन जिसे GetBits कहा जाता है), तो प्रोग्राम एक परत छील देता है (एक रैंडम बिट, 0 या 1 उत्पन्न करता है)।
  • जादू: यदि आप बाद में और अधिक अंक मांगते हैं, तो यह एक और परत छील देता है। यह संख्या को बिट-दर-बिट बनाता है, उतनी ही गति से जितनी आपको आवश्यकता है। यह सुनिश्चित करता है कि आपको कभी भी अनंत सूची के साथ काम न करना पड़े, लेकिन आप जितना चाहें उतना सटीक उत्तर प्राप्त कर सकते हैं।

2. चुनौती: यह सिद्ध करना कि शेफ ईमानदार है

कठिन काम कोड लिखना नहीं है; बल्कि यह सिद्ध करना है कि आलसी शेफ वास्तव में निष्पक्ष रूप से संख्याएं चुन रहा है।

  • यदि शेफ एक परत छीलता है, तो क्या वह वास्तव में यादृच्छिक (random) है?
  • यदि आप 10 परतें मांगते हैं, तो क्या परिणामी संख्या वास्तव में पूरी रेंज में वितरित है?
  • आप यह कैसे सिद्ध करेंगे जब शेफ ने अभी तक प्याज की पूरी परतें नहीं छीली हैं?

पिछले उपकरण केवल सरल, विविक्त (discrete) चीजों (जैसे पासा फेंकना) के लिए इसे सिद्ध कर सकते थे। वे निरंतर संख्याओं (continuous numbers) के "अनंत प्याज" को नहीं संभाल सकते थे, विशेष रूप से जब कोड जटिल हो, मेमोरी का उपयोग करता हो, और मानों को बदलता हो।

3. समाधान: "अनंत टेप" और "समय रसीद" (The "Infinite Tape" and "Time Receipts")

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

A. "पूर्व-निर्मित टेप" (Pre-Drawn Tape - Pre-sampling)

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

B. "समय रसीद" (The "Time Receipt" - The Budget)

यहाँ पेचीदा हिस्सा है: कंप्यूटर प्रमाण में एक टेप वास्तव में अनंत नहीं हो सकता।
इसलिए, वे टाइम रसीद (Time Receipts) का उपयोग करते हैं। इसे एक "चरण बजट" (step budget) के रूप में सोचें।

  • तर्क कहता है: "हम प्रोग्राम को केवल 100 चरणों के लिए देखेंगे।"
  • चूंकि प्रोग्राम एक बिट उत्पन्न करने के लिए एक चरण लेता है, इसलिए यदि हम केवल 100 चरणों के लिए देखते हैं, तो हमें हमारे जादुई टेप पर केवल पहले 100 बिट्स को जानने की आवश्यकता है।
  • "टाइम रसीद" एक टोकन है जो कहता है: "मेरे पास 100 चरण बचे हैं।" हर बार जब प्रोग्राम एक चरण लेता है, तो आप एक रसीद खर्च करते हैं।
  • यह उन्हें यह मानने की अनुमति देता है कि टेप अनंत है, क्योंकि प्रमाण के किसी भी विशिष्ट क्षण के लिए, उन्हें केवल सीमित बिट्स की आवश्यकता होती है, और उनके पास भुगतान करने के लिए एक "रसीद" होती है।

C. "त्रुटि क्रेडिट" (The "Error Credit" - The Safety Net)

अंत में, वे त्रुटि क्रेडिट (Error Credits) का उपयोग करते हैं। कल्पना कीजिए कि आपके पास "गलतियों" का एक बजट है जिन्हें आप करने की अनुमति प्राप्त हैं।

  • यदि आप यह सिद्ध करना चाहते हैं कि प्रोग्राम 99.9% सही है, तो आप अपने क्रेडिट का 0.1% खर्च करते हैं।
  • लेखकों ने इन क्रेडिट्स को यह सिद्ध करने के लिए उपयोग करने का तरीका विकसित किया है कि प्रोग्राम के गलत व्यवहार करने की संभावना नगण्य है।
  • उन्होंने इन असतत (discrete) "गलती बजटों" को एक सुचारू, निरंतर गणितीय उपकरण (इंटीग्रल्स का उपयोग करके) में बदलने का तरीका निकाला ताकि वे वास्तविक संख्याओं की पूरी रेंज के लिए कोड के काम करने का प्रमाण दे सकें, न कि केवल विशिष्ट बिंदुओं के लिए।

4. उन्होंने वास्तव में क्या सिद्ध किया

इस नई प्रणाली का उपयोग करते हुए, लेखकों ने केवल सिद्धांत की बात नहीं की; उन्होंने निम्नलिखित के लिए वास्तविक कोड बनाया और सत्यापित किया:

  1. यूनिफॉर्म डिस्ट्रीब्यूशन (Uniform Distribution): 0 और 1 के बीच एक यादृच्छिक संख्या चुनना।
  2. गौसियन (Gaussian - Bell Curve): एक ऐसी संख्या चुनना जो एक औसत के आसपास केंद्रित होती है (जैसे मानव ऊंचाई)।
  3. लाप्लास डिस्ट्रीब्यूशन (Laplace Distribution): डिफरेंशियल प्राइवेसी (डेटा साझा करने का एक तरीका जिससे व्यक्तिगत रहस्यों का खुलासा न हो) में उपयोग किया जाने वाला एक विशिष्ट प्रकार का शोर (noise)।

उन्होंने सिद्ध किया कि इन वितरणों के लिए उनका कोड गणितीय रूप से सटीक है। यदि आप उनके कोड का उपयोग करते हैं, तो आप केवल एक "लगभग सही" फ्लोटिंग-पॉइंट नंबर प्राप्त नहीं कर रहे हैं; आप एक ऐसी संख्या प्राप्त कर रहे हैं जो बिट-दर-बिट गारंटी के साथ पूर्ण गणितीय नियमों का पालन करती है।

निष्कर्ष

यह शोध पत्र एक नया "नियम पुस्तिका" (Continuous-Eris) प्रस्तुत करता है जो प्रोग्रामर्स को जटिल, 'लेजी', सटीक सैंपलिंग कोड लिखने और यह सिद्ध करने की अनुमति देता है कि यह 100% सही है। उन्होंने इसे एक "जादुई पूर्व-लिखित टेप" को "स्टेप-बजट" प्रणाली के साथ जोड़कर किया, जिससे उन्हें सीमित, प्रबंधनीय चरणों का उपयोग करके अनंत संभावनाओं के बारे में सोचने की अनुमति मिली। यह सुनिश्चित करने की दिशा में एक बड़ा कदम है कि गोपनीयता-संरक्षण एल्गोरिदम और अन्य महत्वपूर्ण प्रणालियों में राउंडिंग एरर के कारण छिपे हुए गणितीय बग न हों।

अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?

आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।

Digest आज़माएँ →

इसी तरह के और पेपर

इस विषय के सभी पेपर देखें 💻 cs →