1086 पेपर
यह शोध पत्र एक रस्ट (Rust) वेरीफायर में कार्यान्वित एक नवीन परिशोधन तकनीक प्रस्तुत करता है जो संरचना, प्रदर्शन और प्रमाण लचीलेपन में मौजूदा सीमाओं को दूर करती है, जिससे घोस्ट लॉक्स (ghost locks) के उपयोग के माध्यम से कुशल, निष्पादन योग्य प्रोग्रामों के लिए सुरक्षा और जीवंतता (liveness) दोनों गुणों के सत्यापन को सक्षम बनाया जा सके।
यह शोध पत्र JustAct को प्रस्तुत करता है, जो अंतर-संगठनात्मक नीतियों द्वारा विनियमित ऑडिट करने योग्य मल्टी-एजेंट सिस्टम के लिए एक ढांचा है, जो डायनेमिक पॉलिसी जस्टिफिकेशन के माध्यम से गैर-खंडनीय अनुमति निर्णयों की गारंटी देता है, जिसे एक रस्ट (Rust) कार्यान्वयन और एक मेडिकल डेटा प्रोसेसिंग केस स्टडी के माध्यम से मान्य किया गया है।
यह शोध पत्र NCPO को प्रस्तुत करता है, जो बीटा-एटा-नॉर्मल फॉर्म्स पर हायर-ऑर्डर रीराइटिंग को संभालने के लिए विस्तारित एक कंप्यूटेबिलिटी पाथ ऑर्डर है, जो NHORPO की तुलना में इसकी बेहतर व्यावहारिक प्रभावशीलता और SAT/SMT सॉल्वर के माध्यम से इसके स्वचालन की सुगमता को प्रदर्शित करता है।
यह शोध पत्र एक केस स्टडी प्रस्तुत करता है जहाँ एक गणितज्ञ एक AI सिस्टम को लीन 4 (Lean 4) में व्लासोव समीकरण (Vlasov equation) के मीन-फील्ड व्युत्पन्न (mean-field derivation) को औपचारिक रूप देने के लिए निर्देशित करता है, जो इस प्रक्रिया को एक "रणनीति खेल" (strategy game) के रूप में फ्रेम करता है जिसने लगभग एक महीने के भीतर सफलतापूर्वक एक पूर्ण, अक्षम-मुक्त (axiom-clean) प्रमाण और एक पुन: प्रयोज्य ऑप्टिमल-ट्रांसपोर्ट लाइब्रेरी का निर्माण किया।
यह शोध पत्र Diversify2Verify पेश करता है, जो एक LLM-आधारित पाइपलाइन है जो यह प्रदर्शित करती है कि कैसे विविध, कार्य-तुल्य प्रोग्राम कार्यान्वयन उत्पन्न करना स्वचालित सत्यापन सफलता दरों में महत्वपूर्ण सुधार करता है, उन वेरिएंट्स की पहचान करके जो औपचारिक प्रमाण (formal proof) के लिए अधिक अनुकूल हैं।
यह शोध पत्र एक उच्च-क्रम रैखिक क्वांटम कार्यात्मक भाषा (higher-order linear quantum functional language) प्रस्तुत करता है जो एक कारण-अनुशासित प्रकार प्रणाली (causally disciplined type system) और परिचालन अर्थविज्ञान (operational semantics) से सुसज्जित है जो अनिश्चित कारण क्रमों (indefinite causal orders) की पूर्ण कम्प्यूटेशनल शक्ति को निष्ठापूर्वक कैप्चर करता है, जिसमें सामान्य क्वांटम चैनलों और मापन पर सुसंगत नियंत्रण शामिल है, जबकि भौतिक वैधता सुनिश्चित करता है और पुनरावृत्ति (recursion) के लिए भविष्य के विस्तारों का समर्थन करता है।
यह शोधपत्र ब्रांचिंग वेक्टर एडिशन सिस्टम्स के लिए पहुँच योग्यता (reachability) की लंबे समय से चली आ रही खुली समस्या को यह सिद्ध करके हल करता है कि अप्राप्य कॉन्फ़िगरेशन (non-reachable configurations) अर्ध-रैखिक प्रेरक अपरिवर्तनों (semilinear inductive invariants) द्वारा अलग किए जा सकते हैं, जिससे इस समस्या को हल करने के लिए एक सरल गणनात्मक एल्गोरिदम सक्षम होता है।
यह शोध पत्र "क्वांटम ऑर्केस्ट्रा मोनाड" (quantum orchestra monad) प्रस्तुत करता है, जो पुनरावर्ती हाइब्रिड क्वांटम कार्यक्रमों को औपचारिक रूप से मॉडल करने के लिए क्वांटम इंस्ट्रूमेंट्स और DCPOs पर आधारित एक डेनोटेशनल सिमेंटिक्स है, जिसमें मिड-सर्किट मेजरमेंट्स, नॉन-टर्मिनेशन और क्यूबिट रेफरेंस शामिल हैं।
यह शोध पत्र विभिन्न रैखिक तर्कशास्त्रों (linear logics) के लिए घातांकीय प्रमाण-आकार निचली सीमाएं (exponential proof-size lower bounds) स्थापित करता है, यह प्रदर्शित करते हुए कि संरचनात्मक नियमों (संकुचन और विलोपन) और कट नियम का संयोजन उन प्रणालियों की तुलना में नाटकीय रूप से तीव्र गति प्रदान करता है जिनमें इन विशिष्ट घटकों का अभाव है, जिससे प्रमाण जटिलता (proof complexity) में उनकी व्यक्तिगत और सामूहिक शक्ति को अलग किया जा सके।
यह शोधपत्र होमोटोपी टाइप थ्योरी (homotopy type theory) में एक ऐसे ढांचे को प्रस्तुत करता है जो ब्रौवर ऑर्डिनल्स (Brouwer ordinals) का उपयोग करके डिसाइडेबिलिटी (decidability) का सामान्यीकरण करता है ताकि -डिसाइडेबल प्रपोज़िशन्स (propositions) के एक पदानुक्रम को स्थापित किया जा सके, जो तार्किक संक्रियाओं (logical operations) और क्वांटिफायर्स (quantifiers) के अंतर्गत उनके क्लोजर गुणों (closure properties) को अभिलक्षणिक बनाता है, और जिसके सभी परिणाम क्यूबिकल एगडा (Cubical Agda) में औपचारिक रूप से सिद्ध किए गए हैं।