💻 Category

cs.LO

1105 पेपर

💻 computer science

Pseudo-Formalization for Automatic Proof Verification

यह शोध पत्र 'स्यूडो-फॉर्मलाइजेशन' (Pseudo-Formalization) प्रस्तुत करता है, जो प्राकृतिक भाषा की लचीलेपन और औपचारिक मॉड्यूलैरिटी (formal modularity) का संयोजन करने वाला एक हाइब्रिड प्रूफ़ फॉर्मेट है, और एक संबंधित 'ब्लॉक वेरिफिकेशन' (Block Verification) एल्गोरिदम भी प्रस्तुत करता है जो ओलंपियाड और अनुसंधान-स्तर के बेंचमार्क में गणितीय प्रमाणों को सटीक रूप से सत्यापित करने में मौजूदा 'LLM-as-judge' बेसलाइनों की तुलना में काफी बेहतर प्रदर्शन करता है।

Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid, Tengyu Ma2026-05-21
💻 computer science

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

यह शोध पत्र कॉज़ल पास्ट लॉजिक (CPL) को प्रस्तुत करता है, जो ज़िपरजेन (ZipperGen) फ्रेमवर्क में एकीकृत एक स्रोत-स्तरीय टेम्पोरल लॉजिक है, जो वितरित LLM एजेंटों को अनुक्रमिक लॉग के बजाय कारण-संबंधी रूप से दृश्यमान घटनाओं के आधार पर कंट्रोल फ्लो के ऑनलाइन रनटाइम सत्यापन को सक्षम बनाता है, जिसमें सिमेंटिक शुद्धता सुनिश्चित करने के लिए एक वेक्टर-क्लॉक मॉनिटर का उपयोग किया गया है।

Benedikt Bollig2026-05-21
💻 computer science

Complete Supermartingale Certificates for ω\omega-Regular Properties

यह शोधपत्र एक सामान्य कार्यप्रणाली प्रस्तुत करता है जो ω\omega-नियमित गुणों को लगभग-निश्चित समाप्ति दायित्वों में विभाजित करता है, जिससे गणनीय अनंत अवस्था स्थानों वाले समय-समरूप मार्कोव श्रृंखलाओं पर लगभग-निश्चित और मात्रात्मक ω\omega-नियमित गुणों के सत्यापन के लिए प्रथम सुदृढ़ और पूर्ण (या ε\varepsilon-पूर्ण) सुपरमार्टिंगेल प्रमाण-पत्रों का निर्माण संभव हो पाता है।

Alessandro Abate, Mirco Giacobbe, Sergey Ichtchenko, Diptarko Roy2026-05-21
💻 computer science

Tao's Equational Proof Challenge Accepted (Technical Report)

यह शोध पत्र क्रिम्पा (Krympa) को प्रस्तुत करता है, जो एक प्रमाण न्यूनीकरण उपकरण (proof minimization tool) है जो टेरेंस ताओ के 62-चरणीय समीकरण संबंधी प्रमाण को सफलतापूर्वक 20 चरणों तक कम करता है और ब्रूट फोर्स, ह्यूरिस्टिक्स और कई स्वचालित प्रूवर्स के संयोजन द्वारा अन्य जटिल प्रमाणों को महत्वपूर्ण रूप से संकुचित करता है।

Lydia Kondylidou, Jasmin Blanchette, Marijn J. H. Heule2026-05-21
💻 computer science

Verification of Configurable SRA Systems

यह शोधपत्र कंपोजिशनल प्रूफ नियमों, स्वचालित विधि सारांशीकरण (automatic method summarization) और कॉन्फ़िगरेशन स्पेस सरलीकरण को संयोजित करके, कॉन्फ़िगर करने योग्य शेड्यूलर-प्रतिबंधित एसिंक्रोनस (SRA) प्रणालियों के भीतर सभी कानूनी इंस्टेंशिएशन की शुद्धता को सिद्ध करने के लिए Dafny सॉफ़्टवेयर वेरीफायर का उपयोग करते हुए एक अनुबंध-आधारित, निगमित सत्यापन ढांचा प्रस्तावित करता है।

Alessandro Cimatti, Alberto Griggio, Christian Lidström, Gianluca Redondi, Dylan Trenti2026-05-21
💻 computer science

