English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present a tool for computing exact forward and backward reachable sets ofdeep neural networks with rectified linear unit (ReLU) activation. We thendevelop algorithms using this tool to compute invariant sets and regions ofattraction (ROAs) for control systems with neural networks in the feedbackloop. Our algorithm is unique in that it builds the reachable sets byincrementally enumerating polyhedral regions in the input space, rather thaniterating layer-by-layer through the network as in other methods. Whenperforming safety verification, if an unsafe region is found, our algorithm canreturn this result without completing the full reachability computation, thusgiving an anytime property that accelerates safety verification. Furthermore,we introduce a method to accelerate the computation of ROAs in the case thatdeep learned components are homeomorphisms, which we find is surprisinglycommon in practice. We demonstrate our tool in several test cases. We compute aROA for a learned van der Pol oscillator model. We find a control invariant setfor a learned torque-controlled pendulum model. We also verify specific safetyproperties for multiple deep networks related to the ACAS Xu aircraft collisionadvisory system. Finally, we apply our algorithm to find ROAs for animage-based aircraft runway taxi problem. Algorithm source code:https://github.com/StanfordMSL/Neural-Network-Reach .

Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems