💻 computer science

Traces via Strategies in Two-Player Games

यह शोधपत्र अनिश्चित (nondeterministic) या संभाव्य (probabilistic) वातावरण वाले दो-खिलाड़ी नियंत्रक-बनाम-पर्यावरण (controller-versus-environment) खेलों के लिए एक कोएल्जेब्रिक ट्रेस सिमेंटिक्स (coalgebraic trace semantics) ढांचे को स्थापित करता है, जो यह प्रदर्शित करता है कि ट्रेस तत्व एक विशिष्ट रणनीति के माध्यम से एक नियंत्रक द्वारा थोपे जा सकने वाले खेलों के संग्रह के अनुरूप होते हैं, जो सभी एक कमजोर वितरणात्मक नियम (weak distributive law) द्वारा पैरामीटराइज्ड हैं।

Benjamin Plummer, Corina Cirstea2026-03-03
💻 computer science

Compact Quantitative Theories of Convex Algebras

यह शोध पत्र कॉम्पैक्ट क्वांटिटेटिव इक्वेशनल थ्योरीज़ (compact quantitative equational theories) की अवधारणा प्रस्तुत करता है, जो यह सिद्ध करता है कि इंटरपोलेटिव बैरीसेंट्रिक अल्जेब्रा (interpolative barycentric algebras) का सिद्धांत कॉम्पैक्ट है और इस परिणाम का उपयोग करके अन्य कॉम्पैक्ट सिद्धांतों को व्युत्पन्न करता है जो सीमित समर्थित प्रायिकता वितरणों (finitely supported probability distributions) पर दूरियों को स्वयंसिद्ध (axiomatize) करते हैं।

Matteo Mio2026-03-03
💻 computer science

Towards Language Model Guided TLA+ Proof Automation

यह शोध पत्र एक प्रॉम्प्ट-आधारित दृष्टिकोण प्रस्तुत करता है जो प्रतीकात्मक सत्यापन (symbolic verification) के लिए TLA+ प्रमाण दायित्वों (proof obligations) को सरल उप-दावों में पदानुक्रमित रूप से विघटित करने के लिए लार्ज लैंग्वेज मॉडल्स का लाभ उठाता है, जिससे संरचनात्मक चुनौतियों पर विजय प्राप्त होती है और 119 प्रमेयों के एक नए बेंचमार्क पर बेसलाइन विधियों से बेहतर प्रदर्शन होता है।

Yuhao Zhou, Stavros Tripakis2026-03-03
🤖 machine learning

Polynomial Surrogate Training for Differentiable Ternary Logic Gate Networks

यह शोध पत्र पॉलीनोमियल सरोगेट ट्रेनिंग (PST) को प्रस्तुत करता है, जो एक स्केलेबल विधि है जो न्यूरॉन्स को सीखने योग्य पॉलीनोमियल्स के रूप में निरूपित करके टर्नरी लॉजिक गेट नेटवर्क के कुशल डिफरेंशिएबल प्रशिक्षण को सक्षम बनाती है, जिससे मौजूदा दृष्टिकोणों के अव्यवहार्य सर्च स्पेस पर विजय प्राप्त होती है और बाइनरी समकक्षों की तुलना में बेहतर अनिश्चितता प्रबंधन और प्रशिक्षण गति प्रदर्शित होती है।

Sai Sandeep Damera, Ryan Matheu, Aniruddh G. Puranic, John S. Baras2026-03-03
🔢 mathematics

Unbiasing symmetric monoidal categories in Lean

