paper-with-me

홈 › Papers

Exact Verification of Graph Neural Networks with Incremental Constraint Solving

2025-08-12 · Minghao Liu, Chia-Hsuan Lu, Marta Kwiatkowska arxiv

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.

📄 PDF Abstract BibTeX arXiv:2508.09320

Code (0)

등록된 구현이 없습니다.

Tasks

Adversarial RobustnessGraph ClassificationNode ClassificationFraud Detection

Similar Papers 제목 키워드 기반

Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks

2023-02-10 · Pengfei Yang, Zhiming Chi, Zongxin Liu, Mengyu Zhao 외

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…

valid

Incremental Pruning: A Simple, Fast, Exact Method for Partially Observable Markov Decision Processes

2013-02-06 · Anthony R. Cassandra, Michael L. Littman, Nevin Lianwen Zhang

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

2016-08-02 · N. Dinesh Reddy, Iman Abbasnejad, Sheetal Reddy, Amit Kumar Mondal 외

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 Segmentation

SemanticForge: Repository-Level Code Generation through Semantic Knowledge Graphs and Constraint Satisfaction

2025-11-10 · Wuyang Zhang, Chenkai Zhang, Zhen Luo, Jianming Ma 외 arxiv

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 Generation

e-boost: Boosted E-Graph Extraction with Adaptive Heuristics and Exact Solving

2025-08-18 · Jiaqi Yin, Zhan Song, Chen Chen, Yaohui Cai 외 arxiv

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…