Dependent Multiplicities in Dependent Linear Type Theory

यह शोध पत्र एक नवीन डिपेंडेंट लीनियर टाइप थ्योरी प्रस्तुत करता है जो चरों (variables) की बहुलता (multiplicities) को अन्य चरों पर निर्भर करने में सक्षम बनाता है, जिससे डिपेंडेंट टाइप थ्योरी में लीनियर लॉजिक के एम्बेडिंग के माध्यम से ब्रांचिंग और रिकर्सिव प्रोग्राम्स के लिए सटीक रिसोर्स एनोटेशन प्रदान किया जाता है, जिसे एक कैटेगोरिकल सेमैntिक्स और एक एगडा (Agda) कार्यान्वयन द्वारा समर्थित किया गया है।

Maximilian Doré2026-05-20
💻 computer science

Computation and Size of Interpolants for Hybrid Modal Logics

यह शोध पत्र यह सिद्ध करने के लिए एक नई हाइपरमोज़ेक उन्मूलन तकनीक प्रस्तुत करता है कि मानक हाइब्रिड मोडल लॉजिक में क्रेग इंटरपुलेंट्स की गणना चार गुना घातीय समय (fourfold exponential time) में की जा सकती है, और साथ ही यह भी प्रदर्शित करता है कि इन लॉजिक्स में यूनिफॉर्म इंटरपुलेंट्स का अस्तित्व अनिर्णय योग्य (undecidable) है।

Jean Christoph Jung, Jędrzej Kołodziejski, Frank Wolter2026-05-20
💻 computer science

Satisfiability Modulo Extensional Constant Arrays (Extended Version)

यह शोध पत्र एक्सटेंशनल एरेज़ (extensional arrays) के साथ कॉन्स्टेंट एरेज़ (constant arrays) की SMT थ्योरी के लिए एक नवीन, सुदृढ़ निर्णय प्रक्रिया प्रस्तुत करता है जो अनिश्चित इंडेक्स डोमेन (arbitrary index domains) का समर्थन करती है, जो परिमित (finite) या अनंत (infinite) मामलों की पिछली सीमाओं को दूर करती है, और बिटज़ुला (Bitwuzla) सॉल्वर में कार्यान्वयन के माध्यम से इसकी प्रभावशीलता को प्रदर्शित करती है।

Mathias Preiner, Aina Niemetz, Clark Barrett2026-05-20
💻 computer science

Ordered Adjoint Logic (Extended Version)

यह शोध पत्र एडजॉइंट मोडैलिटीज़ (adjoint modalities) की एक प्रणाली पेश करके क्रमबद्ध तर्कशास्त्र (ordered logics) पर पूर्ववर्ती कार्यों का सामान्यीकरण करता है जो वीकनिंग (weakening) और कॉन्ट्रैक्शन (contraction) जैसे विभिन्न संरचनात्मक गुणों वाले तर्कशास्त्रों को संयोजित करता है, यह सिद्ध करते हुए कि परिणामी सीक्वेंट कैलकुलस (sequent calculus) कट एलिमिनेशन (cut elimination) को स्वीकार करता है और इसका नेचुरल डीडक्शन (natural deduction) निरूपण निर्णायक प्रूफ चेकिंग (decidable proof checking) का समर्थन करता है।

Sophia Roshal, Frank Pfenning2026-05-20
💻 computer science

Executable Boundary Contracts for Sound Event Traces

यह शोध पत्र समयबद्ध सीमा व्यवहारों (timed boundary behaviors) के सटीक मापन को सक्षम करने के लिए परिमित ध्वनि घटना ट्रेस (finite sound event traces) हेतु निष्पादन योग्य सीमा अनुबंधों (executable boundary contracts) को प्रस्तुत करता है, जो विविध डेटासेट पर प्रयोगों के माध्यम से यह प्रदर्शित करता है कि मानक स्कोरिंग मेट्रिक्स अक्सर उन विशिष्ट सीमा विफलताओं का पता लगाने में विफल रहते हैं जिन्हें ये अनुबंध स्पष्ट रूप से पहचान सकते हैं।

Faruk Alpay, Hamdi Alakkad2026-05-20