Art: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
Art: Abstraction Refinement-Guided Training for Provably Correct Neural Networks
复制标题
DOI：
10.34727/2020/isbn.978-3-85448-042-6_22
复制
发表时间：
2019-07
期刊：
影响因子：
--
通讯作者：
Xuankang Lin;He Zhu;R. Samanta;S. Jagannathan
中科院分区：
文献类型：
--
作者：
Xuankang Lin;He Zhu;R. Samanta;S. Jagannathan
人工神经网络（ANNs）在各种具有挑战性的机器学习应用中显示出显著的实用性。虽然人们非常希望对其行为的属性进行正式验证，但事实证明，它们很难派生和执行。现有的方法通常将此问题表述为事后分析过程。在本文中，我们提出了一个新的学习框架，以确保这种形式的保证是由结构强制执行的。我们的技术能够训练可证明正确的网络，涉及广泛的安全属性，这是一种远远超出现有方法的能力，而不会影响太多的准确性。我们的关键见解是，我们可以将基于优化的抽象改进循环集成到学习过程中，并在考虑准确性和安全性目标的输入空间的动态构造分区上进行操作。细化过程迭代地分割从中提取训练数据的输入空间，并以这些分区能够进行安全验证的有效性为指导。我们已经在一个工具（ART）中实现了我们的方法，并将其应用于无人驾驶飞行员避碰系统ACAS Xu数据集和碰撞检测数据集上强制执行一般安全属性。重要的是，我们的经验证明，实现安全并不是以准确性为代价的。我们的方法表明，抽象细化方法为构建准确和正确的机器学习网络提供了有意义的途径。
Artificial Neural Networks (ANNs) have demonstrated remarkable utility in various challenging machine learning applications. While formally verified properties of their behaviors are highly desired, they have proven notoriously difficult to derive and enforce. Existing approaches typically formulate this problem as a post facto analysis process. In this paper, we present a novel learning framework that ensures such formal guarantees are enforced by construction. Our technique enables training provably correct networks with respect to a broad class of safety properties, a capability that goes well-beyond existing approaches, without compromising much accuracy. Our key insight is that we can integrate an optimization-based abstraction refinement loop into the learning process and operate over dynamically constructed partitions of the input space that considers accuracy and safety objectives synergistically. The refinement procedure iteratively splits the input space from which training data is drawn, guided by the efficacy with which such partitions enable safety verification. We have implemented our approach in a tool (ART) and applied it to enforce general safety properties on unmanned aviator collision avoidance system ACAS Xu dataset and the Collision Detection dataset. Importantly, we empirically demonstrate that realizing safety does not come at the price of much accuracy. Our methodology demonstrates that an abstraction refinement methodology provides a meaningful pathway for building both accurate and correct machine learning networks.