Building verified neural networks with specifications for systems
Cheng Tan, Yibo Zhu, Chuanxiong Guo · 2021
Neural networks (NNs) are beneficial to many services, and we believe systems—such as OSes, databases, networked systems—are not an exception. But applying NNs in these critical systems is challenging: people have to risk getting unexpected outcomes from NNs because NN behaviors are not well-defined. To tame these undefined behaviors, we introduce a framework ouroboros, which builds verified NNs that follow user-defined specifications. These specifications comprise input and output constraints which characterize the behaviors of a NN. We do a case study on database learned indexes to demonstrate that training verified NN models is possible. Though many challenges remain, ouroboros enables us, for the first time, to apply NNs in critical systems with _confidence_.