Venue: NeurIPS 2021 Conference

Reviews:

final_score: rating: 7: Good paper, accept
review_content: summary: The paper targets the verification of probabilistic specifications of neural networks, e.g., where the specification to a deterministic network can be probabilistic, or for verifying deterministic specifications over a probabilistic neural network. The authors pose the probabilistic verification as an intractable stochastic optimization problem. They leverage functional lagrangian framework to solve the problem approximately. The framework enables the decomposition of the problem into smaller sub-problems which are relatively tractable to solve. The authors experimentally demonstrate the effectiveness of their approach on three specifications against Wicket et al. and obtain more precise results while remaining scalable.
main_review: Originality: The use of functional lagrangian optimization for probabilistic neural networks verification is an original contribution to the best of my knowledge. The authors develop tractable algorithms that exploit the structure of the verification problem for approximately solving the optimization problems. This enables them to verify novel specifications such as distributionally robust OOD detection not possible with prior work. 

Quality: The verification framework provided in this work is sound and the experimental results are convincing. In the experiments, the authors use a closed-form solution for the inner optimization problems by instantiating their framework with linear multipliers. This is shown to be equivalent to Dvijotham et al. It is not clear to me whether the closed-form solution is the best solution possible layerwise or an approximation when considering linear multipliers? The Lagrangian dual from Dvijotham et al. does not provide the best layerwise convex relaxation and more precise relaxations were achieved by [1,2].  

Clarity: The paper is well motivated and understandable. The authors demonstrate the instantiation of their framework well on an example. I believe that the high-level ideas of the paper should be accessible to a relatively wider audience. However, the authors do not provide details about the CPU cluster used for their experiments in Section 5.1. It is also not clear to me whether the experiments in Section 5.3 were performed on CPUs or GPUs. 

Significance: There is relatively less work on verifying probabilistic specifications compared to the deterministic ones. The authors provide a generalized framework for verifying such specifications and show how the existing works can be seen as an instantiation of their framework. I believe that this is a significant contribution and may lead to more specialized verification algorithms with better scalability while maintaining sufficient precision in the future.

More questions:
1. Is the formulation with functional lagrangian presented here the tightest possible or one can define non-decomposable lagrangians which might be more precise?

2. The closed-form solution in C.4 assumes box constraints on x, therefore, processing each neuron independently. If instead, one considered polyhedral dependencies between the input neurons, will the bounds will improve even with linear multipliers?

3. What is the dropout rate for VGG-x networks considered in the experiments?

4. Will the source code of the verifier be publicly available?

References:
1. The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification.
2. Beyond the Single Neuron Convex Barrier for Neural Network Certification.
limitations_and_societal_impact: The authors address these concerns adequately in their paper.
review_title: null

final_score: rating: 6: Marginally above the acceptance threshold
review_content: summary: This paper presents a general formulation of probabilistic specifications for neural networks which can capture both probabilistic networks and uncertain inputs. The authors generalize the notion of Lagrangian duality by defining functional Lagrange multipliers that can be arbitrary functions of the activations at a given layer. 
main_review: Strengths
------------
- Probabilistic specifications are an important yet underexplored area in neural network verification
- The proposed general framework can handle stochasticity in both the specifications and the network architectures in a unified manner
- The functional Lagrangian formulation is interesting 
- The results demonstrate gains over existing probabilistic verification methods for some properties

Weaknesses
-----------------
- No clear demonstration of the relationship between the probabilistic guarantees and actual attack success rate using SOTA attacks.
- It is not clear whether it is feasible for the framework to verify other types of property beyond the ones presented in the paper. 

The authors propose a new probabilistic verification framework for neural networks that can handle stochasticity both in the input specifications as well as model architectures. The proposed functional Lagrangian formulation is interesting. The results seem to indicate gains over existing probabilistic verification methods. However, the implications of probabilistic verification in terms of attack success are not clear to me. What are the actual attack success rates for probabilistically verified networks? Are they lower than unverified ones? The authors did not provide any data. Moreover, it is not clear how generic the proposed framework is. The authors mention that in many cases obtaining a non-trivial upper bound is challenging. What are such cases? Beyond the properties presented in the paper, what other types of properties can be supported by the framework? 

