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.

本文提出了一种新的神经网络学习框架，该框架通过集成基于优化算法的抽象精炼循环并在动态构建的具有准确性和安全性目标的输入空间的分区上操作，实现训练可证明正确的机器学习网络的目标。通过实现我们的方法并将其应用于强制执行 ACAS Xu 数据集和碰撞检测数据集的一般安全属性，我们证明实现安全不会以很多精度的代价为代价，关键在于采用一个抽象精炼方法对于构建准确和正确的机器学习网络提供了一条有意义的路径。