1091 पेपर
यह शोधपत्र जटिल सदिश स्थानों (complex vector spaces) पर सीमित ऑपरेटरों (bounded operators) का Isabelle/HOL में एक व्यापक औपचारिकीकरण प्रस्तुत करता है, जो यूनिटरीज (unitaries), एडजॉइंट्स (adjoints) और लोएनर ऑर्डर (Loewner order) जैसी उन्नत अवधारणाओं के साथ मौजूदा वास्तविक-मान वाले विकासों का विस्तार करता है, और साथ ही परिमित-आयामी मामलों के लिए मैट्रिक्स-आधारित कोड जनरेशन भी प्रदान करता है।
यह शोध पत्र एक मल्टीलेयर स्पेसिफिकेशन सुरक्षा मॉडल और एक सुरक्षा ज्ञान संक्रमण पद्धति का प्रस्ताव करके स्पेसिफिकेशन-संचालित एआई विकास में सुरक्षा अंतराल को संबोधित करता है जो सुरक्षा आवश्यकताओं को क्रियान्वित करते हैं, और अनुभवजन्य अध्ययनों के माध्यम से यह प्रदर्शित करता है कि ये दृष्टिकोण बेसलाइन और ASVS-सशर्त जनरेशन की तुलना में एपीआई विफलताओं को महत्वपूर्ण रूप से कम करते हैं।
यह शोध पत्र रोबस्ट मार्कोव निर्णय प्रक्रियाओं (Markov decision processes) के लिए एक नवीन, सुदृढ़ और इष्टतम शिल्डिंग फ्रेमवर्क प्रस्तुत करता है जो सैंपलिंग विधियों के साथ संयोजन करते हुए, सीखी गई मॉडलों के लिए प्रोबेबली एप्रोक्सिमेटली करेक्ट (PAC) सुरक्षा गारंटी प्रदान करने के लिए, सबसे खराब स्थिति वाली ट्रांज़िशन अनिश्चितताओं के तहत सुदृढीकरण लर्निंग (reinforcement learning) एजेंटों की सुरक्षा सुनिश्चित करता है।
यह शोधपत्र डिपेंडेंस लॉजिक (dependence logic) के लिए एक नया एरेनफिच-फ्रैइसे खेल (Ehrenfeucht-Fraïssé game) प्रस्तुत करता है जो एलिमेंट्री इक्विवेलेंस (elementary equivalence) को अभिलक्षणिक बनाने के लिए एकल-तत्व चालों (single-element moves) और स्वतंत्रता घोषणाओं (independence declarations) का उपयोग करता है, जिससे पिछले टीम-आधारित सूत्रीकरणों की जटिलता पर विजय प्राप्त होती है।
यह शोध पत्र लीन4 (Lean4) में मल्टीग्रेटेड बीजगणितीय ज्यामिति (multigraded algebraic geometry) की रचनाओं का एक विस्तृत औपचारिक रूप प्रस्तुत करता है, जो विशेष रूप से ब्रेनर-श्रोएर प्रोज (Brenner-Schröer Proj) निर्माण और वलयों के बीजगणितीय विरूपण (algebraic dilatations of rings) पर केंद्रित है।
यह शोध पत्र एक ऐसे प्रयोग की रिपोर्ट करता है जहाँ एक लेखक ने चर्च के बेसिक रिकर्सिव अरिथमेटिक (Basic Recursive Arithmetic) के लिए एगडा (Agda) में गोडेल के दूसरे अपूर्णता प्रमेय (Gödel's second incompleteness theorem) को ऑटोफॉर्मलाइज़ करने के लिए एआई मॉडल क्लॉड (Claude) का उपयोग किया, जिसके परिणामस्वरूप 50,000 पंक्तियों का एक पोस्टुलेट-मुक्त (postulate-free) मशीन-चेक्ड प्रमाण प्राप्त हुआ जो मॉडल की निहित गणितीय तर्कों को पुनर्गठित करने की क्षमता और अपर्याप्त विशिष्टताओं (specifications) दिए जाने पर गणितीय रूप से गलत परिणाम उत्पन्न करने की उसकी प्रवृत्ति पर एक केस स्टडी के रूप में भी कार्य करता है।
यह शोध पत्र Q-MICE को प्रस्तुत करता है, जो #QBF के लिए एक नवीन प्रूफ़ सिस्टम है जो ध्वनि अनुमान नियमों (sound inference rules) पर आधारित है, जो विस्तार-आधारित प्रणालियों की संरचनात्मक कमजोरियों को दूर करता है और उन सूत्रों के लिए ऊपरी सीमाएँ (upper bounds) प्रदान करता है जो मौजूदा #SAT सॉल्वरों के लिए कठिन ज्ञात हैं।
यह पूर्व-पंजीकृत अध्ययन प्रदर्शित करता है कि निर्भरता टोपोलॉजी (dependency topology) सात विविध सब्सट्रेट्स—औपचारिक गणित और सॉफ़्टवेयर से लेकर जैविक और प्रीबायोटिक प्रणालियों तक—में कार्यात्मक भार-वहन संगठन (functional load-bearing organization) के साथ सह-संबद्ध है, जो एक मापने योग्य "संरचनात्मक भूमिका ज्यामिति" (structural role geometry) को प्रकट करता है जहाँ परिचालन तर्क (operational logic) की पहचान करने में बिटवीननेस-आधारित दृढ़ता (betweenness-based persistence), डिग्री-आधारित मेट्रिक्स से बेहतर प्रदर्शन करती है।
यह शोधपत्र ProofWala को प्रस्तुत करता है, जो एक पुन: प्रयोज्य लाइब्रेरी पर आधारित एक बहुभाषी ढांचा है जो इंटरैक्टिव थ्योरम प्रूवर्स के साथ प्रोग्रामेटिक इंटरेक्शन के लिए सक्षम बनाता है, जो स्केलेबल, सिमेंटिक रूप से निष्ठावान प्रमाण डेटा निष्कर्षण और समानांतर खोज को सक्षम करता है, और यह प्रदर्शित करता है कि Lean और Rocq में क्रॉस-लिंगुअल प्रशिक्षण थ्योरम-प्रूविंग प्रदर्शन और डोमेन अनुकूलन को महत्वपूर्ण रूप से सुधारता है।
यह शोध पत्र मल्टी-क्लॉकड गार्डेड रिकर्सन (multi-clocked guarded recursion) के एक्सटेंशनल प्रेशेफ मॉडल (extensional presheaf model) को उच्च ऑर्डिनल्स (higher ordinals) तक विस्तारित करता है, जिससे उन सेट-थ्योरेटिक व्याख्याओं को सक्षम किया जा सके जो परिमित पॉवरसेट (finite powersets), वितरण (distributions), और अस्तित्वपरक क्वांटिफिकेशन (existential quantification) से युक्त जटिल कोइंडक्टिव प्रकारों (coinductive types) के एनकोडिंग की शुद्धता को सत्यापित करती हैं।