Boosting Verification of Deep Reinforcement Learning via Piece-Wise Linear Decision Neural Networks
Authors: Jiaxu Tian
Dapeng Zhi
Si Liu
Peixin Wang
Cheng Chen
Min Zhang
Venue: NeurIPS 2023 poster (2023)
Keywords: Deep reinforcement learning
Reachability analysis
Hybrid system
State abstraction
TL;DR: We propose a novel DNN-based piece-wise linear decision model to facilitate the verification of DRL systems while achieving the comparable performance as ordinary DNN.

Abstract: Formally verifying deep reinforcement learning (DRL) systems suffers from both inaccurate verification results and limited scalability. The major obstacle lies in the large overestimation introduced inherently during training and then transforming the inexplicable decision-making models, i.e., deep neural networks (DNNs), into easy-to-verify models. In this paper, we propose an inverse transform-then-train approach, which first encodes a DNN into an equivalent set of efficiently and tightly verifiable linear control policies and then optimizes them via reinforcement learning.  We accompany our inverse approach with a novel neural network model called piece-wise linear decision neural networks (PLDNNs), which are compatible with most existing DRL training algorithms with comparable performance against conventional DNNs. Our extensive experiments show that, compared to DNN-based  DRL systems, PLDNN-based systems can be more efficiently and tightly verified with up to $438$ times speedup and a significant reduction in overestimation.  In particular, even a complex $12$-dimensional DRL system is efficiently verified with up to 7 times deeper computation steps.

Boosting Verification of Deep Reinforcement Learning via Piece-wise Linear Decision Neural Networks
Jiaxu Tian ' Dapeng Zhi Si Liu 2, Peixin Wang*: 3 Cheng Chen 1, Min Zhang*
Shanghai Key Laboratory of Trustworthy Computing, East China Normal University
2 ETH Zürich
University of Oxford
512159020140stu. ecnu. edu. en, zhi www..dappnge6..comm com, si si.liu@inf.ette wtwpiiinffeehzccc.. ch, peixin. wang@cs ac.ac.a....aa................... uk, {chchen, [hhangmin]@sell ecnu, edu en
Abstract
Formally verifying deep reinforcement learning (DRL) systems suffers from both inaccurate verification results and limited scalability. The major obstacle lies in the large overestimation introduced inherently during training and then transforming the inexplicable decision-making models i.e., deep neural networks (DNNs), into easy-to-verify models. In this paper, we propose an inverse transform-then thrttt-rnnnnnn approach, which first encodes a DNN into equivalent set of efficiently and tightly verifiable linear control policies and then optimizes them via reinforcement learning. We accompany our inverse approach with novel neural network model called piece-wise linear decision neural networks (PLDNNs), which are compatible with most existing DRL training algorithms with comparable performance against conventional DNNs. Our extensive experiments show that, compared to DNN- based DRL systems, PLDNN-based systems can be more efficiently and tightly verified with up to 438 times speedup and significant reduction in overestimation. In particular, even complex 12-dimensional DRL system is efficiently verified with up to times deeper computation steps.
Introduction
Deep neural networks (DNNs) have been exhibiting appealing advantages in decision-making and control for deep reinforcement learning (DRL) systems 114 Nonetheless, the complexity and inexplicability [5] 6 of DNNs render the formal verification of their hosting systems, quite often even themselves, inaccurate and unscalable. Most existing approaches 7710 over-approximate both embedded DNNs and non-linear environment dynamics to build verifiable models, which inevitably introduces dual overestimation. In particular, DNN-specific overestimation is extremely unpredictable due to many factors such as the dimension of system states, the complexity of environment dynamics, and the size, weight, and activation function of a neural network. For example, the verification results may deviate significantly even if the DNNs of the same DRL system differ only in their weights (as we also observed; see Appendix A.4). Unsurprisingly, verifying nigh-dimensione DRL systems would only exacerbate the problems of large overestimation and limited scalability.
Common practice for formally verifying DRL systems is to train and then transform the embedded DNNs into easy-to-veriff models where, for any input set, output ranges can enclose the outputs of the over-approximated DNNs 7710 Taylor models [1]] are widely adopted due to their preservation of input-output dependencies and less overestimation (accumulated in multiple steps) than the range analysis approaches such as interval over-approximation [12 13]. However, they are still prone to intractable overestimation as the accuracy of verification depends heavily on the weights of DNNs
Corresponding authors.
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

whose effects are difficult to quantify. Several other approaches attempt to extract approximated
state-action policies, e.g.. decision trees [14 [5], from DNNs via model compression [16] and
distillation [17 techniques. However, no equivalence guarantee is established between DNNs and
the extracted policies. Consequently, verification results are just probably approximately correct [8]
Inspired by recent advances [19H22] in training near-optimal policies even with reduced training state space imposed by aggregated adjacent states, we propose a novel, inverse transform-then-rrait approach: encoding a DNN into an equivalent set of easy-to-verify linear control policies and then optimizing them by training the DNN using reinforcement learning. We accompany our inverse approach by devising a novel neural network model called piece-wise linear decision neural networks (PLDNNs), which make linear decisions on each abstract state. Unlike conventional DNNs which build state-action relation for each actual state, a PLDNN defines a linear relationship, called Linear Control Unit (I.C)), between actions and actual states associated with the same abstract state. To this end, PLDNN is essentially set of LCUs for all abstract states. In contrast to DNNs, LCUU are more explainable and verifiable without any over-approximmaion. Moreover, PLDNNN are compatible with most existing DRL training algorithms as both share the same input and output layers for the same control task.
We extensively assess PLDNN, along with the state-of-the-art tools, with respect to both performance (in terms of cumulative rewards and system robustness) and verifiability (in terms of overestimation and time cost for the reachability analysis of trained systems) on a collection of benchmarks, including a 12-dimensional control task. Our experimental results show that, compared to the DNN- based sys- tems, the FL.DN--based systems can be verified more precisely, with significantly less overestimation, and more efficiently, with up to 438 times speedup, while achieving comparable performance. More- over, compared to the state-of-the arrt tools, the complex 12-dimensional control task can be trained and verified with up to 7 times deeper computation steps, along with notable tightness improvement.
Main Contributions. Overall, we provide: (i) a novel inverse approach for boosting the formal veri- fication of DRL systems by learning efficiently and directly (without over-approximation) verifiable piece-wise linear policies with comparable performance; (ii) novel neural network model to realize the learned piece-wise linear policies, which compatible with most existing DRL algorithms; and (iii) prototype called LINCON, along with an extensive assessment which demonstrates its tightness in verification results, outperformance over the state-of-the-an tools (up to 438 times speedup), and scalability (up to 12-dimensional control task).
2 Problem Formulation and Motivation
A DRL system is driven by a DNN-implemented controller x, which is trained for decision-making, and physical model defined by the ordinary differential equations (ODEs) s(1) = f(((), a()), with s the state variables and a control action. In what follows, we omit the time variable 1. Typically, for DRL systems, continuous time is discretized, and we have x(s) state y and assume à 0 during a small time step e.g., 6. At the time point kō, k E N. the decision network receives the current state s and outputs an action dg x(S)). The state variables then evolve according to the physical model during the time interval [0, 5]. The reachable state 5k+1 at 8 from is 5k+1 S& . f(s, ad) which is called the successor state of sg. Note that the system evolves continuously from s& to Sk+1- The intermediate states can be computed by substituting the time clapses for ö in the above formula.
Definition 1 (Path of DRL systems). Given a DRL system D with an environment dynamics f. decision network n, time step size ô and initial state set So. a path of D is finite or infinite state sequence: [s0. vol - - [si.ui] S [s2.az]] S
/ [s3.as] 5 S. such that:
1. 50 So.
2. S/11 = S So" a(s, and a; for 1,
A DRL system is essentially a DNN-controlled hybrid system. Definition 2 gives formal definition of regular hybrid systems. The state space of a hybrid system the Cartesian product of set of discrete locations and state space of n real-valued variables V.. At each location / E L, the continuous variables evolve continuously according to a dynamical law = fi(v). When the guard condition on the transition between locations (4, I2) E T is triggered, the system moves to 12, and the continuous variables are reset by R. There are two steps involved in the state transition from (4: vi) to its successor state (1, 1/+1): first, from (4, vi) to its time successor (4, 11, (vi, t)), and then, to

---

(1+ Vi+1) that is the transition successor of (4, Py, (Pi, f;)), where 94, is the solution of fi with initial condition v() = v;. mapping the initial state Vi to the state y (v;,)) (i.e., the reachable state at time r from vi). Accordingly, the state of hybrid system can be changed in two ways [23 (i) by a time delay that changes only the value of continuous variables according to the dynamies of the current
location defined in F; and (ii) by discrete and instantaneous transition that changes both location and continuous variables according to the rules in
Definition 2 (Hybrid Automata 9 ). A hybrid automaton is an 8-tuple (L., Var, Inv, G. Ro). where:
L Lis finite set of discrete locations;
Var is aafoafii finite set of real-valued variables with state space Ve S I
Inv L- 2%. a function assigning each location an invariant condition;
F : + (Ve- -e) is a fanction associating each location to a continuous dynamics
À = fí(v);
T - L L is a set of transitions between locations;
G 2% is a function assigning each transition (4, 12) T a guard condition G(4,
Inv(h;;
R 2V. is a function assigning each transition (1,12) E T a reset R(41,22) S Inv(l2):
to S Lx Ve is an initial state set.
Definition 3 (Path of Hybrid Automaton (23)) Let H = (L, Var, F.V.F.T,GRRI. be a hybrid automata. A path of H is a finite or infinite sequence of location and state value pairs, starting from an initial pair (lo, vo) To. i.e. Vo)) to
(11,1)) ", (12, 12) fn
" (13, v3) _ such that:
fi
fn
fn
1. VO S 1 R, 9, (V,, E Inv(I) 2. (41) T A P4, (vi, E G(1,4+) VoI E R(1
Theorem 1 (Modeling DRL Systems as Hybrid Automata). A DRL system with environment
dynamics f, decision network n, time step size 6, and initial state set So, state space S, can be equivalently modeled as the following hybrid automaton:
Var: state variable s, action a, and clock variable
t
Iy: 100. (s So. 0,1,
L: Mol
Inv: Inv(l)) = (s E S, fc G: G(lo lo) = (t. =
5)
F: F(l)) = 15 f(s, a). à 0,
(0)
R: R(o, lo) it. 0. a a(s))
Proof. We first analyze the path of the modeled hybrid automaton H. For an arbitrary initial state (lo, [5p. O, 51), so E So. since 6, the only transition with guard condition (r, = 5) will be triggered and transition to (lo- [So. ao. 0}) where ag (s))). Then (lo, [50, ag 0J) will move to its time successor (o [S1, da. 6)) where $ so + I f(s,an)dt. Next, the transition with guard condition (le = 6) will be made and conduct the reset operation f. 0, s(Si) in R to obtain the transition successor (lo [s1, aj 0l) in which a = (ss). Repeating the evolution to the time successor and the transition successor yields the following sequence:
0 (lo. Su. 0, ? (lo- [Su. ao, 01) - (lo. [s], a1 0I)
5 - (lo, [S2, a2, 01) -
According to Definition there exists the same transition relation 5/+1 = s + L f(s, d))r with a, x(s;) in D and the modeled hybrid automaton H at each time point i6. Thus, given an arbitrary initial state So, the value of state variable and action of D and remain the same at each 6. Then with the same state-action pair and dynamics ff at each D and H also have the same state-action value during each time interval [18, (i + 1)6).
Figure depicts the hybrid automaton defined in Theorem There exists only one location 4o- The invariants in Inv claim that any state belongs to the state space S and the clock variable f, is less than or equal to the time step size 8. The flow in F defines the dynamics f of the system. The only transition is triggered when f, 8, updating the action and resetting & defined in R. The continuous change happens during the time interval [16, (i + 1)6]. with i e N, and the discrete change of actions occurs each 8.
Unfortunately, the hybrid automaton of DRL system cannot verified by using existing hybrid automata model checkers such Flow* (24). Ariadne [25), and CORA (26). The reason is that
3

---

the action a in R depends on the uninterpretable DNN π by a := T(s), and = f(s, a) can not be expressed in a known closed-form, which however is required by regular hybrid automata supported by these tools [27] Hence, almost all reachability- verification methods for systems such as Polar [0], Sherlock 77. and ReachNN (28] inevitably over-approximate I using a Taylor model,
at the cost of large overestimation and time overhead.
3 Frece-Wise Linear Control Policies
To bypass the crux of over-approximating DNNs, we devise a novel, alternative neural network model which essentially realizes a set of linear control policies. Our approach bases on the common assump- tion that there exists near-optimal linear control policy for every Our objec- tive is then to discretize the state space S of DRL system and to train a linear control policy for each discretized region. Specifically, given an n-dimensional DRL system with m m-dimennsoonl control input, we train a DNN which implements a linear control function aj = b' b' xi + x2. +c,x,, i for each control dimension S j S m and each discretized region.
G
8
R
x(s)
0
small region of the entire state space 22
30 21 31.
Inv EES
(G.a)
b. s
à
Figure 1: Hybrid automaton for a DRL system.
3.1 Abstracting State Space via Abstract Interpretation
Abstract Interpretation is an effective technique for scaling up formal verification of complex systems or programs by reducing the system space while preserving the soundness of verification results. For instance, an infinite state space [-2. 0] x [0. 2] can be abstracted be an abstract state represented as (-2, 2),, when all the states in [-2, 0] x [O, 2] share a same property. In general, given system state space S, we denote S. as a finite set of abstract states (each abstract state represents possibly infinite set of actual system states in S). Let Φ S + So be an abstraction function that maps each actual state s in S to the corresponding abstract state in S d.. and Φ-1 S - 2 be the inverse concretization function such that &f (x,)) = [s|s E S, (ss) spl.
For state space abstraction, choose the very primitive but effective abstraction approach which abstracts actual system states as intervals. is known as interval abstract domain and has been well studied for system [3]] and program verification [34] and even the approximation of neural networks [35]. Specifically, let L and U; be the lower and upper bounds for the i-th dimension value of S. We first define the abstraction granularity as an n-dimensional vector y (d,, d2............... dz). Then the i-th dimension will be divided evenly into (U, - Ld)dd, intervals which means each abstract state can be represented
2n-dimensional vector (41, (I,,u)...., las un).
Definition (Interval- Based Abstraction Function). Given an n-dimensional continuous state space S and an abstract state space So which discretizes S based on abstraction granularity y, $ S - S called an interval-bat based abstraction function such that, for every actual state s (X),..., Xxp) E and abstract state S = (/1, (i.uu.....lp Un) E S g. we have d(s) S6 if and only if 1 S xi < H, holds for each dimension 1 S is n.
Example 1 (Running Example). Consider a 2-dimensional system in 36 with state space [-2, 2) x (-),2). The dynamics f is defined by following ordinary differential equations (ODE) i.e., x1 x2 x and x/2 = a. The sign means the control action. The objective is to train DNN for determining action based on x2) so that the agent can move from the initial region xi [0.77 0.91 and X2 E [0.7, 0.9] to the goal region x1 E 1-0.3, 0.1] and X2 E [-0.35, 0.05] as soon as possible.
Suppose that the abstraction granularity is (2, 2). The continuous state space [-2, 2) x (- then partitioned into four regions, corresponding to four abstract states represented by S, [(-2, -2.00,22,,,, 0), (-2.000. (0, -2 0), (0. 2, 0, 2)), respectively.
3.2 Piece-Wiss Linear Decision Neural Networks
We devise an alternative DNN model called piece-wise linear decision neural networks (PLDNNs). Unlike conventional DNNs, PLDNN contains an abstraction layer between the input layer and the first hidden layer. The abstraction layer is used to convert an actual system state into its corresponding abstract state. Then the output of a PI.DNN is the control action that is the dot product result of state variables of the actual state and the linear coefficients determined by the corresponding abstract state.

---

Algorithm 1: The Training Procedure based on the DDPG algorithm
Input:
State space S, abstraction granularity y. Output: A PLDNN // obtain abstraction function, Sec3.1
& < discretize S according to y;
3 Initialize actor network π as a PLDNN by encoding & into the coefficient network ne: // Sec3.2
Initialize critic network Q, target networks n' + Q' Q:
DDPG(T, Q, !))
// train π based on DDPG algori thm
return π
Figure 2 exemplifies the architecture of the PLDNN π for a two-dimensional DRL system. The decision-making of is based coefficient network n that outputs the linear coefficients. The sec- ond layer of is the inserted abstraction layer which consists of the blue neurons and the red neurons. The output layer of π. contains that output the + linear coefficients depicted for the weights setting
neurons
Abstraction Layer
as purple neurons. between the input layer and the abstraction layer, the weights of the connections between the i-th neuron in the input layer and the (2i 1)-th and 2i-th neurons the abstraction layer are set to I which are represented by blue lines and red lines, respectively. While the weights of other connections denoted by the black dashed lines are set to O. Under this setting of weights, the inputs both (2i 1)-th and 2i-th neurons in the abstraction layer are x, Moreover, the activation function of the (2i 1)-th neuron in the abstraction layer is set to du with the responsibility of computing the upper bound u; and that of the 2i-th neuron set to di for calculating the lower bound 4. Specifically, for a continuous state space partitioned by the abstraction granularity y (d)....,d,, the activation functions for the (2i 1)-th and 2i-th neurons in the abstraction layer can be formulated follows:
(T.(()
w=0
= x x2) X2) (1, x2)
Figure 2: The arch. of the PLDNN for Example
(x; Li) jd
(xi L)) Jd + di
81(x)) L, +
(x((x) = L, +
di
d:
With the above activation functions, the abstraction layer can output the same abstract state Sp. (1,44....44 Mn) for E (sp). The abstract state Sy is then propagated to the fully connected layers of n, to generate the linear control coefficients (b, c2) denoted by (s).)).
To obtain the final output of action a, an additional dot product operation between x, (s) and [1, ss] is performed with the result of the operation as the control action where [s-]] is the concatenation operation. For multiple dimensional control action a (a,.-.. -.m)). we only need modify the output dimension of n. to m(n 1), such that each и 1 neurons output the linear coefficients of one dimension of More specifically, we can obtain aj as follows:
aj A(s) n (s) -) 1): (n 1) [1. s], S js i m.
where vector[star start end) denotes the slicing operation that extracts the elements of vertor from index start up to but not including index end.
With the additional abstraction layer that output an identical vector into the fully connected layers of ne for Vs E & (sg),, we can ensure that n, always produces the same coefficients for all actual states located in the same abstract state. Consequently, we can extract a piecewise linear decision function with this structure of π on each abstract state.
3.3 The Training Procedure
Training a PLDNN can be achieved by extending existing deterministic policy gradient algorithms such as Deep Deterministic Policy Gradient (DDPG) (37] and Twin Delayed Deep Deterministic Policy Gradient (38] since the modifications made stay inside neural networks and are invisible to the DRL algorithms. The pseudo code of the training procedure is given in Algorithm [] where we take the DDPG algorithm an example. The training procedure starts with defining the abstraction
5

---

