Venue: ICLR 2023 Conference

Reviews:

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: This paper provides theoretical results on the formal verifiability of message passing neural networks (MPNNs), a popular class of graph neural network models, for graph and node classification tasks. 
In particular, it proves that, without assuming a bound on the degree of the graph, the formal verification of output reachability and adversarial robustness is undecidable for graph classification problems. At the same time, the paper provides positive results by showing that bounding the degree makes the verification of node classifiers decidable.


strength_and_weaknesses: Strengths:
- The paper contributes to a fundamental problem in the context of safe/verifiable AI for a popular class of ML models
- The theoretical groundwork provided in the paper, such as the connection between formal verification of GNNs and the newly introduced Graph Linear Programming (GLP), could benefit future efforts in this area.

Weaknesses:
- The presentation could be improved in some parts
- It is not clear to me how realistic are the setting and assumptions made by the authors
clarity,_quality,_novelty_and_reproducibility: I think that the writing is overall clear and crisp. I did not spot any major problem in the formal proofs, the high-level approach and reductions make sense to me but I couldn't carefully check the details in the appendix. I think that the paper could be improved as follows.

---

**The presentation could be improved**

I understand that the main text is meant to provide intuitions and key ideas behind the theoretical results, whose formal treatment must be deferred to the appendix.

Nonetheless, I think that Section 3 would be much more accessible if the input/output specifications in Fig. 1 were introduced at the beginning, maybe with some examples on what they entail.

---

While the relation between ORP and ARP is clear, I wish that the relation between the graph and node classification task was discussed, connecting the negative (Th/Cor. 1) and positive (Th/Cor. 2) results.


---

    "[..] where φ discr is built like above [..]"

That formula is not defined above.

---

**It is not clear how realistic are the setting and assumptions made by the authors**

    "In this paper, we only consider MPNN where the aggregation, combination and readout parts are given as follows"

How limiting and how realistic is this restriction described here? Even if an in-depth discussion is deferred to Section 6, it would be good to motivate it, possibly citing multiple influential works that fall into this category. 

---

**Minors**


    "[..] most work considers GNN used for node-classification and
    among such most common are edge modifications of a fixed input
    graph [..]"

Most common *attacks*?

---

    "Using this lemma, in order to prove Theorem 1, it suffices to show that GCP is not formally verifiable"

that GCP is *undecidable*.

---

    "[..] - here: words witnessing a solution of a PCP instance – by means of
    vectors and the operations that can be carried out on them inside a MPNN."

I don't understand this sentence.

---

    "To keep the notation clear we write – if unambiguous – we denote some variable x i in node and graph conditions by its index i."

Typo?
  
summary_of_the_review: The paper contributes with some key theoretical results on the problem of verifying MPNNs, as well as providing useful groundwork for future efforts in the area. I think that the problem considered in this paper is very relevant. The overall methodology seems correct and, to the best of my knowledge, novel. However, I couldn't verify the correctness of the proofs in the appendix. The presentation could be improved in some parts, but overall I think that the authors did a good job in clearly presenting the key concepts and intuitions.
review_title: null

final_score: rating: 10: strong accept, should be highlighted at the conference
review_content: summary_of_the_paper: This problem considers the question of whether or not it is possible to verify robustness and output reachability properties of message passing neural network (MPNN), e.g. graph neural networks. The paper proves via a succinct reduction to Post's Correspondence Problem that verification of such properties on large classes on MPNNs is undecidable. Furthermore, the illustrate that limiting the class of input graphs, e.g., limiting the degree of the nodes, is sufficient to make the problem decidable. This generalizes the feasibility established by explicit algorithms appearing in the literature.
strength_and_weaknesses: # Strengths

1. The topic of verification is a very important problem, particularly as such systems get deployed in more safety critical systems. Knowing the limitations of verification is critical to carving out tractable subsets of the problem space. Theoretical treatment of such topics typically lags behind the development of the models, and so this is welcomed progress.

2. The provided reduction is succinct and fairly easy to follow, although I must admit to needing a refresher on PCP.

# Weaknesses

1. The paper focuses on a fairly small (but as far as I know practically used) subset of MPNNs. There is a discussion that the specifics could be relaxed, but many alternative formulations exist, e.g., a different aggregation function. 
clarity,_quality,_novelty_and_reproducibility: This paper was very well written and I was able to follow the proof sketches. If there is an error, i believe it is either subtle or in the full proof which was not fully checked. 

As stated above the work is very important and to my knowledge novel.

I would perhaps ask for another pass on the PCP exposition, in particular making figure 2 contain the set of tiles next to the concatenation shown.
summary_of_the_review: Overall, I think this i an excellent contribution to the theoretical understanding of message passing and the limits on verification.

The main take aways are that:

1. arbitrary graphs are too expressive.
2. reasonable restrictions on node degree is sufficient.
review_title: null

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: This paper presents theoretical results about the decidability of verification problems of Message Passing Neural Networks, which are a type of graph neural network.
Graph neural network are a flexible deep learning architecture that operate on graph data, which can be of variable sizes.

The first main result of the paper is in Theorem 1, proving that if the input specification is permissive enough (allowing unbounded size of input graphs and without imposing restrictions on node degrees and labels), then it is not possible to perform reachability verification (answer the question "is there a graph such that a certain output will be produced by the MPNN when evaluated over this graph?").
The proof is performed by reducing a known undecidable problem (Post's correspondence Problem) to a graph satisfiability problem based on linear constraints ( in section 4.1) and then, reducing that graph satisfiability problem to a MPNN verification problem (in section 4.2).

The other main result  is Theorem 2 which shows that if the input graph have bounded degrees, then the verification problem become decidable. The proof rely on the fact that due to the way MPNN work (each node can only process information that is most $\texttt{GNN depth}$ nodes away, then if a graph satisfy a feasibility problem, there must a tree that satisfy it as well. Due to the assumption of bounded degrees, only a finite amount of those trees can exist, so it's possible to enumerate them, and to perform verification independently on each tree using traditional verification technique.
strength_and_weaknesses: The paper is very clearly written, with the authors having made a clear effort to be rigorous and provide definitions for all the constructions that they use. There is a clear structure to the paper, with the results being announced first, the strategy of the proof being presented and then executed, with the detailed version being present in the appendix. 
The proofs are decomposed into logical parts, making it possible to get relatively quickly an intuition for the reduction being operated.

In addition, the paper is quite clear in Section 6 to delineate the settings in which their results are applicable and the ones in which they are not.
clarity,_quality,_novelty_and_reproducibility: The work does not contain any experimental elements, so there is no consideration of reproducibility. 
The proof of the paper in the appendix are self-contained, so the arguments can be independently checked. To the best of my knowledge, the results in this work are novel.


## Minor typos:
- In the first half of page 2 -> "(in-)valud output"
- In proof of Lemma 2. -> "for each for each"
- In proof of Theorem 4. -> In the definition of $\langle x = m \rangle$, should it be an abbreviation of $\langle -x \leq -m\rangle + \langle x \leq m \rangle$?
- Appendix B.2 -> "Reducable" -> "Reducible"?
summary_of_the_review: This is a completely theoretical paper that proves results on the limitations of verifiability of graph neural network. 
This is useful as it tells us that there is no point in researching verification algorithms that would be applicable to the most general settings, as these problems are not going to be decidable. The whole paper is self contained and clearly written, so I recommend acceptance, even if this does not inform real applications (where we could always consider that the graph considered would be bounded).
review_title: null

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: This paper studies the formal output reachability verification of message passing neural networks (MPNN). The paper claims that the verification is impossible if for general graphs (unbounded size, nontrivial degree and node labels). But the verification is possible if there is a bound on the degree of the graph. 


strength_and_weaknesses: Strengths:
- This paper has theoretical results showing the impossibility of generally verifying MPNN, and a theoretical construction showing the possibility of verifying MPNN when the degree of the graph is bounded. 

Weaknesses:
- The problem considered in this paper has little importance and the results are not useful in practice. For verification in practice, we not only want decidability, but also computationally feasibility. NP-hardness of verifying NN is known. Therefore, considering the decidability of verification for graphs with unbounded size and degrees is not important, as computational complexity would play a more important role for larger graphs, which limits complete verification. Decidability is minor here, which is not the major factor hindering formal verification. 
- In practice, it is reasonable and acceptable for verification to only support specifications with some constraints, such as the size and degree of the graphs. While Theorem 1 says the impossibility of general verification, it would not fundamentally limit verification in practice. 
- The contribution of Theorem 2 is not significant. It only proves the possibility of verification when the degree is bounded, without proposing a computationally feasible algorithm (the construction seems to have an exponential complexity and thus it does not automatically imply a computationally feasible algorithm). On regular NNs, there already exist many concrete algorithms for formal verification. Then the contribution here is relatively insignificant. 

clarity,_quality,_novelty_and_reproducibility: The presentation is good and the work is original for the particular problem it is studying, to my best knowledge. But the problem seems to be minor and the conclusions are not practically useful for now. Reproducibility is not applicable for this purely theoretical paper.

summary_of_the_review: This work has theoretical merits on showing the impossibility of general GNN verification. But the problem is minor. The “fundamental limit” is not a critical limit in practice and is not the critical factor hindering the development of formal verifiers, for two reasons: 1) computational complexity plays a more important role given the NP-hardness of NN verification; 2) constraints can be added on graphs in practice, which makes the verification possible. The second point corresponds to Theorem 2 in the paper, but the paper does not provide a concrete and computationally feasible algorithm while only proving the possibility of verification, and thus the contribution is not significant. 

Updates: 

I am recommending a rejection because I think the contributions in this paper are insufficient, not because this is purely a theory paper. As I have said, NP-hardness in verification is known and is already fundamentally limiting the verification [1, 2]. Especially on verification for graphs with unbounded degree/size, NP-hardness is a stronger limit that can hinder exact verification in practice for unbounded cases. That’s also partly why I said verification for the unbounded case is not important as we have already known NP-hardness on verification so I would not pursue generalizing verification to the unbounded case in practice. Therefore, for now, the limit revealed by Theorem 1 (decidability) is not an important limit compared to NP-hardness done by previous works and the contribution is minor. However, it could potentially become more significant if the paper can prove that the verification is not NP-hard in the special case for MPNN considered in this paper, to eliminate the limit revealed in previous works so that decidability could really be interesting and important. Theorem 2 only showing the possibility without a computationally feasible method is not making a sufficient contribution either.

Actually the failure to support that decidability is "worse than NP-hard" ([unconvincingly claimed by the authors](https://openreview.net/forum?id=WlbG820mRH-&noteId=LXeVO_iFIJ)) poses a significant weakness of this paper. This paper provides no evidence to support such a claim. Without it, given the existing works on NP-hardness [1 2], showing the undecidability is insufficient to support the significance of this work. See [my previous thread](https://openreview.net/forum?id=WlbG820mRH-&noteId=u3TrgCTLzp) on why I disagree decidability is worse than NP-hard.

The authors refuse to compare with existing works on regular NN, by saying this paper works on GNN but not regular NN. GNN is an extension of regular NN. There are works about NP-hardness of verification on regular NN and this paper needs to show that why their results don't apply to this paper in a formal way, e.g., by proving that the verification in their case is not NP-hard, which is missing in this paper and I am not sure if it is actually possible to prove that. The authors are responsible for ensuring their claims are sufficiently supported. 

Overall, there is a significant lack of evidence supporting the significance of the work. I believe this paper is not ready for publication at ICLR.

[1] Katz, G., Barrett, C., Dill, D. L., Julian, K., & Kochenderfer, M. J. (2021). Reluplex: a calculus for reasoning about deep neural networks. Formal Methods in System Design, 1-30.

[2] Sälzer, Marco, and Martin Lange. "Reachability is NP-Complete Even for the Simplest Neural Networks." International Conference on Reachability Problems. Springer, Cham, 2021.

My latest discussion [post1](https://openreview.net/forum?id=WlbG820mRH-&noteId=u3TrgCTLzp) and [post2](https://openreview.net/forum?id=WlbG820mRH-&noteId=sbBDJ-bL3L).
review_title: null

Meta-review: metareview:_summary,_strengths_and_weaknesses: The authors prove fundamental limits on the ability to formally verify graph neural networks. In particular, they prove that the neural network verification problem is undecidable when the degree of the graph is unbounded. 

Strengths:
1. The authors establish a strong fundamental limitation to formally verifying graph neural networks. 
2. The proof techniques used by the authors to establish undecidability are novel and could be of independent interest to the community

Weaknesses:
1. The limitations established by the authors only apply to graphs where the degree can grow unboundedly, and still allows for algorithms that assume an a-priori bound on the degree of the graph. 
justification_for_why_not_higher_score: While the authors establish an important theoretical limitation of graph neural network verification, the significance of this result to practical verification problems is not clear since in many applications an assumption of bounded degree suffices.
justification_for_why_not_lower_score: The authors establish a stronger theoretical limit on verifiability of graph neural networks than any previous work.
Decision: Accept: poster