Shield Synthesis for LTL Modulo Theories

要約

近年、機械学習（ML）モデルは、さまざまなドメインで顕著な成功を収めています。
ただし、これらのモデルは、安全性が批判的なシステムでの展開を妨げる危険な動作を実証する傾向もあります。
この問題に対処するために、十分な研究では、特定のMLモデルの安全な動作を保証する方法の開発に焦点を当てています。
顕著な例は、不要な動作をブロックする外部コンポーネント（「シールド」）を組み込んだシールドです。
大きな進歩にもかかわらず、シールドは主なset折に苦しんでいます。現在、命題ロジック（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