2019

Correctness Verification of Neural Networks

Yang, Yichen, Rinard, Martin

Understand

We present a novel framework for specifying and verifying correctness globally for neural networks on perception tasks.

Most previous works on neural network verification for perception tasks focus on robustness verification.
Unlike robustness verification, which aims to verify that the prediction of a network is stable in some local regions around labelled points, our framework provides a way to specify correctness globally in the whole target input space and verify that the network is correct for all target inputs (or find the regions where the network is not correct).
We provide a specification through 1) a state space consisting of all relevant states of the world and 2) an observation process that produces neural network inputs from the states of the world.

Built on

Liu, C., Arnon, T., Lazarus, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. CoRR abs/1903.06758
Original
1903
Earlier work this paper cites.
Lin, X., Zhu, H., Samanta, R., Jagannathan, S.: ART: abstraction refinement-guided training for provably correct neural networks. CoRR abs/1907.10662
Original
1907
Earlier work this paper cites.
Kelly J., H., Dan S., V., John J., C., Leanna K., R.: A practical tutorial on modified condition/decision coverage. Tech. rep. (2001)
2001
Earlier work this paper cites.
Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. CoRR abs/1412.6572
Original
2014
Earlier work this paper cites.
Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. CoRR abs/1412.6980
Original
2014
Earlier work this paper cites.
Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. CoRR abs/1312.6199
Original
2014
Earlier work this paper cites.
Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A.V., Criminisi, A.: Measuring neural net robustness with constraints. In: Proceedings of the 30th International Conference on Neural Information Processing Systems. pp. 2621–2629. NIPS’16, Curran Associates Inc., USA (2016), http://dl.acm.org/citation.cfm?id=3157382.3157391
2016
Earlier work this paper cites.
Papernot, N., McDaniel, P.D., Jha, S., Fredrikson, M., Celik, Z.B., Swami, A.: The limitations of deep learning in adversarial settings. 2016 IEEE European Symposium on Security and Privacy (EuroS&P) pp. 372–387 (2016)
2016
Earlier work this paper cites.
Albarghouthi, A., D’Antoni, L., Drews, S., Nori, A.V.: Fairsquare: Probabilistic verification of program fairness. Proc. ACM Program. Lang. 1
2017
Earlier work this paper cites.
Bunel, R., Turkaslan, I., Torr, P.H.S., Kohli, P., Kumar, M.P.: A unified view of piecewise linear neural network verification (2017)
2017
Earlier work this paper cites.
Cheng, C.H., Nührenberg, G., Ruess, H.: Maximum resilience of artificial neural networks. In: ATVA (2017)
2017
Earlier work this paper cites.
Dong, Y., Liao, F., Pang, T., Hu, X., Zhu, J.: Discovering adversarial examples with momentum. CoRR abs/1710.06081
Original
2017
Earlier work this paper cites.
Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. CoRR abs/1705.01320
Original
2017
Earlier work this paper cites.
Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 3–29. Springer International Publishing, Cham (2017)
2017
Earlier work this paper cites.
Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Computer Aided Verification, pp. 97–117. Springer International Publishing (2017). https://doi.org/10.1007/978-3-319-63387-9_5, https://doi.org/10.1007%2F978-3-319-63387-9_5
2017
Earlier work this paper cites.

Similar

Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. CoRR abs/1706.07351
Original
2017
Cited alongside, same era.
Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. ArXiv abs/1706.06083
Original
2017
Cited alongside, same era.
Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: Automated whitebox testing of deep learning systems. In: Proceedings of the 26th Symposium on Operating Systems Principles. pp. 1–18. SOSP ’17, ACM, New York, NY, USA (2017). https://doi.org/10.1145/3132747.3132785, http://doi.acm.org/10.1145/3132747.3132785
2017
Cited alongside, same era.
Xiang, W., Tran, H., Johnson, T.T.: Reachable set computation and safety verification for neural networks with relu activations. CoRR abs/1712.08163
Original
2017
Cited alongside, same era.
Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Learning and verification of feedback control systems using feedforward neural networks. IFAC-PapersOnLine 51
2018
Cited alongside, same era.
Dvijotham, K., Stanforth, R., Gowal, S., Mann, T., Kohli, P.: A dual approach to scalable verification of deep networks. In: Proceedings of the Thirty-Fourth Conference Annual Conference on Uncertainty in Artificial Intelligence (UAI-18). pp. 162–171. AUAI Press, Corvallis, Oregon (2018)
2018
Cited alongside, same era.
Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: Safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy (SP). pp. 3–18 (May 2018). https://doi.org/10.1109/SP.2018.00058
2018
Cited alongside, same era.
Ma, L., Juefei-Xu, F., Sun, J., Chen, C., Su, T., Zhang, F., Xue, M., Li, B., Li, L., Liu, Y., Zhao, J., Wang, Y.: Deepgauge: Comprehensive and multi-granularity testing criteria for gauging the robustness of deep learning systems. CoRR abs/1803.07519
Original
2018
Cited alongside, same era.
Odena, A., Goodfellow, I.J.: Tensorfuzz: Debugging neural networks with coverage-guided fuzzing. CoRR abs/1807.10875
Original
2018
Cited alongside, same era.
O’Kelly, M., Sinha, A., Namkoong, H., Duchi, J., Tedrake, R.: Scalable end-to-end autonomous vehicle testing via rare-event simulation (2018)
2018
Cited alongside, same era.
Raghunathan, A., Steinhardt, J., Liang, P.: Certified defenses against adversarial examples. In: International Conference on Learning Representations (2018), https://openreview.net/forum?id=Bys4ob-Rb
2018
Cited alongside, same era.
Sun, Y., Huang, X., Kroening, D.: Testing deep neural networks. CoRR abs/1803.04792
Original
2018
Cited alongside, same era.

Then

Wong, E., Schmidt, F., Metzen, J.H., Kolter, J.Z.: Scaling provable adversarial defenses. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31, pp. 8400–8409. Curran Associates, Inc. (2018), http://papers.nips.cc/paper/8060-scaling-provable-adversarial-defenses.pdf
2018
Later among the works it cites.
Xiang, W., Tran, H., Rosenfeld, J.A., Johnson, T.T.: Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. In: 2018 Annual American Control Conference (ACC). pp. 1574–1579 (June 2018). https://doi.org/10.23919/ACC.2018.8431048
2018
Later among the works it cites.
Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multi-layer neural networks. IEEE Transactions on Neural Networks and Learning Systems (TNNLS) (Mar 2018). https://doi.org/10.1109/TNNLS.2018.2808470
2018
Later among the works it cites.
Balunovic, M., Baader, M., Singh, G., Gehr, T., Vechev, M.: Certifying geometric robustness of neural networks. In: Wallach, H., Larochelle, H., Beygelzimer, A., d'Alché-Buc, F., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32, pp. 15313–15323. Curran Associates, Inc. (2019), http://papers.nips.cc/paper/9666-certifying-geometric-robustness-of-neural-networks.pdf
2019
Closest in time.
Bastani, O., Zhang, X., Solar-Lezama, A.: Probabilistic verification of fairness properties via concentration. Proc. ACM Program. Lang. 3
2019
Closest in time.
Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: A language for scenario specification and scene generation. In: Proceedings of the 40th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI) (June 2019)
2019
Closest in time.
Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: Verifying safety properties of hybrid systems with neural network controllers. In: Proceedings of the 22Nd ACM International Conference on Hybrid Systems: Computation and Control. pp. 169–178. HSCC ’19, ACM, New York, NY, USA (2019). https://doi.org/10.1145/3302504.3311806, http://doi.acm.org/10.1145/3302504.3311806
2019
Closest in time.
Salman, H., Yang, G., Zhang, H., Hsieh, C.J., Zhang, P.: A convex relaxation barrier to tight robustness verification of neural networks (2019)
2019
Closest in time.
Singh, G., Ganvir, R., Püschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. In: Wallach, H., Larochelle, H., Beygelzimer, A., d'Alché-Buc, F., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32, pp. 15098–15109. Curran Associates, Inc. (2019), http://papers.nips.cc/paper/9646-beyond-the-single-neuron-convex-barrier-for-neural-network-certification.pdf
2019
Closest in time.
Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3
2019
Closest in time.
Singh, G., Gehr, T., Püschel, M., Vechev, M.: Robustness certification with refinement. In: International Conference on Learning Representations (2019), https://openreview.net/forum?id=HJgeEh09KQ
2019
Closest in time.
Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: International Conference on Learning Representations (2019), https://openreview.net/forum?id=HyGIdiRqtm
2019
Closest in time.
Zhu, H., Xiong, Z., Magill, S., Jagannathan, S.: An inductive synthesis framework for verifiable reinforcement learning. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 686–701. PLDI 2019, ACM, New York, NY, USA (2019). https://doi.org/10.1145/3314221.3314638, http://doi.acm.org/10.1145/3314221.3314638
2019
Closest in time.
Jia, K., Rinard, M.C.: Efficient exact verification of binarized neural networks. vol. abs/2005.03597 (2020)
Original
2020
Closest in time.
Jin, C., Rinard, M.C.: Manifold regularization for adversarial robustness. ArXiv abs/2003.04286
Original
2020
Closest in time.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

Reading the bibliography…