1086 पेपर
यह शोधपत्र फैक्टर्ड मार्कोव डिसीजन प्रोसेस (factored Markov Decision Processes) के लिए एक प्रॉपर्टी-ड्रिवन कॉज़ल एब्स्ट्रैक्शन तकनीक प्रस्तुत करता है जो बड़े पैमाने की प्रणालियों में निकट-इष्टतम नीतियां (near-optimal policies) गणना करने और सामान्यीकरण करने में सक्षम सघन, स्केलेबल मॉडल उत्पन्न करने के लिए अवस्था चरों (state variables) के बीच कॉज़ल संबंधों का लाभ उठाता है।
यह शोध पत्र टर्म और टाइप मोर्फिज्म फाइब्रेशन के माध्यम से बाद वाले के लक्षण वर्णन करके और तत्पश्चात जैकब्स कॉम्प्रिहेन्शन कैटेगरीज पर फ्री कॉम्प्रिहेन्शन कैटेगरीज और जैकब्स कॉम्प्रिहेन्शन कैटेगरीज पर फ्री लॉवरे-एहरहार्ड कॉम्प्रिहेन्शन कैटेगरीज के लिए निर्माण प्रदान करके, जैकब्स कॉम्प्रिहेन्शन कैटेगरीज और लॉवरे-एहरहार्ड कॉम्प्रिहेन्शन कैटेगरीज के उपवर्ग के बीच संबंध की जांच करता है।
यह शोध पत्र क्लिफोर्ड सर्किट के गुणों को कुशलतापूर्वक सत्यापित करने के लिए गोट्समैन के हाइजेनबर्ग प्रतिनिधित्व से व्युत्पन्न एक हल्का होअर-समान तर्क प्रस्तुत करता है और -गेट्स तथा मैजिक स्टेट्स को शामिल करके इसे यूनिवर्सल क्वांटम कंप्यूटिंग तक विस्तारित करता है, जो क्यूबिट डिस्पोजल सर्टिफिकेशन, सेपरेबिलिटी चेक और -गेट जटिलता पर निचली सीमाएं स्थापित करने जैसे अनुप्रयोगों को सक्षम बनाता है।
यह शोध पत्र एक क्षयित (degenerated) "कॉल-बाय-सिली" (call-by-silly) कैलकुलस प्रस्तुत करता है जो कॉल-बाय-नेम और कॉल-बाय-वैल्यू के सबसे बुरे पहलुओं को सममित रूप से संयोजित करता है ताकि यह प्रदर्शित किया जा सके कि कॉल-बाय-वैल्यू की प्रासंगिक तुल्यता (contextual equivalence) दक्षता के प्रति अंध है, और साथ ही एक संगत रणनीति, एब्स्ट्रैक्ट मशीन, और एक सटीक मल्टी-टाइप सिस्टम भी प्रदान करता है जो यह सिद्ध करता है कि यह अधिकतम लंबाई वाले मूल्यांकन अनुक्रमों (evaluation sequences) की गणना करता है।
यह शोध पत्र लेयर्ड मोनोइडल थ्योरीज (layered monoidal theories) को मोनोइडल थ्योरीज के एक सामान्यीकरण के रूप में प्रस्तुत करता है जो एकल स्ट्रिंग डायग्राम फ्रेमवर्क के भीतर बहु-अमूर्त स्तरों (multiple abstraction levels) के सटीक, आरेखीय एकीकरण को सक्षम बनाता है, जो क्वांटम भौतिकी, रसायन विज्ञान और कंप्यूटर विज्ञान जैसे विविध वैज्ञानिक डोमेन में सूचना प्रवाह को मॉडल करने के लिए एक एकीकृत बीजगणितीय दृष्टिकोण प्रदान करता है।
यह शोध पत्र एक लीन 4-मैकेनाइज्ड कैलकुलस और "हर्डी-गर्डी" नामक एक ड्यूल-प्लेन सिस्टम प्रस्तुत करता है जो गैर-विश्वसनीय (untrusted) LLMs को भाषाओं के बढ़ते, मानव-सत्यापित ग्राफ के भीतर विश्वसनीय अनुवाद मार्गों को संयोजित करके प्रोग्राम प्रश्नों के स्व-प्रमाणित, फिडेलिटी-ग्रेड उत्तर उत्पन्न करने में सक्षम बनाता है।
यह अध्ययन प्रदर्शित करता है कि जहाँ फ्रंटियर लार्ज लैंग्वेज मॉडल्स केवल रिपॉजिटरी आर्टिफैक्ट्स से कार्यात्मक रूप से परिचालन योग्य मल्टी-सर्विस डॉकर एनवायरनमेंट को सफलतापूर्वक उत्पन्न कर सकते हैं, वहीं वे सुरक्षा नीतियों और बिल्ड ऑप्टिमाइज़ेशन जैसे महत्वपूर्ण परिनियोजन-इरादा विनिर्देशों (deployment-intent specifications) का अनुमान लगाने में लगातार विफल रहते हैं, जिससे कार्यात्मक शुद्धता और प्रोडक्शन तत्परता के बीच के अंतर को पाटने के लिए एक स्पष्ट विनिर्देश-संचालित दृष्टिकोण की आवश्यकता होती है।
यह शोध पत्र दो miniKanren लाइब्रेरी कॉम्बिनेटर्स, `prute` और `defrel/bank` को प्रस्तुत करता है, जो गहरे लक्ष्यों (deep targets) पर रिलेशनल प्रोग्राम सिंथेसिस के प्रदर्शन को महत्वपूर्ण रूप से सुधारने के लिए ऑब्जर्वेशनल डिडुप्लिकेशन (observational deduplication) और मेमोइज़ेशन (memoization) के साथ बॉटम-अप एन्यूमरेशन को सक्षम करते हैं, साथ ही उन मामलों को संबोधित करने के लिए एक वेटेड वेरिएंट का भी प्रस्ताव देते हैं जहाँ कैनोनिकल डेप्थ-फर्स्ट ऑर्डरिंग कॉम्पैक्ट रिप्रेजेंटेटिव्स खोजने में विफल रहती है।
यह शोधपत्र एक पूर्णतः कर्नेल-सत्यापित (kernel-verified) लीन 4 (Lean 4) औपचारिकीकरण प्रस्तुत करता है जो यह सिद्ध करता है कि 1 से बड़ी विशिष्ट विषम माड्यूली (odd moduli) द्वारा पूर्णांकों का कोई भी परिमित आवरण (finite covering) का लघुत्तम समापवर्त्य (least common multiple) 10,000 से अधिक होगा, जिससे अनवेरिफाइड कम्प्यूटेशनल सॉल्वर पर निर्भर किए बिना एर्डोस-सेल्फ्रिज ऑड कवरिंग समस्या (Erdős-Selfridge odd covering problem) के लिए एक यांत्रिक रूप से प्रमाणित अपवर्जन (mechanically certified exclusion) स्थापित होता है।
यह शोधपत्र सटीक परिमेय केस-ट्री प्रमाणपत्रों और दो स्वतंत्र चेकरों (एक पायथन में और एक लीन 4 में औपचारिक रूप से सिद्ध) को पेश करके न्यूनतम कोचेन-स्पेक्टर सीमा में एक महत्वपूर्ण सत्यापन अंतराल को समाप्त करता है, जो प्रकाशित ब्लॉकिंग डेटाबेस के सभी 180 विशिष्ट ग्राफों की ज्यामितीय गैर-एम्बेडेबिलिटी को मशीन-सत्यापित करने के लिए है, जिससे अप्रमाणित Z3 निर्णयों को कर्नेल-चेक्ड प्रमेयों से प्रतिस्थापित किया जाता है और साथ ही मूल प्रमाण पाइपलाइन में कई छिपे हुए दोषों और विसंगतियों को उजागर कर उन्हें हल किया जाता है।