1115 पेपर
यह शोध पत्र CTLF को प्रस्तुत करता है, जो काउंटिंग वर्ल्ड्स (counting worlds) सिमेंटिक्स वाला एक ब्रांचिंग-टाइम लॉजिक है, जो आउटपुट अनुक्रमों में निष्पक्षता के उल्लंघनों के सत्यापन, भविष्यवाणी और सुधार को सक्षम करके जनरेटिव एआई में पोस्ट-हॉक पूर्वाग्रह शमन (post-hoc bias mitigation) के लिए औपचारिक गारंटी प्रदान करता है।
यह शोध पत्र इस बात की जांच करता है कि क्या बड़े भाषा मॉडल (large language models) तार्किक तर्क कार्यों को हल करते समय प्रमाण वैधता (proof validity) और औपचारिकीकरण निष्ठा (formalization faithfulness) के बीच के अंतर का लाभ उठाते हैं, जिसमें यह पाया गया है कि हालांकि मॉडल आम तौर पर विफलता रिपोर्ट करने को प्राथमिकता देकर "औपचारिकीकरण गेमिंग" (formalization gaming) से बचते हैं, फिर भी अक्षत (axiom) निर्माण और आधारवाक्य गलत अनुवाद (premise mistranslation) जैसे विशिष्ट अविश्वसनीय व्यवहार बने रहते हैं और उच्च संकलन दरों (compilation rates) द्वारा भी अनपेक्षित रहते हैं।
यह शोध पत्र maude2athena को प्रस्तुत करता है, जो एक ऐसा फ्रेमवर्क है जो माउडे (Maude) के समीकरण संबंधी विनिर्देशों (equational specifications) को एथेना (Athena) थ्योरम प्रूवर में अनुवादित करता है ताकि संरचनात्मक अभिलेखों (structural axioms) के सापेक्ष इंडक्शन (induction modulo structural axioms) सहित आगमनात्मक और निगमनात्मक तर्क (inductive and deductive reasoning) को सक्षम किया जा सके, जबकि अर्थ संबंधी निष्ठा (semantic fidelity) को बनाए रखा जाए और एक संक्षिप्त अनुवाद सुनिश्चित किया जाए।
यह शोध पत्र लीन 4 (Lean 4) में ग्रोबनर बेसिस (Gröbner basis) सिद्धांत के एक औपचारिकीकरण को प्रस्तुत करता है जो मनमाने (अनंत सहित) चरों वाले बहुपद रिंग्स (polynomial rings) के लिए बुचबर्गर मानदंड (Buchberger's criterion) और रिड्यूस्ड बेसिस (reduced bases) जैसे मुख्य आधारों को स्थापित करता है, साथ ही मोनोमियल-ऑर्डर एम्बेडिंग्स (monomial-order embeddings) और फिल्टर-आधारित सीमाओं (filter-based limits) के माध्यम से इन अनंत परिवेशों को परिमित उप-रिंग्स (finite subrings) से जोड़ता है।
यह शोध पत्र लीन एटलस (Lean Atlas) का परिचय देता है, जो एक ओपन-सोर्स इंटरैक्टिव वेब टूल है जिसमें लीन कम्पास (Lean Compass) एल्गोरिदम है जो प्रोजेक्ट निर्भरताओं को विज़ुअलाइज़ करने और उन विशिष्ट परिभाषाओं और प्रमेयों की स्वचालित रूप से पहचान करने में सक्षम बनाता है जिन्हें मानव अर्थ संबंधी सत्यापन (semantic verification) की आवश्यकता होती है ताकि AI-जनित प्रमाणों में अर्थ संबंधी मतिभ्रम (semantic hallucinations) प्रदर्शित होने से रोका जा सके, जिससे गणित को औपचारिक बनाने में स्केलेबल मानव-AI सहयोग संभव हो सके।
यह शोध पत्र एक नवीन दो-साक्षी (two-witness) निर्माण के माध्यम से, जो शास्त्रीय तर्क, विकर्णन (diagonalization), और गैर-समाप्ति पर केस स्प्लिट्स से बचता है, हिल्बर्ट की दसवीं समस्या की अनिर्णयता में अपचयित करके, सहज बोधपरक तर्क (intuitionistic logic) के भीतर राइस के प्रमेय और हाल्टिंग समस्या का एक रचनात्मक प्रमाण प्रस्तुत करता है।
यह शोधपत्र यह स्थापित करता है कि -सघन (dense) मोडल लॉजिक्स के लिए संतुष्टि (satisfiability) समस्या पैरामीटराइज्ड कॉम्प्लेक्सिटी क्लास para- में आती है, जो मौजूदा विश्लेषण उपकरणों को सामान्यीकृत करने के लिए रिकर्सिव विंडोज़ (recursive windows) को पेश करता है, जिससे मोडल डेप्थ (modal depth) को एक पैरामीटर के रूप में मानने पर एक पॉलीनोमियल-स्पेस एल्गोरिदम के अस्तित्व को सिद्ध किया जा सके।
यह शोध पत्र एक SAT-आधारित डिकपलिंग पद्धति प्रस्तावित करता है जो विभिन्न यूनिट कमिटमेंट प्रॉब्लम वेरिएंट्स को मानक SAT इंस्टेंस में एकीकृत करती है, जिससे एक एकल, सामान्यीकरण योग्य एल्गोरिदम समाधान की गुणवत्ता और विकसित होते पावर सिस्टम आवश्यकताओं के अनुकूलन, दोनों में विशिष्ट सॉल्वर से बेहतर प्रदर्शन करने में सक्षम होता है।
यह शोध पत्र "परमाणु निर्णय सीमाओं" (atomic decision boundaries) की अवधारणा प्रस्तुत करता है ताकि औपचारिक रूप से यह सिद्ध किया जा सके कि स्वायत्त प्रणालियों में निष्पादन-समय स्वीकार्यता (execution-time admissibility) की गारंटी देना संरचनात्मक रूप से नीति मूल्यांकन (policy evaluation) और अवस्था संक्रमण (state transition) को एक एकल अविभाज्य चरण में युग्मित करने की आवश्यकता रखता है, क्योंकि विभाजित मॉडल समवर्ती वातावरणों (concurrent environments) में स्वीकार्यता उल्लंघनों को रोकने में स्वाभाविक रूप से अक्षम होते हैं।
यह शोध पत्र TensorRocq प्रस्तुत करता है, जो Rocq प्रूफ असिस्टेंट के लिए एक सत्यापित टूलकिट है जो सिमेट्रिक मोनोइडल कैटेगरी टर्म्स को हाइपरग्राफ में बदलकर औपचारिक प्रमाणों और आरेखीय तर्क (डायग्रामैटिक रीजनिंग) के बीच के अंतर को पाटता है ताकि सहज स्ट्रिंग डायग्राम हेरफेर और समीकरण संबंधी रीराइटिंग सक्षम की जा सके।