1086 पेपर
यह शोध पत्र यह प्रदर्शित करता है कि बड़े भाषा मॉडलों का बाधा तर्क (constraint reasoning) कार्यों पर प्रदर्शन समस्या के उदाहरणों की अंतर्निहित सॉल्वर जटिलता (solver hardness) द्वारा निर्धारित नहीं होता है, जैसा कि सावधानीपूर्वक नियंत्रित, घनत्व-मिलान वाले बेंचमार्क में प्रूफ़-कठोरता प्रॉक्सी (proof-hardness proxies) और मॉडल सटीकता या टोकन व्यय के बीच सहसंबंध की कमी से सिद्ध होता है।
यह शोध पत्र न्यूरल नेटवर्क सत्यापन के लिए एक सामान्य लुकअहेड ब्रांचिंग रणनीति प्रस्तुत करता है जो ब्रांच-एंड-बाउंड वेरीफायर को बेहतर निर्णय लेने और अतिरिक्त लेम्मा उत्पन्न करने में सुधार करके मौजूदा वेरीफायर को उन्नत करता है, जिसके परिणामस्वरूप निरंतर गति वृद्धि और 57% तक अधिक हल किए गए उदाहरण प्राप्त होते हैं।
यह शोध पत्र एक अमूर्त सिंक्रोनस परमाणु बीजगणित (abstract synchronous atomic algebra) के भीतर उन्हें स्थापित करके और यह प्रदर्शित करके कि कमांड रूपों को प्रतिबंधित करना बीजगणितीय तर्क के लिए मजबूत समानता नियमों को सक्षम करता है, एक रिलाय-गारंटी (rely-guarantee) समवर्ती ढांचे के भीतर समानांतर संयोजन (parallel composition) के लिए वितरणात्मक नियमों (distributive laws) को विकसित और औपचारिक रूप देता है।
यह खंड 42वें अंतर्राष्ट्रीय लॉजिक प्रोग्रामिंग सम्मेलन (ICLP 2026) के कार्यवाही विवरण को प्रस्तुत करता है, जो जुलाई 2026 में लिस्बन में आयोजित किया गया था, जिसमें मुख्य और हाल ही में प्रकाशित अनुसंधान ट्रैक्स दोनों से सैद्धांतिक आधार, भाषा डिजाइन, प्रोग्राम विश्लेषण और अनुप्रयोगों पर तकनीकी संचार और विस्तृत सार शामिल हैं।
यह शोध पत्र निरंतर-चर क्वांटम कंप्यूटिंग (CQC) के लिए पहला औपचारिक सिमेंटिक्स और होअर लॉजिक स्थापित करता है ताकि अनंत-आयामी हिल्बर्ट स्पेस और अनबाउंडेड मेजरमेंट आउटकम्स द्वारा उत्पन्न चुनौतियों को दूर किया जा सके, जिससे एक नए कार्यान्वित सिम्बोलिक वीकेस्ट-प्रीकंडिशन कैलकुलेटर के माध्यम से CQC प्रोग्रामों, गेट डिकम्पोज़िशन और संसाधन आवश्यकताओं का सत्यापन सक्षम हो सके।
यह शोध पत्र स्थानीय सारणीबद्धता (local tabularity) और बिज़िमुलशन खेलों (bisimulation games) का उपयोग करते हुए विशिष्ट प्रेडिकेटल मोडल लॉजिक के अंशों के लिए निर्णय क्षमता (decidability) के परिणामों को स्थापित करने हेतु, S5 के साथ प्रपोजीशनल मोडल लॉजिक के उत्पादों और अर्ध-उत्पादों (semiproducts) के अभिलेखन (axiomatization) और परिमित मॉडल गुण (finite model property) के संबंध में नए उदाहरण और प्रति-उदाहरण प्रस्तुत करता है।
यह शोध पत्र समय-संवेदनशील महत्व विभाजन (importance splitting) के लिए दूरी मेट्रिक्स का एक वर्गीकरण प्रस्तावित करता है जो महत्व को विशिष्ट नमूनों से अलग करने के लिए टाइमर रीसैंपलिंग को पेश करके और अनुत्पादक सिमुलेशन पथों को छाँटने के लिए वैश्विक आयु (global age) का उपयोग करके दुर्लभ घटना संभाव्यता अनुमान को बढ़ाता है।
यह शोध पत्र उपयोगकर्ता द्वारा प्रदान किए गए संचार विनिर्देशों (communication specifications) का उपयोग करके नियतात्मक पैरामीटराइज्ड MPI प्रोग्रामों को अनुक्रमिक (sequential) प्रोग्रामों में रूपांतरित करके उन्हें सत्यापित करने की एक विधि प्रस्तुत करता है, जिसे C/MPI कोड के लिए Frama-C/WP के एक विस्तार के रूप में कार्यान्वित किया गया है।
यह शोध पत्र स्ट्रॉन्ग फंक्टर्स (strong functors) के एक द्वैत के रूप में कोस्ट्रॉन्ग फंक्टर्स (costrong functors) की अवधारणा प्रस्तुत करता है, जो यह प्रदर्शित करता है कि उनकी कोस्ट्रेंथ (costrength) ग्रेडेड डिस्ट्रिब्यूटिव लॉज़ (graded distributive laws) के अनुरूप है और एंडोफंक्टर्स (endofunctors) तथा मोनाड्स (monads) के बीच के संबंध को ग्रेडेड सेटिंग में सामान्यीकृत करती है, जिसके ऑप्टिक्स (optics) और कोएल्जेब्रा (coalgebras) में अनुप्रयोग हैं।
यह शोध पत्र टोपोस कॉज़ल मॉडल्स (topos causal models) का क्यूबिकल एगडा (Cubical Agda) में पहला मशीन-चेक्ड फॉर्मलाइजेशन प्रस्तुत करता है, जो विशेषतात्मक मानचित्रों (characteristic maps) के रूप में हस्तक्षेप और शीफ ग्लूइंग (sheaf gluing) जैसी मुख्य अवधारणाओं को सत्यापित करता है, साथ ही पर्ल के नियमों की स्थिरता स्थापित करने के लिए लॉवरे-टायनी (Lawvere-Tierney) अभिगृहीतों में एक अंतराल की पहचान और मरम्मत करता है, और एक सुरक्षित, अक्षोमित (axiom-free) ढांचे के भीतर एक संदर्भता बाधा (contextuality obstruction) को प्रदर्शित करता है।