为神经策略合成高效且灵活的程序化运行时防护机制

《ACM Transactions on Software Engineering and Methodology》：Synthesizing Efficient and Permissive Programmatic Runtime Shields for Neural Policies

神经控制系统中实时防护盾牌的轻量化生成方法。针对现有程序化实时防护盾牌计算成本高或约束过严的问题，提出Aegis框架，将防护生成建模为草图驱动程序合成问题，结合反例引导归纳合成和贝叶斯优化实现高效求解。实验表明其生成的防护盾牌时间开销降低2.2倍，内存占用减少3.9倍，平均干预次数减少1.5倍，在保证系统安全性的同时显著提升效率。

　　

摘要

随着神经策略在控制系统中的使用日益增加，确保其安全性和可靠性已成为一项至关重要的软件工程任务。一种常见的确保神经策略安全性的方法是部署程序化运行时防护机制来纠正其中的不安全指令。然而，现有方法生成的程序化运行时防护机制要么计算成本高昂，要么允许的操作范围过窄，从而导致系统开销增加和不必要的干预。为了解决这些问题，我们提出了Aegis，这是一个用于为神经策略生成轻量级且操作范围较广的程序化运行时防护机制的新框架。Aegis通过将运行时防护机制的生成问题表述为一个基于草图的程序合成问题，并提出了一种结合反例引导的归纳合成和贝叶斯优化的新方法来实现这一目标。为了评估Aegis及其生成的防护机制，我们使用了八个具有代表性的控制系统，并将其与当前最先进的技术进行了比较。结果表明，Aegis生成的程序化运行时防护机制能够纠正神经策略中的所有不安全指令，确保系统在任何时候都不违反任何预期的安全属性。与当前最先进的技术相比，Aegis的防护机制在时间开销上减少了2.2倍，在内存使用上减少了3.9倍，这表明它们的性能更为优越。此外，Aegis的防护机制平均比其他防护机制少进行1.5次干预，显示出更好的灵活性。