Building Verified Neural Networks for Computer Systems with Ouroboros
Building Verified Neural Networks for Computer Systems with Ouroboros
复制标题
DOI：
--
复制
发表时间：
2023
影响因子：
--
通讯作者：
Tianhao Wei;Zhihao Jia;Changliu Liu;Cheng Tan
中科院分区：
文献类型：
--
作者：
Tianhao Wei;Zhihao Jia;Changliu Liu;Cheng Tan
神经网络是一种强大的工具。将它们应用于计算机系统--操作系统、数据库和网络系统--引起了人们的极大关注。然而，神经网络是复杂的黑匣子，可能会产生意想不到的结果。为了训练具有良好定义的行为的网络，我们引入了Oroboros，这是一个构建经过验证的神经网络的系统。经过验证的神经网络是那些满足用户定义的安全属性的网络，称为规范。Ouroboros通过结合深度学习训练和神经网络验证的训练验证循环来建立经过验证的网络。该系统采用多种技术来填补今天的验证和系统所需的性能之间的差距。Ouroboros还通过规范感知学习加快了训练-验证循环。我们的实验表明，Oroboros可以为我们研究的五个应用训练经过验证的网络，与普通的训练-验证循环相比，平均加速比为2.8倍。
Neural networks are powerful tools. Applying them in computer systems—operating systems, databases, and networked systems—attracts much attention. However, neural networks are complicated black boxes that may produce unexpected results. To train networks with well-defined behaviors, we introduce ouroboros, a system that constructs verified neural networks . Verified neural networks are those that satisfy user-defined safety properties, known as specifications. Ouroboros builds verified networks by a training-verification loop that combines deep learning training and neural network verification. The system employs multiple techniques to fill the gap between today’s verification and the properties required for systems. Ouroboros also accelerates the training-verification loop by spec-aware learning. Our experiments show that ouroboros can train verified networks for five applications that we study and has a 2.8 × speedup on average compared with the vanilla training-verification loop.