Fundamental Limits in Formal Verification of Message-Passing Neural Networks
Authors: Marco Sälzer, Martin Lange
ICLR 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | This work presents fundamental (im-)possibility results about formal verification of ARP and ORP of MPNN. Our first core contribution is that, in contrast to verification of ORP of classical NN, there are natural sets of graph-classifier ORP, which cannot be verified formally. We prove that in direct contrast to formal verification of NN there are non-trivial classes of ORP and ARP used for MPNN graph classification, that cannot be verified formally. This transfers the undecidability from DGLP to GCP. We formally prove this statement in the following. |
| Researcher Affiliation | Academia | Marco S alzer School of Electr. Eng. and Computer Science University of Kassel, Germany marco.saelzer@uni-kassel.de Martin Lange School of Electr. Eng. and Computer Science University of Kassel, Germany martin.lange@uni-kassel.de |
| Pseudocode | No | The paper contains mathematical definitions, lemmas, and proofs, but it does not include structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not provide concrete access to source code for the methodology described. It is a theoretical paper and does not mention code release. |
| Open Datasets | No | The paper does not describe the use of any specific publicly available datasets for training or evaluation. It deals with abstract graph structures and properties for theoretical analysis. |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology) needed to reproduce data partitioning, as it is a theoretical work and does not use datasets for empirical evaluation. |
| Hardware Specification | No | The paper does not provide specific hardware details (exact GPU/CPU models, processor types with speeds, memory amounts, or detailed computer specifications) used for running experiments, as it is a theoretical paper. |
| Software Dependencies | No | The paper does not provide specific ancillary software details (e.g., library or solver names with version numbers) needed to replicate the experiment, as it is a theoretical paper. |
| Experiment Setup | No | The paper does not contain specific experimental setup details (concrete hyperparameter values, training configurations, or system-level settings) in the main text, as it is a theoretical paper and does not describe empirical experiments. |