Venue: ICLR 2023 Conference

Reviews:

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: ###  Problem
The paper tackles the problem of neural network verification, which aims to give guarantees of whether a trained NN follows certain specifications.

###  Proposed method
The authors claim that the current adversarial robustness specification used by the verification community is improper. Their claim is that this specification does not allow verification of test set inputs as they lie outside the verified region.

Authors propose neural representation as specification. Essentially, they propose to use neural activation patterns as specifications.

### Experimental Validation
Experiments are conducted on the MNIST dataset, where it shows that with the proposed specification, the certified region can go well beyond adversarial examples and even verify test set inputs.

### My one line understanding
Authors claim to have found a condition which:
1. adversarial examples don't follow, so verification won't stop at them and will be able to go beyond
2. test examples from same class follow, so test set examples can be verified
strength_and_weaknesses: ## STRENGTHS
1. Finding alternative specifications is a good direction to explore

## WEAKNESSES

1. Writing needs to be improved
- Not put into context properly: Doing adversarial verification is not necessarily an *overfitted* specification, as you call it. There are many applications where we also want to verify against adversarial examples. I don't think you need to belittle previous work. Your work is complementary, and that is how you should write the paper.
- I don't agree with the entire 'data as specification' vs 'neural representation as specification' angle.  Because if one looks at equations in Sec3.2, you have the same formulation, but an extra constraint/specification. So you can write we add a new specification, instead of saying one vs the other.
- Many equations are not numbered. How should I refer to them?

2. Strong and probably incorrect assumptions
- What is the guarantee that test examples will definitely follow same NAP?
- What is the guarantee that adversarial examples will not follow NAP
- Isn't such an assumption against the whole point of verification?

3. Weak experimental validation
- One main limitation of adv verification methods is their inability to scale beyond small epsilons. This is especially critical for your work because for going upto the test inputs, you would require large epsilon. Current methods don't allow that. So your method might not work on bigger datasets at all. Whereas, adv verification will still work on big datasets with small epsilon. 
- The experiments are only conducted on the MNIST dataset. I feel that MNIST is too easy and that is why your assumptions hold there. Since your assumptions are so strong, can you validate them on a bigger dataset?
clarity,_quality,_novelty_and_reproducibility: The work is Novel.

But I doubt the correctness of the claims and lack of proper experimental validation. Please see my detailed answer in the previous question.

QUESTION:

If you find a specification which all same class test examples follow, have you not solved ML?  If you have such a constraint, then just use that to make class prediction and your accuracy will be 100% ($- \delta$)?
summary_of_the_review: It is important to look for alternate specification.

But the assumptions made in this work feel incorrect and are not properly validated, so I cannot draw a conclusion from the current version.
review_title: null

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: This paper proposes a novel robustness specification for neural networks. Unlike canonical specifications where pre-conditions are defined as constraints on the neural network input,  the specification used in this paper are defined as particular activation patterns. The paper presents a strategy to extract activation patterns, shows how the specification can be checked with existing verifiers, and how this specification achieves better coverage of the test set. 
strength_and_weaknesses: Strength:

I really like this work. Adding activation patterns to the pre-conditions of the specification is a simple but clever extension. It seems to be able to cover more test images than the canonical way does, where the constraint is only put on the input. Instead of only having the activation patterns as the pre-condition, still specifying a (now larger) epsilon ball in the input region not only makes the specification more relevant (as it focus the verification on valid images of digits instead of some noise input) but also likely to make the verification task easier. 
This work might also motivation development of verification techniques that can handle constraints on NAP more effectively. 
 
Weakness:

The experiment is performed only on small neural networks. The verification is in general challenge, and using tools other than Marabou is unlikely to suddenly allow us to scale to SoTA perception networks. However, I would still be curious to see how scalable the NAP extraction procedure is and what the neural specifications look like on more complex image dataset and networks.

clarity,_quality,_novelty_and_reproducibility: The paper is well-written and very clear. 
The contribution is original to my knowledge. Could the author discuss the relation of their work to [a,b]?

[a] Gopinath et al, "Property Inference for Deep Neural Networks."

[b] Sabour et al, "Adversarial Manipulation of Deep Representations."
summary_of_the_review: Overall, I think the paper contains several good and novel ideas and could motivate future work both in application and verification techniques.
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: The paper introduces a novel specification for neural network verification,
where instead of checking whether sets of inputs are classified equivalently by
a network, it concerns checking the robustness of networks when their behaviour
is restricted to certain neural activation patterns.
strength_and_weaknesses: + The specifications introduced present in my opinion a step towards obtaining
stronger neural network robustness guarantees when used in conjunction with
existing specifications.

