cs.LO पेपर | Gist.Science

TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

यह शोधपत्र TaoBench प्रस्तुत करता है, जो टेरेन्स ताओ की *Analysis I* से व्युत्पन्न एक नवीन बेंचमार्क है जो विशेष गणितीय संरचनाओं पर स्वचालित प्रमेय प्रुवरों (automated theorem provers) का मूल्यांकन करता है, जो मानक MathLib समस्याओं की तुलना में प्रदर्शन में 26% की महत्वपूर्ण गिरावट को प्रकट करता है और यह रेखांकित करता है कि वर्तमान प्रणालियों की प्राथमिक सीमा कार्यों की अंतर्निहित कठिनाई के बजाय विभिन्न परिभाषात्मक ढांचों (definitional frameworks) में सामान्यीकरण करने की उनकी अक्षमता है।

Alexander K Taylor, Junyi Zhang, Ethan Ji, Vigyan Sahai, Haikang Deng, Yuanzhou Chen, Yifan Yuan, Di Wu, Jia-Chen Gu, Ka (…)2026-03-16

💻 computer science

Are Dependent Types in Set Theory Feasible?

यह शोध पत्र Lisa प्रूफ़ असिस्टेंट के भीतर टार्स्की-ग्रोथेंडिक सेट थ्योरी (Tarski-Grothendieck set theory) में डिपेंडेंट टाइप्स और यूनिवर्स के एक मेकेनाइज्ड एम्बेडिंग को प्रस्तुत करता है, जो एक सत्यापित, प्रूफ़-प्रोड्यूसिंग टाइप-चेकिंग टैक्टिक को सक्षम बनाता है जो स्वचालित तर्क के लिए मानक सेट-थ्योरेटिक समानता और प्रतिस्थापन नियमों का लाभ उठाता है।

Yunsong Yang, Simon Guilloud, Viktor Kunčak2026-03-16

🤖 AI

ODRL Policy Comparison Through Normalisation

यह शोध पत्र एक अर्थ-संरक्षण करने वाले सामान्यीकरण दृष्टिकोण का प्रस्ताव करता है जो जटिल ODRL नीतियों को सरल बाधाओं के साथ न्यूनतम, केवल-अनुमति वाले रूपों में परिवर्तित करता है, जिससे प्रत्यक्ष संरचनात्मक पहचान जाँचों के माध्यम से कुशल नीति तुलना सक्षम होती है।

Jaime Osvaldo Salas, Paolo Pareti, George Konstantinidis2026-03-16

🤖 AI

Delta1 with LLM: symbolic and neural integration for credible and explainable reasoning

यह शोध पत्र Delta1 with LLM को प्रस्तुत करता है, जो एक न्यूरो-सिम्बोलिक फ्रेमवर्क है जो स्वास्थ्य सेवा और अनुपालन जैसे महत्वपूर्ण डोमेन में विश्वसनीय, ऑडिट करने योग्य और स्वाभाविक रूप से व्याख्यात्मक तर्क उत्पन्न करने के लिए ऑटोमेटेड थ्योरम जनरेटर Delta1 के नियत (deterministic), बहुपद-समय (polynomial-time) प्रमेय जनरेशन को लार्ज लैंग्वेज मॉडल्स के साथ जोड़ता है।

Yang Xu, Jun Liu, Shuwei Chen, Chris Nugent, Hailing Guo2026-03-16

🔢 mathematics

Support is Search

यह शोध पत्र प्रदर्शित करता है कि सैंडक्विस्ट (Sandqvist) का सहजनात्मक प्रस्तावात्मक तर्क (intuitionistic propositional logic) के लिए आधार-विस्तार अर्थविज्ञान (base-extension semantics), एक रचनात्मक, गणनात्मक व्याख्या को स्वीकार करता है जहाँ एक निश्चित आधार में समर्थन (support), दूसरे क्रम के हेरेडिटरी हैरोप (hereditary Harrop) तर्क कार्यक्रम में प्रमाण-खोज (proof-search) के ठीक अनुरूप होता है।

Alexander V. Gheorghiu2026-03-16

💻 computer science

Dynamic direct (ranked) access of MSO query evaluation over SLP-compressed strings

यह शोध पत्र एक गतिशील एल्गोरिदम प्रस्तुत करता है जो अनकंप्रेस्ड (uncompressed) और स्ट्रेट-लाइन प्रोग्राम (SLP)-कंप्रेस्ड दोनों प्रकार के स्ट्रिंग्स पर मोनैडिक सेकंड-ऑर्डर (MSO) क्वेरीज़ के उत्तरों तक लॉगरिदमिक-समय (logarithmic-time), रैंक वाले डायरेक्ट एक्सेस को सक्षम बनाता है, जबकि कंप्रेस्ड रिप्रेजेंटेशन में कुशल अपडेट का समर्थन भी करता है।

Martín Muñoz2026-03-16

💻 computer science

Verification of Robust Properties for Access Control Policies

यह शोध पत्र रोबस्ट प्रॉपर्टी वेरिफिकेशन (robust property verification) को प्रस्तुत करता है, जो एक कंपोजिशनल और एक्जीक्यूटेबल विधि है जो भविष्य के विस्तारों के बावजूद यह निर्धारित करती है कि एक अपूर्ण या विकसित होती एक्सेस कंट्रोल पॉलिसी क्या प्रतिबद्धता करती है, और यह वेरिफिकेशन समस्या को सेकंड-ऑर्डर लॉजिक प्रोग्रामिंग में प्रूफ सर्च में घटाकर किया जाता है।

Alexander V. Gheorghiu2026-03-16

💻 computer science

Positionality in Σ_0^2 and a completeness result

यह शोध पत्र स्थापित करता है कि एक न्यूट्रल लेटर के साथ $\Sigma_0^2$ में प्रीफिक्स-स्वतंत्र पोजीशनल ऑब्जेक्टिव्स, गणनीय ऑर्डिनल्स (countable ordinals) पर हिस्ट्री-डिटरमिनिस्टिक मोनोटोन को-बुची ऑटोमेटा द्वारा अभिलक्षित होते हैं, जो कि पूर्व मानदंडों का सामान्यीकरण करता है, यूनियन के तहत क्लोजर का एक नया प्रमाण प्रदान करता है, मनमाने ग्राफों पर मीन-पेऑफ गेम्स की पोजीशनैलिटी को सिद्ध करता है, और परिमित ग्राफों पर पोजीशनल ऑब्जेक्टिव्स के लिए एक पूर्णता गुण (completeness property) प्रदर्शित करता है।

Pierre Ohlmann, Michał Skrzypczak2026-03-13

💻 computer science

Slightly Non-Linear Higher-Order Tree Transducers

यह शोध पत्र ट्री-टू-ट्री (tree-to-tree) फलनों के एक मॉडल के रूप में अफ़ाइन $\lambda$ -ट्रांसड्यूसर्स (affine $\lambda$ -transducers) की जांच करता है, यह प्रदर्शित करते हुए कि उनके अफ़ाइन वेरिएंट ट्री-वॉकिंग ट्रांसड्यूसर (tree-walking transducers) के समकक्ष हैं और एक थोड़ा गैर-रैखिक विस्तार इनविज़िबल पेबल ट्री ट्रांसड्यूसर (invisible pebble tree transducers) की अभिव्यक्ति शक्ति से मेल खाता है, जिसके प्रमाण एक इनएक्सप्रेसिविटी अनुमान (inexpressivity conjecture) को हल करने के लिए इंटरैक्शन एब्स्ट्रैक्ट मशीन (Interaction Abstract Machine) पर निर्भर करते हैं।

Lê Thành Dũng Nguyên, Gabriele Vanoni2026-03-13

💻 computer science

On Reduction and Synthesis of Petri's Cycloids

यह शोध पत्र अपरिमेय रूपों (irreducible forms) को निरूपित करने के लिए न्यूनीकरण प्रणालियों (reduction systems) को परिभाषित करके और नेट संरचनाओं से मापदंडों को संश्लेषित करने की एक विधि व्युत्पन्न करके पेट्री के साइक्लॉइड्स (Petri's cycloids) की संरचना की जांच करता है, जिससे साइक्लॉइड समरूपता (cycloid isomorphism) के लिए एक कुशल निर्णय प्रक्रिया स्थापित होती है।

Rüdiger Valk, Daniel Moldt2026-03-13

← पिछला अगला →