1115 पेपर
यह शोधपत्र डिपेंडेंट टाइप थ्योरी में कंपोजिशनल प्रोग्राम वेरिफिकेशन के लिए एक फ्रेमवर्क प्रस्तुत करता है जो इंटरफेस, इम्प्लीमेंटेशन और स्पेसिफिकेशन को मॉडल करने के लिए पॉलिनॉमियल फंक्टर्स का उपयोग करता है, और यह प्रदर्शित करता है कि कैसे ये घटक वायरिंग डायग्राम और मील मशीनों के माध्यम से कंपोज़ होते हैं जबकि इन्हें एगडा (Agda) में पूर्ण रूप से औपचारिक बनाया गया है।
यह शोध पत्र लीन-एजेंट प्रोटोकॉल (Lean-Agent Protocol) प्रस्तुत करता है, जो एक औपचारिक सत्यापन प्रणाली है जो लीन 4 (Lean 4) प्रमेय सिद्ध करने का उपयोग करती है ताकि गणितीय रूप से यह गारंटी दी जा सके कि स्वायत्त वित्तीय एआई (AI) क्रियाएं सख्त नियामक आवश्यकताओं का अनुपालन करती हैं, जिससे अपर्याप्त संभाव्य गार्डरेल्स (probabilistic guardrails) को नियतात्मक, क्रिप्टोग्राफिक रूप से सत्यापन योग्य सुरक्षा से प्रतिस्थापित किया जा सके।
यह शोध पत्र टू-डायमेंशनल सिंगल स्टॉक साइज कटिंग स्टॉक समस्या के लिए एक SAT-आधारित ढांचे को प्रस्तुत करता है जो डिमांड एक्सपेंशन, ओरिएंटेशन एलिमिनेशन और विभिन्न सॉल्विंग रणनीतियों का उपयोग करता है ताकि बेंचमार्क इंस्टेंस पर अनुकूलता (optimality) प्रमाणित करने और गैप्स को कम करने में OR-Tools, CPLEX और Gurobi जैसे वाणिज्यिक सॉल्वर की तुलना में महत्वपूर्ण रूप से बेहतर प्रदर्शन किया जा सके।
यह शोध पत्र -वेरिएबल, क्वांटिफायर-रैंक- वाले काउंटिंग लॉजिक के अभिव्यंजक सामर्थ्य को -पेबल फॉरेस्ट कवर्स की गहराई वाले ग्राफ्स पर होमोमोर्फिज्म अविभेद्यता (homomorphism indistinguishability) के माध्यम से अभिलक्षित करता है, जो यह सिद्ध करता है कि यह वर्ग बाउंडेड ट्रीविड्थ (bounded treewidth) और बाउंडेड ट्रीडेप्थ (bounded treedepth) ग्राफ्स के प्रतिच्छेदन से भिन्न है और एक नवीन मोनोटोनिक कॉप्स-एंड-रोबर्स गेम विश्लेषण के माध्यम से रोबर्सन के उस अनुमान की पुष्टि करता है कि ये वर्ग होमोमोर्फिज्म डिस्टिंग्विशिंग क्लोज्ड (homomorphism distinguishing closed) हैं।
यह शोध पत्र क्वांटम बाधाओं के समाधान (quantum constraint satisfaction) के लिए एक बीजगणितीय ढांचे को स्थापित करने हेतु क्वांटम पॉलीमॉर्फिज्म की अवधारणा प्रस्तुत करता है, जो कम्यूटेटिविटी गैजेट्स (commutativity gadgets) का पूर्णतः लक्षण वर्णन करता है और विषम चक्रों (odd cycles) तथा सिग्र्स क्लॉज़ (Sigglers clauses) द्वारा पैरामीटराइज़्ड विशिष्ट क्वांटम CSPs की अनडिसाइडेबिलिटी (undecidability) को सिद्ध करता है।
यह शोध पत्र LLM-संचालित सूचना प्रणालियों के लिए एक एकीकृत आर्किटेक्चर मेटामॉडल का प्रस्ताव करता है जो कोड और दस्तावेज़ीकरण के बीच स्थिर, दोहराने योग्य और उच्च-गुणवत्ता वाले क्लोज्ड-लूप रूपांतरणों को सक्षम करने के लिए व्यावसायिक, सिस्टम और डेवलपर परतों में प्रमुख आर्किटेक्चरल आरेखों को व्यवस्थित करता है।
यह शोध पत्र एक मॉड्यूलर फ्रेमवर्क और डियोन्टिक STIT लॉजिक के लिए सुदृढ़, पूर्ण अनुक्रम कैलकुली (sequent calculi) प्रस्तुत करता है जो 'ओट-इम्प्लाइज-कैन' (Ought-implies-Can) सिद्धांत की दस विशिष्ट व्याख्याओं के बीच तार्किक संबंधों को औपचारिक रूप देता है, तुलना करता है और उनका विश्लेषण करता है।
यह शोध पत्र सीमित विन्यासों (bounded configurations) पर व्युत्क्रम सेलुलर ऑटोमेटा (inverse cellular automata) के लिए इंजेक्टिविटी (injectivity) निर्धारित करने की co-NP-पूर्णता का एक सरलीकृत प्रमाण प्रदान करता है और पेरिस-विल्की अनुवाद (Paris–Wilkie translation) के माध्यम से बाउंडेड-डेप्थ फ्रेगे सिस्टम्स (bounded-depth Frege systems) के ज्ञात निचले स्तरों को स्थानांतरित करके उनके प्रस्तावात्मक प्रमाणों (propositional proofs) के आकार पर निचले स्तर स्थापित करता है।
यह शोधपत्र XOR-SMOO को प्रस्तुत करता है, जो एक नवीन एल्गोरिदम है जो SAT ओरेकल और रैंडमाइजेशन का लाभ उठाकर स्टोकेस्टिक मल्टी-ऑब्जेक्टिव ऑप्टिमाइज़ेशन में उच्च प्रायिकता के साथ कॉन्स्टेंट-फैक्टर एप्रोक्सिमेशन गारंटी प्राप्त करने के लिए पारेटो फ्रंटियर्स का कुशलतापूर्वक अनुमान लगाता है, जो कम्प्यूटेशनल दक्षता और समाधान की गुणवत्ता दोनों में मौजूदा विधियों से काफी बेहतर प्रदर्शन करता है।
यह शोध पत्र रिवॉर्ड-सेंसिटिव (इनाम-संवेदनशील) बिसिमिलरिटीज़ (समरूपता) को मॉडल करने के लिए फाइब्रेशनल और ग्लूइंग तकनीकों का उपयोग करते हुए एक एकीकृत को-अल्जेब्रिक ढांचे को प्रस्तुत करता है जो गुणात्मक और मात्रात्मक पहलुओं को सहजता से एकीकृत करता है, जिससे संबंध-आधारित और मीट्रिक-आधारित बिसिमिलरिटीज़ जैसे विभिन्न मौजूदा धारणाओं का सामान्यीकरण होता है।