On the Trade-off Between Efficiency and Precision of Neural Abstraction

要約

ニューラル抽象化は、複雑な非線形動的モデルの形式的な近似として最近導入されました。
それらは、ニューラル ODE と、抽象ニューラル ネットワークと具体的な動的モデルの間の誤差に関する認定された上限で構成されます。
これまでのところ、ニューラル抽象化はもっぱら $ReLU$ 活性化関数のみで構成されるニューラル ネットワークとして取得されており、その結果、区分的アフィン ダイナミクスを持ち、線形ハイブリッド オートマトンとして等価に解釈できるニューラル ODE モデルが得られます。
この研究では、抽象化の有用性がその用途に依存することを観察しました。シナリオによっては、分析が容易な大まかな抽象化が必要な場合もあれば、より複雑で洗練された抽象化が必要な場合もあります。
したがって、代替形状、つまり区分的定数または非線形非多項式 (具体的にはシグモイド活性化によって得られる) のニューラル抽象化を検討します。
私たちは、形式的な帰納的合成手順を使用して、これらのセマンティクスを備えた動的モデルをもたらすニューラル抽象化を生成します。
これらのさまざまなニューラル抽象化テンプレートが、その精度と合成時間、および安全性検証 (到達可能性計算によって行われる) に必要な時間に関してトレードオフを有することを経験的に示します。
既存の合成技術を改良して高次元モデルの抽象化を可能にし、さらに、これらのモデルの到達可能性解析の効率を向上させるために複雑なニューラル ODE の抽象化について説明します。

要約(オリジナル)

Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. They comprise a neural ODE and a certified upper bound on the error between the abstract neural network and the concrete dynamical model. So far neural abstractions have exclusively been obtained as neural networks consisting entirely of $ReLU$ activation functions, resulting in neural ODE models that have piecewise affine dynamics, and which can be equivalently interpreted as linear hybrid automata. In this work, we observe that the utility of an abstraction depends on its use: some scenarios might require coarse abstractions that are easier to analyse, whereas others might require more complex, refined abstractions. We therefore consider neural abstractions of alternative shapes, namely either piecewise constant or nonlinear non-polynomial (specifically, obtained via sigmoidal activations). We employ formal inductive synthesis procedures to generate neural abstractions that result in dynamical models with these semantics. Empirically, we demonstrate the trade-off that these different neural abstraction templates have vis-a-vis their precision and synthesis time, as well as the time required for their safety verification (done via reachability computation). We improve existing synthesis techniques to enable abstraction of higher-dimensional models, and additionally discuss the abstraction of complex neural ODEs to improve the efficiency of reachability analysis for these models.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google