function & according to y (Line 2), initializing PLDNN with an abstraction layer based on & (Line 3), and, following [37], initializing the critic network and the two target networks (Line 4). The procedure then invokes the DDPG algorithm with the networks as arguments (Line 5) since the PLDDN has the same input and output as the actor network implemented by DNN. During this procedure, we freeze the parameters between the input and the abstraction layers of æ. The parameters in the fully connected layers are trained based on backpropagation [39] and gradient descent optimization [40].
4 Equivalent Policy Extraction and Verification
After training, we can extract [S LCUs based on the learned coefficients of linear control policies for the abstract states in g.- Specifically, we choose an arbitrary actual state 8 E d (s,) for each abstract state Sa and feed it to a PLDNN to obtain the coefficients defined on the abstract state. For instance, we can feed -1) to the PLDNN Example [ and obtain the coefficients (-0.16610557, - -1.7437580, - 1.82278774 of the linear control policy for the region [-2. 0) [[= [-2, 0). FiowreJJshows shows the LCUs extracted from a trained PLDNN in Example[] They are depicted by planes with different colors in Figure These four planes denote the following linear control functions:
TTI, x2) -0. 16610677 1.7437580.r 1.8227874x2,
(-2,0),
x2 e (-2,0) (LCU))
π(x, x2) -.224400033 18806037xx 1.8679885x2,
xi E [-2,
x2 e
(LCU,)
x(),,)) x2) -0.27547930 1.8884722X1 1.9342268x2.
E [0,
x2 e (-2.0) (LCU3)
T(51 -0.29549897 011-9999711.02238665 1.9022338.r -.942333111194444463363
1.9436346x2,
xi E [0, 2),
X2 E (0,
(LCU,)
The underlying X1 X X2 plane in Figure is the projection of the four LCUs. Under the control of these four LCUs, the agent can reach the goal region (orange box). The two sequences of purple boxes represent the range reachable states from corresponding initial regions to the goal region.
With exacted LCUs from a PLDNN, we can build a verifiable hybrid automaton for the system by substi- tuting equivalently the neural networks using corre- sponding LCUs. Theorem formulates the hybrid automaton after a decision network is substituted by LCUs. The differences from Theorem [ include the definitions of transitions T, guard condition G and reset formula R. For the PLDNN controlled sys- tems, We use [S al transitions each of which contains a guard condition and reset formula to update the action (s) [1, s] at each 6. Notice that, (T,(s) is a determined vector since Vx E & (s,),, the outputs of n. are the same according to the dedicated struc- ture of ne- Thus, the reset formula for is simplified to an affine mapping.
T T221,
2
5
0
32
-1
-2
Figure 3: The LCUs extracted from a trained PLDNN for Example
Theorem 2. Given a DRL system with environment dynamics f. PLDNN æ, time step size ö and initial state set So. it can be equivalently modeled as hybrid automaton defined as follows:
Var: state variable s, action a, clock variable l.
In: (loo So, 0,4, =)) 6))
L: (la)
Inv: Inv(lo) = [s E 5, s 5)
F:: F(h) (8 =
T: (0o, (la,44)) 1o)) where [7] = pl
G: G(T()) (1. ö, o (5,)(s))) where 0 i < E
R(T(i)) = (t. = 0, (s) [1. s]} where 0 < i (TA
Proof. We prove that the path of hybrid automaton H, in Theorem iis the same the corresponding hybrid automaton H2 in Theorem for an arbitrary initial state (lo, [so. 0, The path H2 can be described by the following sequence:
8 + (lo, [s).a), OD) o - (lo. [82, az 0D) 3 (lo. [so. 0. - (lo. [So. do 01)
0
where Si+1 = 8; + 1 fs, di and a; (s)) s:]. With the dedicated structure of PLDNN π, we have z(5) (s) - s]. Thus, at each 6, the discrete transitions of H₁ and H2 change both location

---

and continuous variables in the same way. We can conclude that the paths of H1 and H2 are exactly the same. By Theorem T it is obvious that D, H1 and H₂ produce the same state-action value for the same initial state.
According to Theorem 2 we can build a hybrid automaton that is equivalent to the DRL system in Example] Assuming the trained system has four linear control units as shown in Formulas (LCU1 LCU4 and = 0.2, we construct the corresponding hybrid automaton as depicted Figure The Tour transitions in the automaton correspond to the four LCUs, respectively. The guard of each transition represents the condition of triggering the corresponding policy.
Thanks to the linearity of control policies in R, a hybrid automaton built for a PLDNN- controlled system can be efficiently veri- fied by state-of-the- tools. For instance,
G
COR 10.2]
R
Xi é [-2,2] E [-2.2]
a == L=
a LCU
f 0
... U...S.
Flow* (24] is representative tool for the reachability analysis of hybrid systems. this paper we are focused on the verifica- tion of both goal-reach and reach-avoid properties. The former means that given a set of initial states, a system must even- tually reach the goal region from any ini- tial state. The latter means that the system never enters unsafe regions within a spe- cific time horizon. Both properties can be verified via reachability analysis.
4 0.2
G3 f = 002
[-2.0]
lo. X2
xi E [0.2]
xx 1-2.0
Rsia LCU,
E [-2.0]
Raja : LCU.
J2
G, Te 02, n (0. x [0.2]
Figure 4: The hybrid automaton of the DRL system with the trained piece-wise lincar controllers in Figure 3
5 Experimental Evaluations
We prototype our approach into tool called LiNCos, with DDPG as the backend DRL algorithm and Flow* as the verification engine. We extensively assess it, along with the state-of-the-art tools. Our goal is to show, for the PLDNN-based training. (i) the reduction in the number of partitions with comparable cumulative rewards, robustness, and time overhead with respect to conventional DNN- based training: (ii) its high verification performance including the tightness of over-approximation sets and the efficiency of verification; and (iii) its scalability for large-sized neural networks and systems with complex dynamics and high- nigh-dimessionll state space.
Experimental Setup. All experiments were conducted on a workstation equipped with a 32-core AMD Ryzen Threadripper CPU @ 3.6GHz and 256GB RAM, running Ubuntu 22.04.
Benchmarks. We choose eight benchmarks, including six regular benchmarks from Verisig 2.0 [9] (B1-B5 and Tora) and two complex benchmarks (CartPole with extreme complex dynamics from OpenAl Gym 41 and quadrotor (QUAD) with 12-dimensional state space and 3-dimensional action space from [10). For fair comparisons, we use the same training configuration and guarantee that all trained systems reach the specified reward threshold. See Appendix I for the detailed setting. For B1-B5 and Tora the environment dynamics are the same with [9]. The dynamics of QUAD are the same with 10. We omit their detailed definition here. However, the dynamics of CartPole are originally represented as a discrete-time model in [41 by difference equations. In our experiment, we consider its dynamics as a continuous-ting model and formalize with the following ODEs:
xi =x2, X4,
x (a (1 0000:/000000ttt00ooo00000000001) olt
(0.5(4.0/3.0 - - (
X =9.8sin(xg) - owt.://wwwo..oooo///o///////////
5.1 Performance Evaluation
We assess the performance of PLDNN, together with the conventional DNNs, in terms of cumulative reward, robustness, and training time under the same training configuration. We also measure the number of abstracted states required for training linear control policies and constant policies (2T]. Due to space limitations, present the experimental results only for B1, B2, and two complex cases
7

---

B1
B2
CartPole
QUAD
1000
Performance
Reward
500
-100
0
DNN PLONN
DNN PLONN
DNN
DNN PLONN
-50
-200
100
200
300
100
200 Episode
300
0
1000
2000
3000
1000 Episode
2000
Episode
Episode
60
90
900
1006
Robustness
Reward
80
800
DNN PLDNN
70
DNN PLDNN
DNN
DNN PLDNN
700
PLONN
50
100
25
75
100
25
50
100
50
100
Nolse (0.0004)
Noise (0.0002)
Noise (0.000 (0.0001)
Noise (0. (0.0005)
Figure 5: Performance and robustness comparison between PLDNNS and DNNs. The number in the parentheses is the base of O, e.g., when the abscissa is 50 in B1, we have o = 50 x 0.0004 0.02.
(i.e., CartPole and QUAD). The associated conclusions (from Table | and Figure 55 also apply to the other four cases, see Appendix A.2 for the detailed experimental results.
Cumulative Reward. Figure 3 plots the
Table 1: Training time and number of partitions
system cumulative reward (the average of five trials) during the training process. The solid lines and shadows refer the aver- age reward and 95% confidence interval, respectively. Apparently, the trends of ac- cumulative rewards by PLDNNs and DNNs comparable. Despite slightly more time required for training with PLDNN due its additional conversion from actual state to abstract state (see Table "Training Time"), we can, however, obtain significant advance in the efficiency and tightness of verification (see Section 5.2).
Task
B1
B2
CartPole
QUAD
Training Time
PLDNN
14.3
7.9
428.2
871.1
DNN
11.0
6.6
403.6
781.5
LCU
1
4
16
#partitions
Const.
4
100
25
4
Robustness. We also evaluate the robustness of PLDNNs as training the linear controller on each partition may lead to discontinuity of control decisions in the boundaries of partitions. For current state = (xI....,,, we add a Gaussian noise XI...,, to s and obtain a perturbed state s' = (x) XI..... X, + X,,) for caleulating the control action, where X, N(H, of) with 1 I i and μı; O. For each benchmark, we train 10 different policies and evaluate their robustness under 100 different perturbation levels to obtain the average and 95% confidence interval of the cumulative reward. Figure depicts the reward trend with the increasing perturbation level. As or increases, the decline ratio of the system with PLDNNs is comparable that with DNNs, which implies that both achieve similar robustness.
Reduction in the Number of Partitions. We measure the effect of reducing the number of partitions by utilizing a linear policy, instead of the constant action on each partition, which adopted by the work (2I) In both cases, start training from coarse grainedd abstraction granularity (with only one partition) and gradually increase the number of partitions until the preset reward threshold can be reached by the trained PLDNN. As shown in Table T linear policies significantly reduce the number of partitions required for reaching the reward threshold, which benefits both the verification efficiency and accuracy will see in the next section.
5.2 Verification Efficiency and Tightness
We evaluate the verification efficiency and tightness for the PLDNN-based and DaNed DRL systems, respectively. Regarding tightness, we choose two state-of-the-ard tools, i.c., Polar [10] and Verisig 2.0 [9] for the reachability analysis of DNN-controlled systems. We do not consider ReachNN* which both Polar and Verisig 2.0 have been demonstrated to outperform efficiency, we employ Flow to perform reachability analysis, which is used by both Polar and Verisig 2.0 the backend reachability analysis tool.
99] [T]. For
the comparison results for the verification efficiency. For each regular case, we choose four different network configurations: two smaller networks (e.g., Tanhzxa)) from I0] and two larger networks (e.g., To)h)y)oo) Our approach LINCoN can handle all 26 instances including the two complex instances, while Polar succeeds only in 20 cases. Verisig 2.0 is not applicable to
Efficiency. Table
8

---

Table 2: Verification results and time in seconds.
LiNCo
Polar
Verisig 2.0
Task
Dim
Network
Core
V.R.
Core
Impr.
Core
Impr.
Cores
Impr.
Tanh
2.31
17
7.4x
45
19.5x
38
16.5x
Tanhsvao
54.8x
413
53.9x
B1
ReLU2x20
2.11
1.4x
ReLUs
2.59
x
Tanhaza
0.57
8.8x
5
8.8x
7.0x
x
Tinhawino
0.56
B2
Kel.Us,20
4.7X
ReLUs
0.60
Tanhg-20
2.69
18
6.7%
36
13.4x
28
10,4x
Tanhszuo
3.57
91
25.5%
357
100.0x
88
24.6x
B3
ReLUss0
3.05
2.0%
x
ReLUsx100
2.92
14
4.8x
Tanbixau
1.44
3.5x
4.9X
3,5x
Tanhssine
1.45
27
18.6x
114
78.6x
31
21.4x
B4
ReLU2.20
1.4X
x
Rel.Uxxt
1.43
3.5x
Tanh
3.24
38
11.7%
157
48.5x
44
13,4x
Tunheeano
3.29
157
47.7x
1443
438.6x
191
58.1x
BS
ReloUsxtoo
2.1X
ReLU
3.29
49
14.9x
Tanh
1.57
45
28.7x
69
43.9x
46
29.3x
Tora
Tanhezino
1.75
X
ReLUneu
30
19.0x
x
ReLUasio
1.62
53
32.7x
CariPole
Tanhsas4
151
X
x
QUAD
Tanhsa64
1054
Remarks. Impr. time speedup of LiNCON compared Verisig or Polar (Verisig Polar/LaNCows
Tanh/ReL. DNN with the activation function Tanh/ReLU, hidden layers, and & neurons per hidden layer. VR: verification result. V: the reachability problem is successfully verified. xtyPe the reachability problem cannot be verified due to type: (a) large over-approximation error, (b) the calculation did not finish, (c) not applicable. -: no data available due x or X
ReLU networks (marked by x²) and succeeds only in 9 instances. Overall, LINCON outperforms both Polar (up to 47.7x speedup) and Verisig 2.0 (up to 438.6x speedup). In particular, LINCON achieves even up to 58. 1x speedup compared to Verisig 2.0 accelerated by 20-core parallelization. For our approach LINCON, the only time overhead for encoding networks stems from extracting LCUs from PLDNNs, which is polynomial and negligible (less than 0.05s). Consequently, LINCON scale up to large-sized neural networks.
Tightness. We compare the tightness of the over-approximation sets computed by different ap- proaches. Tigure/ the experimental results, along with the corresponding simulation trajecto- rics. For B2 and Tora, LINCON has significant tightness improvement over Polar: the range of the over-approximation sets (red boxes) calculated by Polar far outreaches the range of the reachable states obtained from the simulation. Verisig 2.0 terminates prematurely in Tora since the range of the action reaches 107 during the calculation which is too large to proceed. We defer to Appendix A.. the experimental results for the remaining four cases where all three tools obtain similar tightness results.
Discussion on CartPole and QUAD. We discuss the verification results of the two complex cases, namely CartPole and QUAD. Both Polar and Verisig 2.0 fail to verify them. As shown in Figure 6 Polar and Verisig 2.0 abort after 20 steps due to the huge over-approximation error in CartPole. In contrast, such complex policy trained with our approach can be efficiently and tightly verified. In particular, the trajectories diverge first and finally merge. The computed reachable states tightly over-approximate these trajectories, and the computation takes only 151 seconds. Regarding the 12-dimensional QUAD case, Polar and Verisig 2.0 time out (two hours) after only two steps, while LinCoN produces a very tight set reachable states 1054 seconds even after 15 steps, which is 7 times deeper than Polar. To the best of our knowledge, this is the first time that QUAD can be formally verified more than ten steps under various decision networks. Note that the trained policies used in the comparison differ due different decision networks, and thus agents may follow different paths to the goal region (see the simulated trajectories in Figure (). Hence, for a fair comparison, draw the same conclusion from Figure 6 The evaluations, from which results are given in Appendix A.3
conduct

---

B2
Tora
CartPole
QUAD
1.0
LINCON
0.02
0.5
0.5
X
0.0
X
0.0
0.00
2
0.0
-0.02
-1.0
0.2
-0.5
0.0
0..
1.0
-1.0
-0.5
0.0
0.5
1.0
10
20
40
40
50
0
10
15
X1
X1
Time
stop
Time stop
1.0
1.0
Polar
0.00
0.0
8.0.02
2
0.6
-0.5
-0.04
0.4
1.0
40
15
Time step
Time
1.0
1.0
Verisig 2.0
0.8
-.0.02
0.0
-0.04
0.4
0055
-0.06
0.2
step
step
Figure 6: Tightness comparison with respect the DRL systems with larger decision networks (red
box: over-approximation sets; green lines: simulation trajectories; blue box: goal region).
Related Work
Policy Synthesis. Several works adopt programmatic policies (e.g., decision trees and program controllers) which are more interpretable and amenable to formal verification than neural policies. Bastani al. [15] construct decision
represent DNN policy based imitation learning [42). 43 follow a similar routine, distilling neural network policies into predefined
Verma et al.
program templates. Trivedi al. 45 use two-stage learning scheme synthesize programmatic policies. Some efforts are dedicated to exploring the combination of training and verification. Zhu et al. [30] propose an inductive framework for synthesizing deterministic policy program from neural policies. Wang et al. 31 learn programmatic controllers based on verification feedback to avoid safety violations. Our proposed PLDNN is essentially DNN-based implementation of programmatic controllers, which could be integrated with these verification- guided synthesis approaches.
Reachability Analysis. Our work is also built atop the approaches for reachability analysis of neural- network-controlled systems. NNV [46] utilizes star set [47 to perform range analysis of decision zonotope propagation
cover the output of decision network. Verisig 49 9 models a decision network with differentiable activation functions (e.g.. Tanh) as hybrid system and analyzes its reachability for over-approximatin the network. ReachNN [28] g) abstracts the input-output mapping of decision network with a Bernstein polynomial, together with an error bound on the approximation. Sherlock [7] focuses ReLU-based networks and computes tight Taylor models via rule generation. Polar [10] integrates the Taylor and Bernstein approximation techniques for building Taylor model which over-approximmtes decision networks. All these efforts over-approximate the embedded DNNs, which limit their scalability and verification accuracy.
networks. JuliaReach [48]
7 Conclusion and Future Work
We have presented PLDNN that seamlessly integrates DNN and programmatic controls via state abstraction for boosting the reachability analysis of DRL systems. Unlike traditional train-then- transform approaches, PLDNN accompanies novel inverse training and verification method, in which a DNN first transformed into an equivalent set linear control policies and then trained to optimize them. Experimental results have shown that PLDNN-controlled systems can be more efficiently and tightly verified than DNN-based systems, with up to 438 times speedup and times deeper computation steps for 12-dimensions control task.
Our work sheds light on a promising direction towards developing dependable DRL systems: learning casy-to-verify and high-perffrmance control policies via DRL and abstraction techniques. Given the encouraging results of linear control policies, our work would also stimulate passion for substituting them with, e.g., polynomial control policies, for training and verifying more complex DRL systems.
10

---

Acknowledgment
We thank all the anonymous reviewers for their valuable feedback on this work. The work has been supported by the National Key Research Program (2020AAA0107800), NSFC-ISF Joint Program (62161 14600,,,42//21,, Huawei Technologies Co., Ltd., the Shanghai International Joint Lab of Trustworthy Intelligent Software (Grant No. 22510750100), the Shanghai Trusted Industry Internet Software Collaborative Innovation Center, the Engineering and Physical Sciences Research Council (EP/T00657//I), the National Research Foundation (NRF-RSS2022-009) Singapore, and the Shanghai Jiao Tong University Postdoc Scholarship.
References
[1] Z. Zhang and K. P. Lam, "Practical implementation and evaluation of deep reinforcement learning control for radiant heating system," in Proceedings of the 5th Conference Systems for Built Environments, 2018, pp. 148-157.
[2] Y. Pan, C.-A. Cheng. K. Saigol, K. Lee, X. Yan, E. Theodorou, and B. Boots, "Agile autonomous driving using end-to-end deep imitation learning," " in Roboties: science and systems, 2018.
[3] X. Qi, Y. Luo, G. Wu, K. Boriboonsomsin, and M. Barth, "Deep reinforcement learning enabled self- learning control for energy efficient driving," " Transportation Research Part C: Emerging Technologies, vol. 99. pp. 67-81, 2019.
[4] B. R. Kiran, I. Sobh, V. Talpacrt, P. Mannion, A. A. Al Sallab, Yogamani, and P. Pérez, "Deep reinforcement learning for autonomous driving: A survey," JEEE Transactions on Intelligent Transportation Systems, vol. 23, 6. pp. 4909 -9266 2021.
[5] E.-.. Fan, J. Xiong, M. Li, and G. Wang, "On interpretahility of artificial neural networks: A survey," IEEE Transactions Radiation and Plasma Medical Sciences, vol. 5, no. 6. pp. 741-760, 2021.
[6] R. V. Yampolskiy. "Unexplainability and incomprchensibility of A1," Journal of Artificial Intelligence and Consciousness, vol. no. 02, pp. 277-291, 2020.
S. Dutta, X. Chen, and S. Sankaranarayanan, "Reachability analysis for neural feedhack systems using regressive polynomial rule inference," in ACM International Conference on Hybrid Systems: Computation and Control (HSCC'19) 2019. pp. 157-168.
[8] J. Fan, C. Huang, X. Chen, W. Li, and Q Zhu, "Reachnn": A tool for reachability analysis of neural- network controlled systems." in International Symposium on Automated Technology for Verification and Analysis.
Springer, 2020, pp. 537-542.
[9] R. Ivanov. T. Carpenter. J. Weimer, R. Alur, G. Pappas, and I. Lee. "Verisig 2.0: network controllers using taylor model preconditioning." in International Conference on Computer Aided Verification (CAV'2I). Springer, 2021, pp. 249-262.
Verification of neural
[10] C. Huang, Fan, X. Chen, W. Li, and Q Zhu, "Polar: A polynomial arithmetic framework for verifying neural-network controlled systems," in The 20th International Symposium on Automated Technology for Verification and Analysis (ATVA '22). Springer, 2022, pp. 414-430.
[11] K. Makino and M. Berz, "Taylor models and other validated functional inclusion methods," International Journal of Pure and Applied Mathematics, vol. 6, pp. 239-316, 2003.
[12] W. Ruan, X. Huang, and M. Kwiatkowska, "Reachability analysis of deep neural networks with provable guarantees," in Proceedings of the 27th International Joint Conference on Artificial Intelligence, 2018, pp. 2651-2659.
[13] S. Dutta, S. Jha. S. Sankaranarayanan, and A. Tiwari, "Output range analysis for deep feedforward neural networks," in 10th International Symposium on NASA Formal Methods (NFM'18) 18). Springer, 2018, pp. 121 133.
[14] L. M. Schmidt, G. Kontes, A. Plinge, and C. Mutschler, "Can you trust your autonomous car? interpretable and verifiably safe reinforcement learning," in 2021 IEEE Intelligent Vehicles Symposium (IV). IEEE, 2021, pp. 171-178.
[15] O. Bastani. Y. Pu, and A. LelamaL "Veritiable reinforcement learning via policy extraction." Advances in Neural Information Processing Systems (NeurIPS' 18), vol. 31, 2018
11

---

[16] C. Buciluu, R. Caruana, and A. Niculescu-Mizil, "Model compression." in Proceedings of the 12th ACM SIGKDD international conference on Knowledge discovery and data mining (KDD (0)))0))...0)) 2006, pp. 535-541.
[17] G. Hinton, O. Vinyals, and J. Dean, "Distilling the knowledge in neural network," arXiv preprint 10X3v:1503.025555 2015.
[18] T. Brázdil, K. Chatterjee. M. Chmelik, V. Forejt, J. Křetínský, M. Kwiatkowska, D. Parker, and M. Ujma, "Verification of markov decision processes using learning algorithms." " in 12th International Symposiun on Automated Technology for Verification and Analysis (A7VA (4)). Springer, 2014, pp. 1811
[19] D. Abel, D. E. Hershkowitz. and M. L. Littman. "Near optimal behavior via approximate state abstraction." in International Conference on Machine Learning (ICML' 16), vol. 48, 2016, pp. 2915-2923.
[20] D. Abel, "A theory of state abstraction for reinforcement learning," in AAAI Conference Artificial Intelligence (AAAI' 19), vol. 33, no. 01, 2019, pp. 9876-9877.
[21] P. Jin, J. Tian, D. Zhi, X. Wen, and M. Zhang, "Trainify: A CEGAR-driven training and verification frame- work for safe deep reinforcement learning," " International Conference on Computer Aided Verification (2) Springer, 2022, pp. 193-218.
[22] Tian, Zhi, S. Liu, P. Wang. G. Katz, and Zhang, "Taming reachability analysis dnn-controlled systems via iestractiionbassl training," in 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'23). Springer, 2023.
[23] R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.H.. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The algorithmic analysis of hybrid systems." Theoretical Computer Science, vol. 138, no. 1, pp. 3-34, 1995.
[24] X. Chen, E. Ábrahám, and S. Sankaranarayanan, "Flow*: An analyzer for non-linear hybrid systems." in 25th International Conference on Computer Aided Verification (CVV13). Springer, 2013, pp. 258-263.
[25] P. Collins, D. Bresolin, L. Geretti, and T. Villa, "Computing the evolution of hybrid systems using rigorous function calculus," " IFAC Proceedings Volumes, vol. 45, no. 9, pp. 284-290,, 2012.
[26] M. Althoff, "An introduction to cora 2015." ARCH@ CPSWeek, vol. 34, pp. 120-151, 2015.
[27] X. Chen. "Reachability analysis of non-linear hybrid systems using taylor models," Ph.D. dissertation. Fachgruppe Informatik, RWTH Aachen University. 2015.
[28] C. Huang, J. Fan, W. Li, X. Chen, and Q. Zhu, "Reachnn: Reachability analysis of neural-network controlled systems," ACM Transactions on Embedded Computing Systems, vol. 18, Ss, pp. 1-22, 2019.
[29] M. Grzeš and D. Kudenko, "Multigrid reinforcement learning with reward shaping," in 18th International Conference Artificial Neural Networks (ICANN'08). Springer, 2008. pp. 357-366.
[30] H. Zhu, 7. Xiong, S. Magill, and S. Jagannathan, "An inductive synthesis framework for verifialle reinforcement learning," in Proceedings of the 40th ACM SIGPLAN conference Programming Language Design and Implementation (PLDI'19), 2019, pp. 686-701.
[31] Y. Wang and H. Zhu, "Verification-guidee programmatic controller synthesis," in 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (3)) Springer, 2023, pp. 229 250.
[32] P. Cousot and Cousot, "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints." in Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of progranming languages (POPL'77), 1977,
[33] M. Afzal, A. Asia. A. Chauhan, B. Chimdyalwar, P. Darke, A. Datar, S. Kumar, and R. Venkatesh, "Veriabs: Verification by abstraction and test generation." in The 34th IEEEAAM International Conference on Automated Software Engineering (ASE*19). IREE, 2019, pp. 1138-1141.
[34] K. Heo, H. Oh, and H. Yang, "Resource aware program analysis via online abstraction coarsening." in 2019 IEEEJACM 41st International Conference on Software Engincering (ICSE' 19). IEEE, 2019, pp. 94-104.
[35] Z. Wang, A. Albarghouthi, G. Prakriya, and S. Jha, "Interval universal approximation for neural networks," Proceedings of the ACM on Programming Languages (POPL), vol. no. POPL, pp. 1-29, 2022.
[36] E. Gallestey and P. Hokayem, 'Lecture notes in nonlinear systems and control," 2019.
12

---

[37] T. P. Lillicrap. J. J. Hunt, A. Pritzel et al., "Continuous control with deep reinforcement learning," in International Conference Learning Representations (ICLR' 16). OpenReview.nee 2016.
[38] S. Fujimoto, H. Hoof, and D. Meger, "Addressing function approximation error in actor-critic methods," in International Conference Machine Learning (ICML'18) PMLR, 2018. pp. 1587-1596.
[39] D. E. Rumelhart, R. Durbin, R. Golden, and Y. Chauvin, "Backpropagation: The basic theory," Backpropa- gation: Theory, architectures and applications, pp. 1-34, 1995.
[40] S.-i. Amari, "Backproaagttion and stochastic gradient descent method," Neurocomputting, vol. 5, no. 4-5,
pp. 185-196, 1993.
[41] G. Brockman, V. Cheung. L. Pettersson, J. Schneider, J. Schulman, J. Tang, and W. Zaremba, "OpenAI Gym," 2016, #EXiv:1606001544
[42] P. Abbecl and A. Y. Ng. "Apprenticeship learning via inverse reinforcement learning." in Proceedings of the twenty-first International Conference Machine Learning (ICML '04), 2004, p.
[43] A. Verma, V. Murali, R. Singh, P. Kohli, and S. Chaudhuri, "Programmatically interpretable reinforcement learning," in International Conference Machine Learning. PMLR, 2018, pp. 5045-5054.
[44] A. Verma, H. Le, Y. Yuc, and S. Chaudhuri, "Imitation- Advances in Neural Information Processing Systems, vol. 32, 2019.
programmatic reinforcement learning,"
[45] D. Trivedi, J. Zhang, S.-H. Sun, and J. J. Lim, "Learming synthesize programs as interpretable and gencralizable policies," Advances Neural Information Processing Systems (NeurIPS' vol. 34, pp. 25 146-25 163, 2021.
[46] H.-D. Tran, X. Yang, D. Manzanas Lopez, P. Musau, L. V. Nguyen et al., "NNV: the neural network verification tool deep neural networks and learning-enabled cyber-physical systems," in International Conference on Computer Aided Verification (0) Springer, 2020, pp. 3-17.
[47] H.-D. Tran, Bak, W. Xiang, and Johnson, "Verification deep convolutional neural networks using imagestars," in International Conference on Computer Aided Verification (CAV'20). Springer, 2020, pp- 18-22.
[48] C. Schilling, M. Forcts, and S. Guadalupe, "Verification of neural-network control systems by integrating taylor models and zonotopes," in AAAI Conference Artificial Intelligence (AAAI'22), 2022, pp. 8 8169- 8177.
[49] R. Ivanov, T. Carpenter, J. Weimer, R. Alur, G. Pappas, and I. Lee, "Verifying the safety of autonomous systems with neural network controllers." ACM Transactions Embedded Computing Systems, vol. 20. no. pp. 1-26, 2020.
13

---

A
Appendix
A.1 Benchmarks Setting
We first present the goal region and unsafe region of each benchmark Table
As for the training settings, for the 6 regular benchmarks, the target is training a policy to guide the agent reach the goal region. Therefore, region. Once the agent reaches the goal region, it will be awarded positive reward. In CartPole, the target of training to prevent the pole from falling over, namely the pole angle -0.2 & X3 0.2. We modify the original discrete reward function to continuous reward function - to try to balance the pole to stay upright. As for QUAD, aim control the altitude of the quadrotor above 0.6 (X3 2 0.6). Thus we set a continuous reward function -|X;- 0.8) for training a policy that drives the quadrotor to ascend above 0.6.
set negative reward when the agent is not in the goal
Table 3: Benchmarks Setting
Task
Initial Region
Goal Region
Unsafe Region
X1 E
[0.8, 0.9]
Xi [0,0.2]
B1
X2
0.65
X2 [0.05, 0.3]
[0.7,0.9)
[-0.3,
B2
X2
0.97
X2 [-0.35, 0.5]
X1 0.98
X1 (0.2,
B3
X2 E [0.4,0.5]
X2 E -0.05)
Xi [0.25, 0.27]
X1 0..00.55.0005
B4
X2 E [0.08, 0.1]
X2 [-0.05.0]
X3 E [0.25, 0.27]
[0.38, 0.4]
x1 [-0.4, -0.28]
B5
X2 E [0.45, 0.47]
X2 [0.05, 0.22]
X3 6 [0.25, 0.27]
X1 [-011000
x1 [-0.25, 0.10]
Tora
X2 E [-0.9.00.6]
X2 (0.2.0.7)
X2, é [0.02, 0.02]
[26, 29] X3 [-0.2, 0.2]
CartPole
X3 E [0.02, 0.021]
X1. X E [0.35, 0.4] xy.... X12 E [0
QUAD
X 0.6
A.2
Comparison on cumulative reward and robustness
In this section, provide the comparison results cumulative reward and robustness of B3-B5 and Tora in Figure 7 The solid lines and shadows refer to the average reward and 95% confidence interval, respectively. For these four cases, it is obvious that there comparable trends in the cumulative rewards of PLDNNS and DNNs during training and under perturbation. Therefore, we can conclude that using PLDNNs will affect the training efficiency and the robustness of trained systems.
A.3 Comparison on the tightness of over-approximation sets
Tightness results of regular cases. We present the tightness comparison results of B3-B5 in Figure For these four regular cases, both Polar and Verisig 2.0 can produce tight over-approximation for decision networks, thus all three methods achieve similar tightness results and successfully verify the goal-reach properties.
Multiple evaluations on CartPole and QUAD. Since the trained policies used in the comparison differ due to different decision networks, we conduct more evaluations on these two complex cases. For each case, we train three more decision networks with the same configuration and the corresponding results are shown in Figure I0 For CartPole, Polar did not finish the calculation under three different networks as depicted in Figure d-f)... Additionally, on the basis of result of dealing with divergent traces shown in Figure 10 10(d), we can see that Polar is not suitable for dealing with the DNN-controlled systems with divergent traces. As for QUAD, we record the computation results within 12 hours and obtain the results as shown in Figure 10 jl). We can observe that only
14

---

200
1000
400
750
200
500
-200
DNN PLONN
DNN PLONN
200
DNN
250
DNN
PLDNN
PLDNN
100
-200
400
100
Episode
Episode
Episode
Episode
(a) B3
(b) B4
(c) B5
(d) Tora
500
500
1000
175
400
800
300
DNN
300
DNN
DNN
600
DNN
PLDNN
FLONN
PLONN
FLONN
100
Noise
00.00021
Noise (0.0002)
Noise (0.0005)
(c) B3
(f) B4
(g) B5
(h) Tora
Figure 7: Performance (a-d) and robustness comparison (e-h) of the pldnn and DNN under the same settings. The number in the parentheses is the base of or. For example, in B3 when the abscissa is equal 50, 50 0.0005 0.025.
few time steps completed by Polar, while LINCON can accomplish more than 10 steps within about 1000 seconds under multiple evaluations.
0.5
0.
0.03
0.50
0.45
0.0
X
0.81
2 0.30
-0.5
-0.5
-0.5
0.0
0.5
1.0
x1
X1
X1
X1
(a) B1 by LiNCON
(b) B3 by LINCON
(c) B4 by LINCON
(d) B5 by LINCON
0.5
0.08
0.3
X 0.0
N 0.30
0.00
035
-0.5
-0.04
0.00
-0.5
1.0
0.8
1.0
-0.15
0.00
-02
0.0
(c) B1 by Polar
(f) B3 by Polar
(g) B4 by Polar
(h) B5 by Polar
0.3
X 0.0
0.04
00
0.00
-0.04
-0.
0.2
2.4
2.5
9.8
1.0
-0.15
0.00
0.35
0.30
-24
-0.2
0.0
0.2
(i Verisig 2.0
B3 by Verisig 2.0
(k) B4 by Verisig 2.0
B5 Verisig 2.0
Figure 8: Tightness comparison on the DRL systems with larger decision networks (red box: over- approximation sets; green lines: simulation trajectories; blue box: goal region.)
A.4 Evaluation on Verisig 2.0 with Big Weights
Verisig 2.0 produces large over-approximation error when dealing with neural networks with big weights. To demonstrate this, initialize the weights of the neural network with larger values (random numbers
NNu, o²) with μ 0, 0.1) and show the experimental results in Figure 9 contain large over-approximation error except
We observe that the calculated over-approximation for B4. In Tora, Verisig 2.0 fails to calculate the complete reachable sets due to too large over- approximation error. Hence, fairly to say that Verisig 2.0 is sensitive the DNNs with big weights.
15

---

65
0.0
8
60
-05
-0.
-1.
-03
0/0
-05
08
x1
x1
(a)
(b)
(c) B3
0.60
1.0
0.02
0.45
0.5
0.04
0.30
0.0
x1
x1
(d) B4
(c)
(f) Tora
Figure Assessing Verisig 2.0 on the larger networks with big weights. red box: over-approximation
set; green lines: simulation trajectories; blue box: goal region; purple dashed box: unsafe region.
Network (
Network ( ii
Network (iii
CP by LinCON
0.02
0.92
0.02
9 0.00
6
0.00
0.00
-0.02
10
20
30
50
Time
step
Time step
Time step
(h)
(c)
0.06
0.06
CP by Polar
0.34
0.02
0.04
0.02
0.00
0.02
0.00
0.00
-0.02
0.02
20
50
10
20
30
40
50
10
50
Time step
Time step
Time step
(d)
(c)
(f)
QUAD by LINCON
1.0
0.8
0.8
0.8
0.66
0.6
12 0.6
0.4
Time
(h)
QUAD by Polar
1.0
1.0
1.0
0.6
2
0.4
0.2
0.2
0.2
5
10
15
0
10
15
5
10
15
Time step
Time step
Time step
(k)
())
Figure 10: Multiple evaluations CartPole (CP) and QUAD. red box: over-approximation green lines: simulation trajectories;
16


Reviews:
[{"review_id": "1eHNyQrRCG", "reviewer": "Reviewer_DN9m", "summary": "This paper presents an approach towards more easily verifiable DRL agent. Instead of training a neural network and then applying verification tools to it, the paper proposes to partition the input state, train linear policies in each of the partition, and verify the resulting piecewise-linear policy as a hybrid automation in Flow*.", "questions": "How do you determine the number of segments along each dimension?\n\nHow is the system dynamic handled? Is it encoded precisely?\n\nTo my knowledge, Verisig 2.0 also uses Flow*. Is it fair to say that the main difference between LinCon and Verisig 2.0 is that the former verifies a PLDNN while the latter verifies a canonically trained neural network?", "limitations": "The paper does not explicitly discuss its current limitation. ", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- Verifying DRL systems has gained research attention in the past several years due to its supposed application in many safety/cost-critical scenarios. Currently, scalability is a major concern. Therefore, the topic of the paper is of interests to the ML and verification community.\n\n- While most existing work verifies a neural network controller via input splitting + abstract interpretation, the paper proposes an interesting and novel alternative, which is to eagerly partition the input region before training and make sure that a linear policy is trained for each partition. Compared to the train-and-transform approach, the proposed approach guarantees linearity in each partition, which leads to faster verification empirically.\n\n- The proposed method is relatively easy to implement in existing training framework. The engineering trick that inserts hand-crafted neural network layers to make sure input from the same partition will be multiplied with the same weights is clever.", "weaknesses": "Conceptually, the method leverages the observation that a relatively small set of linear functions is sufficient to achieve comparable performance to a more complex neural network. This observation is itself rather surprising and deserve a closer study. For the same input region where the PLDNN is linear, is the behavior of the neural network also relatively linear? Are there input region where non-linearity is truly needed and PLDNN's behavior is problematic?\n \nIf low training loss can truly be obtained by a set of linear functions, it seems reasonable to expect that the behavior of the neural network in the same partition is close to linear as well, making abstract interpretation based techniques relatively precise. Following this thought,  the performance gain in verification precision might be a construct of the baseline neural network being unnecessarily large. Have the authors tried whether smaller networks can result in similar performance?\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Weaknesses 1:**\\\n(i) The observation that a relatively small set of linear functions is\nsufficient to achieve comparable performance deserves a closer study.\\\n(ii) For the same input region where the PLDNN is linear, is the\nbehavior of the neural network also relatively linear?\\\n(iii) Are there input region where non-linearity is truly needed and\nPLDNN's behavior is problematic?\n\n**Response:** (i) We hold the same opinion and believe that this\nobservation would stimulate more studies in this research direction. In\nfact, there have recently been several related works. For example,\nin [1], a deterministic program with a small set of\nlinear functions (less than four) is learned as a safety shield. In\n[2], the \"if-then-else\\\" structured programs whose\ndepth of syntax tree is between two and five can fulfill different\ncontrol tasks. Hence, it is feasible to achieve good performance with a\nrelatively small set of linear functions.\n\n\\(ii\\) The answer is yes if there is a unique optimal control policy.\nThis is because the PLDNN can be considered as an approximation of the\noptimal decision neural network. However, if there can be multiple\noptimal control policies, an agent may make different decisions even in\nthe same state with different policies, but all the different decision\nsequences can achieve optimal performance globally. In this case, the\nlinearity of a PLDNN in the same input region does not necessarily imply\nthat the neural network has the same relatively linear behavior.\n\n\\(iii\\) Yes, in theory, regions may exist where non-linearity behavior\nis truly needed. However, a nonlinear function can be well-fitted by a\nset of linear functions from the perspective of function fitting. The\nwidely-used ReLU neural networks are such an example, which are\nessentially a piece-wise linear function as well (see\n[3] for details). More partitions can be applied to\nperform a similar non-linear decision.\n\n**Weaknesses 2:** Can smaller networks result in similar\nperformance?\n\n**Response:** Yes, that is possible in practice. However, whether\nsmaller networks result in similar performance depends on the complexity\nof DRL control tasks, such as the system dynamics and the control\ntarget. Our experimental results show that: for some simple cases such\nas B1 in Table 2 in our submission, the smaller networks Tanh$(2 \\times 20)$ and\nReLU$(2 \\times 20)$ can achieve comparable performance. In contrast, in\nCartPole with relatively complex system dynamics, a small neural network\nsuch as Tanh$(2 \\times 20)$ can not obtain high performance.\n\n**Question 1:** How do you determine the number of segments along\neach dimension?\n\n**Response:** The number of partitions depends on the training reward of\nthe DRL control system. We start training from a small number of\npartitions. If the preset reward threshold is not reached, meaning that\nthere may exist some regions that need a non-linear decision, we will\nfurther divide the state space till the preset reward threshold can be\nreached.\n\n**Question 2:** How is the system dynamic handled? Is it encoded\nprecisely?\n\n**Response:** Yes, the system dynamics $f$ is exactly encoded into the\nflow component of a hybrid automaton in the form of ordinary\ndifferential equations (ODEs)\n$F(l_0): \\{\\dot{s} = f(s, a), \\dot{a} = 0, \\dot{t}_c = 1\\}$. We then\nuse the tool Flow\\* to compute conservative results that contain the\nsolution of the ODEs.\n\n**Question 3:** Is it fair to say that the main difference between\nLinCon and Verisig 2.0 is that the former verifies a PLDNN while the\nlatter verifies a canonically trained neural network?\n\n**Response:** Yes, that is the main difference. Our insight is that\ntraining verification-friendly controllers such as PLDNNs can be a good\nalternative to developing certified DRL systems. As shown in our\nexperiments, the verification results by LinCon are very close to the\nsimulation results, while the results by Verisig 2.0 may fail the\nverification (Table 2 in our submission) due to the over-approximation of canonically\ntrained neural networks.\n\n[1] H. Zhu, Z. Xiong, S. Magill, and S. Jagannathan, “An inductive synthesis frame-\nwork for verifiable reinforcement learning,” in Proceedings of the 40th ACM SIG-\nPLAN conference on programming language design and implementation, 2019, pp.\n686–701.\n\n[2] Y. Wang and H. Zhu, “Verification-guided programmatic controller synthesis,” in\nInternational Conference on Tools and Algorithms for the Construction and Analysis\nof Systems. Springer, 2023, pp. 229–250.\n\n[3] G. F. Montufar, R. Pascanu, K. Cho, and Y. Bengio, “On the number of linear re-\ngions of deep neural networks,” Advances in neural information processing systems,\nvol. 27, 2014.\n9\n"}, {"review_id": "kRQsXAIMja", "reviewer": "Reviewer_uQsi", "summary": "The paper proposed a new neural network architecture, PLDNN, for better verification of DRL trained / neural-network controlled closed-loop controlled systems. PLDNN differs by abstracting the input space with intervals and applying linear mappings in each abstract states. The controller represented by PLDNN can be integrated with different DRL algorithms. The experimental results showed that the PLDNN can retain the performance by training with DRL algorithms directly and achieve tighter reachable sets with better verification efficiency.", "questions": "- Could you provide more details about the linear policy for reducing the partitions?\n- Could you provide more details on how network are trained for benchmarks in the experimental section, e.g., training time? Are all network trained from scratch?", "limitations": "Some limitation discussion on training time cost would be great to have.", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper is sound and the topic of the paper is of high interest to the research community.\n- The paper does a good job at introducing technical details and makes the paper easy to follow.\n- The empirical study shows great improvement of the proposed method over existing reachability analysis methods for neural-network controlled systems.", "weaknesses": "- My main concern of the paper is lack of analysis on the policy of reducing the partitions. Though the experimental results show strong results of PLDNN, it is not clear how partitioning plays a role in the performance improvement. It could be for some partitioned space in the state space, a linear control policy is almost close to the optimal control policy. Some other partitioned region may need finer partitions to approach the optimal control policy with a combination of linear control policies. However, similar insights or observations are not provided in the paper. Some analysis on how number of partitions evolves during training or a comparison between the linear policy of partition reduction and a baseline, like a fixed number of partition, would be great to have.\n- The paper positioned PLDNN as a new transform-then-train approach. Training with PLDNN may result in some implicit benefits of finding near-optimal policy represented by PLDNN. But PLDNN and the partition schema are still applicable for the train-then-transform process, e.g., distilling a trained DNN to PLDNN. I would recommend authors to provide an empirical comparison between using PLDNN with transform-then-train and train-then-transform processes.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Weaknesses 1:** My main concern of the paper is lack of analysis on\nthe policy of reducing the partitions. Though the experimental results\nshow strong results of PLDNN, it is not clear how partitioning plays a\nrole in the performance improvement. Some analysis on how number of\npartitions evolves during training or a comparison between the linear\npolicy of partition reduction and a baseline, like a fixed number of\npartitions, would be great to have.\n\n**Response:** From the perspective of function fitting, more partitions\ntend to obtain a policy that fits the optimal decision function better,\nwhich implies a better reward performance. In our experiment, we compare\nwith an approach which trains constant actions on partitioned regions\n[1]. Under a similar performance constraint, the\npartition reduction is significant by our approach (Table 1 in our submission). Using a\nfixed number of partitions is a reasonable baseline which can also show the\neffect of partition reduction. In our future work, besides the baseline with a fixed number of partitions, we will further\nconsider building another baseline, i.e., the minimal number of\npartitions that are needed for training near-optimal piece-wise linear\ncontrollers. \n\n**Weaknesses 2:** I would recommend authors to provide\nan empirical comparison between using PLDNN with transform-then-train\nand train-then-transform processes.\n\n**Response:** Thanks for your insightful suggestion!\nTrain-then-transform via PLDNN is indeed a direction that deserves\nfurther study. We did not consider this as one of our intentions is to\ndemonstrate the feasibility of training verification-friendly and\nnear-optimal PLDNNs directly. We agree that PLDNNs are also achievable\nvia the train-then-transform approaches. Encouraged by the suggestion,\nwe carried out a quick experiment on the comparison. The results show\nthat the directly trained PLDNN exhibits similar performance (reward is\n52.97) to a canonically trained DNN (reward is 52.45), while there is\na small decrease in performance (reward is 51.25) of the PLDNN\ntransformed from the trained DNN. See the attached PDF file and our\nglobal response for more details. However, such a decrease is almost\nnegligible and more comprehensive experiments are required to draw fair,\nconclusive results.\n\n**Question 1:** Could you provide more details about the linear\npolicy for reducing the partitions?\n\n**Response:** We compare the partition reduction of linear policy with\nan approach [1] that trains a constant action on each\npartition (Table 1 in our submission). For both approaches, we start from a coarse-grained\npartition (i.e., one region) to train using the DDPG algorithm and\nincrease the number of partitions on each dimension until the preset\nreward threshold is achieved. The linear policy relaxes the constraint\nthat each abstract state needs to correspond to a constant action. Our\nevaluation shows that using linear policy, rather than a constant, can\nsignificantly reduce the number of partitions under the same reward\nthreshold setting, e.g., from $25^4$ to $16$.\n\n**Question 2:** Could you provide more details on how networks are\ntrained for benchmarks in the experimental section, e.g., training time?\nAre all networks trained from scratch?\n\n**Response:** We use DDPG as the training algorithm for all PLDNNs and\nDNNs. In addition, all the networks are trained from scratch and the\ncorresponding average training time is reported in Table 1 in our submission (in seconds).\nThe setting of the reward functions is given in Appendix A.1 of our\naccompanying technical report (submitted as supplementary material). We\nuse the larger network structure with the Tanh activation function\n(Table 2 in our submission) to conduct the training and robustness evaluation.\n\n[1] P. Jin, J. Tian, D. Zhi, X. Wen, and M. Zhang, “Trainify: A cegar-driven training\nand verification framework for safe deep reinforcement learning,” in International\nConference on Computer Aided Verification. Springer, 2022, pp. 193–218.\n10\n"}, {"review_id": "4hfkQO1Lii", "reviewer": "Reviewer_63JN", "summary": "The paper presents an approach for designing neural network policies, in the context of deep reinforcement learning (DRL) with continuous state and action spaces, that are more amenable to verification compared to standard networks. A standard approach to verifying continuous DRL systems is to abstract the system after learning the policy and to then verify the abstracted system. In contrast, the proposed approach first abstracts the state space (such that the state space is discretized) and then learns a linear policy for each abstract state. The coefficients of the linear policy are learnt using a coefficient network that maps each abstract state to its resulting policy coefficients. This mapping itself need not be linear and can be a complex neural network. However, since the state space is discretized and the policy for each abstract state is fixed and linear, tight and efficient verification of the resulting DRL system becomes feasible. Moreover, the state abstraction computation is itself encoded as the first layer of the coefficient network, so that the resulting policy network (referred to as piece-wise linear decision neural networks or PLDNNs) has a standard input (system state) and an output (actions), and can be directly trained using off-the-shelf DRL algorithms. The empirical evaluation shows that the performance of PLDNNs, measured in terms of cumulative reward and robustness of the policy, is comparable to standard policy networks. At the same time, DRL systems with PLDNN policies are much more amenable to verification.", "questions": "I have some clarification questions about the evaluation.\n\n1. What were the model architectures used for the results reported in Section 5.1? Are these the same architectures as in Section 5.2?\n\n2. Are the architectures for PLDNN and DNN the same (except for the first layer) for the results in Section 5.1 and Section 5.2? If not, how were the DNN architectures chosen and how do we ensure that it is an apples-to-apples comparison?\n\n3. Is the time reported in Table 1 in seconds? And is it the total training time over all episodes?\n\n4. How is the reward for the robustness experiments calculated, i.e., what is the horizon length? More generally, what is the reward function? The appendix gives some details; it says that for the 6 regular benchmarks \"we set a negative reward when the agent is not in the goal region. Once the agent reaches the goal region, it will be awarded a positive reward\". How and what is the positive reward assigned? Why is the final cumulative reward so different across the 6 regular benchmarks (based on Fig 5 and 7) if their reward functions are so similar?\n\n5. Are the models used for the robustness experiment the same as the ones used for the cumulative reward experiment? If yes, then why do you say that 10 different policies are trained for the former while you conduct five trials for the latter? My understanding is that the models used for the robustness experiment are trained on non-perturbed data but the evaluation is conducted with perturbed data. If this is so, then the same models can and should be used for both sets of experiments.\n\n6. What are precisely the properties of the DRL systems being verified? Based on Table 3 in the appendix, my guess is that for B1-B5, Tora, and QUAD the verified property is a liveness property whereas for CartPole it is a safety property? Can you please confirm? Is the time horizon for properties bounded or unbounded? It would be helpful to include this detail in the paper as well.\n\nSome more general questions:\n\n1. Can you comment on the applicability of this approach in settings where the inputs are high-dimensional images?\n\n2. Can the approach be adapted to settings where the action space is discrete?", "limitations": "The paper does not necessarily discuss the limitations and might benefit from a small discussion about the same.", "rating": 7, "confidence": 3, "soundness": 4, "presentation": 3, "contribution": 4, "strengths": "Even when the system dynamics are known, formal verification of safety and liveness properties of DRL systems is challenging to scale, specially for continuous state and action spaces. The paper proposes a very interesting idea for architecting policy networks that are easier to verify. I believe that the proposed notion of abstracting the state space before learning the policy will be a fruitful research direction. I also find the observation that a small set of linear policies can perform as well as a complicated non-linear policy to be surprising and interesting in its own right. I should add the disclaimer that I am not an expert on the topic of reinforcement learning and do not have a good sense of the broader literature on the topic.", "weaknesses": "My main concern is about the \"scalability of verification vs cumulative reward\" tradeoff for DRL systems with high-dimensional state spaces (for instance, when the inputs to the policy network are images). As the state space becomes more complex, I suspect that a finer-grained partition becomes necessary to learn a good policy, directly impacting the scalability of verification. The presented evaluation considers system states with up to 12 dimensions, so it is hard to make an assessment about PLDNNs in settings where inputs are images required hundreds to thousands of dimensions.\nI am also curious about how the proposed approach would be used when the action space is discrete. Would each abstract state be mapped to a fixed action? Some discussion about this setting could be interesting and helpful. Finally, I have minor concerns about the empirical evaluation (described in the Questions section below).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Weaknesses 1:** (i) It is hard to make an assessment about PLDNNs in\nsettings where inputs are images. (ii) How the proposed approach would\nbe used when the action space is discrete?\n\n**Response:** (i) Yes, applying PLDNNs when inputs are images is\ndifficult due to the high dimensionality. At present, we are only\nfocused on state-based cases. One potential solution to adapting PLDNNs\nto images is first to extract features from images and train PLDNNs on\nthe extracted features. We believe that this is an interesting research\ndirection to follow.\n\n\\(ii\\) For discrete action space, please refer to our response to\n**General Question 2** below.\n\n**Question 1:** What were the model architectures used for the\nresults reported in Section 5.1? Are these the same architectures as in\nSection 5.2?\n\n**Response:** We use the larger network structure with Tanh activation\nfunction (e.g. Tanh$_{3 \\times 100}$), as shown in Table 2 in our submission, to conduct\nthe training and robustness evaluation.\n\n**Question 2:** Are the architectures for PLDNN and DNN the same\n(except for the first layer) for the results in Section 5.1 and Section\n5.2?\n\n**Response:** Yes, they are almost the same. Precisely, they have the\nsame architectures except that PLDNN has an abstraction layer and an\nadditional output layer for outputing linear coefficients. The hidden\nlayers of PLDNN and DNN are exactly the same in our comparison\nexperiments.\n\n**Question 3:** Is the time reported in Table 1 in seconds? And is\nit the total training time over all episodes?\n\n**Response:** Yes, the time reported in Table 1 in our submission is in seconds, and it is\nthe total training time over all episodes.\n\n**Question 4:** How is the reward for the robustness experiments\ncalculated, i.e., what is the horizon length? reward function? Why is\nthe final cumulative reward so different across the 6 regular\nbenchmarks?\n\n**Response:** The horizon length in CartPole is set to 200. In the other\nbenchmarks, the settings of horizon length depend on the number of\ncontrol steps needed to reach the goal region. For example, in B1, it\ntakes about 30 control steps to reach the goal region after the training\nphase. In B2, the agent needs about 15 control steps to reach the goal\nregion. Based on this, we set the horizon length slightly larger than\nthe control steps, e.g. 35 for B1 and 20 for B2.\n\nFor the reward function, the positive reward when the agent reaches the\ngoal region is set to a constant such as 100. The negative reward\nfunction is set according to the distance between the agent and the\ncenter of the goal region. For instance, since the goal region of B1 is\n$x_1 \\in [0,0.2], x_2 \\in [0.05,0.3]$, we set the negative reward\nfunction as $-|x_1 -0.1| - |x_2 - 0.2|$. Hence, to obtain a higher\ncumulative reward, the agent needs to reach the goal region as soon as\npossible.\n\nAs different control steps are needed to reach the goal region in each\nbenchmark, the cumulative reward is different across the six regular\nbenchmarks even if their reward functions are similar.\n\n**Question 5:** Are the models used for the robustness experiment\nthe same as the ones used for the cumulative reward experiment?\n\n**Response:** Yes, the five models used in the reward evaluation are the\nsame as for the robustness evaluation. However, as the robustness\nassessment is based on perturbed data, which may cause uncertainties, we\nhave therefore performed five additional trials to produce more precise\naveraged robustness evaluation results.\n\n**Question 6:** (i) What are the properties being verified? (ii) Is\nthe time horizon for properties bounded or unbounded?\n\n**Response:** (i) For B1-B5, Tora, and QUAD, we verify a liveness\nproperty that checks whether the agent can reach the goal region within\nsome bounded control steps. For CartPole, we verify a safety property:\nwhether the agent can stay in the safe region within some specific\ncontrol steps. (ii) Yes, all the time horizons are bounded because our\nverification is based on reachability analysis which only calculates the\noverestimated sets of reachable states in finite steps, as required by\nthe off-the-shelf tool $\\text{Flow}^*$.\n\n**General Question 1:** Can you comment on the applicability of this\napproach in settings where the inputs are high-dimensional images?\n\n**Response:** Since PLDNN-based training only costs slightly more time\nthan traditional DNN-based training, we believe that PLDNNs can be\napplied to the training phase when dealing with high-dimensional image\ninput such as image classification. That is, the piece-wise linear\nfunction $\\pi$ and softmax function $\\mathit{softmax}$ are composed to\nyield a function that outputs the probability of each category in the\nform of $\\mathit{softmax}(\\pi(s))$. However, the verification cannot\ndirectly handle the high-dimensional image input due to the extremely\nhigh-dimensional input space. Another reason is that the dynamics of\npixels may not be definable. If we can extract some informative features\nfrom the image input first, combining the verification technique may be\nfeasible.\n\n**General Question 2:** Can the approach be adapted to settings\nwhere the action space is discrete?\n\n**Response:** Yes. One straightforward approach is to make each abstract\nstate perform the same action. Moreover, if we still want to maintain a\nlinear output on each abstract state, we only need to generate a mapping\nbetween the continuous output and the discrete action space. For\nexample, given a discrete action space $\\{1,-1\\}$, when the output of\nthe decision neural network is greater than 0, the agent executes action\n1; otherwise, it performs action -1:\n\n$$a=\n\\begin{cases}\n    1 &  \\text{if }\\pi(s)>0,\\\\\\\\\n    -1 & \\text{otherwise.}\n\\end{cases}$$"}, {"review_id": "JosSm431AE", "reviewer": "Reviewer_eCb4", "summary": "This paper proposes an inverse transform-then-train approach for verifying deep reinforcement learning systems. It encodes a DNN into efficiently verifiable linear control policies and optimizes them via reinforcement learning. The approach is compatible with existing DRL training algorithms and shows that PLDNN-based systems can be more efficiently and tightly verified, with up to 438 times speedup and a significant reduction in overestimation.\n", "questions": "##\n## Originality\n\nTo efficiently verify deep reinforcement learning systems, this paper proposes an inverse transform-then-train technique. It efficiently converts a DNN into verifiable linear control policies, which it then uses reinforcement learning to improve. The method is compatible with current DRL training algorithms and demonstrates that PLDNN-based systems can be more effectively and tightly verified, with speedups of up to 438 times and a notable decrease in overestimation.\n\n##\n## Importance of contribution\n\nThe idea of using PLDNN to boost the verification of DRL is interesting. However, it seems like it converts the DNN into a different structure before training, and the PLDNN is different from the original DNN. To me, it is more like a synthesis technique, rather call it as verification. Moreover, the authors claim that it is compatible with most existing DRL training algorithms, but in the evaluation, the details of the training algorithms are not shown.\n\n##\n## Soundness\n\nThis paper proposes an inverse transform-then-train approach for verifying deep reinforcement learning systems, overcoming inaccuracies and scalability issues. It uses piece-wise linear decision neural networks (PLDNNs) for efficient verification, reducing overestimation. However, there are some technical parts that are not so clear and need further clarification. \n\nPage 1, Line 21\n> Most existing approaches [7–10] over-approximate both embedded DNNs and non-linear environment dynamics to build verifiable models, which inevitably introduces dual overestimation.\n\nI am not sure what this dual-estimation is. The sentence following seems only talk about the disadvantage of over-approximation.\n\nPage 2, Line 40\n> ..., we propose a novel, inverse transform-then-train approach:\n\nIt seems like the approach cannot verify a trained DRL agent. So it is more like a synthesis technique.\n\nPage 5, Line 197\n> Consequently, we can extract a piecewise linear decision function with this structure of π on each abstract state.\n\nHow the piecewise linear functions are extracted? Could you explain it more detailedly?\n\n##\n## Evaluation\n\nThe authors try to evaluate whether PLDNN-based training offers reduced partitions, comparable rewards, robustness, time overhead, high verification performance, and scalability for large-sized neural networks and complex systems with high-dimensional state space. In Section 5.2, the authors compare Lincon with polar and verisig 2.0. Have you compared the efficiency of these tools on the original DNNs? Since, maybe the architecture of PLDNN is not easy to be handled for Polar and Verisig 2.0.\n\n##\n## Quality of presentation\n\nThe paper is not that easy to follow. I would recommend the authors add more motivations for the design of each single component.\n\n##\n## Comparison with Related Work\n\nThe PLDNN structure is similar to the DNN with abstract states listed below. What are the main difference and advantages of using PLDNN?\n\n- Jin, Peng, et al. \"Trainify: a CEGAR-driven training and verification framework for safe deep reinforcement learning.\" ", "limitations": "No, the authors did not discuss the limitation of the work. I think more attention should be given to the disadvantages of using PLDNN, like is it still the same original network?\n", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "+ The paper explores an interesting and important direction\n+ Innovative and practical methodology", "weaknesses": "- Some technical parts are unclear\n- The way of presenting contributions of the work is somewhat misleading\n- The limitation of using PLDNN is not discussed", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Question for the importance of contribution:** (i) It is more like a\nsynthesis technique, rather call it verification. (ii) Algorithm\ncompatibility of PLDNN.\n\n**Response:** (i) Yes, it can be understood as a synthesis method for\ndeveloping verification-friendly models. We show that the powerful\nfitting capability of DNN can be leveraged to train easy-to-verify\nPLDNNs. One novelty of our work is that we use DNN as a backbone to\nimplement policy synthesis. (ii) Our approach is compatible with most\nexisting DRL training algorithms because we do not change the input and\noutput structure of the decision network. Namely, the differences with\nthe original DNN are invisible to the DRL algorithms.\n\n**Question for Page 1, Line 21:** What this dual-estimation is?\n\n**Response:** The first overestimation is introduced when dealing with\nthe DNN controller. For the traditional DNN, it cannot be expressed in a\nknown closed-form expression. Consequently, most approaches resort to\ncomputing a conservative model such as a Taylor model that encloses the\noutput of DNN given an input set, which is the first overestimation for\nthe decision neural network. The second overestimation is introduced to\nobtain an overestimation model for the solution of ODE system dynamics.\nThat is unavoidable as most nonlinear ODEs do not have closed-form\nsolutions. Using PLDNN as the decision neural network, we can eliminate\nthe first overestimation as PLDNN can be expressed in a known\nclosed-form (i.e., piece-wise linear function).\n\n**Question for Page 2, Line 40:** It seems like the approach cannot\nverify a trained DRL agent. So it is more like a synthesis technique.\n\n**Response:** Yes, the traditional DNN-based agent cannot be verified\ndirectly in our approach. Our insight is that training/synthesizing\nverification-friendly models is more practical to develop certified DRL\nsystems than directly verifying the complex canonically trained DNNs. We\ndemonstrate this in the paper.\n\n**Question for Page 5, Line 197:** How the piecewise linear\nfunctions are extracted?\n\n**Response:** The extraction is straightforward. Due to the special\ndesign of PLDNNs (Figure 2 in our submission), we can feed an arbitrary\nstate in each partition into the embedded coefficient network $\\pi_c$\nand it will output the linear coefficients of the corresponding linear\ncontroller defined on each partition. As partitions are finite, we can\ntraverse all the partitions and obtain the extracted linear controllers\nthat are equivalent to the PLDNN.\n\n**Question for Evaluation:** Have you compared the efficiency of\nthese tools on the original DNNs? Since, maybe the architecture of PLDNN\nis not easy to be handled for Polar and Verisig 2.0.\n\n**Response:** It is true that PLDNNs cannot be handled by Polar and\nVerisig 2.0, but that is not our intention in this work. As we can\nextract equivalent linear controllers from a PLDNN, we do not need to\ncope with the network decision model for verification. Instead, we can\nleverage the off-the-shelf hybrid system verification tools such as\nFlow\\* to verify PLDNN-based systems. To demonstrate the\nverification-friendliness, we provide the verification results by PLDNN\nand original DNNs in Table 2 in our submission, respectively. The\nresults show that DNN-based systems are difficult to verify even by\nusing state-of-the-art tools like Polar and Verisig 2.0 and hardware\nacceleration. In contrast, PLDNN-based systems are more efficient to\nverify even without hardware acceleration. Moreover, the verification\nresults are more precise as the DNN over-approximation is avoided.\n\n **Question for Comparison with Related Work:** What are the main\ndifferences and advantages of using PLDNN?\n\n**Response:** There are two main advantages of our approach. First, we\ntrain a linear controller on each partition while other approaches such\nas Trainify [1] train a constant action. Consequently, the number of\npartitions we need is far less than that needed by Trainify. Second,\nwith PLDNN, we can solve the verification problem by transforming the\nPLDNN-based system into an equivalent hybrid model, which can be\nverified using off-the-shelf tools such as Flow\\*. However, Trainify\nneeds to build Kripke structures from the trained models, which, quite\noften, suffers from the notorious state explosion problem due to the\nexponential increase of partitions during training.\n\n[1] P. Jin, J. Tian, D. Zhi, X. Wen, and M. Zhang, “Trainify: A cegar-driven training and verification framework for safe deep reinforcement learning,” in International Conference on Computer Aided Verification. Springer, 2022, pp. 193–218. 10"}]

Author rebuttal:
## Discussion on Limitations
We thank all the reviewers for the valuable feedback. We first briefly
discuss the main limitations of our method, as raised by all the
reviewers.

One limitation concerns a potential rapid increase in the number of
partitions when a preset reward threshold can never be reached. One
solution would be to locate and partition the regions with poor
performance. These regions that result in the failure of training can be
regarded as *counterexamples* and should be further divided. We plan to
leverage the counterexample-guided abstraction and refinement (CEGAR)
formal method to cope with this problem.

Another potential limitation is that the verification complexity may
still be high for piece-wise linear controllers, although we show in the
paper that they are more amenable and verification-friendly than neural
network controllers. At present, we employ off-the-shelf hybrid
verification tools [1] to demonstrate the effectiveness of
our approach. We are considering implementing dedicated algorithms to
improve the verification efficiency.

## Train-Then-Transform using PLDNN

Encouraged by Reviewer 63JN's suggestion, we have conducted a quick
experiment to compare the two approaches: transform-then-train and
train-then-transform. The experiment was conducted on B1. The results
are presented in Table 1 in our PDF file.

**Experimental Setting.** We use the same network structure
Tanh$_{2 \times 20}$ for training the following three decision networks
(i.e. DNN, PLDNN, and Distilled PLDNN). For DNN and PLDNN, the training
algorithm is DDPG. The distilled PLDNN is obtained using supervised
learning in which the training data is obtained through sampling from
the traces generated by the DNN controller.

In the train-then-transform approach, we first train a DNN controller
whose cumulative reward is about 52.45. Then we use supervised learning
to distill the DNN's policy into a PLDNN containing four partitions.

**Results.** Regarding performance, i.e., the cumulative reward, the
directly trained PLDNN can reach 52.97, which is similar to that of the
canonically trained DNN (52.45). We also observe that there is a slight
decrease in the system performance after the DNN is distilled to a PLDNN
(51.25).

Regarding verification, both the distilled PLDNN and the directly
trained PLDNN can be verified faster than the DNNs, which demonstrates
PLDNN's verification-friendliness. Moreover, the verification result of
the directly trained PLDNN is more precise, i.e., tightly closer to the
simulation results. Both the distilled PLDNN and original DNN result in
larger overestimation due to the over-approximation.

**Conclusion.** The preliminary experimental results show that, compared
to our transform-then-train approach, the train-then-transform approach
can achieve similar verification performance, but may cause a
performance decrease and extra overestimation of verification results.
Nevertheless, our comparison is preliminary; more comprehensive
experiments are therefore needed to draw a fair conclusion.

[1] X. Chen, E.  ́Abrah ́am, and S. Sankaranarayanan, “Flow*: An analyzer for non-
linear hybrid systems,” in Computer Aided Verification: 25th International Confer-
ence, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. Springer,
2013, pp. 258–263.

Meta-review: The paper gives a new approach to learning verified RL policies, in which a neural policy is transformed into a collection of verifiable linear control policies, which are then optimized using RL. 

The idea that a small number of verifiable linear controllers can collectively achieve comparable performance to a neural policy -- at least in some interesting domains -- is very intriguing. While the reviewers originally had some concerns about the evaluation, these concerns were addressed during the discussion period. Given all this, I am delighted to recommend acceptance. Please carefully incorporate the reviewers' feedback in the final version.
Decision: Accept (poster)