यह शोध पत्र Mathlib के भीतर एक Lean 4 औपचारिकीकरण (formalization) प्रस्तुत करता है जो उनके डेटा को परिमित समुच्चयों के स्पैन (spans) पर एक Cat-मानित स्यूडोफंक्टर (pseudofunctor) तक विस्तारित करके सममित मोनॉइडल श्रेणियों (symmetric monoidal categories) को निष्पक्ष बनाता है, जो उच्च-अैरिटी (higher-arity) टेंसर उत्पादों और उनकी सुसंगति (coherences) को संभालने के लिए मैक लेन के कोहेरेंस प्रमेय (Mac Lane's coherence theorem) और एक क्लेइसली बायकेटिगरी (Kleisli bicategory) एन्कोडिंग का लाभ उठाता है।

Robin Carlier2026-03-03
🤖 machine learning

Integrating LTL Constraints into PPO for Safe Reinforcement Learning

यह शोध पत्र PPO-LTL प्रस्तुत करता है, जो एक सुरक्षित सुदृढीकरण शिक्षण (reinforcement learning) ढांचा है जो लिमिट-डिटरमिनिस्टिक बुची ऑटोमेटा (limit-deterministic Büchi automata) और एक लैग्रेंजियन योजना के माध्यम से LTL उल्लंघनों को दंड संकेतों में अनुवादित करके प्रॉक्सिमल पॉलिसी ऑप्टिमाइज़ेशन (Proximal Policy Optimization) में लीनियर टेम्पोरल लॉजिक (Linear Temporal Logic) बाधाओं को एकीकृत करता है, जो रोबोटिक्स वातावरण में उत्कृष्ट सुरक्षा और प्रदर्शन प्रदर्शित करता है।

Maifang Zhang, Hang Yu, Qian Zuo, Cheng Wang, Vaishak Belle, Fengxiang He2026-03-03
💻 computer science

On the Metric Nature of (Differential) Logical Relations

यह शोधपत्र प्रोग्राम दूरियों को मॉडल करने के लिए क्वासी-क्वासी-मेट्रिक स्पेस (quasi-quasi-metric spaces) को पेश करके, कंपोजिशनल रीजनिंग (compositional reasoning) के लिए एक मौलिक लेम्मा स्थापित करके, और यह प्रदर्शित करके कि जबकि ये स्पेस एक फाइनएस्ट डिफरेंशियल प्रीलॉजिकल रिलेशन (finest differential prelogical relation) का समर्थन करते हैं, वे पारंपरिक कॉन्टेक्स्टुअल इक्विवेलेंस (contextual equivalences) के विपरीत एक कोर्सेस्ट काउंटरपार्ट (coarsest counterpart) का अभाव रखते हैं, डिफरेंशियल लॉजिकल रिलेशंस की मेट्रिक प्रकृति को स्पष्ट करता है।

Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone2026-03-03
💻 computer science

Implementing Dependent Type Theory Inhabitation and Unification

यह शोधपत्र 'कैनोनिकल-मिन' (Canonical-min) प्रस्तुत करता है, जो डिपेंडेंट टाइप थ्योरी में अनिर्णायक समस्याओं—इनहैबिटेशन (inhabitation) और यूनिफिकेशन (unification)—के लिए एक संक्षिप्त और सुदृढ़ सॉल्वर है, साथ ही टाइप चेकर्स को कुशल सॉल्वरों में बदलने के लिए एक नवीन मोनैडिक फ्रेमवर्क और मूल्यांकन के लिए 'DTTBench' बेंचमार्क भी प्रस्तुत करता है।

Chase Norman, Jeremy Avigad2026-03-03
💻 computer science

Generalization of terms via universal algebra

यह शोधपत्र प्रक्षेपिक (projective) और सटीक (exact) बीजगणितों का लाभ उठाकर समीकरण सिद्धांतों (equational theories) तक पदों (terms) के सामान्यीकरण के लिए एक सार्वभौमिक-बीजगणितीय ढांचे को प्रस्तुत करता है, जो सामान्यता पोसेट (generality poset) और समस्याओं के प्रकार को अभिलक्षणिक बनाने के लिए है, और अंततः उन विविधताओं (varieties) की एक श्रेणी की पहचान करता है जहाँ ये गुण 1-जनित मुक्त बीजगणित के संग्रति जालक (congruence lattice) में सिमट जाते हैं और विभिन्न बीजगणितीय संरचनाओं और तर्कशास्त्रों में एकात्मक सामान्यीकरण प्रकारों (unitary generalization types) को प्रदर्शित करते हैं।

Tommaso Flaminio, Sara Ugolini2026-03-02
💻 computer science

Rings and Boolean Algebras as Algebraic Theories

यह शोध पत्र एक एकीकृत श्रेणीगत ढांचा स्थापित करता है जो क्रमविनिमेय (commutative) और बूलियन (Boolean) वलयों को क्रमशः एफाइन (affine) और हाइपर-एफाइन (hyperaffine) बीजगणितीय सिद्धांतों से जोड़ता है, जबकि एक बूलियन वलय पर उनके मॉडलों के नवीन लक्षण वर्णन प्रदान करता है और हाइपर-एफाइन सिद्धांतों को बहुआयामी बूलियन बीजगणितों से जोड़ता है।

Arturo De Faveri2026-03-02