cs.LO पेपर | Gist.Science

Nominal Type Theory by Nullary Internal Parametricity

यह शोधपत्र नलरी इंटरनली पैरामीट्रिक टाइप थ्योरी (Nullary Internally Parametric Type Theory) और एक विशिष्ट नाम इंडक्शन सिद्धांत पर आधारित एक नवीन टाइप थ्योरी प्रस्तुत करता है जो यूनिवर्सल नेम एब्स्ट्रैक्शंस के स्वच्छ टाइपिंग नियमों को एक्सिस्टेंशियल नेम एब्स्ट्रैक्शंस की शक्तिशाली पैटर्न-मैचिंग क्षमताओं के साथ सफलतापूर्वक एकीकृत करता है, जिससे बाइंडर्स वाले सिंटैक्स को निरूपित करने के लिए एक सुव्यवस्थित नोमिनल फ्रेमवर्क स्थापित होता है।

Antoine Van Muylder, Andreas Nuyts, Dominique Devriese2026-05-25

💻 computer science

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT

यह शोध पत्र डिवाइड-एंड-कॉन्कर और प्रोजेक्टेड एन्यूमरेशन जैसी स्केलेबल तकनीकों का उपयोग करके थ्योरी लेम्मा के पूर्ण सेटों को कुशलतापूर्वक सूचीबद्ध करने के लिए एक थ्योरी-अग्नोस्टिक फ्रेमवर्क पेश करता है, जिससे क्लासिक ईगर एनकोडिंग की सीमाओं को दूर किया जा सकता है और अनसैट-कोर एक्सट्रैक्शन और मैक्सएसएमटी (MaxSMT) जैसे जटिल एसएमटी कार्यों के लिए प्रदर्शन में महत्वपूर्ण सुधार किया जा सकता है।

Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani2026-05-25

💻 computer science

Expressive Power of Deep Homomorphism Networks over Relational Databases

यह शोधपत्र डीप होमोमोर्फिज्म नेटवर्क्स (DHNs) को रिलेशनल डेटाबेस के लिए एक शक्तिशाली आर्किटेक्चर के रूप में प्रस्तावित करता है, जो प्रथम-क्रम तर्क (first-order logic) और SQL के विशिष्ट अंशों के साथ उनकी सटीक अभिव्यंजक तुल्यता स्थापित करके, प्रमुख स्टैटिक एनालिसिस समस्याओं के लिए निर्णायकता (decidability) सिद्ध करके, और प्रयोगों के माध्यम से उनके श्रेष्ठ प्रदर्शन को मान्य करके किया गया है।

Moritz Schönherr, Balder ten Cate, Maurice Funk, Benny Kimelfeld, Carsten Lutz, Arie Soeteman2026-05-25

🤖 AI

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

यह शोध पत्र ImProver 2 को प्रस्तुत करता है, जो एक न्यूरोसिम्बोलिक ढांचा है जो डेटा-कुशल विशेषज्ञ पुनरावृत्ति (expert iteration) को एक संरचनात्मक स्कैफोल्डिंग प्रणाली के साथ जोड़ता है ताकि छोटे भाषा मॉडलों को Lean 4 में जटिल औपचारिक प्रमाणों (formal proofs) को प्रभावी ढंग से अनुकूलित करने में सक्षम बनाया जा सके, जो काफी बड़े मॉडलों से बेहतर प्रदर्शन करता है और प्रमाण अनुकूलन को एक स्केलेबल, सीखने योग्य कार्य के रूप में स्थापित करता है।

Riyaz Ahuja, Tate Rowney, Jeremy Avigad, Sean Welleck2026-05-25

🤖 AI

Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems

यह शोध पत्र इंडक्टिव डिडक्टिव सिंथेसिस (IDS) को प्रस्तुत करता है, जो एक एजेंटिक LLM सिस्टम है जो वितरित प्रणालियों (डिस्ट्रीब्यूटेड सिस्टम्स) के लिए कार्यान्वयन और औपचारिक प्रमाणों को संयुक्त रूप से संश्लेषित करता है, और की-वैल्यू स्टोर विनिर्देशों पर मानव विशेषज्ञों और अत्याधुनिक कोडिंग एजेंटों दोनों की तुलना में काफी कम समय और लागत के साथ 100% सफलता प्राप्त करता है।

Shubham Agarwal, Alexander Krentsel, Shu Liu, Mert Cemri, Audrey Cheng, Rui Meng, Tomas Pfister, Chun-Liang Li, Sylvia R (…)2026-05-25

💻 computer science

Formal Verification of Probing Security via Conditional Independence

यह शोधपत्र नॉन-इंटरफेरेंस गुणों और कंडीशनल इंडिपेंडेंस के बीच संबंध स्थापित करने के लिए प्रोबेबिलिस्टिक सेपरेशन लॉजिक (Lilac) का लाभ उठाते हुए, मास्क्ड क्रिप्टोग्राफिक एल्गोरिदम की प्रोबिंग सुरक्षा के लिए एक नवीन औपचारिक सत्यापन दृष्टिकोण प्रस्तावित करता है।

Satoshi Kura, Katsuyuki Takashima2026-05-25

💻 computer science

Arrow-Type Impossibility for Genuinely Modal Judgments

यह शोध पत्र यह प्रदर्शित करता है कि निर्णय एकत्रीकरण (judgment aggregation) में एयरो-प्रकार के असंभवता परिणाम तब भी पुन: प्रकट होते हैं जब उन्हें वास्तविक रूप से मोडल निर्णयों तक सीमित कर दिया जाता है, जो यह सिद्ध करता है कि विशिष्ट मोडल सिमेंटिक संरचनाएं अकेले ही बिना किसी छद्म तथ्यात्मक प्रस्तावों पर निर्भर रहे, तानाशाही के लिए आवश्यक तार्किक अंतर्संबंध उत्पन्न कर सकती हैं।

Yutaka Nagai, Hirotaka Ono2026-05-25

💻 computer science

Formally Verified Liveness with Multiparty Session Types in Rocq

यह शोध पत्र लगभग 14,000 लाइनों के कोड के माध्यम से संचार प्रोटोकॉल की सुरक्षा और जीवंतता (liveness) को औपचारिक रूप से सत्यापित करने के लिए, को-इंडक्टिव ट्रीज़ (coinductive trees) और संबंधों का उपयोग करते हुए, रॉक (Rocq) प्रूफ असिस्टेंट में सिंक्रोनस मल्टीपार्टी सेशन टाइप्स के लिए जीवंतता का पहला यांत्रिक प्रमाण प्रस्तुत करता है।

Omer Keskin, Nobuko Yoshida, Rob van Glabbeek2026-05-25

💻 computer science

An ASP-based approach to Solving General Stochastic Two-Player Games

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

Yifan He, Michael Thielscher2026-05-25

🔢 mathematics

The complete classification for quantified equality constraints

यह शोध पत्र समानता भाषाओं (equality languages) पर क्वांटिफाइड कंस्ट्रेंट सैटिस्फिएबिलिटी प्रॉब्लम (QCSP) के लिए एक पूर्ण जटिलता त्रिक विभाजन (Logspace, NP-complete, या PSpace-complete) स्थापित करता है, जो यह सिद्ध करके कि QCSP $(\mathbb{N};x=y\rightarrow y=z)$ PSpace-complete है, और साथ ही सीमित परिवर्तनशीलता (bounded alternation) वाले संस्करण को पॉलीनोमियल हाइरार्की (Polynomial Hierarchy) के भीतर वर्गीकृत करता है।

Dmitriy Zhuk, Barnaby Martin, Michal Wrona2026-05-22

← पिछला अगला →