Abstract
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.
Abstract (translated)
我们开发了第一个可证明正确的神经网络，针对一个精确的计算任务，该任务是通过自动验证算法生成正确性证明的，而没有任何人类输入。先前关于神经网络验证的工作主要集中在部分规格上，即使满足，也无法确保神经网络永远不会出错。我们专注于将神经网络验证应用于具有精确正确性的计算任务，其中可证明正确的神经网络确实可以不加任何限制地解决该任务。特别地，我们开发了一种方法来训练和验证压缩感知中第一个可证明正确的神经网络，即从比向量维度小的几个测量中恢复稀疏向量。我们证明了对于小问题维度（至多50个），我们可以训练神经网络从线性化和二进制化的线性测量中恢复稀疏向量。此外，我们还证明了网络复杂性（神经元/层数）可以适应问题难度，并且可以解决传统压缩感知方法无法保证正确性的问题。
URL
https://arxiv.org/abs/2405.04260
