Reachability Analysis and Safety Veriﬁcation of Neural Feedback Systems via Hybrid Zonotopes Yuhao Zhang and Xiangru Xu

2025-04-29 0 0 474.13KB 8 页 10玖币

侵权投诉

Reachability Analysis and Safety Veriﬁcation of Neural Feedback

Systems via Hybrid Zonotopes

Yuhao Zhang and Xiangru Xu

Abstract— Hybrid zonotopes generalize constrained zono-

topes by introducing additional binary variables and possess

some unique properties that make them convenient to represent

nonconvex sets. This paper presents novel hybrid zonotope-

based methods for the reachability analysis and safety veri-

ﬁcation of neural feedback systems. Algorithms are proposed

to compute the input-output relationship of each layer of a

feedforward neural network, as well as the exact reachable

sets of neural feedback systems. In addition, a sufﬁcient and

necessary condition is formulated as a mixed-integer linear

program to certify whether the trajectories of a neural feedback

system can avoid unsafe regions. The proposed approach

is shown to yield a formulation that provides the tightest

convex relaxation for the reachable sets of the neural feedback

system. Complexity reduction techniques for the reachable

sets are developed to balance the computation efﬁciency and

approximation accuracy. Two numerical examples demonstrate

the superior performance of the proposed approach compared

to other existing methods.

I. INTRODUCTION

Artiﬁcial neural networks have shown their extraordinary

performance in many ﬁelds such as auto-driving systems [1]

and mobile robots [2]. Implementation of neural networks in

such controlled systems also raises safety concerns as even a

small chance of failure may cause catastrophic consequences.

Therefore, it’s critical to ﬁnd an efﬁcient method to verify the

safety properties of controlled systems with neural network

components before real implementations. However, analyz-

ing properties of neural networks is notoriously difﬁcult due

to their highly non-convex and nonlinear natures [3].

Various methods have been proposed to perform reacha-

bility analysis and safety veriﬁcation for the neural feedback

systems (i.e., feedback systems with neural network con-

trollers) [4], [5], [6], [7], [8]. Based on quadratic constraints,

a reachable set over-approximation method was proposed

in [9], [10] using semi-deﬁnite programming (SDP). A

fast reachability method was introduced in [11] by relax-

ing the SDP into linear programming (LP). Learning-based

reachability methods were also developed in [12], [13] for

neural feedback systems with probabilistic guarantees on

the correctness of the approximated reachable sets. Set-

based methods were also proposed to compute the exact

reachable sets of neural feedback systems using star sets

[14] and constrained zonotopes [15]. Despite their interesting

results, these two methods can only deal with convex set

representations which limit their usage for complex safety

Yuhao Zhang and Xiangru Xu are with the Department of Mechanical

Engineering, University of Wisconsin-Madison, Madison, WI, USA. Email:

{yuhao.zhang2,xiangru.xu}@wisc.edu.

Fig. 1: The neural feedback system is given as x(t+ 1) =

Adx(t)+Bdu(t)where the state feedback controller u(t) =

