Summary
The paper proposes for synthesizing (and verifying) Neural Barrier Certificates with ReLU activation functions.
The authors focus on continuous-time systems which are controlled via a control input u(t) and define a dynamical
system as safe if for every state there exists a control output u(t) such that some unsafe region is never reachable.
To synthesize Neural Barrier Certificates, the authors build on characterization of ReLU Barrier Certificates by [15].
In particular, [15] observed that Relu NNs are piece-wise linear and it therefore suffices to check specific linearly constrained
regions at the border of the region $\mathcal{D}$ described by the barrier certificate.
The authors then extend prior work in two directions. First, they propose a technique for training ReLU Barrier Certificates
in a manner that minimizes the number of different linearly constrained regions at the border of $\mathcal{D}$.
Secondly, the authors propose an optimized scheme for verification of the resulting constraints w.r.t. the NN.
References cited below:
- [R1] Bak, Stanley, et al. "Improved geometric path enumeration for verifying relu neural networks." Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I 32. Springer International Publishing, 2020.
- [R2] Wang, Shiqi, et al. "Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification." Advances in Neural Information Processing Systems 34 (2021): 29909-29921.
Strengths
(S10) The approach presented by the authors makes the work described in [15] much more applicable:
As shown in the experiments, both novel techniques improve the performance of the overall approach and push beyond what was analyzable using [15].
(S20) The paper is mostly well-written and provides a good overview of the work.
Weaknesses
Minor opportunities for improvement:
(O1) In Section 4.1 the paper develops a new algorithm for enumerating linear NN regions along the border of $\mathcal{D}$.
I wonder how this technique materially differs from the branch exploration approaches used by branch-and-bound NN verification tools [R1,R2].
For example, geometric path enumeration [R1] also enumerates feasible linear regions.
While I agree that this approach would probably not be directly applicable due to the additional constraints w.r.t. the border of $\mathcal{D}$,
a conceptual comparison might help in making the paper better digestible to the NN verification community.
(O2) For an audience less familiar with neural barrier certificates, it would be helpful to provide insights into how such an NN could be used
to control a dynamical system in practice. I assume the barrier certificate can somehow be used to choose the correct control signal u at runtime, however, this correspondence is not entirely obvious to me.
Minor notes:
- Line 148: $\not\exists u$ makes the text harder to read, I would suggest writing this in english (similarly in other places)
Questions
(Q1) I would be really interested to hear something about (O2).
In a similar direction: I assume there is some limit on how often I have to choose control actions using the barrier certificate to ensure the dynamical system stays safe?
Limitations
The limitations of the work become clear throughout the paper.