1105 पेपर
यह शोध पत्र MathlibPR को प्रस्तुत करता है, जो वास्तविक Lean/Mathlib4 पुल रिक्वेस्ट इतिहास से प्राप्त एक बेंचमार्क है, जिसका उद्देश्य LLMs और एजेंटों की मर्ज-तैयार योगदानों से गैर-मर्ज किए गए योगदानों के बीच अंतर करने की क्षमता का मूल्यांकन करना है, जो उनकी वर्तमान संघर्षों को प्रकट करता है और रिव्यूअर असिस्टेंट और रिवॉर्ड मॉडल विकसित करने के लिए इस बेंचमार्क की क्षमता को उजागर करता है।
यह शोध पत्र पिकोलो (Piccolo) को प्रस्तुत करता है, जो एक नवीन रिलाय-गारंटी (rely-guarantee) ढांचा है जो किसी भी स्वयंसिद्ध स्मृति मॉडल (axiomatic memory model) के लिए कंपोजिशनल रीजनिंग को सामान्य बनाता है और विशेष रूप से एक क्षमता-आधारित परिचालन अर्थविज्ञान (potential-based operational semantics) और थ्रेड अवस्थाओं के क्रमबद्ध अनुक्रमों को निर्दिष्ट करने में सक्षम एक अभिकथन भाषा का उपयोग करके कॉज़ली कंसिस्टेंट (causally consistent) शेयर्ड मेमोरी के लिए पहली प्रमाण तकनीक प्रदान करता है।
AutoQ 2.0 एक उन्नत विवरक (verifier) है जो क्लासिकल कंट्रोल फ्लो से संबंधित सैद्धांतिक और इंजीनियरिंग चुनौतियों का समाधान करके क्वांटम सर्किट सत्यापन को पूर्ण क्वांटम प्रोग्रामों तक विस्तारित करता है, जिसने रिपीट-अनटिल-सक्सेस और वीक-मेज़रमेंट-आधारित ग्रोवर सर्च जैसे जटिल एल्गोरिदम पर अपनी दक्षता को सफलतापूर्वक प्रदर्शित किया है।
यह शोधपत्र समानता के साथ प्रथम- और द्वितीय-क्रम की निर्भरताओं के लिए पहली लक्ष्य-संचालित क्वेरी उत्तर देने वाली तकनीक प्रस्तुत करता है, जो अप्रासंगिक निष्कर्षों से बचने के लिए एक संशोधित सिंगुलराइजेशन वेरिएंट, एक प्रासंगिकता विश्लेषण और एक मैजिक सेट्स अनुकूलन को जोड़कर क्वेरी प्रोसेसिंग को महत्वपूर्ण रूप से तेज करता है।
यह लेख यह प्रदर्शित करके कि एक मोनोटोन (monotone) DNF को पदों के साथ बनाया जा सकता है और साथ ही यह दिखाते हुए कि के कुछ मानों के लिए पदों की आवश्यकता होती है, ठीक संतुष्ट असाइनमेंट (satisfying assignments) वाला एक DNF या CNF फॉर्मूला बनाने के लिए आवश्यक पदों या क्लॉज़ (clauses) की न्यूनतम संख्या पर नए ऊपरी और निचले बंधन (upper and lower bounds) स्थापित करता है।
यह शोध पत्र "एक्सप्रेगुलर फंक्शन्स" (expregular functions) को प्रस्तुत करता है, जो तीन तुल्य मॉडलों (MSO सेट व्याख्याओं, यील्ड-हेनी मशीनों और एरिआडने ट्रांसड्यूसरों) द्वारा परिभाषित घातांकीय वृद्धि वाले स्ट्रिंग-टू-स्ट्रिंग फलनों का एक सुदृढ़ वर्ग है, और यह सिद्ध करने के लिए उनकी तुल्यता को प्रमाणित करता है कि MSO सेट व्याख्याएं नियमितता परावर्तक (regularity reflecting) हैं, जिससे ऑटोमैटिक -शब्दों के गणनीय MSO सिद्धांत से संबंधित एक प्रमुख अनुमान का समाधान होता है।
यह शोधपत्र स्पाइडर आरेख (spider diagrams) का उपयोग करते हुए ग्रीमास अर्धविज्ञानी वर्ग (Greimas semiotic square) के लिए एक आरेखीय प्रमाण-सिद्धांतिक अर्थविज्ञान प्रस्तुत करता है, जिसमें मेटा-पद निर्माण को एक रचनात्मक व्युत्पत्ति प्रक्रिया के रूप में पकड़ा गया है और निषेध को एक बूलियन पूरक के बजाय एक प्रतिबंधित अर्थपूर्ण प्रति-स्थिति के रूप में पुनर्व्याख्यायित किया गया है।
यह शोध पत्र एक विस्तारित सेट-आधारित विनिर्देश भाषा (set-based specification language) और एक रैखिक-जटिलता वाले अनुवाद एल्गोरिदम को प्रस्तुत करता है जो पूर्व ऑटोमेटा-आधारित दृष्टिकोणों में निहित घातांकीय विस्फोट (exponential blow-up) से बचकर क्वांटम प्रोग्रामों के पूर्णतः स्वचालित, स्केलेबल होअर-शैली (Hoare-style) सत्यापन को सक्षम बनाता है।
यह शोधपत्र स्व-सुधारात्मक गॉसिप प्रोटोकॉल के लिए एक डायनेमिक एपिस्टेमिक लॉजिक फ्रेमवर्क प्रस्तावित करता है जो वितरित प्रणालियों को केंद्रीय समन्वय के बिना स्वायत्त रूप से ट्रांसमिशन त्रुटियों को सुधारने में सक्षम बनाता है, जबकि इसके परिणामस्वरूप होने वाले अनुकूलन (ऑप्टिमलिटी) पर प्रभावों का विश्लेषण करता है और बाउंडेड मेमोरी एवं फुल इंफॉर्मेशन प्रोटोकॉल के साथ दृष्टिकोण की तुलना करता है।
यह शोध पत्र परिमित-मान वाले ट्रांसड्यूसर्स (finite-valued transducers) के लिए एडिट डिस्टेंस की गणनीयता (computability) को स्थापित करता है, जो कार्यात्मक ट्रांसड्यूसर्स (functional transducers) के लिए पहले से ज्ञात परिणाम का विस्तार एक अधिक अभिव्यंजक वर्ग तक करता है।