1105 पेपर
यह शोध पत्र Lean 4 के लिए प्रूफ़-स्टेट स्नैपशॉटिंग (proof-state snapshotting) प्रस्तुत करता है, जो एक ऐसी तकनीक है जो समानांतर खोज शाखाओं (parallel search branches) में विस्तृत प्रूफ़ स्टेट्स को कैप्चर और पुन: उपयोग करती है ताकि रेडंडेंट इम्पोर्ट लोडिंग और थ्योरम-बॉडी एलबोरेशन को समाप्त किया जा सके, जिससे ऑटोमेटेड थ्योरम प्रूविंग के लिए 5.6–50x वॉल-टाइम स्पीडअप प्राप्त होता है।
यह शोधपत्र एक पुनर्रूपण प्रमेय (reparameterisation theorem) स्थापित करता है जो यह दर्शाता है कि परिमित स्ट्रिंग्स पर मोनोडिक सेकंड-ऑर्डर और फर्स्ट-ऑर्डर क्वेरीज़, जिनका आउटपुट आकार बहुपद रूप से सीमित (polynomially bounded) है, उन्हें एक स्थिर संख्या में स्थितियों और परिमित डेटा का उपयोग करके MSO-परिभाषित रूप से पहचाना जा सकता है, जिससे यह पुष्टि होती है कि प्रथम-क्रम (first-order) स्ट्रिंग-टू-स्ट्रिंग व्याख्याओं के लिए आयामी न्यूनीकरण (dimension minimisation) लागू होता है।
यह शोधपत्र नलरी इंटरनली पैरामीट्रिक टाइप थ्योरी (Nullary Internally Parametric Type Theory) और एक विशिष्ट नाम इंडक्शन सिद्धांत पर आधारित एक नवीन टाइप थ्योरी प्रस्तुत करता है जो यूनिवर्सल नेम एब्स्ट्रैक्शंस के स्वच्छ टाइपिंग नियमों को एक्सिस्टेंशियल नेम एब्स्ट्रैक्शंस की शक्तिशाली पैटर्न-मैचिंग क्षमताओं के साथ सफलतापूर्वक एकीकृत करता है, जिससे बाइंडर्स वाले सिंटैक्स को निरूपित करने के लिए एक सुव्यवस्थित नोमिनल फ्रेमवर्क स्थापित होता है।
यह शोध पत्र डिवाइड-एंड-कॉन्कर और प्रोजेक्टेड एन्यूमरेशन जैसी स्केलेबल तकनीकों का उपयोग करके थ्योरी लेम्मा के पूर्ण सेटों को कुशलतापूर्वक सूचीबद्ध करने के लिए एक थ्योरी-अग्नोस्टिक फ्रेमवर्क पेश करता है, जिससे क्लासिक ईगर एनकोडिंग की सीमाओं को दूर किया जा सकता है और अनसैट-कोर एक्सट्रैक्शन और मैक्सएसएमटी (MaxSMT) जैसे जटिल एसएमटी कार्यों के लिए प्रदर्शन में महत्वपूर्ण सुधार किया जा सकता है।
यह शोधपत्र डीप होमोमोर्फिज्म नेटवर्क्स (DHNs) को रिलेशनल डेटाबेस के लिए एक शक्तिशाली आर्किटेक्चर के रूप में प्रस्तावित करता है, जो प्रथम-क्रम तर्क (first-order logic) और SQL के विशिष्ट अंशों के साथ उनकी सटीक अभिव्यंजक तुल्यता स्थापित करके, प्रमुख स्टैटिक एनालिसिस समस्याओं के लिए निर्णायकता (decidability) सिद्ध करके, और प्रयोगों के माध्यम से उनके श्रेष्ठ प्रदर्शन को मान्य करके किया गया है।
यह शोध पत्र ImProver 2 को प्रस्तुत करता है, जो एक न्यूरोसिम्बोलिक ढांचा है जो डेटा-कुशल विशेषज्ञ पुनरावृत्ति (expert iteration) को एक संरचनात्मक स्कैफोल्डिंग प्रणाली के साथ जोड़ता है ताकि छोटे भाषा मॉडलों को Lean 4 में जटिल औपचारिक प्रमाणों (formal proofs) को प्रभावी ढंग से अनुकूलित करने में सक्षम बनाया जा सके, जो काफी बड़े मॉडलों से बेहतर प्रदर्शन करता है और प्रमाण अनुकूलन को एक स्केलेबल, सीखने योग्य कार्य के रूप में स्थापित करता है।
यह शोध पत्र इंडक्टिव डिडक्टिव सिंथेसिस (IDS) को प्रस्तुत करता है, जो एक एजेंटिक LLM सिस्टम है जो वितरित प्रणालियों (डिस्ट्रीब्यूटेड सिस्टम्स) के लिए कार्यान्वयन और औपचारिक प्रमाणों को संयुक्त रूप से संश्लेषित करता है, और की-वैल्यू स्टोर विनिर्देशों पर मानव विशेषज्ञों और अत्याधुनिक कोडिंग एजेंटों दोनों की तुलना में काफी कम समय और लागत के साथ 100% सफलता प्राप्त करता है।
यह शोधपत्र नॉन-इंटरफेरेंस गुणों और कंडीशनल इंडिपेंडेंस के बीच संबंध स्थापित करने के लिए प्रोबेबिलिस्टिक सेपरेशन लॉजिक (Lilac) का लाभ उठाते हुए, मास्क्ड क्रिप्टोग्राफिक एल्गोरिदम की प्रोबिंग सुरक्षा के लिए एक नवीन औपचारिक सत्यापन दृष्टिकोण प्रस्तावित करता है।
यह शोध पत्र यह प्रदर्शित करता है कि निर्णय एकत्रीकरण (judgment aggregation) में एयरो-प्रकार के असंभवता परिणाम तब भी पुन: प्रकट होते हैं जब उन्हें वास्तविक रूप से मोडल निर्णयों तक सीमित कर दिया जाता है, जो यह सिद्ध करता है कि विशिष्ट मोडल सिमेंटिक संरचनाएं अकेले ही बिना किसी छद्म तथ्यात्मक प्रस्तावों पर निर्भर रहे, तानाशाही के लिए आवश्यक तार्किक अंतर्संबंध उत्पन्न कर सकती हैं।
यह शोध पत्र लगभग 14,000 लाइनों के कोड के माध्यम से संचार प्रोटोकॉल की सुरक्षा और जीवंतता (liveness) को औपचारिक रूप से सत्यापित करने के लिए, को-इंडक्टिव ट्रीज़ (coinductive trees) और संबंधों का उपयोग करते हुए, रॉक (Rocq) प्रूफ असिस्टेंट में सिंक्रोनस मल्टीपार्टी सेशन टाइप्स के लिए जीवंतता का पहला यांत्रिक प्रमाण प्रस्तुत करता है।