More Web Proxy on the site http://driver.im/

research-article

Public Access

Formal verification of neural network controlled autonomous systems

Authors:

Yasser ShoukryAuthors Info & Claims

HSCC '19: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

Pages 147 - 156

https://doi.org/10.1145/3302504.3311802

Published: 16 April 2019 Publication History

Abstract

In this paper, we consider the problem of formally verifying the safety of an autonomous robot equipped with a Neural Network (NN) controller that processes LiDAR images to produce control actions. Given a workspace that is characterized by a set of polytopic obstacles, our objective is to compute the set of safe initial states such that a robot trajectory starting from these initial states is guaranteed to avoid the obstacles. Our approach is to construct a finite state abstraction of the system and use standard reachability analysis over the finite state abstraction to compute the set of safe initial states. To mathematically model the imaging function, that maps the robot position to the LiDAR image, we introduce the notion of imaging-adapted partitions of the workspace in which the imaging function is guaranteed to be affine. Given this workspace partitioning, a discrete-time linear dynamics of the robot, and a pre-trained NN controller with Rectified Linear Unit (ReLU) non-linearity, we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible assignments of different ReLUs. To accelerate this process, we develop a pre-processing algorithm that could rapidly prune the space of feasible ReLU assignments. Finally, we demonstrate the efficiency of the proposed algorithms using numerical simulations with the increasing complexity of the neural network controller.

References

[1]

Wikipedia, "List of autonomous car fatalities," https://en.wikipedia.org/wiki/List_of_autonomous_car_fatalities.

[2]

A. Ferdowsi, U. Challita, W. Saad, and N. B. Mandayam, "Robust deep reinforcement learning for security and safety in autonomous vehicle systems," arXiv preprint, 2018.

[3]

T. Everitt, G. Lea, and M. Hutter, "AGI safety literature review," arXiv preprint, 2018.

[4]

M. Charikar, J. Steinhardt, and G. Valiant, "Learning from untrusted data," in Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing. ACM, 2017, pp. 47--60.

Digital Library

[5]

J. Steinhardt, P. W. W. Koh, and P. S. Liang, "Certified defenses for data poisoning attacks," in Advances in Neural Information Processing Systems, 2017, pp. 3520--3532.

Digital Library

[6]

L. Muñoz-González, B. Biggio, A. Demontis, A. Paudice, V. Wongrassamee, E. C. Lupu, and F. Roli, "Towards poisoning of deep learning algorithms with back-gradient optimization," in Proceedings of the 10th ACM Workshop on Artificial Intelligence and Security. ACM, 2017, pp. 27--38.

Digital Library

[7]

A. Paudice, L. Muñoz-González, and E. C. Lupu, "Label sanitization against label flipping poisoning attacks," arXiv preprint, 2018.

[8]

W. Ruan, M. Wu, Y. Sun, X. Huang, D. Kroening, and M. Kwiatkowska, "Global robustness evaluation of deep neural networks with provable guarantees for l0 norm," arXiv preprint, 2018.

[9]

K. Pei, Y. Cao, J. Yang, and S. Jana, "Deepxplore: Automated whitebox testing of deep learning systems," in Proceedings of the 26th Symposium on Operating Systems Principles. ACM, 2017, pp. 1--18.

Digital Library

[10]

Y. Tian, K. Pei, S. Jana, and B. Ray, "Deeptest: Automated testing of deep-neural-network-driven autonomous cars," arXiv preprint arXiv:1708.08559, 2017.

[11]

M. Wicker, X. Huang, and M. Kwiatkowska, "Feature-guided black-box safety testing of deep neural networks," in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2018, pp. 408--426.

[12]

Y. Sun, X. Huang, and D. Kroening, "Testing deep neural networks," arXiv preprint, 2018.

[13]

L. Ma, F. Juefei-Xu, J. Sun, C. Chen, T. Su, F. Zhang, M. Xue, B. Li, L. Li, Y. Liu, J. Zhao, and Y. Wang, "Deepgauge: Comprehensive and multi-granularity testing criteria for gauging the robustness of deep learning systems," arXiv preprint, 2018.

[14]

J. Wang, J. Sun, P. Zhang, and X. Wang, "Detecting adversarial samples for deep neural networks through mutation testing," arXiv preprint, 2018.

