arXiv:2406.04184v2 宣告类型: replace-cross 摘要：近年来，机器学习（ML）模型在各个领域都取得了显著的成功。然而，这些模型也倾向于表现出不安全的行为，这阻碍了它们在安全关键系统中的部署。为了解决这一问题，大量的研究集中在开发能够保证给定ML模型安全行为的方法上。一个显著的例子是屏蔽技术，该技术通过引入一个外部组件（称为“屏蔽”）来阻止不希望的行为。尽管取得了显著进展，但屏蔽技术仍面临主要挑战：它目前主要针对编码在命题逻辑（如LTL）之中的属性，而不适用于更丰富的逻辑语言。这反过来限制了屏蔽技术在许多实际系统中的广泛应用。在本文中，我们解决了这一问题，并通过利用反应合成中的近期进展，将屏蔽技术扩展到理论模态LTL语言中。这使我们能够开发出一种生成符合这些更表达力的逻辑的复杂安全规范的新方法。我们评估了我们的屏蔽技术，并展示了它们处理具有时间动态的丰富数据的能力。据我们所知，这是第一个针对此类表达性的合成屏蔽技术的方法。