π(x(t)) is a given `-layer FNN with the ReLU activation

function. At each time step, the neural feedback system maps

a hybrid zonotope as the input set to another hybrid zonotope

as the output set. The initial set is X0and the reachable set

at time tfrom X0is Rt(X0).

veriﬁcation problems. Besides, the computation complexity

increases rapidly for deep neural networks.

Recently, a new set representation named the hybrid zono-

tope was introduced in [16]. Through the addition of binary

generators, hybrid zonotope can represent non-convex sets

with ﬂat faces. And the reachability analysis based on hybrid

zonotopes will lead to the formulation of mixed-integer linear

programs (MILPs), for which many state-of-the-art solvers

such as Gurobi [17] and learning-based solver MLOPT [18]

can be utilized to accelerate the computation.

In this work, we present hybrid zonotope-based methods

for reachability analysis and safety veriﬁcation of neural

feedback systems with ReLU-activated feed-forward neural

network (FNN) controllers (see Figure 1). The contributions

of this paper are threefold: (i) For neural feedback systems

with hybrid zonotopes as the input sets, a novel approach

is presented to compute the nonconvex exact reachable sets

represented as hybrid zonotopes; (ii) Based on the convex

relaxation property of the computed reachable sets and the

properties of hybrid zonotopes, heuristic reduction methods

are proposed to reduce the complexity growth of the hybrid

zonotope sets; (iii) Using the computed reachable sets, an

MILP-based condition is provided to verify the unsafe region

avoidance of neural feedback systems, for which off-the-shelf

solvers can be employed. The efﬁciency of the proposed

methods is demonstrated through two numerical examples.

II. PRELIMINARIES & PROBLEM STATEMENT

A. Hybrid Zonotopes

Deﬁnition 1: Let Z,Zc,Zh⊂Rn.Zis a zonotope if (1)

holds [19], Zcis a constrained zonotope if (2) holds [20],

and Zhis a hybrid zonotope if (3) holds [16]:

∃(c,G)∈Rn×Rn×ng:Z={Gξ+c| kξk∞≤1},(1)

arXiv:2210.03244v1 [math.OC] 6 Oct 2022

∃(c,G,A,b)∈Rn×Rn×ng×Rnc×ng×Rnc:

Zc={Gξ+c| kξk∞≤1,Aξ=b},(2)

∃(c,Gc,Gb,Ac,Ab,b)∈Rn×Rn×ng×Rn×nb×Rnc×ng

×Rnc×nb×Rnc:(3)

Zh=







GcGbξc

ξb+c



ξc

ξb∈ Bng

∞× {−1,1}nb,

AcAbξc

ξb=b











where Bng

∞={x∈Rng| kxk∞≤1}is the unit hy-

percube in Rng. The shorthand notations of the zono-

tope, constrained zonotope and hybrid zonotope are given

by Z=Zhc,Gi,Zc=CZhc,G,A,bi, and Zh=

HZhc,Gc,Gb,Ac,Ab,bi, respectively.

Note that a hybrid zonotope degenerates into a constrained

zonotope when nb= 0, and a constrained zonotope de-

generates into a zonotope when nc= 0. For a given

hybrid zonotope HZhc,Gc,Gb,Ac,Ab,bi, the vector cis

called the center, the columns of Gbare called the binary

generators, and the columns of Gcare called the continuous

generators (or simply generators if binary generators are not

present). For simplicity, we deﬁne the set B(Ac,Ab,b) =

{(ξc,ξb)∈ Bng

∞× {−1,1}nb|Acξc+Abξb=b}.

We denote G[:, i]as the i-th column of a matrix G. The

complexity of a hybrid zonotope is described by its degrees-

of freedom order or simply order oh= (ng+nb−nc)/n.

The equivalence of a hybrid zonotope with a ﬁnite collec-

tion of constrained zonotopes is stated by the result below.

Lemma 1: [16, Theorem 5] The set Zh⊂Rnis a hybrid

zonotope if and only if it is the union of a ﬁnite number of

constrained zonotopes.

Similar to constrained zonotopes, hybrid zonotopes are

closed under linear map and intersections.

Lemma 2: [16, Proposition 7] For any R∈Rm×n,Zh=

HZhcz,Gc

z,Gb

z,Ac

z,Ab

z,bzi ⊂ Rn,Yh=HZhcy,Gc

y,Ac

y,Ab

y,byi ⊂ Rn, and H−={x∈Rm|hTx≤f} ⊂

Rnthe following identities hold:

RZh=HZhRcz,RGc

z,RGb

z,Ac

z,Ab

z,bzi,

Zh∩ Yh=HZhcz,Gc

z0,Gb

z0,





0 Ac

z−Gc



,



0 Ab

z−Gb



,



cy−cz



i,

Zh∩ H−=HZhcz,Gc

z0,Gb

z,Ac

hTGc

2,

Ab

hTGb

z,bz

f−hTcz−dm

2i,

where dm=Png,z

i=1 

hTGc

z[:, i]

+Pnb,z

i=1 

hTGb

z[:, i]

+f−

hTcz.

Hybrid zonotopes are also closed under union operation.

Lemma 3: [21, Proposition 1] (Union) For any Zh=

HZ cz,Gc

z,Gb

z,Ac

z,Ab

z,bz⊂Rnand Wh=

HZ cw,Gc

w,Gb

w,Ac

w,Ab

w,bw⊂Rn, deﬁne the vec-

tors ˆ

Gb∈Rn,ˆ

c∈Rn,ˆ

z∈Rnc,z ,ˆ

bz∈

Rnc,z ,ˆ

w∈Rnc,w , and ˆ

bw∈Rnc,w , such that ˆ

Gb=

(Gb

w1+cz)−(Gb

z1+cw)

2,ˆ

z=−Ab

z1−bz

2,ˆ

w=Ab

w1+bw

2,ˆ

(Gb

w1+cz)+(Gb

z1+cw)

2,ˆ

bz=−Ab

z1+bz

2,ˆ

bw=−Ab

w1+bw

Then the union of Zhand Whis a hybrid zonotope Zh∪

Wh=HZ cu,Gc

u,Gb

u,Ac

u,Ab

u,bu⊂Rnwhere

u=Gc

zGc

w0,Gb

u=Gb

zGb

wˆ

Gb,

u=



z0 0

0 Ac



,Ab

u=



z0ˆ

0 Ab

wˆ



,







−I0

0−I

0 0







,Ab







0 0 1

0 0 −1

2I01

−1

2I01

2I−1

0−1

2I−1







cu=ˆ

c,bu=ˆ

zˆ

wbT

3T,

b3=1

21T1

21T0T1T0T1TT.

The emptiness of a hybrid zonotope can be checked by

solving an MILP.

Lemma 4: [16] Given Zh=HZhc,Gc,Gb,Ac,Ab,bi

⊂Rn,Zh6=∅if and only if min{||ξc||∞|Acξc+Abξb=

b,ξc∈Rng,ξb∈ {−1,1}nb} ≤ 1.

B. Problem Statement

Consider a discrete-time linear system:

x(t+ 1) = Adx(t) + Bdu(t)(4)

where x(t)∈Rn,u(t)∈Rmare the state and the control

input. Ad∈Rn×n,Bd∈Rn×mare the state matrix and the

input matrix, respectively.

We assume a state-feedback controller

u(t) = π(x(t)),(5)

which is parameterized by an `-layer FNN with the Rectiﬁed

