1114 पेपर
यह शोधपत्र व्याख्यान नोट्स प्रस्तुत करता है जो न्यूरल नेटवर्क सत्यापन का एक सैद्धांतिक परिचय प्रदान करते हैं, जिसमें फीड-फॉरवर्ड नेटवर्क, आरएनएन (RNNs) और ट्रांसफॉर्मर जैसे आर्किटेक्चर के साथ-साथ विनिर्देश भाषाओं (specification languages) और एल्गोरिद्मिक तकनीकों को शामिल किया गया है।
यह शोध पत्र यह स्थापित करता है कि जबकि क्लस्टर वर्टेक्स डिलीशन नंबर द्वारा पैरामीटराइज्ड फेयर MSO डेफिनेबल समस्याएं सामान्यतः W[1]-हार्ड होती हैं, वे विशिष्ट पर्याप्त शर्तों के तहत फिक्स्ड-पैरामीटर ट्रैक्टेबल एल्गोरिदम स्वीकार करती हैं जो फेयर वर्टेक्स कवर और फेयर डोमिनेटिंग सेट जैसी विभिन्न स्वाभाविक फेयर ग्राफ समस्याओं को समाहित करती हैं।
होफमैन-स्ट्राइकर लिफ्टिंग के अ्वोडेय (Awodey) के फन्क्टोरियल विश्लेषण से प्रेरित होकर, यह शोधपत्र एक फाइब्रेशन के साथ पोस्टकंपोजिशन (postcomposition) के राइट स्यूडो-एडजॉइंट (right pseudo-adjoint) का उपयोग करके इस निर्माण के एक सापेक्ष संस्करण को परिभाषित करता है और फाइब्रेशन्स के एक नए 2-बिफाइब्रेशन (2-bifibration) के निर्माण के लिए इस ढांचे का उपयोग करता है।
यह शोध पत्र यह प्रदर्शित करता है कि एक एकल बाइनरी जनरेटर द्वारा जनरेट किए गए फ्री प्रोप (free PROP) का कोटिएंट, जिसे पूर्वज फंक्टर (ancestry functor) के माध्यम से प्राप्त किया गया है, नॉन-कौनीटल कोकम्यूटेटिव कोमोनॉइड्स (non-counital cocommutative comonoids) के प्रोप के समतुल्य है, जबकि इस परिणाम को कोरलेशन (corelations) और हाइपरग्राफ श्रेणियों के व्यापक संदर्भ में स्थापित करता है।
यह शोध पत्र ग्लोबल रीडआउट वाले क्वांटटाइज्ड एग्रीगेट-कंबाइन ग्राफ न्यूरल नेटवर्क्स (ACR-GNNs) को चित्रित करने के लिए एक तार्किक भाषा प्रस्तुत करता है और यह सिद्ध करता है कि इन मॉडलों को सत्यापित करना (co)NEXPTIME-पूर्ण है, जो यह दर्शाता है कि हालांकि वे सत्यापित करने के लिए गणनात्मक रूप से जटिल हैं, फिर भी वे व्यवहार में हल्के और सटीक बने रहते हैं।
यह शोध पत्र यह प्रदर्शित करके कि स्थानीय एकत्रीकरण (local aggregation) और वैश्विक रीडआउट (global readout) के बीच की अंतःक्रिया उन्हें तर्क की तार्किक अभिव्यंजना शक्ति से आगे जाने की अनुमति देती है, संदेश-पासिंग GNNs की अभिव्यंजक शक्ति की जांच करता है, साथ ही उन विशिष्ट बाधाओं की पहचान करता है जो एकत्रीकरण या ग्राफ डिग्री पर लागू होने पर ग्लोबल काउंटिंग वाले ग्रेडेड मोडल लॉजिक (graded modal logic with global counting) के माध्यम से विशेषताकरण (characterisability) को पुनः स्थापित करती हैं।
ProofLoop एक टूल-ऑगमेंटेड ReAct एजेंट है जो रिट्रीवल-ऑगमेंटेड डिज़ाइन कॉन्टेक्स्ट गैदरिंग को औपचारिक सत्यापन उपकरणों (formal verification tools) का उपयोग करके एक इटरेटिव, सॉल्वर-इन-द-लूप रिफाइनमेंट प्रक्रिया के साथ जोड़कर, प्राकृतिक भाषा से सिस्टमवेरिलॉग एसेर्शन्स (SVA) के जनरेशन को ऑटोमेट करता है।
यह शोध पत्र अनंत द्विदलीय समूह (infinite dihedral group) के कॉक्सेटर सिस्टम (Coxeter system) के माध्यम से टाइप एफाइन फ्लैग मैनिफोल्ड्स (affine flag manifolds) के लिए कॉम्बिनेटोरियल कर्व नेबरहुड्स (combinatorial curve neighborhoods) को एनकोड करके, लीन 4 (Lean 4) में एक अक्सिओम-मुक्त औपचारिकीकरण प्रस्तुत करता है, जो अंततः इन नेबरहुड्स के लिए एक सत्यापित और पूर्णतः गणनीय ढांचा प्रदान करता है।
यह शोध पत्र लीन थ्योरम प्रूवर (Lean Theorem Prover) का उपयोग करके मैरिना वियाज़ोस्का के 2016 के 8-आयामी गोला पैकिंग (sphere packing) समस्या के समाधान के सफल औपचारिक सत्यापन पर चर्चा करता है, जो मानव गणितज्ञों और ऑटोफॉर्मलाइजेशन मॉडल "गॉस" (Gauss) के बीच एक सहयोगात्मक मील के पत्थर को रेखांकित करता है।
यह शोध पत्र एक परिष्कृत पंपेबिलिटी विश्लेषण (pumpability analysis) को प्रस्तुत करके निश्चित-आयामी वेक्टर एडिशन सिस्टम्स (VAS) के लिए रीचेबिलिटी कॉम्प्लेक्सिटी बाउंड्स में सुधार करता है जो एक ऊपरी सीमा प्रदान करता है और 4-आयामी और 5-आयामी VAS के लिए क्रमशः PSPACE और ELEMENTARY बाउंड्स स्थापित करता है, जो वेक्टर एडिशन सिस्टम विद स्टेट्स (VASS) से विरासत में मिले पिछले परिणामों से बेहतर है।