ReachNN: Reachability Analysis of Neural-Network Controlled Systems

Chao Huang; Jiameng Fan; Qi Zhu; Wenchao Li; Xin Chen

arxiv: 1906.10654 · v1 · pith:KT3GZYLYnew · submitted 2019-06-25 · 📡 eess.SY · cs.LG· cs.SY

ReachNN: Reachability Analysis of Neural-Network Controlled Systems

Chao Huang , Jiameng Fan , Wenchao Li , Xin Chen , Qi Zhu This is my paper

Pith reviewed 2026-05-25 16:27 UTC · model grok-4.3

classification 📡 eess.SY cs.LGcs.SY

keywords reachability analysisneural network controlBernstein polynomialssafety verificationLipschitz continuityactivation functionsclosed-loop systems

0 comments

The pith

Bernstein polynomial abstraction enables reachability analysis for neural network controllers with any Lipschitz continuous activations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a reachability analysis technique for dynamical systems that use neural networks as controllers. It abstracts the networks with Bernstein polynomials over limited input regions and supplies error bounds derived from polynomial theory plus sampling, relying on the network being Lipschitz continuous. This setup covers networks with mixed activation functions rather than restricting to one type such as ReLU. A reader would care because it widens the class of verifiable controllers in safety-critical loops.

Core claim

Feedforward neural networks can be abstracted via Bernstein polynomials on a small input subset; the resulting error is bounded theoretically from Bernstein properties and practically by sampling after estimating the Lipschitz constant through forward reachability, allowing closed-loop reachability computation for networks that contain heterogeneous activation functions.

What carries the argument

Bernstein polynomial abstraction of the neural network over input subsets, with Lipschitz-constant error bounds from both analytic Bernstein theory and sampling-based estimation.

If this is right

Verification becomes possible for controllers that combine different activation functions inside one network.
Both a theoretical guarantee and a practical sampling procedure are available for the same abstraction.
Lipschitz constants can be obtained on the fly from forward reachability without separate global analysis.
The same abstraction pipeline applies to a larger collection of benchmark control systems than earlier methods.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The sampling error estimator could be replaced by tighter concentration inequalities for fewer samples.
The input-subset restriction suggests a natural way to combine the method with state-space partitioning.
The Lipschitz assumption opens a route to certify controllers whose activations are only locally Lipschitz.

Load-bearing premise

The neural networks must be Lipschitz continuous so the abstraction error can be bounded.

What would settle it

A concrete neural-network controller whose true reachable set escapes the computed over-approximation or whose safety violation is missed by the over-approximation would show the bounds are invalid.

Figures

Figures reproduced from arXiv: 1906.10654 by Chao Huang, Jiameng Fan, Qi Zhu, Wenchao Li, Xin Chen.

