1105 पेपर
यह शोध पत्र MANTRA को प्रस्तुत करता है, जो एक ऐसा ढांचा है जो प्राकृतिक भाषा वाले प्रक्रियात्मक मैनुअल (procedural manuals) से प्रतीकात्मक विश्व मॉडल (symbolic world models) और SMT-सत्यापित ट्रेस-स्तरीय जाँच (trace-level checks) उत्पन्न करके, टूल-उपयोग करने वाले LLM एजेंटों के लिए स्वचालित रूप से संश्लेषित और औपचारिक रूप से मान्य, स्केलेबल, मशीन-जांच योग्य अनुपालन बेंचमार्क का संश्लेषण करता है।
यह शोध पत्र बीजगणितीय डेटा प्रकारों (algebraic data types) वाले एक उच्च-क्रम भाषा (higher-order language) में फॉरवर्ड-मोड ऑटोमैटिक डिफरेंशिएशन के लिए सिमेंटिक शुद्धता प्रमाण प्रस्तुत करता है, जो इस पद्धति को एक अद्वितीय संरचना-संरक्षण मैक्रो (structure-preserving macro) के रूप में अभिलक्षित करता है और टेलर सन्निकटन (Taylor approximation) के माध्यम से उच्च-क्रम डेरिवेटिव तक विस्तारित होने वाले डिफियोलॉजिकल स्पेस (diffeological spaces) पर एक ग्लूइंग निर्माण (gluing construction) के माध्यम से इसकी वैधता स्थापित करता है।
यह शोध पत्र स्मॉल ऑब्जेक्ट आर्गुमेंट (small object argument) के माध्यम से फ्री मॉडल्स (free models) का निर्माण करके रिलेशनल और पार्शियल हॉर्न लॉजिक (Relational and Partial Horn Logic) के लिए एक नया बीजगणितीय अर्थविज्ञान (algebraic semantics) प्रस्तुत करता है, जो क्लासिफाइंग मॉर्फिज्म (classifying morphisms) के माध्यम से तार्किक संतुष्टि को अभिलक्षणिक बनाता है और Eqlog Datalog इंजन के लिए सैद्धांतिक आधार प्रदान करता है।
यह शोधपत्र उच्च-क्रम (नेस्टेड) क्रिप्के मॉडलों को प्रस्तुत करता है, जो एक ऐसा सामान्यीकरण है जहाँ संसार स्वयं निम्न-क्रम के मॉडल होते हैं, ताकि अंतर्ज्ञानवादी और गैर-शास्त्रीय मोडल लॉजिक के लिए एक एकीकृत ढांचा प्रदान किया जा सके जो पहुंच संबंधों (accessibility relations) और मोडल अभिगृहीतों (modal axioms) के बीच पत्राचार को संरक्षित करता है।
यह योगदान कंजेक्चर-प्रूफ लूप (CPL) को प्रस्तुत करता है, जो एक ऐसा पाइपलाइन है जो लार्ज लैंग्वेज मॉडल के लिए संदर्भ-आधारित शिक्षण का लाभ उठाता है, जिसमें लीन 4 (Lean 4) में इसके अपने औपचारिक रूप से सत्यापित प्रमेयों और प्रमाणों को पुनरावृत्ति से फीड किया जाता है, जिससे नवीन, कठिन-से-सिद्ध होने वाले गणितीय अनुमानों (conjectures) की खोज दर और सफलता में उल्लेखनीय वृद्धि होती है।
यह शोध पत्र टेलर एक्सपेंशन (Taylor expansions) पर कंसन्ट्रेशन इनइक्वालिटीज़ (concentration inequalities) को लागू करके फ्लोटिंग-पॉइंट राउंड-ऑफ त्रुटियों का विश्लेषण करने के लिए एक स्केलेबल संभाव्य दृष्टिकोण प्रस्तावित करता है, जो समान सटीकता के साथ अत्याधुनिक विधियों की तुलना में काफी उच्च समय दक्षता प्राप्त करते हुए, कम्प्यूटेशनल बाधाओं को दूर करने के लिए साउंड ओवर-एप्रोक्सिमेशन्स (sound over-approximations) और रेंज पार्टिशनिंग का उपयोग करता है।
यह शोध पत्र प्रदर्शित करता है कि पर्याप्त रूप से गहरे द्विदिशीय (bidirectional) ट्रांसफॉर्मर्स, स्प्यूरियस सहसंबंधों (spurious correlations) को समाप्त करके और एल्गोरिद्मिक संरेखण (algorithmic alignment) को लागू करके, हॉर्न क्लॉज़ (Horn clauses) पर निहित निवर्तनात्मक तर्क (implicit deductive reasoning) में स्पष्ट चेन-ऑफ-थॉट स्तर का प्रदर्शन प्राप्त कर सकते हैं, हालांकि अधिक गहराई तक विस्तार करने के लिए स्पष्ट तर्क (explicit reasoning) आवश्यक बना हुआ है।
यह शोध पत्र सिद्ध करता है कि निर्देशित -चक्रों (directed -cycles) का निर्देशित कार्तीय उत्पाद (directed Cartesian product), सभी आयामों और सभी विषम माड्यूली के लिए एक निर्देशित हैमिल्टन विखंडन (directed Hamilton decomposition) स्वीकार करता है, जिसमें नए क्लोजर तंत्रों (closure mechanisms), आधार आयाम परिणामों (base dimension results) और लीन 4 (Lean 4) में औपचारिक सत्यापन (formal verification) का संयोजन उपयोग किया गया है।
यह शोध पत्र एग्जॉस्टिव सिम्बोलिक इंटीग्रेशन (ESI) को प्रस्तुत करता है, जो प्रतीकात्मक समाकलन (symbolic integrability) के परिदृश्य को मैप करने के लिए फलनों (functions) को सूचीबद्ध करने की एक विधि है, जो यह प्रकट करता है कि ऑपरेटर बेसिस का चयन समाकलन दरों को महत्वपूर्ण रूप से निर्धारित करता है और मौजूदा कंप्यूटर अलजेब्रा सिस्टम्स से छूट जाने वाले नवीन क्लोज्ड-फॉर्म एंटीडेरिवेटिव्स की खोज को सक्षम बनाता है।
यह शोध पत्र एक पैरामीट्रिक एक्सट्रपलेशन (extrapolation) विधि और संबद्ध एल्गोरिदम प्रस्तुत करता है जो बाउंडेड पैरामीट्रिक टाइमड ऑटोमेटा में पहुँच (reachability), अपरिहार्यता (unavoidability) और अनटाइम व्यवहार संरक्षण सुनिश्चित करने के लिए पैरामीटर मूल्यांकन के सघन, पूर्णांक-पूर्ण सेटों को संश्लेषित करने हेतु समाप्ति की गारंटी देता है, जबकि इस समस्या की सामान्य अनिर्णयता (undecidability) बनी रहती है।