[15]

L. Ma, F. Zhang, J. Sun, M. Xue, B. Li, F. Juefei-Xu, C. Xie, L. Li, Y. Liu, J. Zhao, and Y. Wang, "Deepmutation: Mutation testing of deep learning systems," arXiv preprint, 2018.

[16]

S. Srisakaokul, Z. Wu, A. Astorga, O. Alebiosu, and T. Xie, "Multiple-implementation testing of supervised learning software," in Proceedings of the AAAI-18 Workshop on Engineering Dependable and Secure Machine Learning Systems (EDSMLS), 2018.

[17]

M. Zhang, Y. Zhang, L. Zhang, C. Liu, and S. Khurshid, "Deeproad: Gan-based metamorphic autonomous driving system testing," arXiv preprint, 2018.

[18]

Y. Sun, M. Wu, W. Ruan, X. Huang, M. Kwiatkowska, and D. Kroening, "Concolic testing for deep neural networks," arXiv preprint, 2018.

[19]

T. Dreossi, A. Donzé, and S. A. Seshia, "Compositional falsification of cyber-physical systems with machine learning components," in NASA Formal Methods Symposium. Springer, 2017, pp. 357--372.

[20]

C. E. Tuncali, G. Fainekos, H. Ito, and J. Kapinski, "Simulation-based adversarial test generation for autonomous vehicles with machine learning components," arXiv preprint arXiv:1804.06760, 2018.

[21]

Z. Zhang, G. Ernst, S. Sedwards, P. Arcaini, and I. Hasuo, "Two-layered falsification of hybrid systems guided by monte carlo tree search," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018.

[22]

Z. Kurd and T. Kelly, "Establishing safety criteria for artificial neural networks," in International Conference on Knowledge-Based and Intelligent Information and Engineering Systems. Springer, 2003, pp. 163--169.

[23]

S. A. Seshia, D. Sadigh, and S. S. Sastry, "Towards verified artificial intelligence," arXiv preprint, 2016.

[24]

S. A. Seshia, A. Desai, T. Dreossi, D. Fremont, S. Ghosh, E. Kim, S. Shivakumar, M. Vazquez-Chanlatte, and X. Yue, "Formal specification for deep neural networks," arXiv preprint, 2018.

[25]

J. Leike, M. Martic, V. Krakovna, P. A. Ortega, T. Everitt, A. Lefrancq, L. Orseau, and S. Legg, "AI safety gridworlds," arXiv preprint, 2017.

[26]

F. Leofante, N. Narodytska, L. Pulina, and A. Tacchella, "Automated verification of neural networks: Advances, challenges and perspectives," arXiv preprint, 2018.

[27]

K. Scheibler, L. Winterer, R. Wimmer, and B. Becker, "Towards verification of artificial neural networks," in Workshop on Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2015, pp. 30--40.

[28]

G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, "Reluplex: An efficient smt solver for verifying deep neural networks," in International Conference on Computer Aided Verification. Springer, 2017, pp. 97--117.

[29]

R. Ehlers, "Formal verification of piece-wise linear feed-forward neural networks," in International Symposium on Automated Technology for Verification and Analysis. Springer, 2017, pp. 269--286.

[30]

R. Bunel, I. Turkaslan, P. H. S. Torr, P. Kohli, and M. P. Kumar, "A unified view of piecewise linear neural network verification," arXiv preprint, 2018.

[31]

W. Ruan, X. Huang, and M. Kwiatkowska, "Reachability analysis of deep neural networks with provable guarantees," arXiv preprint, 2018.

[32]

S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari, "Output range analysis for deep feedforward neural networks," in NASA Formal Methods Symposium. Springer, 2018, pp. 121--138.

[33]

L. Pulina and A. Tacchella, "An abstraction-refinement approach to verification of artificial neural networks," in International Conference on Computer Aided Verification. Springer, 2010, pp. 243--257.

Digital Library

[34]

V. Tjeng and R. Tedrake, "Verifying neural networks with mixed integer programming," arXiv preprint arXiv:1711.07356, 2017.

[35]

T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, "Ai 2: Safety and robustness certification of neural networks with abstract interpretation," in Security and Privacy (SP), 2018 IEEE Symposium on, 2018.

