Verified Neural Compressed Sensing

要約

私たちは、人間の入力を一切必要とせずに自動化された検証アルゴリズムによって正しさの証明が生成される、正確な計算タスク用に (私たちの知る限りでは) 最初に正しいと証明されたニューラル ネットワークを開発しました。
ニューラル ネットワークの検証に関するこれまでの研究は、たとえ満たされていてもニューラル ネットワークがエラーを起こさないことを保証するには十分ではない部分的な仕様に焦点を当ててきました。
私たちは、正しさの正確な概念を使用して、ニューラル ネットワーク検証を計算タスクに適用することに焦点を当てています。検証可能な正しいニューラル ネットワークは、警告なしに当面のタスクを証明します。
特に、圧縮センシング、つまりベクトルの次元よりも小さい多数の測定値からスパース ベクトルを回復するための最初の正しいと証明されたニューラル ネットワークをトレーニングおよび検証するアプローチを開発します。
適度な問題次元 (最大 50) の場合、線形および二値化された線形測定からスパース ベクトルを証明できるニューラル ネットワークを訓練できることを示します。
さらに、ネットワークの複雑さ (ニューロン/層の数) を問題の難易度に適応させ、従来の圧縮センシング手法が機能することが証明されていない問題を解決できることを示します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google