Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 1: Reject
review_content: This paper focuses on verifying sequential properties of deep beural networks. Linear Temporal Logic (LTL) is a 
natural way to express temporal properties, and has been extensively studied in the formal methods community. 
Signal temporal logic (STL) is a natural extension,  of LTL. STL specifications provide a rich set of formulations to encode intent for real valued signal over time. Formally proving STL formulae is intractable. But, it is possible to falsify such properties. This has been the main goal for various tools like Breach, and S-Taliro.


Pros :
A  very  interesting avenue  explored in this paper, is using the syntax of
STL to formulate properties about multiple-MNIST, Safe RL and NLP applications.
Even though the conversion from STL specifications to scalar valued function is a very well known technique.

Cons :
In my opinion, the paper lacks sufficient contributions in itself to be accepted at this conference. The idea of training
for robustness using intervals, has been well known for a while. The authors extend that to get conservative estimates of the level of satisfaction of the STL formula, and use that in the training process. Though training for robustness is an
interesting idea in itself, but the general opinion about using interval propagation to train networks is negative.

Overall : Though the direction of this work is interesting but lacks sufficient technical novelty.
review_title: Official Blind Review #5

final_score: rating: 3: Weak Reject
review_content: This paper extends bound propagation based robust training method to complicated settings where temporal specifications are given. Previous works mainly focus on using bound propagation for robust classification only. The authors first extend bound propagation to more complex networks with gates and softmax, and designed a loss function that replies on a lower bound for quantitative semantics of specifications over an input set S. The proposed framework is demonstrated on three tasks: Multi-MNIST captioning, vacuum cleaning robot agent and language generation. The authors formulate specifications using temporal logic, train models with bound propagation to enforce these specifications, and verify them after training. 

My questions regarding this paper are mostly on the three demonstrated tasks:

1. For the Multi-MNIST dataset, I have the following questions:

1(a). In Table 2, it is surprising that even with perturbation of 0.5, the verified and adversarial accuracy is very high. At perturbation epsilon=0.5, it should be possible to perturb the entire image to gray (value 0.5), so I believe the accuracy should be very low here. It is hard to believe under this setting the verified accuracy is still 99%.

1(b). For Table 3, nominal accuracy should also be reported.

1(c). Additionally, how do you define the nominal accuracy here? An example is nominally correct when all digits are predicted correctly in the sequence, or just when the sequence length is predicted correctly?

1(d). For the termination accuracy, do we only care about the sequence length being predicted correctly, or does it also cover the case that all digits in the sequence are predicted correctly? If it is only concerning about the sequence length, this property is a little bit weak.

2. For the RL Robot agent experiment, I have the following questions:

2(a). Because T=10, are you saying that we can only guarantee that the battery is always recharged for any rollouts less than 10 steps? After 10 steps beyond the initial position, can we get any guarantees? A 10-step only guarantee seems too restrictive.

2(b). Are all the properties only verified assuming that the agent starts from the center? I think this assumption is probably also too strong in practice.

2(c). Since all the %verified cells reported in Table 4 are all 100%, it is probably better to make the problem more challenging, by increasing T or considering different initial positions. It is important to show when the performance of the proposed method starts to degrade, to understand the power of the proposed method.

3. For the language generation experiment, the perplexity of the verified training model looks significantly worse than nominal or sampled models. With a perplexity as high as this, I believe the model actually produces garbage. Can you provide some examples of generated texts? I feel language generation is probably not a suitable task for the proposed training method. 

Other minor issues:

1. Table 1 should have some horizontal lines - it is hard to align the works with categories on the right.

2. Several papers appear multiple times in references, including "Differentiable abstract interpretation for provably robust neural networks", "Towards fast computation of certified robustness for relu networks" (and probably others). Also on page 2, Shiqi et al., should be Wang et al. (Shiqi is the first name).

3. I feel the writing is a bit rushed and the authors should make a few more passes on the paper.


This paper makes valid technical contributions, especially the conversion from STL specifications to lower bounds of the quantitative semantics is interesting. Although bound propagation based robust training method is simple to extend to softmax/GRU with interval analysis, applying robust training techniques to the three interesting applications are good contributions. Since the main contribution of this paper is the empirical results on the three tasks, my concerns regarding the experiments need to be addressed before I can vote for accepting this paper. Also, because this paper uses 10 pages, I am expecting the paper to meet a higher standard. Thus, I am voting for a weak reject at this time.


****** After author response

The author response addressed some of my concerns. However I do believe this paper is relatively weak in contribution, especially the experiments can be done more thoroughly. I also appreciate that the authors reduced paper length to 8 pages. I am okay with accepting this paper as it does have some interesting bits, but it is clearly on the borderline and can be further improved.

review_title: Official Blind Review #2

final_score: rating: 8: Accept
review_content: This paper presents a way to train time-series regressors verifiably with respect to a set of rules defined by signal temporal logic (STL). The bulk of work is in deriving bound propagation rules for the STL language. The resulting lower bound of an auxiliary quantity (which is required to be non-negative) is then maximized for verifiability.

This technique is demonstrated on three tasks and compares favorably to the baseline from Wang et al. (2019).

I am not an expert in this area. However, to the best of my knowledge I don't see anything immediately wrong with this and it seems novel. Therefore I recommend acceptance.

The paper is also above recommended length.
review_title: Official Blind Review #3

final_score: rating: 6: Weak Accept
review_content: This paper concerns verification of neural networks through verified training and interval bound propagation. Namely, the authors rely on the fact (reported in the literature earlier, but also confirmed here) that verified training leads to neural networks that are easier to verify. The main contributions of this work are 1) extending interval bound propagation to recurrent computation and auto-regressive models as often encountered in NLP or RL settings which allows verified training of these models, 2) introducing the Signal Temporal Logic (STL) for specifying temporal constraints for a model, and extending its quantitative semantics for reasoning about sets of inputs, 3) providing empirical proof that the STL with bound propagation can be used to ensure that neural models conform to temporal specification without large performance losses.

The introduced method is well motivated and well-placed within the literature, with the related works section providing a good overview of the field; it also clearly mentions how the proposed method differs from the prior art. Section 3 describes the STL syntax and three specifications for different tasks; while the provided examples are nice, they are also long-winded and make the exposition difficult to follow---I think that their details should be moved to the appendix. Section 4 is very technical, and I do not have enough knowledge to verify it thoroughly, but the proposed approach seems to make sense. Finally, Section 5 presents experimental evaluation, which is performed on three different tasks: image caption generation, RL with a mobile robot, and language generation. These three experiments seem to be enough variety to prove the utility of the method. My only concerns are that 1) the loss of perplexity with verified training in the language modelling setup is disturbingly high as compared to the nominal method, and 2) the proposed method is compared to only one baseline in each experiment, and it is unclear whether the baseline are state-of-the-art without knowing the literature (which I do not know).

I recommend ACCEPTing this paper, albeit with low confidence. This is because the paper addresses an interesting and important problem, and the provided results are convincing. Having said that, I know nothing about the area of formal verification.
review_title: Official Blind Review #1

Meta-review: This submission proposes a deep network training method to verify desired temporal properties of the resultant model.

Strengths:
-The proposed approach is valid and has some interesting components.

Weaknesses:
-The novelty is limited.
-The experimental validation could be improved.

Opinion on this paper was mixed but the more confident reviewers believed that novelty is insufficient for acceptance.
Decision: Reject