We develop the first (to the best of our knowledge) provably correct neural networks for a precise computational task, with the proof of correctness generated by an automated verification algorithm without any human input. Prior work on neural network verification has focused on partial specifications that, even when satisfied, are not sufficient to ensure that a neural network never makes errors. We focus on applying neural network verification to computational tasks with a precise notion of correctness, where a verifiably correct neural network provably solves the task at hand with no caveats. In particular, we develop an approach to train and verify the first provably correct neural networks for compressed sensing, i.e., recovering sparse vectors from a number of measurements smaller than the dimension of the vector. We show that for modest problem dimensions (up to 50), we can train neural networks that provably recover a sparse vector from linear and binarized linear measurements. Furthermore, we show that the complexity of the network (number of neurons/layers) can be adapted to the problem difficulty and solve problems where traditional compressed sensing methods are not known to provably work.

翻译：我们开发了（据我们所知）首个针对精确计算任务的可证明正确神经网络，其正确性证明由自动验证算法生成，无需任何人工输入。先前关于神经网络验证的工作主要关注部分规范，即使满足这些规范，也不足以确保神经网络永远不会出错。我们专注于将神经网络验证应用于具有严格正确性概念的计算任务，其中经过验证的神经网络能够毫无保留地切实解决当前任务。具体而言，我们开发了一种训练和验证首个可证明正确压缩感知神经网络的方法，即从少于向量维度的测量值中恢复稀疏向量。研究表明，在中等维度问题中（最高50维），我们能够训练出可从线性及二值化线性测量中可靠恢复稀疏向量的神经网络。此外，我们还展示了网络复杂度（神经元/层数）可随问题难度自适应调整，并能解决传统压缩感知方法尚无理论保证的难题。