2025-11-21T04:31:15.286585

Lecture Notes on Verifying Graph Neural Networks

Schwarzentruber
In these lecture notes, we first recall the connection between graph neural networks, Weisfeiler-Lehman tests and logics such as first-order logic and graded modal logic. We then present a modal logic in which counting modalities appear in linear inequalities in order to solve verification tasks on graph neural networks. We describe an algorithm for the satisfiability problem of that logic. It is inspired from the tableau method of vanilla modal logic, extended with reasoning in quantifier-free fragment Boolean algebra with Presburger arithmetic.
academic

ग्राफ न्यूरल नेटवर्क्स के सत्यापन पर व्याख्यान नोट्स

मूल जानकारी

  • पेपर ID: 2510.11617
  • शीर्षक: ग्राफ न्यूरल नेटवर्क्स के सत्यापन पर व्याख्यान नोट्स
  • लेखक: François Schwarzentruber (ENS de Lyon)
  • वर्गीकरण: cs.LO (कंप्यूटर विज्ञान में तर्क), cs.LG (मशीन लर्निंग)
  • प्रकाशन समय: 14 अक्टूबर, 2025
  • पेपर लिंक: https://arxiv.org/abs/2510.11617

सारांश

ये व्याख्यान नोट्स सबसे पहले ग्राफ न्यूरल नेटवर्क्स, Weisfeiler-Lehman परीक्षण और प्रथम-क्रम तर्क, श्रेणीबद्ध मोडल तर्क जैसी तार्किक प्रणालियों के बीच संबंधों की समीक्षा करते हैं। फिर एक मोडल तर्क प्रस्तावित किया गया है, जिसमें गणना मोडल रैखिक असमानताओं में दिखाई देते हैं, जो ग्राफ न्यूरल नेटवर्क्स के सत्यापन कार्य को हल करने के लिए उपयोग किया जाता है। इस तर्क की संतुष्टि समस्या के लिए एक एल्गोरिदम का वर्णन किया गया है, जो पारंपरिक मोडल तर्क की तालिका विधि से प्रेरित है, और परिमाणक-मुक्त खंड बूलियन बीजगणित और Presburger अंकगणित के तर्क को विस्तारित करता है।

अनुसंधान पृष्ठभूमि और प्रेरणा

समस्या पृष्ठभूमि

ग्राफ न्यूरल नेटवर्क्स (GNNs) सामाजिक नेटवर्क सिफारिशों, ज्ञान ग्राफ, रासायनिक अणु विश्लेषण, दवा खोज और कई अन्य क्षेत्रों में व्यापक रूप से लागू किए गए हैं। हालांकि, GNNs की सत्यापन समस्या को गंभीर चुनौतियों का सामना करना पड़ता है:

  1. अभिव्यक्ति क्षमता सीमाएं: GNNs की अभिव्यक्ति क्षमता 1-WL (Weisfeiler-Lehman) परीक्षण द्वारा सीमित है, कुछ गैर-समरूप ग्राफ को अलग नहीं कर सकते
  2. सत्यापन कार्य की जटिलता: यह सत्यापित करने की आवश्यकता है कि क्या GNN विशिष्ट विनिर्देशों को संतुष्ट करता है, जैसे सुरक्षा, सही गुण आदि
  3. सैद्धांतिक आधार की कमी: GNN के व्यवहार का वर्णन और सत्यापन करने के लिए एक व्यवस्थित तार्किक ढांचे की कमी है

अनुसंधान प्रेरणा

  • व्यावहारिक आवश्यकता: सुरक्षा-महत्वपूर्ण अनुप्रयोगों में, GNN की विश्वसनीयता और सही कार्यप्रणाली सुनिश्चित करने की आवश्यकता है
  • सैद्धांतिक अंतराल: मौजूदा सत्यापन विधियों में एकीकृत तार्किक सिद्धांत आधार की कमी है
  • तकनीकी चुनौतियां: GNN में एकत्रीकरण संचालन और गणना बाधाओं को संभालने की आवश्यकता है

मुख्य योगदान

  1. सैद्धांतिक संबंध स्थापित करना: GNNs, Weisfeiler-Lehman परीक्षण और तार्किक प्रणालियों (FO, FOC, GML) के बीच गहरे संबंधों को व्यवस्थित रूप से स्पष्ट करना
  2. K# तर्क प्रस्तावित करना: एक नई मोडल तर्क K# डिजाइन करना, जो GNN के गणना और एकत्रीकरण संचालन को व्यक्त कर सकती है
  3. एल्गोरिदम डिजाइन: K# तर्क संतुष्टि समस्या के लिए PSPACE एल्गोरिदम विकसित करना, तालिका विधि और QFBAPA तर्क पर आधारित
  4. जटिलता विश्लेषण: विभिन्न सक्रियण कार्यों के तहत GNN सत्यापन समस्या की कम्प्यूटेशनल जटिलता सीमाओं को साबित करना
  5. व्यावहारिक ढांचा: GNN सत्यापन कार्यों को तार्किक संतुष्टि समस्याओं में कम करने के लिए एक संपूर्ण ढांचा प्रदान करना

विधि विवरण

कार्य परिभाषा

GNN सत्यापन के मुख्य कार्यों में शामिल हैं:

  • संतुष्टि: दिए गए GNN N के लिए, क्या कोई इनपुट मौजूद है जो सकारात्मक आउटपुट देता है?
  • विनिर्देश सत्यापन: क्या GNN दिए गए तार्किक विनिर्देश φ को संतुष्ट करता है?
  • समतुल्यता जांच: क्या दोनों GNN सभी इनपुट पर समतुल्य हैं?

K# तर्क आर्किटेक्चर

वाक्य विन्यास परिभाषा

φ ::= p | ¬φ | φ ∨ φ | ξ ≥ 0
ξ ::= c | 1φ | #φ | ξ + ξ | c × ξ

शब्दार्थ परिभाषा

  • 1φ: यदि φ सत्य है तो मान 1, अन्यथा 0
  • #φ: φ को संतुष्ट करने वाले उत्तराधिकारी नोड्स की संख्या की गणना करता है
  • रैखिक अभिव्यक्ति: जोड़ और स्केलर गुणन का समर्थन करता है

मुख्य विशेषताएं

  1. अभिव्यक्ति क्षमता: K# तर्क में श्रेणीबद्ध मोडल तर्क (GML) एक उपसमुच्चय के रूप में शामिल है
  2. पत्राचार संबंध: truncReLU-GNNs के साथ बहुपद समय के द्विदिशीय अनुवाद मौजूद है
  3. गणना बाधाएं: जटिल गणना संबंधों और एकत्रीकरण संचालन को व्यक्त कर सकता है

GNN-K# पत्राचार संबंध

K# से GNN तक

tr(xi = 1) = xi
tr(¬φ) = 1 - truncReLU(tr(φ))
tr(φ ∧ ψ) = truncReLU(tr(φ) + tr(ψ) - 1)
tr(#φ) = agg(tr(φ))

GNN से K# तक

tr'(truncReLU(ϑ)) = 1tr'(ϑ)≥1
tr'(agg(ϑ)) = #(tr'(ϑ) ≥ 1)

संतुष्टि एल्गोरिदम

QFBAPA आधार

गणना बाधाओं को संभालने के लिए परिमाणक-मुक्त बूलियन बीजगणित और Presburger अंकगणित (QFBAPA) का उपयोग:

  • Venn आरेख तकनीक: समुच्चय अभिव्यक्तियों को क्षेत्र चर में परिवर्तित करता है
  • Carathéodory सीमा: साबित करता है कि केवल बहुपद संख्या में गैर-शून्य क्षेत्रों पर विचार करने की आवश्यकता है
  • NP जटिलता: QFBAPA संतुष्टि समस्या NP के अंदर है

K# तालिका एल्गोरिदम

प्रक्रिया satK#(Γ)
  बूलियन नियमों और 1φ निर्माण को संसाधित करता है
  रैखिक असमानता बाधाएं S निकालता है
  गैर-शून्य क्षेत्र B ⊆ {0,1}d, |B| ≤ 2d log₂(4d) का अनुमान लगाता है
  #ψᵢ को ∑ρ∈B|ρᵢ=1 sρ से प्रतिस्थापित करता है
  QFPA संतुष्टि की जांच करता है
  विभिन्न क्षेत्रों को पुनरावर्ती रूप से सत्यापित करता है

प्रायोगिक सेटअप

सैद्धांतिक सत्यापन

पेपर मुख्य रूप से सैद्धांतिक विश्लेषण करता है, रचनात्मक प्रमाण के माध्यम से सत्यापन:

  1. सही कार्यप्रणाली: एल्गोरिदम की सही कार्यप्रणाली और पूर्णता
  2. जटिलता: समय और स्पेस जटिलता सीमाएं
  3. अभिव्यक्ति क्षमता: विभिन्न तार्किक खंडों के बीच अभिव्यक्ति क्षमता संबंध

जटिलता परिणाम

सक्रियण कार्यनिर्देशित ग्राफअनिर्देशित ग्राफ
truncReLUPSPACE-completePSPACE-complete
ReLUNEXPTIME-completeअनिर्णीय
वैश्विक पढ़ने के साथ truncReLUNEXPTIME-completeअनिर्णीय

प्रायोगिक परिणाम

मुख्य सैद्धांतिक परिणाम

अभिव्यक्ति क्षमता संबंध

  • cr(G,u) = cr(G',u') ⟺ G,u और G',u' समान GML सूत्रों को संतुष्ट करते हैं
  • GML ⊆ K# ⊆ FOC₂
  • K# कड़ाई से FO से मजबूत है

जटिलता सीमाएं

  1. K# संतुष्टि: PSPACE-complete
  2. truncReLU-GNN सत्यापन: PSPACE-complete
  3. ReLU-GNN सत्यापन: NEXPTIME-complete
  4. वैश्विक पढ़ना: अनिर्णीयता की ओर ले जाता है (अनिर्देशित ग्राफ मामला)

एल्गोरिदम दक्षता

  • स्पेस जटिलता: बहुपद स्पेस
  • क्षेत्रों की संख्या: अधिकतम 2d log₂(4d) गैर-शून्य क्षेत्र
  • अनुवाद ओवरहेड: बहुपद समय (पूर्णांक वजन मामला)

तकनीकी अंतर्दृष्टि

Weisfeiler-Lehman कनेक्शन

  • रंग परिशोधन एल्गोरिदम GNN की आवश्यक कम्प्यूटेशनल पैटर्न को पकड़ता है
  • k-WL पदानुक्रम विभिन्न क्रम GNN की अभिव्यक्ति क्षमता से मेल खाता है
  • मोडल तर्क इस पदानुक्रम का वर्णन करने के लिए एक प्राकृतिक भाषा प्रदान करता है

गणना बाधा प्रबंधन

  • QFBAPA एकत्रीकरण संचालन को संभालने के लिए एक प्रभावी ढांचा प्रदान करता है
  • Venn आरेख तकनीक जटिल गणना बाधाओं को रैखिक प्रोग्रामिंग में सरल बनाती है
  • Carathéodory सीमा एल्गोरिदम की बहुपद स्पेस जटिलता सुनिश्चित करती है

संबंधित कार्य

GNN सैद्धांतिक आधार

  • अभिव्यक्ति क्षमता: Xu et al. (2019), Morris et al. (2019) ने GNN और WL परीक्षण के बीच संबंध स्थापित किए
  • तार्किक लक्षण वर्णन: Barceló et al. (2020) ने पहली बार GNN और तर्क के बीच पत्राचार स्थापित किया
  • सत्यापन विधियां: Benedikt et al. (2024) ने निर्णय प्रक्रियाएं प्रस्तावित कीं, लेकिन एकीकृत ढांचे की कमी है

मोडल तर्क सत्यापन

  • पारंपरिक विधियां: तालिका विधि पर आधारित मोडल तर्क निर्णय प्रक्रियाएं
  • गणना विस्तार: श्रेणीबद्ध मोडल तर्क की संतुष्टि एल्गोरिदम
  • जटिलता सिद्धांत: विभिन्न मोडल तर्क खंडों की जटिलता विश्लेषण

तंत्रिका नेटवर्क सत्यापन

  • SMT विधियां: तंत्रिका नेटवर्क गुणों को सत्यापित करने के लिए SMT सॉल्वर का उपयोग
  • अमूर्त व्याख्या: अमूर्त डोमेन के माध्यम से नेटवर्क व्यवहार का विश्लेषण
  • प्रतीकात्मक निष्पादन: नेटवर्क के निष्पादन पथों का प्रतीकात्मक रूप से अन्वेषण

निष्कर्ष और चर्चा

मुख्य निष्कर्ष

  1. सैद्धांतिक एकीकरण: GNN, WL परीक्षण और तार्किक प्रणालियों के बीच एकीकृत सैद्धांतिक ढांचा स्थापित किया
  2. एल्गोरिदम योगदान: GNN सत्यापन के लिए प्रभावी एल्गोरिदम प्रदान किए, जटिलता इष्टतम है
  3. अभिव्यक्ति क्षमता: K# तर्क truncReLU-GNN की कम्प्यूटेशनल क्षमता को सटीक रूप से पकड़ता है
  4. जटिलता पृथक्करण: विभिन्न सक्रियण कार्य सत्यापन जटिलता में महत्वपूर्ण अंतर की ओर ले जाते हैं

सीमाएं

  1. सक्रियण कार्य प्रतिबंध: मुख्य परिणाम truncReLU पर केंद्रित हैं, ReLU मामला अधिक जटिल है
  2. परिमाणीकरण समस्याएं: परिमेय संख्या वजन को घातीय आकार के सामान्य हर की आवश्यकता है
  3. कार्यान्वयन जटिलता: एल्गोरिदम का वास्तविक कार्यान्वयन अभी भी दक्षता चुनौतियों का सामना करता है
  4. अनुप्रयोग सीमा: मुख्य रूप से नोड वर्गीकरण कार्यों के लिए, ग्राफ-स्तरीय कार्यों को अतिरिक्त विचार की आवश्यकता है

भविष्य की दिशाएं

  1. सक्रियण कार्य विस्तार: अधिक सामान्य सक्रियण कार्यों की सत्यापन विधियों का अनुसंधान
  2. एल्गोरिदम अनुकूलन: एल्गोरिदम के व्यावहारिक प्रदर्शन और स्केलेबिलिटी में सुधार
  3. उपकरण विकास: व्यावहारिक GNN सत्यापन उपकरण विकसित करना
  4. अनुप्रयोग विस्तार: अधिक GNN आर्किटेक्चर और कार्य प्रकारों तक विस्तार

गहन मूल्यांकन

शक्तियां

  1. सैद्धांतिक गहराई: गहरे सैद्धांतिक संबंध स्थापित करता है, महत्वपूर्ण सैद्धांतिक अंतराल को भरता है
  2. विधि नवाचार: K# तर्क का डिजाइन अभिव्यक्ति क्षमता और निर्णयशीलता को चतुराई से संतुलित करता है
  3. एल्गोरिदम सुंदरता: तालिका विधि और QFBAPA का संयोजन प्राकृतिक और कुशल दोनों है
  4. परिणाम पूर्णता: संपूर्ण जटिलता विश्लेषण और पत्राचार प्रमाण प्रदान करता है
  5. शिक्षा मूल्य: व्याख्यान नोट्स के रूप में, संरचना स्पष्ट है, सीखने और शिक्षण के लिए उपयुक्त है

कमियां

  1. प्रायोगिक सत्यापन की कमी: व्यावहारिक प्रायोगिक सत्यापन और प्रदर्शन मूल्यांकन की कमी है
  2. कार्यान्वयन विवरण: एल्गोरिदम के विशिष्ट कार्यान्वयन और अनुकूलन रणनीति पर चर्चा अपर्याप्त है
  3. अनुप्रयोग मामले: विशिष्ट अनुप्रयोग परिदृश्य और केस अध्ययन की कमी है
  4. उपकरण समर्थन: कोई उपलब्ध सत्यापन उपकरण या प्रोटोटाइप सिस्टम प्रदान नहीं किया गया है

प्रभाव

  1. सैद्धांतिक योगदान: GNN सत्यापन क्षेत्र के लिए एक ठोस सैद्धांतिक आधार स्थापित करता है
  2. विधि प्रेरणा: बाद के अनुसंधान के लिए महत्वपूर्ण पद्धति संबंधी मार्गदर्शन प्रदान करता है
  3. शिक्षा मूल्य: एक उत्कृष्ट शिक्षण सामग्री के रूप में, क्षेत्र में प्रतिभा विकास में सहायता करता है
  4. व्यावहारिक संभावना: सैद्धांतिक रूप से मजबूत होने के बावजूद, व्यावहारिक उपकरण विकास के लिए दिशा प्रदान करता है

लागू परिदृश्य

  1. सुरक्षा-महत्वपूर्ण प्रणालियां: GNN अनुप्रयोगों को कड़ाई से सत्यापित करने की आवश्यकता है
  2. सैद्धांतिक अनुसंधान: GNN अभिव्यक्ति क्षमता और जटिलता का सैद्धांतिक विश्लेषण
  3. शिक्षण प्रशिक्षण: ग्राफ तंत्रिका नेटवर्क और तार्किक सत्यापन की शिक्षा
  4. उपकरण विकास: GNN सत्यापन उपकरणों के लिए सैद्धांतिक आधार

संदर्भ

पेपर 65 महत्वपूर्ण संदर्भों का हवाला देता है, जिसमें शामिल हैं:

  • GNN सैद्धांतिक आधार (Grohe 2021, Barceló et al. 2020)
  • Weisfeiler-Lehman परीक्षण (Morris et al. 2019, Xu et al. 2019)
  • मोडल तर्क (Blackburn et al. 2001, Tobies 1999)
  • जटिलता सिद्धांत (Grädel et al. 1997, Kuncak and Rinard 2007)
  • तंत्रिका नेटवर्क सत्यापन (Benedikt et al. 2024, Haase and Zetzsche 2019)

समग्र मूल्यांकन: यह सैद्धांतिक गहराई और शिक्षा मूल्य दोनों को संतुलित करने वाला एक उत्कृष्ट पेपर है। यह न केवल GNN सत्यापन की महत्वपूर्ण सैद्धांतिक समस्याओं को हल करता है, बल्कि बाद के अनुसंधान और व्यावहारिक अनुप्रयोगों के लिए एक ठोस आधार स्थापित करता है। हालांकि प्रायोगिक सत्यापन की कमी है, लेकिन इसके सैद्धांतिक योगदान का महत्व अनदेखा नहीं किया जा सकता।