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.

翻译：近年来，机器学习（ML）模型在各个领域取得了显著成功。然而，这些模型也常表现出不安全行为，阻碍其在安全关键系统中的部署。为解决这一问题，大量研究致力于开发确保给定ML模型安全行为的方法。一个典型例子是盾构（shielding），它通过集成外部组件（"盾"）来阻断不良行为。尽管取得重大进展，盾构仍面临主要瓶颈：当前它仅适用于命题逻辑（如LTL）编码的属性，无法处理更丰富的逻辑。这进而限制了盾构在众多现实系统中的广泛应用。在本工作中，我们基于反应式综合与理论相结合的最新进展，将盾构扩展至基于理论的LTL，填补了这一空白。这使我们能够开发出一种新方法，生成符合这些更具表达力的逻辑中复杂安全规范的盾。我们评估了所提出的盾，并展示了其处理含时序动态的丰富数据的能力。据我们所知，这是首个针对此类表达力进行盾构综合的方法。