1090 पेपर
यह शोध पत्र LLM-सॉल्वर लूप्स में "नैरेशन गैप" (कथा अंतराल) की पहचान और विश्लेषण करता है, यह प्रदर्शित करते हुए कि जबकि औपचारिक सॉल्वर सटीक निर्णय प्रदान करते हैं, परिणामों को उपयोगकर्ताओं को सुनाने का अंतिम चरण प्रॉम्प्ट इंजेक्शन और एडेप्टिव हमलों के प्रति संवेदनशील बना रहता है, जिससे सिस्टम के आउटपुट की समग्र सुदृढ़ता से समझौता होता है।
BARReL एक मॉड्यूलर Lean 4 लाइब्रेरी है जो औद्योगिक Atelier B टूल को Lean प्रूफ़ असिस्टेंट के साथ जोड़ती है, जो B के आंशिक ऑपरेटरों (partial operators) को स्पष्ट रूप से सुपरिभाषित स्थितियों के साथ एनकोड करके ऐसा करती है, जिससे एक सुदृढ़ विश्वसनीय ढांचे के भीतर मशीन रिफाइनमेंट्स के इंटरैक्टिव, सिंटैक्स-संरक्षण औपचारिक विकास और सत्यापन को सक्षम बनाया जा सके।
यह शोधपत्र यह सिद्ध करके कि मोनैडिक सेकंड-ऑर्डर लॉजिक (Monadic Second-Order logic) ट्रेewidth बाउंड्स के माध्यम से विभिन्न मेमोरी मॉडलों (जैसे कि Release/Acquire और RC20) को समान रूप से स्वयंसिद्ध (axiomatize) और सत्यापित कर सकता है, साथ ही TSO जैसे अन्य मॉडलों के लिए अंतर्निहित सीमाओं की पहचान करता है और 'रीड्स-फ्रॉम' (reads-from) सुदृढ़ता को एक प्रमुख एल्गोरिद्मिक मानदंड के रूप में प्रस्तुत करता है, वीक-मेमोरी सत्यापन के लिए एक बहुमुखी सैद्धांतिक ढांचा स्थापित करता है।
यह शोध पत्र रेसिजुएटेड लैट्टिस (residuated lattices) द्वारा मॉडल किए गए फर्स्ट-ऑर्डर सबस्ट्रक्चरल लॉजिक्स के संदर्भ में शास्त्रीय हान्फ (Hanf) और गाइफ़मैन (Gaifman) लोकैलिटी थीोरम्स की वैधता की जांच करता है, यह प्रदर्शित करते हुए कि जबकि हान्फ के प्रमेय के लिए विशिष्ट बीजगणितीय शर्तों और लोकैलिटी की वैकल्पिक परिभाषाओं की आवश्यकता होती है, गाइफ़मैन के प्रमेय के मूल लेम्मा को एक ऑर्डर-इंटरप्रेटिंग कनेक्टिव (order-interpreting connective) द्वारा सक्षम बैक-एंड-फॉरथ सिस्टम के सिंटैक्टिक एनकोडिंग के माध्यम से सुव्यवस्थित बीजगणितों के लिए पुनः प्राप्त किया जा सकता है।
यह शोधपत्र यह प्रदर्शित करता है कि एक प्रतिपादित अंतराल प्रकार (interval type) के साथ सिमप्लिशियल टाइप थ्योरी को होमोटॉपी टाइप थ्योरी के रूप में सूत्रबद्ध किया जा सकता है, यह सिद्ध करके कि प्रकारों की वाइल्ड कैटेगरी (wild category) में लीबनीज़ एडजंक्शन (Leibniz adjunction) के माध्यम से -हॉर्न के लिए अद्वितीय फिलर्स (unique fillers), सभी इनर हॉर्न के लिए अद्वितीय फिलर्स का निहितार्थ करते हैं, जो कि क्यूबिकल अगडा (Cubical Agda) में औपचारिक रूप दिया गया एक परिणाम है।
यह शोध पत्र TLA+ और Verus का उपयोग करके मल्टी-एजेंट LLM सिस्टम के लिए एक सख्त कंसिस्टेंसी पदानुक्रम (consistency hierarchy) को औपचारिक रूप से मॉडल और यांत्रिक रूप से सत्यापित करता है, जो साउंड डिटेक्टर्स और रोकथाम तंत्र पेश करता है जो कई तैनात रस्ट (Rust) रनटाइम्स और वास्तविक दुनिया के फ्रेमवर्क्स में चार विशिष्ट कंकरेंसी विसंगतियों (concurrency anomalies) को समाप्त करते हैं।
यह शोध पत्र स्टोन-चेच कॉम्पैक्टिफिकेशन (Stone-Čech compactification) पर आधारित एक संग्रहणीय सिमेंटिक्स (collecting semantics) प्रस्तुत करता है जो गैर-समाप्त होने वाली गणनाओं के अवशिष्ट व्यवहार (residual behavior) के लिए है, जो CCS जैसे सिस्टम में पुनरावृत्ति (recurrence), पलायन (escape) और विचलन (divergence) के विश्लेषण को एक ऐसे ढांचे के माध्यम से एकीकृत करता है जो टेम्पोरल लॉजिक और रिलेशनल कोरिलेशन को संरक्षित करता है और साथ ही परिमित अवलोकन संबंधी कोटिएंट्स (finite observational quotients) के माध्यम से व्यावहारिक गणना को सक्षम बनाता है।
यह शोधपत्र 'ओपन इंडक्शन' (open induction) और 'कॉज़ सेट साइकिल्स' (clause set cycles) की तुलनीयता के संबंध में एक खुले प्रश्न को हल करता है, यह प्रदर्शित करते हुए कि सिंटैक्टिक सिस्टम (syntactic systems) निरंतर क्रम (constant ordering) के बारे में संख्यात्मक तथ्यों तक पहुँचने में अपनी अक्षमता के कारण सिमेंटिक इनवेरियंट्स (semantic invariants) को सिद्ध करने में विफल रहते हैं, जो एक ऐसी सीमा है जिसे लेखक एक "सिंटैक्टिक इनवेरियन्स प्रिंसिपल" (Syntactic Invariance Principle) के रूप में सामान्यीकृत करते हैं और अनुमान लगाते हैं कि यह बनाम समस्या में ज्ञात बाधाओं का आधार हो सकता है।
यह शोध पत्र यूनिफाइड मार्कोव बाइनरी (UMB) प्रारूप प्रस्तुत करता है, जो एक कुशल और विस्तार योग्य बाइनरी फ़ाइल मानक है जिसे संभाव्य मॉडल चेकिंग में अंतर-संचालनीयता की बाधाओं को दूर करने के लिए डिज़ाइन किया गया है, जो संभाव्य प्रणालियों का एक एकीकृत, निम्न-स्तरीय प्रतिनिधित्व प्रदान करता है जिसे प्रमुख उपकरणों द्वारा पहले से ही अपनाया गया है और एक व्यापक पायथन लाइब्रेरी द्वारा समर्थित है।
यह शोधपत्र न्यूरोसिम्बोलिक इन्फरेंस (neurosymbolic inference) के लिए एक होमोटोपी टाइप थ्योरी (homotopy type theory) फ्रेमवर्क प्रस्तावित करता है जो संरचनात्मक समरूपताओं (structural symmetries) और प्रमाण बहुलता (proof multiplicities) को ध्यान में रखने के लिए पारंपरिक सेट-आधारित दृष्टिकोणों का सामान्यीकरण करता है, जिससे तर्क संबंधी शॉर्टकट (reasoning shortcuts) हल होते हैं और एक समरूपता-अपरिवर्तनीय (symmetry-invariant), क्लोज्ड-फॉर्म औसत पद्धति के माध्यम से अंशांकन (calibration) में सुधार होता है।