Shield Synthesis for LTL Modulo Theories

要約

近年、機械学習 (ML) モデルはさまざまな分野で目覚ましい成功を収めています。
ただし、これらのモデルは危険な動作を示す傾向があり、安全性が重要なシステムへの導入が妨げられます。
この問題に対処するために、特定の ML モデルの安全な動作を保証する方法の開発に焦点を当てた十分な研究が行われています。
顕著な例は、望ましくない動作をブロックする外部コンポーネント (「シールド」) を組み込んだシールドです。
シールドは大幅な進歩にもかかわらず、主な後退に悩まされています。シールドは現在、命題ロジック (LTL など) のみでエンコードされたプロパティを対象としており、よりリッチなロジックには適していません。
これにより、現実世界の多くのシステムにおけるシールドの広範な適用が制限されます。
この研究では、反応性合成モジュロ理論の最近の進歩に基づいて、このギャップに対処し、シールドを LTL モジュロ理論に拡張します。
これにより、より表現力豊かなロジックで複雑な安全仕様に準拠したシールドを生成するための新しいアプローチを開発することができました。
私たちはシールドを評価し、時間的ダイナミクスを伴う豊富なデータを処理する能力を実証しました。
私たちの知る限り、これはこのような表現力を備えたシールドを合成するための最初のアプローチです。

要約(オリジナル)

In recent years, Machine Learning (ML) models have achieved remarkable success in various domains. However, these models also tend to demonstrate unsafe behaviors, precluding their deployment in safety-critical systems. To cope with this issue, ample research focuses on developing methods that guarantee the safe behaviour of a given ML model. A prominent example is shielding which incorporates an external component (a ‘shield’) that blocks unwanted behavior. Despite significant progress, shielding suffers from a main setback: it is currently geared towards properties encoded solely in propositional logics (e.g., LTL) and is unsuitable for richer logics. This, in turn, limits the widespread applicability of shielding in many real-world systems. In this work, we address this gap, and extend shielding to LTL modulo theories, by building upon recent advances in reactive synthesis modulo theories. This allowed us to develop a novel approach for generating shields conforming to complex safety specifications in these more expressive, logics. We evaluated our shields and demonstrate their ability to handle rich data with temporal dynamics. To the best of our knowledge, this is the first approach for synthesizing shields for such expressivity.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google