- Unsound claim that standard specifications are impractical for real world
  applications. I think that checking small perturbations radiuses which do not
  alter the semantics of the input is important for any application.

- Not surprising empirical results. As the specifications proposed are
  restricted to certain activation patterns, it is expected that the
  perturbation radiuses that can be verified will be bigger when compared to
  standard specifications. 

- The evaluation is limited in that it only concerns one benchmark.
clarity,_quality,_novelty_and_reproducibility: The paper is well written and presented. The contribution is not particularly
novel as the main contribution restricts specifications for neural network
verification, thus providing a small increment to previous work. Still, the
specifications proposed are significant to check as in conjunction with
standard specifications for small perturbation radiuses can give stronger
robustness guarantees. The significance of this is  however often
overemphasised by what I think are unsound claims pertaining to the
impracticality of existing specifications.
summary_of_the_review: Whilst the paper introduces novel neural network specifications that are
important to check in practice, the overall novelty and significance of the
empirical evaluation are weak.
review_title: null

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: The paper proposed neural activation patterns as a replacement for adversarial robustness specifications to reason about the robustness of the network. The paper argues that this resolves the problem that test samples don't fall into certified regions of an adversarially robust verified network.
strength_and_weaknesses: # Strengths:
- The paper highlights an important issue in adversarial robustness certification (the adversarial robustness verification only covers a minuscule part of the entire input space).
- The paper introduces a novel set of specifications and shows that it covers a larger part of the test inputs.

# Weaknesses:
The main issue with the submission is the lack of proper evaluation of the proposed specifications. Particularly, the paper validates the specification on a 2D example and MNIST. The MNIST dataset is severely outdated and known to have artifacts that are not present in other datasets, such as prototypical samples or high certifiable accuracy (compared to, for instance, CIFAR where the top accuracy and the top certified accuracy have a huge gap).
Additionally, the paper only assesses MLP networks. 
Consequently, the paper provides insufficient experimental validation of whether the proposed specifications are actually useful and reasonable in practice. It is vital to check if the hypothesized NAP specification works on larger and more diverse datasets, different types of data, and different structures of networks 

Moreover, neural activation patterns have already been used in the verification literature of neural networks [1], making the concept less novel.


[1] Henzinger et al. Outside the Box: Abstraction-Based Monitoring of Neural Networks. 2020
clarity,_quality,_novelty_and_reproducibility: Overall the paper is clear. The parts and motivation about why dominance may matter is neural networks could be explained a bit better (e.g., with examples) as it seems to be the main premise of the NAP specifications.
summary_of_the_review: Interesting concept of overcoming the problem of certified adversarial regions having little relevance for the test data. Insufficient experimental validation of whether the proposed specifications are actually reasonable in practice.
review_title: null

Meta-review: metareview:_summary,_strengths_and_weaknesses: This paper introduces a new type of specification for verifying neural networks, based on activation patterns of neural networks (e.g., a set of units that are assumed to be greater than 0, and a set less than 0). The idea is to verify that certain properties of a network hold, conditional on the activation pattern holding.

There was significant debate among the reviewers about this paper, which led to an active discussion.

There was general agreement that researching alternative specifications was a good direction to explore, and several reviewers judged that the overall direction of using activation patterns was a potentially promising approach.

Several reviewers raised concerns about the overall framing of approach (e.g., that standard adversarial specifications may be “overfitted” etc.). It is good that the authors agreed to tone down this language in their response.

The main negative concern was about the scalability. Certainly having experiments only on MNIST, as the original draft did, would not be sufficient for publications. In the response, the authors add additional experiments on CIFAR with a different architecture. This strengthens the work considerably. 

However, there were still concerns raised in the discussion about scalability. Even with these new results, the CIFAR architecture is within the range of networks that can be verified using traditional specifications. So the question was raised about whether NAPs provide a scalability benefit. This seems particularly important to me because NAPS come with a significant decrease in interpretability, so it is much harder for an engineer to check that the specification is correct. Increasing the evidence to support the benefits of NAPS as a specification, while being upfront about their drawbacks, would significantly improve the paper.

justification_for_why_not_higher_score: More evidence about scalability, or alternatively other benefits of NAPs compared to traditional specifications.
Decision: Reject