Linear Unit (ReLU) activation function. The closed-loop

system with system model (4) and controller (5) is denoted

as:

x(t+ 1) = fcl(x(t)) ,Adx(t) + Bdπ(x(t)).(6)

For the closed-loop system (6), we denote Rt(X0),

{x(t)∈Rn|x(0) ∈ X0,x(k+ 1) = fcl(x(k)), k =

0,1, . . . , t −1}the (forward) reachable set at time tfrom

a given set of initial conditions X0⊂Rn.

For the `-layer FNN controller, let W(k−1) be the k-th

layer weight matrix and v(k−1) be the k-th layer bias vector,

for k= 1, . . . , `. Denote x(k)as the neurons of the k-th

layer, then, for k= 1, . . . , ` −1, we have

x(k)=ReLU(W(k−1)x(k−1) +v(k−1))(7)

where x(0) =x(t)and ReLU(x) = max{0,x}. Only the

linear map is applied in the last layer, i.e., π(x(t)) = x(`)=

W(`−1)x(`−1) +v(`−1).

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

ReachabilityAnalysisandSafetyVericationofNeuralFeedbackSystemsviaHybridZonotopesYuhaoZhangandXiangruXuAbstractHybridzonotopesgeneralizeconstrainedzono-topesbyintroducingadditionalbinaryvariablesandpossesssomeuniquepropertiesthatmakethemconvenienttorepresentnonconvexsets.Thispaperpresentsnovelhybri...

展开>> 收起<<

Reachability Analysis and Safety Veriﬁcation of Neural Feedback Systems via Hybrid Zonotopes Yuhao Zhang and Xiangru Xu.pdf

共8页,预览2页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Reachability Analysis and Safety Veriﬁcation of Neural Feedback Systems via Hybrid Zonotopes Yuhao Zhang and Xiangru Xu

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: