Exact Verification of Graph Neural Networks with Incremental Constraint Solving
Graph neural networks (GNNs) are increasingly often employed in high-stakes applications, such as fraud detection or healthcare, but are susceptible to adversarial attacks. A number of techniques have been proposed to provide adversarial robustness guarantees, but support for commonly used aggregation functions in message-passing GNNs is lacking. In this paper, we develop an exact (sound and complete) verification method for GNNs to compute guarantees against attribute and structural perturbations that involve edge addition or deletion, subject to budget constraints. Our method employs constraint solving with bound tightening, and iteratively solves a sequence of relaxed constraint satisfaction problems while relying on incremental solving capabilities of solvers to improve efficiency. We implement GNNev, a versatile exact verifier for message-passing neural networks, which supports three aggregation functions -- sum, max and mean -- with the latter two considered here for the first time. Extensive experimental evaluation of GNNev on real-world fraud datasets (Amazon and Yelp) and biochemical datasets (MUTAG and ENZYMES) demonstrates its usability and effectiveness, as well as superior performance on node classification and competitiveness on graph classification compared to existing exact verification tools on sum-aggregated GNNs.
Code (0)
등록된 구현이 없습니다.
Tasks
Adversarial RobustnessGraph ClassificationNode ClassificationFraud DetectionSimilar Papers 제목 키워드 기반
Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks
Constraint solving is an elementary way for verification of deep neural networks (DNN). In the domain of AI safety, a DNN might be modified in its structure and parameters for its repair or attack. For such situations, w…
validIncremental Pruning: A Simple, Fast, Exact Method for Partially Observable Markov Decision Processes
Most exact algorithms for general partially observable Markov decision processes (POMDPs) use a form of dynamic programming in which a piecewise-linear and convex representation of one value function is transformed into …
Incremental Real-Time Multibody VSLAM with Trajectory Optimization Using Stereo Camera
Real time outdoor navigation in highly dynamic environments is an crucial problem. The recent literature on real time static SLAM don't scale up to dynamic outdoor environments. Most of these methods assume moving object…
Motion SegmentationSemanticForge: Repository-Level Code Generation through Semantic Knowledge Graphs and Constraint Satisfaction
Large language models (LLMs) have transformed software development by enabling automated code generation, yet they frequently suffer from systematic errors that limit practical deployment. We identify two critical failur…
Knowledge GraphsCode Generatione-boost: Boosted E-Graph Extraction with Adaptive Heuristics and Exact Solving
E-graphs have attracted growing interest in many fields, particularly in logic synthesis and formal verification. E-graph extraction is a challenging NP-hard combinatorial optimization problem. It requires identifying op…