1096 पेपर
यह शोध पत्र एक हाइब्रिड रीजनिंग फ्रेमवर्क का प्रस्ताव करता है जहाँ लार्ज लैंग्वेज मॉडल्स (LLMs) प्राथमिकता-आधारित रीजनिंग कार्यों को MaxSAT समस्याओं के रूप में एनकोड करने के लिए पायथन कोड जनरेट करते हैं, जिन्हें फिर डायरेक्ट-आंसर या चेन-ऑफ-थॉट बेसलाइन्स की तुलना में काफी उच्च व्यवहार्यता और शुद्धता दर प्राप्त करने के लिए सटीक सॉल्वर्स द्वारा हल और सत्यापित किया जाता है।
यह शोध पत्र प्योर पाथ्स (pure paths) पर आधारित Dpure डिपेंडेंसी स्कीम को प्रस्तुत करता है, जो DQRAT प्रूफ सिस्टम को शक्तिशाली इंडिपेंडेंट एक्सटेंडेड QU-Res सिस्टम के साथ p-इक्विवेलेंस (p-equivalence) प्राप्त करने में सक्षम बनाता है, और एक प्रोटोटाइप चेकर तथा Qute सॉल्वर में एकीकरण के माध्यम से इस प्रगति को मान्य करता है।
यह शोध पत्र हैडामार्ड और विकर्ण (diagonal) गेट्स से बने क्वांटम सर्किट के सुदृढ़ सिमुलेशन (strongly simulating) के लिए एक फिक्स्ड-पैरामीटर ट्रैकटेबल एल्गोरिदम प्रस्तुत करता है, जो पाथ-वेरिएबल ग्राफ के रैंक-विड्थ (rank-width) में ही घातीय समय (exponential time) में आउटपुट एम्प्लीट्यूड का मूल्यांकन करके विशिष्ट सर्किट परिवारों पर मौजूदा डिसीजन-डायग्राम और टेंसर-नेटवर्क विधियों से बेहतर प्रदर्शन करता है और उनके सैद्धांतिक सीमाओं को एकीकृत करता है।
यह शोध पत्र एक सुदृढ़, कर्नेल-जांचित सत्यापन पाइपलाइन प्रस्तुत करता है जो एथेरियम फाउंडेशन के zkEVM प्रोजेक्ट के भीतर प्रोडक्शन रस्ट (Rust) क्रिप्टोग्राफिक कोड के लिए मशीन-जांचित शुद्धता प्रमाणों को सफलतापूर्वक उत्पन्न करने हेतु रस्ट-टू-लीन (Rust-to-Lean) एक्सट्रैक्शन टूल्स, औपचारिक क्रिप्टोग्राफिक लाइब्रेरीज़ और AI प्रूवर्स को एकीकृत करता है।
यह शोध पत्र अनबाउंडेड (unbounded) लुकासिएविक लॉजिक के अस्तित्वगत सिद्धांत (existential theory) को मानक एमवी-बीजगणित (standard MV-algebra) के अस्तित्वगत सिद्धांत में अपचयित (reduce) करके यह स्थापित करता है कि यह एनपी-कंप्लीट (NP-complete) है, जिससे इस तर्क के प्रमेयों और परिमित परिणाम संबंध (finite consequence relation) के लिए एक जटिलता ऊपरी सीमा (complexity upper bound) प्राप्त होती है।
यह शोध पत्र इंडेक्स्ड भाषाओं के लिए डाउनवर्ड क्लोजर (downward closures) की गणना करने की जटिलता के संबंध में खुले प्रश्न को हल करता है, जो गैर-नियतात्मक (non-deterministic) और नियतात्मक (deterministic) ऑटोमेटा के लिए क्रमशः त्रि-घातीय (triply) और चतुर्घातीय (quadruply) ऊपरी सीमाओं को स्थापित करते हुए, साथ ही मिलान योग्य निचली सीमाओं को भी स्थापित करता है, जिसे सेमीग्रुप-आधारित शब्द सारांशों (semigroup-based word summaries) का उपयोग करके इंडेक्स्ड व्याकरणों को कॉन्टेक्स्ट-फ्री व्याकरणों में बदलने की एक नवीन पद्धति के माध्यम से प्राप्त किया गया है।
यह लेख यह प्रदर्शित करने के लिए कि कैसे वे सामूहिक रूप से Rocq कर्नेल की आवश्यक डिज़ाइन सीमाओं को परिभाषित करते हैं—विशेष रूप से इम्प्रेडिकेटिविटी (impredicativity), लार्ज एलिमिनेशन (large elimination) और यूनिवर्स बाधाओं (universe constraints) के संबंध में—coq-paradoxes लाइब्रेरी में यांत्रिककृत चार विरोधाभासों का विश्लेषण करता है कि सिस्टम को निरंतरता बनाए रखने के लिए कुछ निर्माणों को अस्वीकार क्यों करना चाहिए।
यह शोध पत्र ग्राफ बैकट्रैकिंग (graph backtracking) को प्रस्तुत करता है, जो एक नवीन और सुदृढ़ CDCL-आधारित SAT सॉल्विंग योजना है जो अनअसाइंड लिटरल (unassigned literals) को न्यूनतम करने के लिए इम्पलीकेशन ग्राफ (implication graphs) और उपयोगकर्ता-निर्धारित वेट फंक्शन (user-defined weight functions) का उपयोग करके क्रोनोलॉजिकल और नॉन-क्रोनोलॉजिकल बैकट्रैकिंग का सामान्यीकरण करती है, जिससे प्रोपेगेशन कम होता है और नैपसैट (NapSAT) सॉल्वर में प्रदर्शित रूप से रनटाइम में सुधार होता है।
यह शोध पत्र COVCAL को प्रस्तुत करता है, जो एक जोखिम-नियंत्रण ढांचा (risk-control framework) है जो प्रूफ़ कवरेज और नैदानिक संकेतों (diagnostic signals) के आधार पर उत्तरों को गतिशील रूप से चुनकर, प्राकृतिक-भाषा गणितीय समस्याओं के लिए जज के रूप में लीन (Lean) औपचारिकीकरण (formalization) के उपयोग की विश्वसनीयता को प्रमाणित करता है, यह प्रदर्शित करते हुए कि जहाँ छोटे ऑटोफॉर्मलाइज़र (autoformalizers) जोखिम-नियंत्रित स्वीकृति के लिए बहुत विरल संकेत प्रदान करते हैं, वहीं विशिष्ट फॉर्मलाइज़र सख्त जोखिम सीमाओं के तहत उच्च-सटीकता चयन को सक्षम करते हैं।
यह शोध पत्र LLM-आधारित Oracle-to-PostgreSQL माइग्रेशन के लिए बारह रणनीतियों का मूल्यांकन करते हुए, टोकन अनुकूलन को एक बहु-उद्देश्यीय बाधित रूपांतरण समस्या (multi-objective constrained transformation problem) के रूप में औपचारिक रूप देता है, जिससे यह प्रदर्शित होता है कि जबकि आक्रामक संपीड़न (aggressive compression) से सिमेंटिक फिडेलिटी (semantic fidelity) में भारी गिरावट आती है, एडेप्टिव रूटिंग (adaptive routing) और हल्का संदर्भ छंटनी (mild context pruning) टोकन दक्षता और कोड गुणवत्ता के बीच सबसे प्रभावी संतुलन प्रदान करते हैं।