A Logic for Reasoning About Aggregate-Combine Graph Neural Networks
Not on the map. Why?
Abstract (arXiv)
We propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that a broad class of GNNs can be transformed efficiently into a formula, thus significantly improving upon the literature about the logical expressiveness of GNNs. We also show that the satisfiability problem is PSPACE-complete. These results bring together the promise of using standard logical methods for reasoning about GNNs and their properties, particularly in applications such as GNN querying, equivalence checking, etc. We prove that such natural problems can be solved in polynomial space.
Key facts. Cited by 10 papers in the map (data through 14 Oct 2026). Builds on 9 of its 37 references that are in the map. First posted on arXiv 30 Apr 2024.
Builds on
9 of 37 references.
References · 9
- 2017Neural Message Passing for Quantum Chemistrycited by 3,487
- 2018Graph Neural Networks: A Review of Methods and Applicationscited by 1,576
- 2020Explainability in Graph Neural Networks: A Taxonomic Surveycited by 384
- 2022Graph neural networks for materials science and chemistrycited by 182
- 2021The Logic of Graph Neural Networkscited by 85
- 2022Global Explainability of GNNs via Logic Combination of Learned Conceptscited by 65
- 2023On the Correspondence Between Monotonic Max-Sum GNNs and Datalogcited by 12
- 2022DT+GNN: A Fully Explainable Graph Neural Network using Decision Treescited by 6
- 2020Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraintscited by 5
Built on by
Citing papers per year: 2025: 7; 2026: 3.
10 papers.
- 2025Exact Verification of Graph Neural Networks with Incremental Constraint Solvingcited by 4
- 2025Verifying Quantized Graph Neural Networks is PSPACE-completecited by 2
- 2025The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logicscited by 2
- 2025Sound Logical Explanations for Mean Aggregation Graph Neural Networkscited by 2
- 2025DeepGraphLog for Layered Neurosymbolic AIcited by 1
- 2025From Neural Networks to Logical Theories: The Correspondence between Fibring Modal Logics and Fibring Neural Networkscited by 1
- 2025Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testingcited by 0
- 2026Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approachcited by 0
- 2026Structural Preservation and the Logical Expressiveness of Graph Neural Networkscited by 0
- 2026Beyond Trained Models: Compiling GNNs for a Sound Explainer Benchmarkcited by 0
- 2026Beyond Trained Models: Compiling GNNs for a Sound Explainer Benchmark2 Oct 2026
- 2026Structural Preservation and the Logical Expressiveness of Graph Neural Networks16 Jun 2026
- 2026Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach12 May 2026
- 2025Sound Logical Explanations for Mean Aggregation Graph Neural Networks27 Oct 2025
- 2025Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing21 Oct 2025
- 2025From Neural Networks to Logical Theories: The Correspondence between Fibring Modal Logics and Fibring Neural Networks28 Sep 2025
- 2025DeepGraphLog for Layered Neurosymbolic AI9 Sep 2025
- 2025Exact Verification of Graph Neural Networks with Incremental Constraint Solving12 Aug 2025
- 2025The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics17 May 2025
- 2025Verifying Quantized Graph Neural Networks is PSPACE-complete22 Feb 2025