Verified Neural Compressed Sensing

TL;DR

This work introduces provably correct neural networks for compressed sensing, where the network is trained to recover a sparse vector from reduced or binary measurements and its correctness is certified by automated verification. A compact MLP with a fixed linear preprocessing, skip connections, and ReLU layers forms the decoder, while adversarial training guides it to respect the sparsity and value constraints. Verification uses LiRPA-based bound propagation and a branch-and-bound search over the input domain to prove that the network's outputs align with the true support for all valid inputs, enabling safety-critical correctness guarantees. The results show that the approach adapts network size to problem difficulty, can handle mixed linear and binary measurements, and benefits from jointly learned sensing matrices, offering a practical path to verifiably correct neural solvers for mathematical problems.

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.

Figures (4)

• Figure 1: Distribution of how far the bound is from being sufficient to prove Property \ref{['eq:verif_form_pos']} for $i=49$ on the $n=50,m=30$ network of Figure \ref{['fig:learned_50']}. Each dot correspond to a randomly chosen subdomain of $\left\{\mathbf{x} \in \mathbb{X}^l_{\epsilon, 1}, x_{49} \geq \epsilon\right\}$. The color indicates how many of the signal coordinates have been forced to be non-zero.
• Figure 2: Cactus plots showing the impact of problem dimension on verification times. off coordinates are much slower to verify than on coordinates, and smaller number of measurements $m$ (blue or orange lines) are also associated with harder to verify properties. Increase in the signal size $n$ also influence the verification runtimes, which can be seen by comparing the scales of the time axis of the subfigures.
• Figure 3: Impact of $\textit{Fixed}$ vs. $\textit{Learned}$ sensing matrix. Optimizing the sensing matrix leads to significantly faster verification, particularly for hard problems.
• Figure 4: Runtime for correctness proofs of model handling binary measurements.