# Verified Neural Compressed Sensing

arXiv: https://arxiv.org/abs/2405.04260 · HTML: https://mlsanity.com/paper/2405.04260/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 24 references that are in the map.
- First posted on arXiv 7 May 2024.

## Builds on (most cited first, 14 of 14)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Reliable evaluation of adversarial robustness with an ensemble of diverse parameter-free attacks](https://mlsanity.com/paper/2003.01690/) (2020)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Compressed Sensing using Generative Models](https://mlsanity.com/paper/1703.03208/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Solving Linear Inverse Problems Provably via Posterior Sampling with Latent Diffusion Models](https://mlsanity.com/paper/2307.00619/) (2023)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Learning Certified Individually Fair Representations](https://mlsanity.com/paper/2002.10312/) (2020)
- [Direct Parameterization of Lipschitz-Bounded Deep Networks](https://mlsanity.com/paper/2301.11526/) (2023)
- [IBP Regularization for Verified Adversarial Robustness via Branch-and-Bound](https://mlsanity.com/paper/2206.14772/) (2022)

## Built on by (most cited first, 1 of 1)

- [Algorithmic Language Models with Neurally Compiled Libraries](https://mlsanity.com/paper/2407.04899/) (2024)

## Abstract (arXiv)

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.