limitations_and_societal_impact: N/A
review_title: null

final_score: rating: 6: Marginally above the acceptance threshold
review_content: summary: This paper proposes a general framework for probabilistic robustness verification, with both stochastic networks and probabilistic specifications. The core technique is based on the generalization of Lagrangian duality where the multipliers are functional multipliers and probabilistic constraints are allowed. Under the proposed framework, the paper demonstrates several applications, including robust OOD detection on stochastic NN, adversarial robustness verification for stochastic NN, and distributionally robust OOD detection. 
main_review: Pros:
* The framework this paper proposes is general one for probabilistic robustness verification, that supports both stochastic networks and probabilistic specifications. And the verification has certified guarantees.
* There are empirical demonstrations for the proposed framework, which show the benefit of using functional Lagrangian.
* The paper is clearly written on introducing the techniques, experiments, limitations and social impact. 

Cons:
* The proposed method seems slow (much slower than baseline).

limitations_and_societal_impact: The paper has discussed them in the last section.
review_title: null

final_score: rating: 7: Good paper, accept
review_content: summary: The paper proposes a framework for giving mathematical guarantees on neural networks with probabilistic specifications, e.g. for robustness across distributions or for robustness of models with non-deterministic outputs. The authors first formulate the abstract framework in terms of functional lagrangians and then show how to apply these by using concrete applications and concrete function classes for the lagrangians.
main_review: Strengths:
The paper tackles an important problem and provides general framework from which further methods can be developed. The novel task of worst-case robustness with respect to a family of out-distributions is a valuable contribution. A fair number of examples for the application of the authors' proposed method is given. Implementing the method is technically non-trivial and thus a contribution (more so if the code is published).

Weaknesses:
As the authors openly admit, their approach can only provide certificates for models with outputs that are bounded with probability 1 in each layer, which does pose a practical limitation. 
It is not always clear from the experiments how tight the final bounds are. Table 1 computes an AAUC as upper bound on the worst-case AUC but in Table 3 it should also be possible to give an empirical upper bound on the worst-case AUC by empirically finding an adversarial noise distribution that produces a low AUC.
Because the models were trained in a certification agnostic way, some of the threat models (CIFAR in Table 1 and 2 layers in Table 2) are so small that they would not even allow for any change at all when pixel values are constrained to lie on i/255 for i in {0,...,255}. As such, these guarantees seem fairly meaningless in practice. Using an epsilon of at least 1/255 would help fix this.

Correctness:
As far as I verified (no proofs) the math seems correct.

Clarity:
It seems to me that line 109 has sloppy notation when defining distributionally robust OOD detection. omega is in the set of distributions, but $x_\mathrm{ood}$ is in $\mathbb{R}^d$. It is clear what the authors meant to convey but this should be improved.
While the example starting in line 164 is simple and illustrative, I don't find it obvious how to actually write this in terms of probabilistic neural network layers as defined in Section 2.1. I think writing this explicitly (what is $\pi(x_1|x_0)$ etc.) in the appendix would help make the paper more readable. 

Relation to prior work:
The relation to prior work is sufficiently discussed.

Reproducibility:
Unfortunately, the authors did not provide code. However, the information in the appendix seems sufficient in order to implement their method.

Additional feedback:
Formatting in Table headers. Shouldn't be all italic.
Line 47: "for e.g." = "for for example" 
Formatting of "softmax" in line 234 is inconsistent with formatting in lines 110, 118, 232.
Inconsistent capitalization of "Section" between main text and checklist.
limitations_and_societal_impact: I think the authors adequately address this.
review_title: null

Meta-review: All reviewers unanimously acknowledged the technical contributions in providing mathematical guarantees on neural networks with probabilistic specifications. The authors' responses also addressed the reviewers' concerns. It's a clear accept.
Decision: Accept (Spotlight)