1116 पेपर
यह शोध पत्र डेटा पोर्ट्स के माध्यम से परस्पर क्रिया करने वाले एसिंक्रोनस सॉफ्टवेयर घटकों के कंपोजिशनल वेरिफिकेशन के लिए एक नवीन LTL रीराइटिंग दृष्टिकोण प्रस्तावित करता है, जो अर्थ संबंधी समानता को बनाए रखते हुए और फॉर्मूला आकार को अनुकूलित करते हुए स्थानीय गुणों को वैश्विक गुणों में परिवर्तित करके अनंत और परिमित दोनों ट्रेसों को संभालता है।
यह शोध पत्र पैरिटी ऑटोमेटा के माध्यम से पोजीशनल -रेगुलर भाषाओं का पूर्ण अभिलक्षण प्रदान करता है, उनकी बहुपद-समय (polynomial-time) निर्णायकता, विभिन्न लिफ्टिंग गुणों और यूनियन के तहत क्लोजर को स्थापित करता है, जिससे -रेगुलर मामले के लिए कोपज़िन्स्की के अनुमान (Kopczyński's conjecture) का समाधान होता है।
यह शोध पत्र स्ट्रॉन्ग मोनैड्स (strong monads) से पैरामीटराइज्ड मोनैड्स (parameterized monads) तक प्रभावपूर्ण फंक्शन स्पेस (effectful function spaces) वाले कॉल-बाय-वैल्यू (call-by-value) भाषाओं की व्याख्या का सामान्यीकरण करता है, जिससे गार्डेडनेस (guardedness) को केवल एक श्रेणी पर प्रेडिकेट (predicate) के बजाय प्रोग्रामों के एक अंतर्निहित श्रेणीगत गुण (intrinsic categorical property) के रूप में अभिलक्षित किया जाता है।
यह शोध पत्र मील मशीनों (Mealy machines) और पैरामीटराइज्ड स्टॉक-एंड-फ्लो आरेख (parameterized stock-and-flow diagrams) जैसे तात्कालिक प्रणालियों के संयोजन को सक्षम करने के लिए डिपेंडेंट डायरेक्टेड वायरिंग आरेखों (dependent directed wiring diagrams) के एक ऑपेरैड (operad) को प्रस्तुत करता है, जो एक औपचारिक बीजगणितीय ढांचा और एक सिमेंटिक मोर्फिज्म (semantic morphism) प्रदान करता है जो इन आरेखों को मील मशीनों में मैप करता है।
यह शोध पत्र स्पष्ट रूप से स्थापित करता है कि ट्रुथ टेबल (truth table) विचलनों के तहत इष्टतम सर्किट का आकार अधिकतम तक बदलता है, जो सामान्य हैमिंग दूरियों (Hamming distances) तक इस सीमा का विस्तार करता है और पर गहन SAT-आधारित विश्लेषण के माध्यम से इसकी सटीकता की पुष्टि करता है।
यह शोध पत्र एक सामान्य ढांचे को प्रस्तुत करता है जो इनपुट सूत्रों को पूर्व-गणना किए गए सिद्धांत लेम्मा (theory lemmas) के साथ जोड़कर नॉलेज कंपाइलेशन को सैटिस्फिएबिलिटी मॉड्यूल थ्योरीज (SMT) तक विस्तारित करता है ताकि संकलित SMT d-DNNFs की पॉलीटाइम प्रपोजीशनल-शैली की क्वेरी करने में सक्षम बनाया जा सके।
यह शोध पत्र एक सामान्य ढांचा प्रस्तुत करता है जो प्रथम-क्रम सिद्धांतों के फिक्स्ड-नेगेशन (fixed-negation) अंशों के लिए बहुपद-समय (polynomial-time) निर्णायकता की गारंटी देता है, और यह सिद्ध करके अपनी प्रभावकारिता प्रदर्शित करता है कि कमजोर प्रेस्कर अंकगणित (Presburger arithmetic) और संबंधित प्रतिबंधित सिद्धांत कुशल रूप से निर्णायक हैं, जो पूर्ण प्रेस्कर अंकगणित के अधिक प्रतिबंधित अंशों की एनपी-कठोरता (NP-hardness) के विपरीत है।
यह शोध पत्र पहला ऐसा एल्गोरिदम प्रस्तुत करता है जो, एक धनात्मक प्रथम-क्रम वाक्य (first-order sentence) दिए जाने पर, विशिष्ट वाक्य-रचनात्मक पुनलेखन नियमों (syntactic rewriting rules) के एक विशिष्ट सेट को लागू करके इसके न्यूनतम-चौड़ाई वाले तार्किक रूप से तुल्य रूप की गणना करता है, जिससे टर्म रीराइटिंग (term rewriting), क्वेरी इवैल्यूएशन (query evaluation) और स्ट्रक्चरल डिकंपोजिशन (structural decomposition) सिद्धांतों के अभिसरण के माध्यम से चौड़ाई न्यूनीकरण (width minimization) की एक पूर्ण एल्गोरिद्मिक समझ स्थापित होती है।
यह शोध पत्र एक नवीन हाइब्रिड दृष्टिकोण प्रस्तुत करता है जो ग्राफ एपीआई (Graph APIs) में प्रत्यक्ष और अप्रत्यक्ष दोनों प्रकार के टूटे हुए एक्सेस कंट्रोल (broken access control) भेद्यताओं को व्यवस्थित रूप से खोजने के लिए स्टैटिक ग्राफ ट्रांसफॉर्मेशन-आधारित टेइंट विश्लेषण (taint analysis) को डायनेमिक वेरिफिकेशन के साथ जोड़ता है, जैसा कि GitHub GraphQL API पर इसके अनुप्रयोग के माध्यम से प्रदर्शित किया गया है।
यह शोध पत्र FATE को प्रस्तुत करता है, जो स्नातक स्तर के अभ्यासों से लेकर पीएचडी स्तर की अनुसंधान समस्याओं तक विस्तृत एक नई औपचारिक बीजगणित बेंचमार्क श्रृंखला है, जो यह प्रकट करती है कि वर्तमान अत्याधुनिक LLMs उन्नत गणितीय तर्क को औपचारिक रूप देने में काफी संघर्ष करते हैं, और बेहतर प्राकृतिक-भाषा प्रदर्शन के बावजूद सबसे कठिन कार्यों पर शून्य के करीब सटीकता प्राप्त करते हैं।