**Figure 2.** Figure 2: Schematic diagram of Input Interval and Output [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** Figure 3: Flowpipes computed by interval overapproxima [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

**Figure 4.** Figure 4: Flowpipes for the selected examples: Red curves denote the trajectories of [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗

**Figure 5.** Figure 5: Bernstein polynomial based approximation for dif [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗

**Figure 6.** Figure 6: ReachNN comparison between large Lipschitz con [PITH_FULL_IMAGE:figures/full_fig_p011_6.png] view at source ↗

**Figure 7.** Figure 7: Examples 12 [PITH_FULL_IMAGE:figures/full_fig_p012_7.png] view at source ↗

read the original abstract

Applying neural networks as controllers in dynamical systems has shown great promises. However, it is critical yet challenging to verify the safety of such control systems with neural-network controllers in the loop. Previous methods for verifying neural network controlled systems are limited to a few specific activation functions. In this work, we propose a new reachability analysis approach based on Bernstein polynomials that can verify neural-network controlled systems with a more general form of activation functions, i.e., as long as they ensure that the neural networks are Lipschitz continuous. Specifically, we consider abstracting feedforward neural networks with Bernstein polynomials for a small subset of inputs. To quantify the error introduced by abstraction, we provide both theoretical error bound estimation based on the theory of Bernstein polynomials and more practical sampling based error bound estimation, following a tight Lipschitz constant estimation approach based on forward reachability analysis. Compared with previous methods, our approach addresses a much broader set of neural networks, including heterogeneous neural networks that contain multiple types of activation functions. Experiment results on a variety of benchmarks show the effectiveness of our approach.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

ReachNN abstracts NN controllers via Bernstein polynomials to handle any Lipschitz-continuous activations, including mixed ones, which widens the verifiable class beyond prior activation-specific limits.

read the letter

The main takeaway is that this paper shows how Bernstein polynomials can abstract feedforward neural networks for reachability analysis in closed-loop control systems, provided the network is Lipschitz continuous. That single condition lets the method cover heterogeneous networks with mixed activations, which previous reachability tools could not handle without custom handling per activation type. The abstraction is applied to a small subset of inputs, with error quantified both by Bernstein theory bounds and by a sampling procedure that re-uses a forward-reachability Lipschitz estimate. Experiments on standard benchmarks indicate the approach can verify safety properties on networks that earlier methods simply could not process. The work sits on established polynomial approximation results and standard Lipschitz arguments, so the core reasoning does not appear circular. The central claim—that the method broadens the set of verifiable NN controllers—holds up on the evidence given. Two points are worth watching. First, restricting the abstraction to a small input subset is presented as a design choice, but it will constrain scaling to higher-dimensional inputs. Second, the sampling error bound inherits whatever looseness exists in the Lipschitz estimate; the paper claims the estimate is tight, yet the actual overhead and tightness on larger examples would need checking in the full text. Overall the paper is aimed at people already working on formal verification of neural controllers. Anyone looking for a concrete way to move past ReLU-only or sigmoid-only restrictions will find usable material here. It is coherent on its own terms and addresses a documented limitation in the literature, so it merits a serious referee even if revisions are needed on the scaling and bound tightness questions.

Referee Report

2 major / 3 minor

Summary. The paper introduces ReachNN, a reachability analysis method for neural-network controlled dynamical systems. It abstracts feedforward NNs with Bernstein polynomials over a small subset of inputs, applicable to any Lipschitz-continuous activations (including heterogeneous ones). Theoretical error bounds are derived from Bernstein polynomial theory, supplemented by a practical sampling-based bound that uses a tight Lipschitz constant estimated via forward reachability analysis. Experiments on benchmarks demonstrate effectiveness compared to prior methods limited to specific activations.

Significance. If the central claims hold, the work meaningfully broadens verifiable NN controllers beyond ReLU/sigmoid/tanh restrictions to any Lipschitz-continuous network, which is a substantive advance for safety-critical control verification. Credit is due for grounding the abstraction in established Bernstein theory, providing both theoretical and sampling-based error bounds, and explicitly handling heterogeneous activations. The deliberate restriction to small input subsets is presented as a scalability trade-off rather than a soundness limitation.

major comments (2)

[§4.2] §4.2 (Lipschitz constant estimation): the forward reachability procedure used to compute the sampling-based Lipschitz bound is described at a high level but lacks an explicit statement of how over-approximation error in the reachability step propagates into the final error bound; this is load-bearing for the claim that the sampling bound is 'tight' and practical.
[§5, Table 2] §5 (Experiments, Table 2): the reported verification times and success rates for heterogeneous networks are given without a direct comparison to the same networks under a single-activation baseline; this weakens the cross-method claim that the approach 'addresses a much broader set' because the performance delta attributable to heterogeneity is not isolated.

minor comments (3)

[§3.1] Notation: the symbol for the Bernstein polynomial degree is introduced inconsistently (sometimes n, sometimes d) across §3.1 and the appendix; a single consistent symbol would improve readability.
[Figure 3] Figure 3 caption: the legend does not explicitly state that the shaded regions represent the computed reachable sets under the Bernstein abstraction; this should be clarified.
[§2] Related work: the discussion of prior Bernstein-polynomial uses in verification (e.g., in polynomial systems) is brief; adding one or two sentences contrasting the NN-specific error estimation would strengthen context.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback and positive assessment of the work. We address each major comment below and will incorporate clarifications to strengthen the manuscript.

read point-by-point responses

Referee: [§4.2] §4.2 (Lipschitz constant estimation): the forward reachability procedure used to compute the sampling-based Lipschitz bound is described at a high level but lacks an explicit statement of how over-approximation error in the reachability step propagates into the final error bound; this is load-bearing for the claim that the sampling bound is 'tight' and practical.

Authors: We agree that an explicit discussion of error propagation would improve clarity. In the revised version we will insert a dedicated paragraph in §4.2 that (i) recalls the over-approximation properties of the forward reachability step, (ii) shows how the resulting interval on the Lipschitz constant is used to scale the sampling-based error term, and (iii) argues why the composite bound remains practically tight on the evaluated benchmarks. revision: yes
Referee: [§5, Table 2] §5 (Experiments, Table 2): the reported verification times and success rates for heterogeneous networks are given without a direct comparison to the same networks under a single-activation baseline; this weakens the cross-method claim that the approach 'addresses a much broader set' because the performance delta attributable to heterogeneity is not isolated.

Authors: Prior methods cannot be executed on heterogeneous networks at all, so a same-network single-activation baseline does not exist for the instances in Table 2. The experiments therefore demonstrate capability on a class of networks that previous techniques cannot process. To address the concern we will add one clarifying sentence in §5 noting this limitation of the baselines and reiterating that the reported results already isolate the benefit of handling heterogeneity. revision: partial

Circularity Check

0 steps flagged

Derivation self-contained in established Bernstein polynomial theory

full rationale

The paper abstracts feedforward NNs via Bernstein polynomials over a restricted input subset and derives error bounds from the classical theory of Bernstein polynomials plus the Lipschitz property of the network; both the abstraction technique and the error estimation are imported from external mathematical results rather than being fitted or redefined within the paper. No load-bearing step reduces to a self-citation chain, a fitted parameter renamed as a prediction, or an ansatz smuggled via prior work by the same authors. The central claim therefore remains independent of its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on the domain assumption of Lipschitz continuity for error bounding and on standard properties of Bernstein polynomials; no free parameters or invented entities are identifiable from the abstract alone.

axioms (1)

domain assumption Neural networks are Lipschitz continuous
Invoked to support abstraction and both theoretical and sampling-based error bound estimation.

pith-pipeline@v0.9.0 · 5724 in / 1129 out tokens · 23633 ms · 2026-05-25T16:27:08.781128+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages · 7 internal anchors

[1]

M. Althoff. 2015. An Introduction to CORA 2015. InProc. of ARCH’15 (EPiC Series in Computer Science), Vol. 34. EasyChair, 120–151

work page 2015
[2]

R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. 1995. The Algorithmic Analysis of Hybrid Systems. Theor. Comput. Sci. 138, 1 (1995), 3–34

work page 1995
[3]

Jimmy Ba and Rich Caruana. 2014. Do deep nets really need to be deep?. In Advances in neural information processing systems . 2654–2662

work page 2014
[4]

Randall D Beer, Hillel J Chiel, and Leon S Sterling. 1989. Heterogeneous neural networks for adaptive behavior in dynamic environments. In Advances in neural information processing systems. 577–585

work page 1989
[5]

Berz and K

M. Berz and K. Makino. 1998. Verified Integration of ODEs and Flows Using Differential Algebraic Methods on High-Order Taylor Models.Reliable Computing 4 (1998), 361–369. Issue 4

work page 1998
[6]

BM Brown, D Elliott, and DF Paget. 1987. Lipschitz constants for the Bernstein polynomials of a Lipschitz continuous function. Journal of approximation theory 49, 2 (1987), 196–199

work page 1987
[7]

Cristian BuciluÇŐ, Rich Caruana, and Alexandru Niculescu-Mizil. 2006. Model compression. In Proceedings of the 12th ACM SIGKDD international conference on Knowledge discovery and data mining . ACM, 535–541

work page 2006
[8]

X. Chen. 2015. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Ph.D. Dissertation. RWTH Aachen University

work page 2015
[9]

X. Chen, E. Ábrahám, and S. Sankaranarayanan. 2012. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In Proc. of RTSS’12. IEEE Computer Society, 183–192

work page 2012
[10]

X. Chen, E. Ábrahám, and S. Sankaranarayanan. 2013. Flow*: An Analyzer for Non-linear Hybrid Systems. In Proc. of CA V’13 (LNCS), Vol. 8044. Springer, 258–263

work page 2013
[11]

Chen and S

X. Chen and S. Sankaranarayanan. 2016. Decomposed Reachability Analysis for Nonlinear Systems. In 2016 IEEE Real-Time Systems Symposium (RTSS) . IEEE Press, 13–24

work page 2016
[12]

Louis De Branges. 1959. The stone-weierstrass theorem. Proc. Amer. Math. Soc. 10, 5 (1959), 822–824

work page 1959
[13]

Dreossi, T

T. Dreossi, T. Dang, and C. Piazza. 2016. Parallelotope bundles for polynomial reachability. In HSCC. ACM, 297–306

work page 2016
[14]

P. S. Duggirala, S. Mitra, M. Viswanathan, and M. Potok. 2015. C2E2: A Verification Tool for Stateflow Models. InProc. of TACAS’15 (LNCS), Vol. 9035. Springer, 68–82

work page 2015
[15]

Dutta, X

S. Dutta, X. Chen, and S. Sankaranarayanan. 2019. Reachability Analysis for Neural Feedback Systems using Regressive Polynomial Rule Inference. In Hybrid Systems: Computation and Control (HSCC) . ACM Press, 157–168

work page 2019
[16]

Dutta, S

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

work page 2018
[17]

G. Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In HSCC. Springer, 258–273

work page 2005
[18]

Frehse, C

G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In Proc. of CA V’11 (LNCS), Vol. 6806. Springer, 379–395

work page 2011
[19]

Eduardo Gallestey and Peter Hokayem. 2019. Lecture notes in Nonlinear Systems and Control

work page 2019
[20]

T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. 1998. What’s decidable about hybrid automata? Journal of computer and system sciences 57, 1 (1998), 94–124

work page 1998
[21]

Distilling the Knowledge in a Neural Network

Geoffrey E. Hinton, Oriol Vinyals, and Jeffrey Dean. 2015. Distilling the Knowl- edge in a Neural Network. CoRR abs/1503.02531 (2015)

work page internal anchor Pith review Pith/arXiv arXiv 2015
[22]

Huang, X

C. Huang, X. Chen, W. Lin, Z. Yang, and X. Li. 2017. Probabilistic Safety Verifica- tion of Stochastic Hybrid Systems Using Barrier Certificates. TECS 16, 5s (2017), 186

work page 2017
[23]

Huang, M

X. Huang, M. Kwiatkowska, S. Wang, and M. Wu. 2017. Safety verification of deep neural networks. In International Conference on Computer Aided Verification. Springer, 3–29

work page 2017
[24]

Radoslav Ivanov, James Weimer, Rajeev Alur, George J Pappas, and Insup Lee

work page
[25]

Verisig: verifying safety properties of hybrid systems with neural network controllers

Verisig: verifying safety properties of hybrid systems with neural network controllers. arXiv preprint arXiv:1811.01828 (2018)

work page internal anchor Pith review Pith/arXiv arXiv 2018
[26]

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

work page 2017
[27]

S. Kong, S. Gao, W. Chen, and E. M. Clarke. 2015. dReach:δ-Reachability Analysis for Hybrid Systems. In Proc. of TACAS’15 (LNCS), Vol. 9035. Springer, 200–205

work page 2015
[28]

Continuous control with deep reinforcement learning

Timothy P. Lillicrap, Jonathan J. Hunt, Alexander Pritzel, Nicolas Heess, Tom Erez, Yuval Tassa, David Silver, and Daan Wierstra. 2016. Continuous control with deep reinforcement learning. CoRR abs/1509.02971 (2016)

work page internal anchor Pith review Pith/arXiv arXiv 2016
[29]

George G Lorentz. 2013. Bernstein polynomials. American Mathematical Soc

work page 2013
[30]

Lygeros, C

J. Lygeros, C. Tomlin, and S. Sastry. 1999. Controllers for reachability specifica- tions for hybrid systems. Automatica 35, 3 (1999), 349–370

work page 1999
[31]

Makino and M

K. Makino and M. Berz. 2005. Verified Global Optimization with Taylor Model- based Range Bounders. Transactions on Computers 11, 4 (2005), 1611–1618

work page 2005
[32]

J. D. Meiss. 2007. Differential Dynamical Systems. SIAM publishers

work page 2007
[33]

Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A Rusu, Joel Veness, Marc G Bellemare, Alex Graves, Martin Riedmiller, Andreas K Fidjeland, Georg Ostrovski, et al. 2015. Human-level control through deep reinforcement learning. Nature 518, 7540 (2015), 529

work page 2015
[34]

Yunpeng Pan, Ching-An Cheng, Kamil Saigol, Keuntaek Lee, Xinyan Yan, Evan- gelos Theodorou, and Byron Boots. 2018. Agile autonomous driving using end-to-end deep imitation learning. Proceedings of Robotics: Science and Systems. Pittsburgh, Pennsylvania (2018)

work page 2018
[35]

Prajna and A

S. Prajna and A. Jadbabaie. 2004. Safety verification of hybrid systems using barrier certificates. In HSCC. Springer, 477–492

work page 2004
[36]

H. L. Royden. 1968. Real analysis. Krishna Prakashan Media

work page 1968
[37]

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

work page internal anchor Pith review Pith/arXiv arXiv 2018
[38]

Georgi V Smirnov. 2002. Introduction to the theory of differential inclusions. Vol. 41. American Mathematical Soc

work page 2002
[39]

Intriguing properties of neural networks

C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fer- gus. 2013. Intriguing properties of neural networks.arXiv preprint arXiv:1312.6199 (2013)

work page internal anchor Pith review Pith/arXiv arXiv 2013
[40]

Reachability Analysis and Safety Verification for Neural Network Control Systems

W. Xiang and T. T. Johnson. 2018. Reachability Analysis and Safety Verification for Neural Network Control Systems. arXiv preprint arXiv:1805.09944 (2018)

work page internal anchor Pith review Pith/arXiv arXiv 2018
[41]

Z. Yang, C. Huang, X. Chen, W. Lin, and Z. Liu. 2016. A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In FM. Springer, 721–738

work page 2016
[42]

Yuichi Yoshida and Takeru Miyato. 2017. Spectral norm regularization for im- proving the generalizability of deep learning. arXiv preprint arXiv:1705.10941 (2017)

work page internal anchor Pith review Pith/arXiv arXiv 2017
[43]

F. Zhao. 1992. Automatic Analysis and Synthesis of Controllers for Dynamical Systems Based on Phase-Space Knowledge . Ph.D. Dissertation. Massachusetts Institute of Technology. A APPENDIX We present the plots of flowpipes for each benchmark (see Figure 7). 11 -0.2 0 0.2 0.4 0.6 0.8 1 1.2 -0.6 -0.4 -0.2 0 0.2 0.4 0.6 (a) ex1-relu -1 -0.5 0 0.5 1 1.5 -0.6 -...

work page 1992

[1] [1]

M. Althoff. 2015. An Introduction to CORA 2015. InProc. of ARCH’15 (EPiC Series in Computer Science), Vol. 34. EasyChair, 120–151

work page 2015

[2] [2]

R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. 1995. The Algorithmic Analysis of Hybrid Systems. Theor. Comput. Sci. 138, 1 (1995), 3–34

work page 1995

[3] [3]

Jimmy Ba and Rich Caruana. 2014. Do deep nets really need to be deep?. In Advances in neural information processing systems . 2654–2662

work page 2014

[4] [4]

Randall D Beer, Hillel J Chiel, and Leon S Sterling. 1989. Heterogeneous neural networks for adaptive behavior in dynamic environments. In Advances in neural information processing systems. 577–585

work page 1989

[5] [5]

Berz and K

M. Berz and K. Makino. 1998. Verified Integration of ODEs and Flows Using Differential Algebraic Methods on High-Order Taylor Models.Reliable Computing 4 (1998), 361–369. Issue 4

work page 1998

[6] [6]

BM Brown, D Elliott, and DF Paget. 1987. Lipschitz constants for the Bernstein polynomials of a Lipschitz continuous function. Journal of approximation theory 49, 2 (1987), 196–199

work page 1987

[7] [7]

Cristian BuciluÇŐ, Rich Caruana, and Alexandru Niculescu-Mizil. 2006. Model compression. In Proceedings of the 12th ACM SIGKDD international conference on Knowledge discovery and data mining . ACM, 535–541

work page 2006

[8] [8]

X. Chen. 2015. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Ph.D. Dissertation. RWTH Aachen University

work page 2015

[9] [9]

X. Chen, E. Ábrahám, and S. Sankaranarayanan. 2012. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In Proc. of RTSS’12. IEEE Computer Society, 183–192

work page 2012

[10] [10]

X. Chen, E. Ábrahám, and S. Sankaranarayanan. 2013. Flow*: An Analyzer for Non-linear Hybrid Systems. In Proc. of CA V’13 (LNCS), Vol. 8044. Springer, 258–263

work page 2013

[11] [11]

Chen and S

X. Chen and S. Sankaranarayanan. 2016. Decomposed Reachability Analysis for Nonlinear Systems. In 2016 IEEE Real-Time Systems Symposium (RTSS) . IEEE Press, 13–24

work page 2016

[12] [12]

Louis De Branges. 1959. The stone-weierstrass theorem. Proc. Amer. Math. Soc. 10, 5 (1959), 822–824

work page 1959

[13] [13]

Dreossi, T

T. Dreossi, T. Dang, and C. Piazza. 2016. Parallelotope bundles for polynomial reachability. In HSCC. ACM, 297–306

work page 2016

[14] [14]

P. S. Duggirala, S. Mitra, M. Viswanathan, and M. Potok. 2015. C2E2: A Verification Tool for Stateflow Models. InProc. of TACAS’15 (LNCS), Vol. 9035. Springer, 68–82

work page 2015

[15] [15]

Dutta, X

S. Dutta, X. Chen, and S. Sankaranarayanan. 2019. Reachability Analysis for Neural Feedback Systems using Regressive Polynomial Rule Inference. In Hybrid Systems: Computation and Control (HSCC) . ACM Press, 157–168

work page 2019

[16] [16]

Dutta, S

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

work page 2018

[17] [17]

G. Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In HSCC. Springer, 258–273

work page 2005

[18] [18]

Frehse, C

G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In Proc. of CA V’11 (LNCS), Vol. 6806. Springer, 379–395

work page 2011

[19] [19]

Eduardo Gallestey and Peter Hokayem. 2019. Lecture notes in Nonlinear Systems and Control

work page 2019

[20] [20]

T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. 1998. What’s decidable about hybrid automata? Journal of computer and system sciences 57, 1 (1998), 94–124

work page 1998

[21] [21]

Distilling the Knowledge in a Neural Network

Geoffrey E. Hinton, Oriol Vinyals, and Jeffrey Dean. 2015. Distilling the Knowl- edge in a Neural Network. CoRR abs/1503.02531 (2015)

work page internal anchor Pith review Pith/arXiv arXiv 2015

[22] [22]

Huang, X

C. Huang, X. Chen, W. Lin, Z. Yang, and X. Li. 2017. Probabilistic Safety Verifica- tion of Stochastic Hybrid Systems Using Barrier Certificates. TECS 16, 5s (2017), 186

work page 2017

[23] [23]

Huang, M

X. Huang, M. Kwiatkowska, S. Wang, and M. Wu. 2017. Safety verification of deep neural networks. In International Conference on Computer Aided Verification. Springer, 3–29

work page 2017

[24] [24]

Radoslav Ivanov, James Weimer, Rajeev Alur, George J Pappas, and Insup Lee

work page

[25] [25]

Verisig: verifying safety properties of hybrid systems with neural network controllers

Verisig: verifying safety properties of hybrid systems with neural network controllers. arXiv preprint arXiv:1811.01828 (2018)

work page internal anchor Pith review Pith/arXiv arXiv 2018

[26] [26]

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

work page 2017

[27] [27]

S. Kong, S. Gao, W. Chen, and E. M. Clarke. 2015. dReach:δ-Reachability Analysis for Hybrid Systems. In Proc. of TACAS’15 (LNCS), Vol. 9035. Springer, 200–205

work page 2015

[28] [28]

Continuous control with deep reinforcement learning

Timothy P. Lillicrap, Jonathan J. Hunt, Alexander Pritzel, Nicolas Heess, Tom Erez, Yuval Tassa, David Silver, and Daan Wierstra. 2016. Continuous control with deep reinforcement learning. CoRR abs/1509.02971 (2016)

work page internal anchor Pith review Pith/arXiv arXiv 2016

[29] [29]

George G Lorentz. 2013. Bernstein polynomials. American Mathematical Soc

work page 2013

[30] [30]

Lygeros, C

J. Lygeros, C. Tomlin, and S. Sastry. 1999. Controllers for reachability specifica- tions for hybrid systems. Automatica 35, 3 (1999), 349–370

work page 1999

[31] [31]

Makino and M

K. Makino and M. Berz. 2005. Verified Global Optimization with Taylor Model- based Range Bounders. Transactions on Computers 11, 4 (2005), 1611–1618

work page 2005

[32] [32]

J. D. Meiss. 2007. Differential Dynamical Systems. SIAM publishers

work page 2007

[33] [33]

Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A Rusu, Joel Veness, Marc G Bellemare, Alex Graves, Martin Riedmiller, Andreas K Fidjeland, Georg Ostrovski, et al. 2015. Human-level control through deep reinforcement learning. Nature 518, 7540 (2015), 529

work page 2015

[34] [34]

Yunpeng Pan, Ching-An Cheng, Kamil Saigol, Keuntaek Lee, Xinyan Yan, Evan- gelos Theodorou, and Byron Boots. 2018. Agile autonomous driving using end-to-end deep imitation learning. Proceedings of Robotics: Science and Systems. Pittsburgh, Pennsylvania (2018)

work page 2018

[35] [35]

Prajna and A

S. Prajna and A. Jadbabaie. 2004. Safety verification of hybrid systems using barrier certificates. In HSCC. Springer, 477–492

work page 2004

[36] [36]

H. L. Royden. 1968. Real analysis. Krishna Prakashan Media

work page 1968

[37] [37]

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

work page internal anchor Pith review Pith/arXiv arXiv 2018

[38] [38]

Georgi V Smirnov. 2002. Introduction to the theory of differential inclusions. Vol. 41. American Mathematical Soc

work page 2002

[39] [39]

Intriguing properties of neural networks

C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fer- gus. 2013. Intriguing properties of neural networks.arXiv preprint arXiv:1312.6199 (2013)

work page internal anchor Pith review Pith/arXiv arXiv 2013

[40] [40]

Reachability Analysis and Safety Verification for Neural Network Control Systems

W. Xiang and T. T. Johnson. 2018. Reachability Analysis and Safety Verification for Neural Network Control Systems. arXiv preprint arXiv:1805.09944 (2018)

work page internal anchor Pith review Pith/arXiv arXiv 2018

[41] [41]

Z. Yang, C. Huang, X. Chen, W. Lin, and Z. Liu. 2016. A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In FM. Springer, 721–738

work page 2016

[42] [42]

Yuichi Yoshida and Takeru Miyato. 2017. Spectral norm regularization for im- proving the generalizability of deep learning. arXiv preprint arXiv:1705.10941 (2017)

work page internal anchor Pith review Pith/arXiv arXiv 2017

[43] [43]

F. Zhao. 1992. Automatic Analysis and Synthesis of Controllers for Dynamical Systems Based on Phase-Space Knowledge . Ph.D. Dissertation. Massachusetts Institute of Technology. A APPENDIX We present the plots of flowpipes for each benchmark (see Figure 7). 11 -0.2 0 0.2 0.4 0.6 0.8 1 1.2 -0.6 -0.4 -0.2 0 0.2 0.4 0.6 (a) ex1-relu -1 -0.5 0 0.5 1 1.5 -0.6 -...

work page 1992