[36]

W. Xiang, H.-D. Tran, and T. T. Johnson, "Reachable set computation and safety verification for neural networks with relu activations," arXiv preprint arXiv:1712.08163, 2017.

[37]

W. Xiang, P. Musau, A. A. Wild, D. M. Lopez, N. Hamilton, X. Yang, J. Rosenfeld, and T. T. Johnson, "Verification for machine learning, autonomy, and neural networks survey," arXiv preprint arXiv:1810.01989, 2018.

[38]

W. Xiang and T. T. Johnson, "Reachability analysis and safety verification for neural network control systems," arXiv preprint arXiv:1805.09944, 2018.

[39]

R. Ivanov, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, "Verisig: verifying safety properties of hybrid systems with neural network controllers," in Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control (HSCC), to appear. ACM, 2019.

Digital Library

[40]

M. E. Akintunde, A. Lomuscio, L. Maganti, and E. Pirovano, "Reachability analysis for neural agent-environment systems," in Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2018). AAAI, 2018.

[41]

G. Frehse, C. L. Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler, "SpaceEx: Scalable verification of hybrid systems," in International Conference on Computer Aided Verification (CAV). Springer, 2011, pp. 379--395.

Digital Library

[42]

X. Chen, E. Ábrahám, and S. Sankaranarayanan, "Flow*: An analyzer for nonlinear hybrid systems," in International Conference on Computer Aided Verification (CAV). Springer, 2013, pp. 258--263.

[43]

C. E. Tuncali, J. Kapinski, H. Ito, and J. V. Deshmukh, "Reasoning about safety of learning-enabled components in autonomous cyber-physical systems," in Proceedings of the 55th Annual Design Automation Conference (DAC). ACM, 2018.

Digital Library

[44]

X. Sun, H. Khedr, and Y. Shoukry, "Formal verification of neural network controlled autonomous systems," arXiv preprint arXiv:1810.13072, 2018.

[45]

A. Krizhevsky, I. Sutskever, and G. E. Hinton, "Imagenet classification with deep convolutional neural networks," in Advances in neural information processing systems, 2012, pp. 1097--1105.

Digital Library

[46]

Y. Shoukry, P. Nuzzo, A. L. Sangiovanni-Vincentelli, S. A. Seshia, G. J. Pappas, and P. Tabuada, "SMC: Satisfiability Modulo Convex optimization," in Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (HSCC). ACM, 2017, pp. 19--28.

Digital Library

[47]

Y. Shoukry, P. Nuzzo, A. L. Sangiovanni-Vincentelli, S. A. Seshia, G. J. Pappas, and P. Tabuada, "Smc: Satisfiability modulo convex programming {40pt}," Proceedings of the IEEE, vol. 106, no. 9, pp. 1655--1679, 2018.

[48]

M. d. Berg, O. Cheong, M. v. Kreveld, and M. Overmars, Computational geometry: algorithms and applications. Springer-Verlag TELOS, 2008.

Digital Library

[49]

(2018, Jun.) SatEX Solver. {Online}. Available: https://yshoukry.bitbucket.io/SatEX/

Cited By

Nenchev V(2025)One Stack, Diverse Vehicles: Checking Safe Portability of Automated Driving Software2025 IEEE/SICE International Symposium on System Integration (SII)10.1109/SII59315.2025.10870905(764-769)Online publication date: 21-Jan-2025
https://doi.org/10.1109/SII59315.2025.10870905
Chakraborty SJha SSamii SMundhenk P(2024)Introduction to the Special Issue on Automotive CPS Safety & Security: Part 2ACM Transactions on Cyber-Physical Systems10.1145/36502108:2(1-17)Online publication date: 8-Mar-2024
https://dl.acm.org/doi/10.1145/3650210
Chen HBabar M(2024)Security for Machine Learning-based Software Systems: A Survey of Threats, Practices, and ChallengesACM Computing Surveys10.1145/363853156:6(1-38)Online publication date: 23-Feb-2024
https://dl.acm.org/doi/10.1145/3638531
Show More Cited By

Index Terms

Formal verification of neural network controlled autonomous systems
1. Computing methodologies
  1. Artificial intelligence
    1. Control methods
2. Security and privacy
  1. Formal methods and theory of security

Recommendations

Formal Specification and Verification of Autonomous Robotic Systems: A Survey

Autonomous robotic systems are complex, hybrid, and often safety critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or ...
Formal verification of an autonomous wheel loader by model checking
FormaliSE '18: Proceedings of the 6th Conference on Formal Methods in Software Engineering

In an attempt to increase productivity and the workers' safety, the construction industry is moving towards autonomous construction sites, where various construction machines operate without human intervention. In order to perform their tasks ...
Formal Verification of Neural Network Controllers for Collision-Free Flight
Software Verification
Abstract
We investigate a method for formally verifying the absence of adversarial examples in a neural network controller. Our approach applies to networks with piecewise affine activation units, which may be encoded symbolically as a piecewise affine ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '19: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

April 2019

299 pages

ISBN:9781450362825

DOI:10.1145/3302504

Program Chairs:
Necmiye Ozay
University of Michigan
,
Pavithra Prabhakar
Kansas State University

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 April 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

HSCC '19

Sponsor:

SIGBED

HSCC '19: 22nd ACM International Conference on Hybrid Systems: Computation and Control

April 16 - 18, 2019

Quebec, Montreal, Canada

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

86
Total Citations
View Citations
2,922
Total Downloads

Downloads (Last 12 months)523
Downloads (Last 6 weeks)76

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Nenchev V(2025)One Stack, Diverse Vehicles: Checking Safe Portability of Automated Driving Software2025 IEEE/SICE International Symposium on System Integration (SII)10.1109/SII59315.2025.10870905(764-769)Online publication date: 21-Jan-2025
https://doi.org/10.1109/SII59315.2025.10870905
Chakraborty SJha SSamii SMundhenk P(2024)Introduction to the Special Issue on Automotive CPS Safety & Security: Part 2ACM Transactions on Cyber-Physical Systems10.1145/36502108:2(1-17)Online publication date: 8-Mar-2024
https://dl.acm.org/doi/10.1145/3650210
Chen HBabar M(2024)Security for Machine Learning-based Software Systems: A Survey of Threats, Practices, and ChallengesACM Computing Surveys10.1145/363853156:6(1-38)Online publication date: 23-Feb-2024
https://dl.acm.org/doi/10.1145/3638531
Fatnassi WShoukry Y(2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632970
Perez-Cerrolaza JAbella JBorg MDonzella CCerquides JCazorla FEnglund CTauber MNikolakopoulos GFlores J(2024)Artificial Intelligence for Safety-Critical Systems in Industrial and Transportation Domains: A SurveyACM Computing Surveys10.1145/362631456:7(1-40)Online publication date: 9-Apr-2024
https://dl.acm.org/doi/10.1145/3626314
Sun XShoukry Y(2024)Neurosymbolic Motion and Task Planning for Linear Temporal Logic TasksIEEE Transactions on Robotics10.1109/TRO.2024.339207940(2749-2768)Online publication date: 2024
https://doi.org/10.1109/TRO.2024.3392079
Habeeb PD’Souza DLodaya KPrabhakar P(2024)Interval Image Abstraction for Verification of Camera-Based Autonomous SystemsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.344830643:11(4310-4321)Online publication date: Nov-2024
https://doi.org/10.1109/TCAD.2024.3448306
Fatnassi WFeeney AYamamoto VChandramowlishwaran AShoukry Y(2024)BERN-NN-IBF: Enhancing Neural Network Bound Propagation Through Implicit Bernstein Form and Optimized Tensor OperationsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.344757743:11(4334-4345)Online publication date: Nov-2024
https://doi.org/10.1109/TCAD.2024.3447577
Habeeb PGupta LPrabhakar P(2024)Approximate Conformance Checking for Closed-Loop Systems With Neural Network ControllersIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.344581343:11(4322-4333)Online publication date: Nov-2024
https://doi.org/10.1109/TCAD.2024.3445813
Hagos DRawat D(2024)Neuro-Symbolic AI for Military ApplicationsIEEE Transactions on Artificial Intelligence10.1109/TAI.2024.34447465:12(6012-6026)Online publication date: Dec-2024
https://doi.org/10.1109/TAI.2024.3444746
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten