1117 पेपर
यह शोध पत्र मनमाने अरिटी (arity) वाले अनंत वृक्षों (infinite trees) के लिए EU-automata प्रस्तुत करता है, उनके एल्गोरिद्मिक गुणों और जटिलता सीमाओं (complexity bounds) को स्थापित करता है, और QCTL एवं MSO के लिए इष्टतम निर्णय प्रक्रियाओं (optimal decision procedures) और क्वांटिफायर अल्टरनेशन रिडक्शन परिणामों को प्राप्त करने के लिए उनका लाभ उठाता है।
यह शोध पत्र डिटरमिनिस्टिक और नॉन-डिटरमिनिस्टिक ब्रांचिंग प्रोग्राम्स के लिए प्रूफ सिस्टम्स को कैरेक्टराइज़ करने हेतु पुडलाक-बस शैली के प्रूवर-एडवर्सरी गेम्स पेश करता है, जो इन गेम्स और eLDT एवं eLNDT प्रूफ सिस्टम्स के बीच पॉलिनॉमियल इक्विवेलेंस स्थापित करते हुए इमरमैन-सेलेप्सेनीي थ्योरम का एक प्रूफ कॉम्प्लेक्सिटी वर्ज़न व्युत्पन्न करता है।
यह शोध पत्र एक उपयुक्त स्टार ऑपरेशन को परिभाषित करके सामान्यीकृत मोबियस श्रेणियों (generalised Möbius categories) पर कन्वोल्शन क्लीनी बीजगणित (convolution Kleene algebras) के लिए एक निर्माण स्थापित करता है, जिससे भारित (weighted), संभाव्य (probabilistic) और समवर्ती (concurrent) कार्यक्रमों के साथ-साथ उच्च-आयामी पुनर्लेखन (higher-dimensional rewriting) के लिए बीजगणितीय तर्क और सत्यापन सक्षम होता है।
यह शोध पत्र LeanCat को प्रस्तुत करता है, जो Lean में औपचारिक श्रेणी सिद्धांत (category theory) के 100 कार्यों का एक बेंचमार्क सूट है, जो वर्तमान बड़े भाषा मॉडलों (large language models) में एक गंभीर अमूर्तता अंतराल (abstraction gap) को उजागर करता है, और यह प्रदर्शित करता है कि लाइब्रेरी-आधारित, उच्च-स्तरीय गणितीय तर्क में सार्थक प्रगति प्राप्त करने के लिए LeanBridge जैसे रिट्रीवल-ऑगमेंटेड एजेंट अनिवार्य हैं।
यह शोध पत्र एक तर्क-आधारित व्याख्यात्मकता पद्धति प्रस्तावित करता है जिसमें शुद्धता की गारंटी है जो ह्यूरिस्टिक दृष्टिकोणों की तुलना में 100% स्पष्टीकरण निष्ठा और बेहतर सुदृढ़ता प्राप्त करती है, जिससे क्लिनिकल विश्वास बढ़ता है और चागास कार्डियोमायोपैथी वाले रोगियों में अचानक कार्डिएक डेथ की भविष्यवाणी करने वाले एआई-संचालित उपकरणों की तैनाती को सुगम बनाया जा सकता है।
यह शोध पत्र लेयर्ड मोनोइडल थ्योरीज़ (layered monoidal theories) के लिए फिब्रेनेशनल (fibrational), ओफिब्रेशनल (opfibrational), और डिफ्लेशनल (deflational) मॉडल्स प्रस्तुत करता है, जो ग्रोटेंडिक फिब्रेशन्स (Grothendieck fibrations) और डिस्प्लेड कैटेगरीज (displayed categories) जैसी स्थापित कैटेगोरिकल संरचनाओं के साथ संबंध स्थापित करते हुए उनकी साउंडनेस (soundness) और कम्प्लीटनेस (completeness) को सिद्ध करता है।
यह शोध पत्र RustyDL को प्रस्तुत करता है, जो एक नवीन स्रोत-स्तरीय प्रोग्राम लॉजिक (source-level program logic) है जिसे रस्ट (Rust) प्रोग्राम्स के मानव-इन-द-लूप (human-in-the-loop) निगमनात्मक सत्यापन (deductive verification) को सक्षम करने के लिए डिज़ाइन किया गया है, जो विशिष्ट भाषा संबंधी चुनौतियों का समाधान करता है और KeY सत्यापन टूल के भीतर एक प्रोटोटाइप कार्यान्वयन के माध्यम से इसकी व्यवहार्यता को प्रदर्शित करता है।
यह शोध पत्र न्यूरल नेटवर्क के लिए तर्क-आधारित स्पष्टीकरणों की स्केलेबिलिटी को बढ़ाने के लिए एक डोमेन स्लाइसिंग दृष्टिकोण प्रस्तावित करता है, जो तुलनात्मक प्रयोगों के माध्यम से स्पष्टीकरण समय में 40% तक की कमी प्रदर्शित करता है।
यह शोध पत्र एक तर्क-आधारित व्याख्यात्मक एआई (explainable AI) प्रणाली प्रस्तुत करता है जो न्यूनतम जोखिम कारकों की पहचान करके और नैदानिकों को रोगियों के हृदय रोग संबंधी जोखिम को समझने और कम करने में मदद करने के लिए कार्रवाई योग्य परिदृश्य उत्पन्न करके फ्रैमिंघम रिस्क स्कोर की पारदर्शिता को बढ़ाता है।
यह शोध पत्र यह सिद्ध करके एक खुले प्रश्न का समाधान करता है कि गार्डेड मोनोटोन स्ट्रिक्ट NP (GMSNP) के लिए कंटेनमेंट (containment) और FO-रीराइटेबिलिटी (FO-rewritability) समस्याएँ 2NEXPTIME ऊपरी सीमा के साथ निर्णायक (decidable) हैं, जिसे -कैटेगोरिकल संरचनाओं पर CSPs के परिमित संघों (finite unions) के रूप में GMSNP वाक्यों के मॉडल-सैद्धांतिक लक्षण वर्णन को परिष्कृत करके और कंटेनमेंट को रीकलरिंग अस्तित्व समस्या (recolouring existence problem) में बदलकर प्राप्त किया गया है।