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维）下，我们能够训练出可证明从线性测量和二值化线性测量中恢复稀疏向量的神经网络。此外，我们还证明网络的复杂度（神经元/层数）可适应问题难度，并能解决传统压缩感知方法尚无法保证可证明工作的问题。